feat: improve error message in the case of type class synthesis failure (#11245)

This PR improves the error message encountered in the case of a type
class instance resolution failure, and adds an error explanation that
discusses the common new-user case of binary operation overloading and
points to the `trace.Meta.synthInstance` option for advanced debugging.

## Example

```lean4
def f (x : String) := x + x
```

Before:
```
failed to synthesize
  HAdd String String ?m.5

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
```

After:
```
failed to synthesize instance of type class
  HAdd String String ?m.5

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Error code: lean.failedToSynthesizeTypeclassInstance
[View explanation](https://lean-lang.org/doc/reference/latest/find/?domain=Manual.errorExplanation&name=lean.failedToSynthesizeTypeclassInstance)
```

The error message is changed in three important ways:
* Explains *what* failed to synthesize, using the "type class"
terminology that's more likely to be recognized than the "instance"
terminology
* Points to the `trace.Meta.synthInstance` option which is otherwise
nearly undiscoverable but is quite powerful (see also
leanprover/reference-manual#663 which is adding commentary on this
option)
* Gives an error explanation link (which won't actually work until the
next release after this is merged) which prioritizes the common-case
explanation of using the wrong binary operation

Author: robsimmons

src/Lean/Elab/Term/TermElabM.lean

@@ -1113,6 +1113,16 @@ def containsPendingMVar (e : Expr) : MetaM Bool := do
   | some _ => return false
   | none   => return true
 
+/--
+If the `trace.Meta.synthInstance` option is not already set, gives a hint explaining this option.
+-/
+def useTraceSynthMsg : MessageData :=
+  MessageData.lazy fun ctx =>
+    if trace.Meta.synthInstance.get ctx.opts then
+      pure ""
+    else
+      pure <| .hint' s!"Type class instance resolution failures can be inspected with the `set_option {trace.Meta.synthInstance.name} true` command."
+
 /--
   Try to synthesize metavariable using type class resolution.
   This method assumes the local context and local instances of `instMVar` coincide
@@ -1171,7 +1181,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}{useDiagnosticMsg}"
+      throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{extraErrorMsg}{useTraceSynthMsg}"
 
 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.lean

@@ -16,4 +16,5 @@ public import Lean.ErrorExplanations.InvalidDottedIdent
 public import Lean.ErrorExplanations.ProjNonPropFromProp
 public import Lean.ErrorExplanations.PropRecLargeElim
 public import Lean.ErrorExplanations.RedundantMatchAlt
+public import Lean.ErrorExplanations.SynthInstanceFailed
 public import Lean.ErrorExplanations.UnknownIdentifier

src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean

@@ -20,7 +20,7 @@ constructor if the inductive type being defined has no indices.
 
 # Examples
 
-## Typo in resulting type
+## Typo in Resulting Type
 ```lean broken
 inductive Tree (α : Type) where
   | leaf : Tree α
@@ -38,7 +38,7 @@ inductive Tree (α : Type) where
   | node : α → Tree α → Tree α
 ```
 
-## Missing resulting type after constructor parameter
+## Missing Resulting Type After Constructor Parameter
 
 ```lean broken
 inductive Credential where

src/Lean/ErrorExplanations/DependsOnNoncomputable.lean

@@ -26,7 +26,7 @@ definitions.
 
 # Examples
 
-## Necessarily noncomputable function not appropriately marked
+## Necessarily Noncomputable Function Not Appropriately Marked
 
 ```lean broken
 axiom transform : Nat → Nat
@@ -50,7 +50,7 @@ axiom, it does not contain any executable code; although the value `transform 0`
 there is no way to compute its value. Thus, `transformIfZero` must be marked `noncomputable` because
 its execution would depend on this axiom.
 
