Add missing file

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 :=

src/Lean/ErrorExplanations/PropRecLargeElim.lean

@@ -29,7 +29,7 @@ proved rather than the type of data-valued term.
 
 # Examples
 
-## Defining an intermediate data value within a proof
+## Defining an Intermediate Data Value Within a Proof
 
 ```lean broken
 example {α : Type} [inst : Nonempty α] (p : α → Prop) :
@@ -68,7 +68,7 @@ type `α : Type`. Thus, pattern-matching on the proof of `Nonempty α` (a propos
 `Prop`-valued proof of the existential claim stated in the example's header. This restructuring
 could also be done using a pattern-matching `let` binding.
 
-## Extracting the witness from an existential proof
+## Extracting the Witness from an Existential Proof
 
 ```lean broken
 def getWitness {α : Type u} {p : α → Prop} (h : ∃ x, p x) : α :=

src/Lean/ErrorExplanations/RedundantMatchAlt.lean

@@ -40,7 +40,7 @@ matches with redundant alternatives to be compiled by discarding the unused arms
 
 # Examples
 
-## Incorrect ordering of pattern matches
+## Incorrect Ordering of Pattern Matches
 
 ```lean broken
 def seconds : List (List α) → List α
@@ -64,7 +64,7 @@ Since any expression matching `(_ :: x :: _) :: xss` will also match `_ :: xss`,
 alternative in the broken implementation is never reached. We resolve this by moving the more
 specific alternative before the more general one.
 
-## Unnecessary fallback clause
+## Unnecessary Fallback Clause
 
 ```lean broken
 example (p : Nat × Nat) : IO Nat := do
@@ -87,7 +87,7 @@ Here, the fallback clause serves as a catch-all for all values of `p` that do no
 However, no such values exist, so the fallback clause is unnecessary and can be removed. A similar
 error arises when using `if let pat := e` when `e` will always match `pat`.
 
-## Pattern treated as variable, not constructor
+## Pattern Treated as Variable, Not Constructor
 
 ```lean broken
 example (xs : List Nat) : Bool :=

src/Lean/ErrorExplanations/SynthInstanceFailed.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rob Simmons
+-/
+module
+
+prelude
+public import Lean.ErrorExplanation
+meta import Lean.ErrorExplanation
+
+public section
+
+/--
+[Type classes](lean-manual://section/type-class) are the mechanism that Lean and many other
+programming languages use to handle overloaded operations. The code that handles a particular
+overloaded operation is an _instance_ of a typeclass; deciding which instance to use for a given
+overloaded operation is called _synthesizing_ an instance.
+
+As an example, when Lean encounters an expression `x + y` where `x` and `y` both have type `Int`,
+it is necessary to look up how it should add two integers and also look up what the resulting type
+will be. This is described as synthesizing an instance of the type class `HAdd Int Int t` for some
+type `t`.
+
+Many failures to synthesize an instance of a type class are the result of using the wrong binary
+operation. Both success and failure are not always straightforward, because some instances are
+defined in terms of other instances, and Lean must recursively search to find appropriate instances.
+It's possible to inspect Lean's instance synthesis](lean-manual://section/instance-search), and this
+can be helpful for diagnosing tricky failures of type class instance synthesis.
+
+# Examples
+
+## Using the Wrong Binary Operation
+
+```lean broken
+#eval "A" + "3"
+```
+```output
+failed to synthesize instance of type class
+  HAdd String String ?m.4
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+```
+```lean fixed
+#eval "A" ++ "3"
+```
+
+The binary operation `+` is associated with the `HAdd` type class, and there's no way to add two
+strings. The binary operation `++`, associated with the `HAppend` type class, is the correct way to
+append strings.
+
+## Modifying the Type of an Argument
+
+```lean broken
+def x : Int := 3
+#eval x ++ "meters"
+```
+```output
+failed to synthesize instance of type class
+  HAppend Int String ?m.4
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+```
+```lean fixed
+def x : Int := 3
+#eval ToString.toString x ++ "meters"
+```
+
+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.
+-/
+register_error_explanation lean.synthInstanceFailed {
+  summary := "Failed to synthesize instance of type class"
+  sinceVersion := "4.26.0"
+}

src/Lean/ErrorExplanations/UnknownIdentifier.lean

@@ -35,7 +35,7 @@ message itself.
 
 # Examples
 
-## Missing import
+## Missing Import
 
 ```lean broken
 def inventory :=
