feat: suggest deriving an instance when the instance might be derivable (#11346)

This PR modifies the error message for type synthesis failure for the
case where the type class in question is potentially derivable using a
`deriving` command. Also changes the error explanation for type class
instance synthesis failure with an illustration of this pattern.

## Example

```lean4
inductive MyColor where
  | chartreuse | sienna | thistle
def forceColor (oc : Option MyColor) :=
  oc.get!
```

Before this PR, this gives the potentially confusing impression that
Lean may have decided that `MyColor` is _not_ inhabited — people used to
Rust may be especially inclined towards this confusion.
```
failed to synthesize instance of type class
  Inhabited MyColor

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
```

After this PR, a targeted hint suggests precisely the command that will
fix the issue:
```
error: failed to synthesize instance of type class
  Inhabited MyColor

Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.
```

Author: robsimmons

src/Lean/Elab/Deriving/Basic.lean

@@ -223,6 +223,7 @@ example, `deriving instance Foo for Bar, Baz` invokes ``fooHandler #[`Bar, `Baz]
 def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
+  Term.registerDerivableClass className
   derivingHandlersRef.modify fun m => match m.find? className with
     | some handlers => m.insert className (handler :: handlers)
     | none => m.insert className [handler]

src/Lean/Elab/Term/TermElabM.lean

@@ -1119,10 +1119,27 @@ If the `trace.Meta.synthInstance` option is not already set, gives a hint explai
 def useTraceSynthMsg : MessageData :=
   MessageData.lazy fun ctx =>
     if trace.Meta.synthInstance.get ctx.opts then
-      pure ""
+      pure .nil
     else
       pure <| .hint' s!"Type class instance resolution failures can be inspected with the `set_option {trace.Meta.synthInstance.name} true` command."
 
+builtin_initialize derivableRef : IO.Ref NameSet ← IO.mkRef {}
+
+/--
+Registers a deriving handler for the purpose of error message delivery in `synthesizeInstMVarCore`.
+This should only be called by `Lean.Elab.Term.registerDerivingHandler`.
+-/
+def registerDerivableClass (className : Name) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register derivable class, it can only be registered during initialization")
+  derivableRef.modify fun m => m.insert className
+
+/--
+Returns whether `className` has a `deriving` handler installed.
+-/
+def hasDerivingHandler (className : Name) : IO Bool := do
+  return (← derivableRef.get).contains className
+
 /--
   Try to synthesize metavariable using type class resolution.
   This method assumes the local context and local instances of `instMVar` coincide
@@ -1181,7 +1198,16 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{extraErrorMsg}{useTraceSynthMsg}"
+      let msg ← match type with
+        | .app (.const cls _) (.const typ _) =>
+          -- This has the structure of a `deriving`-style type class, alter feedback accordingly
+          if ← hasDerivingHandler cls then
+            pure <| extraErrorMsg ++ .hint' m!"Adding the command `deriving instance {cls} for {typ}` may allow Lean to derive the missing instance."
+          else
+            pure <| extraErrorMsg ++ useTraceSynthMsg
+        | _ =>
+            pure <| extraErrorMsg ++ useTraceSynthMsg
+      throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{msg}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
     (mkErrorMsg? : Option (MVarId → (expectedType e : Expr) → MetaM MessageData) := none)

src/Lean/ErrorExplanations/SynthInstanceFailed.lean

@@ -49,7 +49,7 @@ The binary operation `+` is associated with the `HAdd` type class, and there's n
 strings. The binary operation `++`, associated with the `HAppend` type class, is the correct way to
 append strings.
 
-## Modifying the Type of an Argument
+## Arguments Have the Wrong Type
 
 ```lean broken
 def x : Int := 3
@@ -69,6 +69,55 @@ def x : Int := 3
 Lean does not allow integers and strings to be added directly. The function `ToString.toString` uses
 type class overloading to convert values to strings; by successfully searching for an instance of
 `ToString Int`, the second example will succeed.
+
+## Missing Type Class Instance
+
+```lean broken
+inductive MyColor where
+  | chartreuse | sienna | thistle
+
+def forceColor (oc : Option MyColor) :=
+  oc.get!
+```
+```output
+failed to synthesize instance of type class
+  Inhabited MyColor
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+```
+```lean fixed (title := "Fixed (derive instance when defining type)")
+inductive MyColor where
+  | chartreuse | sienna | thistle
+deriving Inhabited
+
+def forceColor (oc : Option MyColor) :=
+  oc.get!
+```
+```lean fixed (title := "Fixed (derive instance separately)")
+inductive MyColor where
+  | chartreuse | sienna | thistle
+
+deriving instance Inhabited for MyColor
+
+def forceColor (oc : Option MyColor) :=
+  oc.get!
+```
+```lean fixed (title := "Fixed (define instance)")
+inductive MyColor where
+  | chartreuse | sienna | thistle
+
+instance : Inhabited MyColor where
+  default := .sienna
+
+def forceColor (oc : Option MyColor) :=
+  oc.get!
+```
+
+Type class synthesis can fail because an instance of the type class simply needs to be provided.
+This commonly happens for type classes like `Repr`, `BEq`, `ToJson` and `Inhabited`. Lean can often
+[automatically generate instances of the type class with the `deriving` keyword](lean-manual://section/type-class),
+either when the type is defined or with the stand-alone `deriving` command.
+
 -/
 register_error_explanation lean.synthInstanceFailed {
   summary := "Failed to synthesize instance of type class"

tests/lean/defInst.lean.expected.out

@@ -2,7 +2,7 @@
 defInst.lean:8:26-8:32: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   BEq Foo
 
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+Hint: Adding the command `deriving instance BEq for Foo` may allow Lean to derive the missing instance.
 fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool

tests/lean/run/derivingReflBEq.lean

@@ -61,7 +61,7 @@ info: RegularBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq
 error: failed to synthesize instance of type class
   BEq Foo
 
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+Hint: Adding the command `deriving instance BEq for RegularBEq.Foo` may allow Lean to derive the missing instance.
 -/
 #guard_msgs in
 structure Foo where
@@ -162,7 +162,7 @@ info: LinearBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq
 error: failed to synthesize instance of type class
   BEq Foo
 
-Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+Hint: Adding the command `deriving instance BEq for LinearBEq.Foo` may allow Lean to derive the missing instance.
 -/
 #guard_msgs in
 structure Foo where

tests/lean/run/mightBeDerivable.lean

@@ -0,0 +1,96 @@
+import Lean
+open Lean
+
+inductive MyColor where
+  | chartreuse | sienna | thistle
+
+/--
+error: failed to synthesize instance of type class
+  Inhabited MyColor
+
+Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance.
+-/
+#guard_msgs in
+def forceColor (oc : Option MyColor) :=
+  oc.get!
+
+/--
+error: failed to synthesize instance of type class
+  ToJson MyColor
+
+Hint: Adding the command `deriving instance Lean.ToJson for MyColor` may allow Lean to derive the missing instance.
+-/
+#guard_msgs in
+def jsonMaybeColor (oc : MyColor) :=
+  ToJson.toJson oc
+
+/--
+error: failed to synthesize instance of type class
+  ToJson MyColor
+
+Hint: Adding the command `deriving instance Lean.ToJson for MyColor` may allow Lean to derive the missing instance.
+---
+error: failed to synthesize instance of type class
+  ToExpr MyColor
+
+Hint: Adding the command `deriving instance Lean.ToExpr for MyColor` may allow Lean to derive the missing instance.
+---
+error: No deriving handlers have been implemented for class `ToString`
+-/
+#guard_msgs in
+inductive MyList where
+  | nil : MyList
+  | cons : MyColor → MyList
+deriving ToJson, ToExpr, ToString, Nonempty
+
+
+-- It would be very cool if this case could give us "maybe derive ToJson MyColor", but that's more sophisticated than we can presently manage
+/--
+error: failed to synthesize instance of type class
+  ToJson (Option MyColor)
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+def jsonColor (oc : Option MyColor) :=
+  ToJson.toJson oc
+
+-- It would be very cool if this case could give us "maybe derive DecidableEq MyColor"
+/--
+error: failed to synthesize instance of type class
+  Decidable (oc = some MyColor.thistle)
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+def checkColor (oc : Option MyColor) :=
+  if oc = .some .thistle then 1 else 2
+
+inductive MyTree where
+  | nil : MyTree
+  | cons : MyColor → MyTree → MyTree
+
+-- The suggestion here will fail, it would be super awesome if we gave the full recommendation,
+-- but each hint makes progress
+/--
+error: failed to synthesize instance of type class
+  ToJson MyTree
+
+Hint: Adding the command `deriving instance Lean.ToJson for MyTree` may allow Lean to derive the missing instance.
+-/
+#guard_msgs in
+def jsonListColor (oc : MyTree) :=
+  ToJson.toJson oc
+
+/--
+error: failed to synthesize instance of type class
+  ToJson MyColor
+
+Hint: Adding the command `deriving instance Lean.ToJson for MyColor` may allow Lean to derive the missing instance.
+-/
+#guard_msgs in
+deriving instance Lean.ToJson for MyTree
+
+deriving instance Lean.ToJson for MyColor
+
+deriving instance Lean.ToJson for MyTree