-## Noncomputable dependency can be made computable
+## Noncomputable Dependency Can Be Made Computable
 
 ```lean broken
 noncomputable def getOrDefault [Nonempty α] : Option α → α
@@ -81,7 +81,7 @@ version of `getOrDefault` (using the `Inhabited` type class), allowing `endsOrDe
 computable. (The differences between `Inhabited` and `Nonempty` are described in the documentation
 of inhabited types in the manual section on [Basic Classes](lean-manual://section/basic-classes).)
 
-## Noncomputable instance in namespace
+## Noncomputable Instance in Namespace
 
 ```lean broken
 open Classical in

src/Lean/ErrorExplanations/InductiveParamMismatch.lean

@@ -26,7 +26,7 @@ parameters to indices.
 
 # Examples
 
-## Vector length index as a parameter
+## Vector Length Index as a Parameter
 
 ```lean broken
 inductive Vec (α : Type) (n : Nat) : Type where

src/Lean/ErrorExplanations/InductiveParamMissing.lean

@@ -24,7 +24,7 @@ between indices and parameters.
 
 # Examples
 
-## Omitting parameter in argument to higher-order predicate
+## Omitting Parameter in Argument to Higher-Order Predicate
 
 ```lean broken
 inductive List.All {α : Type u} (P : α → Prop) : List α → Prop

src/Lean/ErrorExplanations/InferBinderTypeFailed.lean

@@ -43,7 +43,7 @@ The first three cases are demonstrated in examples below.
 
 # Examples
 
-## Binder type requires new type variable
+## Binder Type Requires New Type Variable
 
 ```lean broken
 def identity x :=
@@ -63,7 +63,7 @@ specified explicitly. Note that if automatic implicit parameter insertion is ena
 default), a binder for `α` itself need not be provided; Lean will insert an implicit binder for this
 parameter automatically.
 
-## Uninferred binder type due to resulting type annotation
+## Uninferred Binder Type Due to Resulting Type Annotation
 
 ```lean broken
 def plusTwo x : Nat :=
@@ -86,7 +86,7 @@ determined, resulting in the shown error. It is therefore necessary to include t
 its binder.
 
 
-## Attempting to name an example declaration
+## Attempting to Name an Example Declaration
 
 ```lean broken
 example trivial_proof : True :=
@@ -106,7 +106,7 @@ be named, and an identifier written where a name would appear in other declarati
 elaborated as a binder, whose type cannot be inferred. If a declaration must be named, it should be
 defined using a declaration form that supports naming, such as `def` or `theorem`.
 
-## Attempting to define multiple opaque constants at once
+## Attempting to Define Multiple Opaque Constants at Once
 
 ```lean broken
 opaque m n : Nat
@@ -128,7 +128,7 @@ instead elaborated as defining a single constant (e.g., `m` above) with paramete
 subsequent identifiers (`n`), whose types are unspecified and cannot be inferred. To define multiple
 global constants, it is necessary to declare each separately.
 
-## Attempting to define multiple structure fields on the same line
+## Attempting to Define Multiple Structure Fields on the Same Line
 
 ```lean broken
 structure Person where

src/Lean/ErrorExplanations/InferDefTypeFailed.lean

@@ -35,7 +35,7 @@ will never attempt to use the theorem body to infer the proposition being proved
 
 # Examples
 
-## Implicit argument cannot be inferred
+## Implicit Argument Cannot be Inferred
 
 ```lean broken
 def emptyNats :=
@@ -60,7 +60,7 @@ the expected type of the definition allows Lean to infer the appropriate implici
 `List.nil` constructor; alternatively, making this implicit argument explicit in the function body
 provides sufficient information for Lean to infer the definition's type.
 
-## Definition type uninferrable due to unknown parameter type
+## Definition Type Uninferrable Due to Unknown Parameter Type
 
 ```lean broken
 def identity x :=

src/Lean/ErrorExplanations/InvalidDottedIdent.lean

@@ -23,7 +23,7 @@ universe (e.g., `Prop` or `Type`), as dotted-identifier notation is not supporte
 
 # Examples
 
-## Insufficient type information
+## Insufficient Type Information
 
 ```lean broken
 def reverseDuplicate (xs : List α) :=
@@ -46,7 +46,7 @@ resolves: if the return type is  `T`, then Lean will (attempt to) resolve `.reve
 `T.reverse` whose return type is `T`—even if `T.reverse` does not take an argument of type
 `List α`.
 
-## Dotted identifier where type universe expected
+## Dotted Identifier Where Type Universe Expected
 
 ```lean broken
 example (n : Nat) :=

src/Lean/ErrorExplanations/ProjNonPropFromProp.lean

@@ -25,7 +25,7 @@ such elimination is only valid if the resulting value is also in `Prop`; if it i
 
 # Examples
 
-## Attempting to use index projection on existential proof
+## Attempting to Use Index Projection on Existential Proof
 
 ```lean broken
 example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > 0 :=