@@ -56,7 +56,7 @@ The constant `Std.HashSet.ofList` is defined in the `Std.Data.HashSet.Basic` mod
 been imported in the original example. This import is suggested by the unknown identifier code
 action; once it is added, this example compiles.
 
-## Variable not in scope
+## Variable Not in Scope
 
 ```lean broken
 example (s : IO.FS.Stream) := do
@@ -80,7 +80,7 @@ not in scope. The `let`-binding on the third line is scoped to the inner `do` bl
 accessed in the outer `do` block. Moving this binding to the outer `do` block—from which it remains
 in scope in the inner block as well—resolves the issue.
 
-## Missing namespace
+## Missing Namespace
 
 ```lean broken
 inductive Color where
@@ -121,7 +121,7 @@ dotted-identifier notation `.rgb` can also be used, since the expected type of `
 `Color`. Alternatively, one can open the `Color` namespace and continue to omit the `Color` prefix
 from the identifier.
 
-## Protected constant name without namespace prefix
+## Protected Constant Name Without Namespace Prefix
 
 ```lean broken
 protected def A.x := ()
@@ -156,7 +156,7 @@ example—allows a `protected` constant to be referred to by its unqualified nam
 remainder of the namespace in which it occurs (see the manual section on
 [Namespaces and Sections](lean-manual://section/namespaces-sections) for details).
 
-## Unresolvable name inferred by dotted-identifier notation
+## Unresolvable Name Inferred by Dotted-Identifier Notation
 
 ```lean broken
 def disjoinToNat (b₁ b₂ : Bool) : Nat :=

src/Lean/Meta/SynthInstance.lean

@@ -860,9 +860,14 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
               mvarId.assign val
               return true
 
+register_builtin_option trace.Meta.synthInstance : Bool := {
+  group := "trace"
+  defValue := false
+  descr := "track the backtracking attempt to synthesize type class instances"
+}
+
 builtin_initialize
   registerTraceClass `Meta.synthPending
-  registerTraceClass `Meta.synthInstance
   registerTraceClass `Meta.synthInstance.instances (inherited := true)
   registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
   registerTraceClass `Meta.synthInstance.answer (inherited := true)

tests/lean/1007.lean.expected.out

@@ -6,7 +6,7 @@
 1007.lean:34:0-34:8: warning: declaration uses 'sorry'
 1007.lean:38:4-38:8: warning: declaration uses 'sorry'
 1007.lean:39:4-39:7: warning: declaration uses 'sorry'
-1007.lean:56:64-56:78: error: failed to synthesize
+1007.lean:56:64-56:78: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   IsLin fun x => sum fun i => norm x
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/1102.lean.expected.out

@@ -1,4 +1,4 @@
-1102.lean:22:35-22:49: error: failed to synthesize
+1102.lean:22:35-22:49: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   DVR 1
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/2273.lean.expected.out

@@ -1,4 +1,4 @@
-2273.lean:9:8-9:14: error: failed to synthesize
+2273.lean:9:8-9:14: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   P 37
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/297.lean.expected.out

@@ -1,7 +1,7 @@
-297.lean:1:10-1:11: error: failed to synthesize
+297.lean:1:10-1:11: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   OfNat (Sort ?u) 0
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Sort ?u
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/386.lean.expected.out

@@ -1,4 +1,4 @@
-386.lean:9:2-9:46: error: failed to synthesize
+386.lean:9:2-9:46: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   Fintype ?m
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/448.lean.expected.out

@@ -1,4 +1,4 @@
-448.lean:21:2-23:20: error: failed to synthesize
+448.lean:21:2-23:20: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   MonadExceptOf IO.Error M
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/attrCmd.lean.expected.out

@@ -1,4 +1,4 @@
-attrCmd.lean:6:0-6:6: error: failed to synthesize
+attrCmd.lean:6:0-6:6: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   Pure M
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/defInst.lean.expected.out

@@ -1,8 +1,8 @@
 [4, 5, 6]
-defInst.lean:8:26-8:32: error: failed to synthesize
+defInst.lean:8:26-8:32: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   BEq Foo
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool

tests/lean/defaultInstance.lean.expected.out

@@ -1,7 +1,7 @@
-defaultInstance.lean:20:20-20:23: error: failed to synthesize
+defaultInstance.lean:20:20-20:23: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   Foo Bool (?m x)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck
   Foo Bool (?m x)
 

tests/lean/eagerUnfoldingIssue.lean.expected.out

@@ -1,8 +1,8 @@
-eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
+eagerUnfoldingIssue.lean:6:2-6:17: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   MonadLog (StateM Nat)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+eagerUnfoldingIssue.lean:12:2-12:17: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   MonadLog (StateM Nat)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/eraseInsts.lean.expected.out

@@ -1,4 +1,4 @@
-eraseInsts.lean:12:22-12:27: error: failed to synthesize
+eraseInsts.lean:12:22-12:27: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   HAdd Foo Foo ?m
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/forErrors.lean.expected.out

@@ -1,4 +1,4 @@
-forErrors.lean:3:29-3:30: error: failed to synthesize
+forErrors.lean:3:29-3:30: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   Std.ToStream α ?m
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/interactive/4880.lean.expected.out

@@ -17,10 +17,11 @@
    {"start": {"line": 16, "character": 12},
     "end": {"line": 17, "character": 0}},
    "message":
-   "failed to synthesize\n  A\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize instance of type class\n  A\n\nHint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.",
    "fullRange":
    {"start": {"line": 16, "character": 12},
-    "end": {"line": 20, "character": 0}}},
+    "end": {"line": 20, "character": 0}},
+   "code": "lean.synthInstanceFailed"},
   {"source": "Lean 4",
    "severity": 1,
    "range":
@@ -37,10 +38,11 @@
    {"start": {"line": 22, "character": 17},
     "end": {"line": 22, "character": 20}},
    "message":
-   "failed to synthesize\n  A\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize instance of type class\n  A\n\nHint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.",
    "fullRange":
    {"start": {"line": 22, "character": 17},
-    "end": {"line": 22, "character": 20}}},
+    "end": {"line": 22, "character": 20}},
+   "code": "lean.synthInstanceFailed"},
   {"source": "Lean 4",
    "severity": 1,
    "range":

tests/lean/interactive/strInterpSynthError.lean.expected.out

@@ -7,27 +7,30 @@
    {"start": {"line": 15, "character": 25},
     "end": {"line": 15, "character": 28}},
    "message":
-   "failed to synthesize\n  ToString Bar\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize instance of type class\n  ToString Bar\n\nHint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.",
    "fullRange":
    {"start": {"line": 15, "character": 25},
-    "end": {"line": 15, "character": 28}}},
+    "end": {"line": 15, "character": 28}},
+   "code": "lean.synthInstanceFailed"},
   {"source": "Lean 4",
    "severity": 1,
    "range":
    {"start": {"line": 20, "character": 15},
     "end": {"line": 20, "character": 18}},
    "message":
-   "failed to synthesize\n  ToString Bar\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize instance of type class\n  ToString Bar\n\nHint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.",
    "fullRange":
    {"start": {"line": 20, "character": 15},
-    "end": {"line": 20, "character": 18}}},
+    "end": {"line": 20, "character": 18}},
+   "code": "lean.synthInstanceFailed"},
   {"source": "Lean 4",
    "severity": 1,
    "range":
    {"start": {"line": 26, "character": 17},
     "end": {"line": 26, "character": 20}},
    "message":
-   "failed to synthesize\n  ToString Bar\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize instance of type class\n  ToString Bar\n\nHint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.",
    "fullRange":
    {"start": {"line": 26, "character": 17},
-    "end": {"line": 26, "character": 20}}}]}
+    "end": {"line": 26, "character": 20}},
+   "code": "lean.synthInstanceFailed"}]}

tests/lean/kernelMVarBug.lean.expected.out

@@ -1,4 +1,4 @@
-kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
+kernelMVarBug.lean:5:15-5:20: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   HAdd α α α
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/macroStack.lean.expected.out

@@ -9,10 +9,10 @@ while expanding
 while expanding
   if h : (x > 0) then 1 else 0
 macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
-macroStack.lean:17:0-17:6: error: failed to synthesize
+macroStack.lean:17:0-17:6: error: failed to synthesize instance of type class
   HAdd Nat String ?m
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
 while expanding

tests/lean/macroSwizzle.lean.expected.out

@@ -1,7 +1,7 @@
-macroSwizzle.lean:4:7-4:23: error: failed to synthesize
+macroSwizzle.lean:4:7-4:23: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   HAdd Bool String ?m
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 macroSwizzle.lean:6:7-6:10: error: Application type mismatch: The argument
   "x"
 has type

tests/lean/openScoped.lean.expected.out

@@ -1,8 +1,8 @@
 openScoped.lean:1:7-1:14: error(lean.unknownIdentifier): Unknown identifier `epsilon`
-openScoped.lean:4:2-4:24: error: failed to synthesize
+openScoped.lean:4:2-4:24: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   Decidable (f = g)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 openScoped.lean:15:7-15:14: error(lean.unknownIdentifier): Unknown identifier `epsilon`
 openScoped.lean:20:7-20:14: error(lean.unknownIdentifier): Unknown identifier `epsilon`

tests/lean/run/1163.lean

@@ -11,13 +11,13 @@ elab "obviously2" : tactic =>
 theorem result2 : False := by obviously2
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat Bool 0
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 def x : Bool := 0
@@ -25,13 +25,13 @@ def x : Bool := 0
 theorem result3 : False := by obviously2
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat Bool 0
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error

tests/lean/run/345.lean

@@ -1,38 +1,38 @@
 set_option pp.mvars false
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat (Sort _) 1
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 axiom bla : 1
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat (Sort _) 1
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 structure Foo where
   foo : 1
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat (Sort _) 1
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 inductive Bla (x : 1) : Type

tests/lean/run/4203.lean

@@ -12,15 +12,15 @@ def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ
   ∃ (D : Mappish dOut (dOut₂)), D.k = Λ.k + Λ₂.k
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   Fintype v
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder
     (Σ dOut : Sigma (fun t ↦ Fintype t × DecidableEq t), let fin := dOut.snd.1; Mappish dIn dOut.fst) where
-  le Λ₁ Λ₂ := by
+le Λ₁ Λ₂ := by
     let u := Λ₁.fst.fst;
     let v := Λ₂.fst.fst;
     let ⟨w,x⟩ := Λ₁.fst.snd;

tests/lean/run/4365.lean

@@ -32,49 +32,49 @@ error: numerals are data in Lean, but the expected type is a proposition
 #check (1 : ∀ (n : Nat), True)
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat String 1
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 #check (1 : String)
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat Bool 1
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 #check (1 : Bool)
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat (Bool → Nat) 1
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool → Nat
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 #check (1 : Bool → Nat)
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat String 0
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 def foo : String :=

tests/lean/run/by_cases.lean

@@ -11,10 +11,10 @@ example (p : Prop) : True := by
 /-! Should not accidentally leak `open Classical` into branches. -/
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   Decidable p
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 example (p : Prop) : True := by

tests/lean/run/derivingDelta.lean

@@ -143,10 +143,10 @@ Can catch mixin failure
 instance (inst : DecidableEq (Type _)) : C1 List := {}
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   DecidableEq (Type u_1)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ---
 error: Failed to delta derive `C1` instance for `MyList'`.
 
@@ -281,10 +281,10 @@ No such definition
 Delta deriving fails due to synthesis failure.
 -/
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   Inhabited (Fin n)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ---
 error: Failed to delta derive `Inhabited` instance for `D2`.
 
@@ -295,10 +295,10 @@ def D2 (n : Nat) := Fin n
 deriving Inhabited
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   Inhabited (D2 n)
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ---
 error: Failed to delta derive `Inhabited` instance for `D2'`.
 

tests/lean/run/derivingReflBEq.lean

@@ -58,10 +58,10 @@ info: RegularBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq
 -- No `BEq` derived? Not a great error message yet, but the error location helps, so good enough.
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   BEq Foo
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 structure Foo where
@@ -71,10 +71,10 @@ structure Foo where
 
 /--
 @ +2:16...25
-error: failed to synthesize
+error: failed to synthesize instance of type class
   ReflBEq Bar
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs (positions := true) in
 structure Bar where
@@ -159,10 +159,10 @@ info: LinearBEq.instLawfulBEqWithHEq.{u_1} {α✝ : Type u_1} {a✝ : Nat} [BEq
 -- No `BEq` derived? Not a great error message yet, but the error location helps, so good enough.
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   BEq Foo
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 structure Foo where
@@ -172,10 +172,10 @@ structure Foo where
 
 /--
 @ +2:16...25
-error: failed to synthesize
+error: failed to synthesize instance of type class
   ReflBEq Bar
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs (positions := true) in
 structure Bar where

tests/lean/run/guard_msgs.lean

@@ -48,13 +48,13 @@ example : α := x
 
 #guard_msgs in
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   OfNat α 22
 numerals are polymorphic in Lean, but the numeral `22` cannot be used in a context where the expected type is
   α
 due to the absence of the instance above
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs(error) in
 example : α := 22

tests/lean/run/mergeSort.lean

@@ -32,10 +32,10 @@ inductive NoLE
 /--
 error: could not synthesize default value for parameter 'le' using tactics
 ---
-error: failed to synthesize
+error: failed to synthesize instance of type class
   LE NoLE
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 example : mergeSort [NoLE.mk] = [NoLE.mk] := sorry

tests/lean/run/trace_synth.lean

@@ -0,0 +1,52 @@
+class Foo (s : String) : Type where
+instance : Foo "one" where
+instance [Foo "three"] : Foo "two" where
+
+def f (s : String) [Foo s] := ()
+
+/-- info: () -/
+#guard_msgs in
+#eval f "one"
+
+/--
+error: failed to synthesize instance of type class
+  Foo "two"
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+#eval f "two"
+
+/--
+error: failed to synthesize instance of type class
+  Foo "two"
+---
+trace: [Meta.synthInstance] ❌️ Foo "two"
+  [Meta.synthInstance] new goal Foo "two"
+    [Meta.synthInstance.instances] #[@instFoo_1]
+  [Meta.synthInstance] ✅️ apply @instFoo_1 to Foo "two"
+    [Meta.synthInstance.tryResolve] ✅️ Foo "two" ≟ Foo "two"
+    [Meta.synthInstance] no instances for Foo "three"
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
+[Meta.synthInstance] ❌️ Foo "two"
+  [Meta.synthInstance] result <not-available> (cached)
+-/
+#guard_msgs in
+set_option trace.Meta.synthInstance true in
+#eval f "two"
+
+/--
+error: failed to synthesize instance of type class
+  Foo "three"
+---
+trace: [Meta.synthInstance] ❌️ Foo "three"
+  [Meta.synthInstance] no instances for Foo "three"
+    [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
+[Meta.synthInstance] ❌️ Foo "three"
+  [Meta.synthInstance] result <not-available> (cached)
+-/
+#guard_msgs in
+set_option trace.Meta.synthInstance true in
+#eval f "three"

tests/lean/run/variable.lean

@@ -78,10 +78,10 @@ section
 variable [ToString α] [ToString β]
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   ToString α
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 omit [ToString α] in
@@ -89,10 +89,10 @@ theorem t8 (a : α) (b : β) : True :=
   let _ := toString a; let _ := toString b; trivial
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   ToString β
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 omit [ToString β] in
@@ -100,15 +100,15 @@ theorem t9 (a : α) (b : β) : True :=
   let _ := toString a; let _ := toString b; trivial
 
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   ToString α
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 ---
-error: failed to synthesize
+error: failed to synthesize instance of type class
   ToString β
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 omit [ToString _] in

tests/lean/scopedLocalInsts.lean.expected.out

@@ -1,15 +1,15 @@
-scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize
+scopedLocalInsts.lean:12:6-12:39: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   ToString A
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 "A.mk 10 20"
-scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize
+scopedLocalInsts.lean:21:6-21:39: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   ToString A
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 "{ x := 10, y := 20 }"
-scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize
+scopedLocalInsts.lean:32:6-32:39: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   ToString A
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 "A.mk 10 20"

tests/lean/semicolonOrLinebreak.lean.expected.out

@@ -8,7 +8,7 @@ but this term has type
 
 Note: Expected a function because this term is being applied to the argument
   y
-semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize
+semicolonOrLinebreak.lean:20:2-20:9: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   Singleton ?m Point
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

tests/lean/setLit.lean.expected.out

@@ -1,8 +1,8 @@
 setLit.lean:22:19-22:21: error: overloaded, errors 
-  failed to synthesize
+  failed to synthesize instance of type class
     EmptyCollection String
   
-  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+  Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
   
   Fields missing: `bytes`, `isValidUTF8`
   
@@ -10,9 +10,9 @@ setLit.lean:22:19-22:21: error: overloaded, errors
      ̲b̲y̲t̲e̲s̲ ̲:̲=̲ ̲_̲
     ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲i̲s̲V̲a̲l̲i̲d̲U̲T̲F̲8̲ ̲:̲=̲ ̲_̲ ̲
 setLit.lean:24:31-24:38: error: overloaded, errors 
-  failed to synthesize
+  failed to synthesize instance of type class
     Singleton Nat String
   
-  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+  Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
   
   24:33 `val` is not a field of structure `String`

tests/lean/typeOf.lean.expected.out

@@ -1,11 +1,11 @@
-typeOf.lean:11:22-11:25: error: failed to synthesize
+typeOf.lean:11:22-11:25: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   HAdd Nat Nat Bool
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-typeOf.lean:12:0-12:5: error: failed to synthesize
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+typeOf.lean:12:0-12:5: error(lean.synthInstanceFailed): failed to synthesize instance of type class
   HAdd Bool Nat Nat
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool
 but is expected to have type

tests/pkg/module/Module/Imported.lean

@@ -65,10 +65,10 @@ info: theorem trfl : f = 1 :=
 
 -- Should not fail with 'unknown constant `inst*`
 /--
-error: failed to synthesize
+error: failed to synthesize instance of type class
   X
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
 -/
 #guard_msgs in
 def fX : X := inferInstance

tests/pkg/prv/Prv.lean

@@ -12,10 +12,10 @@ import Prv.Foo
 
 /--
 error: overloaded, errors ⏎
-  failed to synthesize
+  failed to synthesize instance of type class
     EmptyCollection (Name "hello")
   ⏎
-  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+  Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
   ⏎
   invalid {...} notation, constructor for `Name` is marked as private
 -/