diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 2aa865b78c..a418d20a31 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -30,6 +30,8 @@ register_builtin_option maxHeartbeats : Nat := {
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
+def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
+
 namespace Core
 
 builtin_initialize registerTraceClass `Kernel
@@ -253,7 +255,7 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
-  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
+  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index 11d6319c10..67c5ce0835 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/src/Lean/Elab/Calc.lean
@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 91d631d98e..f508f9785b 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -784,7 +784,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize instance{indentExpr type}"
+      throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index b4f00c8625..cb7ae0c730 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -212,7 +212,17 @@ instance : Hashable InfoCacheKey :=
   ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)⟩
 end InfoCacheKey
 
-abbrev SynthInstanceCache := PersistentHashMap (LocalInstances × Expr) (Option Expr)
+structure SynthInstanceCacheKey where
+  localInsts        : LocalInstances
+  type              : Expr
+  /--
+  Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
+  See issue #2522.
+  -/
+  synthPendingDepth : Nat
+  deriving Hashable, BEq
+
+abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo
@@ -273,6 +283,8 @@ structure Diagnostics where
   heuristicCounter : PHashMap Name Nat := {}
   /-- Number of times a TC instance is used. -/
   instanceCounter : PHashMap Name Nat := {}
+  /-- Pending instances that were not synthesized because `maxSynthPendingDepth` has been reached. -/
+  synthPendingFailures : PHashMap Expr MessageData := {}
   deriving Inhabited
 
 /--
@@ -296,6 +308,11 @@ structure SavedState where
   meta        : State
   deriving Nonempty
 
+register_builtin_option maxSynthPendingDepth : Nat := {
+  defValue := 1
+  descr    := "maximum number of nested `synthPending` invocations. When resolving unification constraints, pending type class problems may need to be synthesized. These type class problems may create new unification constraints that again require solving new type class problems. This option puts a threshold on how many nested problems are created."
+}
+
 /--
   Contextual information for the `MetaM` monad.
 -/
@@ -311,8 +328,8 @@ structure Context where
     Track the number of nested `synthPending` invocations. Nested invocations can happen
     when the type class resolution invokes `synthPending`.
 
-    Remark: in the current implementation, `synthPending` fails if `synthPendingDepth > 0`.
-    We will add a configuration option if necessary. -/
+    Remark: `synthPending` fails if `synthPendingDepth > maxSynthPendingDepth`.
+  -/
   synthPendingDepth : Nat                  := 0
   /--
     A predicate to control whether a constant can be unfolded or not at `whnf`.
@@ -470,21 +487,30 @@ variable [MonadControlT MetaM n] [Monad n]
 
 /-- If diagnostics are enabled, record that `declName` has been unfolded. -/
 def recordUnfold (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
     let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
-    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter }
+    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter, synthPendingFailures }
 
 /-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
 def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
     let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
-    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter }
+    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter, synthPendingFailures }
 
 /-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
 def recordInstance (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
     let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
-    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
+    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC, synthPendingFailures }
+
+/-- If diagnostics are enabled, record that synth pending failures. -/
+def recordSynthPendingFailure (type : Expr) : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    unless (← get).diag.synthPendingFailures.contains type do
+      -- We need to save the full context since type class resolution uses multiple metavar contexts and different local contexts
+      let msg ← addMessageContextFull m!"{type}"
+      modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+        { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures := synthPendingFailures.insert type msg }
 
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean
index 8dd0537aa2..72b0fe6282 100644
--- a/src/Lean/Meta/Diagnostics.lean
+++ b/src/Lean/Meta/Diagnostics.lean
@@ -60,11 +60,20 @@ def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM Dia
 def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
   mkDiagSummary (← get).diag.instanceCounter
 
-def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
+def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM DiagSummary := do
+  if failures.isEmpty then
+    return {}
+  else
+    let mut data := #[]
+    for (_, msg) in failures do
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{msg}"
+    return { data }
+
+def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : MessageData :=
   if s.isEmpty then
     m
   else
-    let header := s!"{header} (max: {s.max}, num: {s.data.size}):"
+    let header := if resultSummary then s!"{header} (max: {s.max}, num: {s.data.size}):" else header
     m ++ .trace { cls } header s.data
 
 def reportDiag : MetaM Unit := do
@@ -75,13 +84,17 @@ def reportDiag : MetaM Unit := do
     let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
     let heu ← mkDiagSummary (← get).diag.heuristicCounter
     let inst ← mkDiagSummaryForUsedInstances
+    let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
     let unfoldKernel ← mkDiagSummary (Kernel.getDiagnostics (← getEnv)).unfoldCounter
-    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
+    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty && synthPending.isEmpty do
       let m := MessageData.nil
       let m := appendSection m `reduction "unfolded declarations" unfoldDefault
       let m := appendSection m `reduction "unfolded instances" unfoldInstance
       let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
       let m := appendSection m `type_class "used instances" inst
+      let m := appendSection m `type_class
+                 s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
+                 synthPending (resultSummary := false)
       let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
       let m := appendSection m `kernel "unfolded declarations" unfoldKernel
       let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index feaace0c8c..bcbfd9595f 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -637,7 +637,7 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
        (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {})
        fun ex =>
          if ex.isRuntime then
-           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}"
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}\n{useDiagnosticMsg}"
          else
            throw ex
 
@@ -720,7 +720,8 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
       unless defEq do
         trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
       return defEq
-    match s.cache.synthInstance.find? (localInsts, type) with
+    let cacheKey := { localInsts, type, synthPendingDepth := (← read).synthPendingDepth }
+    match s.cache.synthInstance.find? cacheKey with
     | some result =>
       trace[Meta.synthInstance] "result {result} (cached)"
       if let some inst := result then
@@ -767,7 +768,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
             pure (some result)
           else
             pure none
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert (localInsts, type) result? }
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
       pure result?
 
 /--
@@ -778,14 +779,17 @@ def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM
     (toLOptionM <| synthInstance? type maxResultSize?)
     (fun _ => pure LOption.undef)
 
+def throwFailedToSynthesize (type : Expr) : MetaM Expr :=
+  throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
+
 def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Expr :=
   catchInternalId isDefEqStuckExceptionId
     (do
       let result? ← synthInstance? type maxResultSize?
       match result? with
       | some result => pure result
-      | none        => throwError "failed to synthesize{indentExpr type}")
-    (fun _ => throwError "failed to synthesize{indentExpr type}")
+      | none        => throwFailedToSynthesize type)
+    (fun _ => throwFailedToSynthesize type)
 
 @[export lean_synth_pending]
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
@@ -799,9 +803,10 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
     | none   =>
       return false
     | some _ =>
-      /- TODO: use a configuration option instead of the hard-coded limit `1`. -/
-      if (← read).synthPendingDepth > 1 then
+      let max := maxSynthPendingDepth.get (← getOptions)
+      if (← read).synthPendingDepth > max then
         trace[Meta.synthPending] "too many nested synthPending invocations"
+        recordSynthPendingFailure mvarDecl.type
         return false
       else
         withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) do
diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out
index c776ae3043..535431abf0 100644
--- a/tests/lean/1007.lean.expected.out
+++ b/tests/lean/1007.lean.expected.out
@@ -6,5 +6,6 @@
 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 instance
+1007.lean:56:64-56:78: error: failed to synthesize
   IsLin fun x => sum fun i => norm x
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/1102.lean.expected.out b/tests/lean/1102.lean.expected.out
index c4e4a416ad..d94f2b5cb6 100644
--- a/tests/lean/1102.lean.expected.out
+++ b/tests/lean/1102.lean.expected.out
@@ -1,2 +1,3 @@
-1102.lean:22:35-22:49: error: failed to synthesize instance
+1102.lean:22:35-22:49: error: failed to synthesize
   DVR 1
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/1163.lean.expected.out b/tests/lean/1163.lean.expected.out
index 2e3c5a1c10..27d50a2426 100644
--- a/tests/lean/1163.lean.expected.out
+++ b/tests/lean/1163.lean.expected.out
@@ -1,7 +1,9 @@
 1163.lean:6:8-6:15: warning: declaration uses 'sorry'
 1163.lean:11:8-11:15: warning: declaration uses 'sorry'
-1163.lean:13:16-13:17: error: failed to synthesize instance
+1163.lean:13:16-13:17: error: failed to synthesize
   OfNat Bool 0
+use `set_option diagnostics true` to get diagnostic information
 1163.lean:15:8-15:15: warning: declaration uses 'sorry'
-1163.lean:18:18-18:19: error: failed to synthesize instance
+1163.lean:18:18-18:19: error: failed to synthesize
   OfNat Bool 0
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/2040.lean.expected.out b/tests/lean/2040.lean.expected.out
index bee56f1b47..9cf0cfb86e 100644
--- a/tests/lean/2040.lean.expected.out
+++ b/tests/lean/2040.lean.expected.out
@@ -1,9 +1,12 @@
-2040.lean:8:8-8:13: error: failed to synthesize instance
+2040.lean:8:8-8:13: error: failed to synthesize
   HPow Nat Nat Int
-2040.lean:14:8-14:13: error: failed to synthesize instance
+use `set_option diagnostics true` to get diagnostic information
+2040.lean:14:8-14:13: error: failed to synthesize
   HPow Nat Nat Int
-2040.lean:20:8-20:13: error: failed to synthesize instance
+use `set_option diagnostics true` to get diagnostic information
+2040.lean:20:8-20:13: error: failed to synthesize
   HPow Nat Nat Int
+use `set_option diagnostics true` to get diagnostic information
 2040.lean:18:2-20:22: error: type mismatch
   trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
 has type
diff --git a/tests/lean/2220.lean.expected.out b/tests/lean/2220.lean.expected.out
index 5857adb753..8b03b90883 100644
--- a/tests/lean/2220.lean.expected.out
+++ b/tests/lean/2220.lean.expected.out
@@ -6,11 +6,13 @@
   (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3))
     (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
 @HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
-2220.lean:25:19-25:24: error: failed to synthesize instance
+2220.lean:25:19-25:24: error: failed to synthesize
   HPow Nat Nat Int
+use `set_option diagnostics true` to get diagnostic information
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
-2220.lean:26:12-26:17: error: failed to synthesize instance
+2220.lean:26:12-26:17: error: failed to synthesize
   HPow Nat Nat Int
+use `set_option diagnostics true` to get diagnostic information
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
diff --git a/tests/lean/2273.lean.expected.out b/tests/lean/2273.lean.expected.out
index 2c16d7eafc..c15377bb35 100644
--- a/tests/lean/2273.lean.expected.out
+++ b/tests/lean/2273.lean.expected.out
@@ -1,2 +1,3 @@
-2273.lean:9:8-9:14: error: failed to synthesize instance
+2273.lean:9:8-9:14: error: failed to synthesize
   P 37
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out
index 00e5143b01..ad6159c11b 100644
--- a/tests/lean/297.lean.expected.out
+++ b/tests/lean/297.lean.expected.out
@@ -1,2 +1,3 @@
-297.lean:1:10-1:11: error: failed to synthesize instance
+297.lean:1:10-1:11: error: failed to synthesize
   OfNat (Sort ?u) 0
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/345.lean.expected.out b/tests/lean/345.lean.expected.out
index 44f54843bd..bdbcc2fdb1 100644
--- a/tests/lean/345.lean.expected.out
+++ b/tests/lean/345.lean.expected.out
@@ -1,6 +1,9 @@
-345.lean:1:12-1:13: error: failed to synthesize instance
+345.lean:1:12-1:13: error: failed to synthesize
   OfNat (Sort ?u) 1
-345.lean:4:8-4:9: error: failed to synthesize instance
+use `set_option diagnostics true` to get diagnostic information
+345.lean:4:8-4:9: error: failed to synthesize
   OfNat (Sort ?u) 1
-345.lean:6:19-6:20: error: failed to synthesize instance
+use `set_option diagnostics true` to get diagnostic information
+345.lean:6:19-6:20: error: failed to synthesize
   OfNat (Sort ?u) 1
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/386.lean.expected.out b/tests/lean/386.lean.expected.out
index f0238a0bc6..21c952dd87 100644
--- a/tests/lean/386.lean.expected.out
+++ b/tests/lean/386.lean.expected.out
@@ -1,2 +1,3 @@
-386.lean:9:2-9:46: error: failed to synthesize instance
+386.lean:9:2-9:46: error: failed to synthesize
   Fintype ?m
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/448.lean.expected.out b/tests/lean/448.lean.expected.out
index 76e64e6e3f..14d369862a 100644
--- a/tests/lean/448.lean.expected.out
+++ b/tests/lean/448.lean.expected.out
@@ -1,2 +1,3 @@
-448.lean:21:2-23:20: error: failed to synthesize instance
+448.lean:21:2-23:20: error: failed to synthesize
   MonadExceptOf IO.Error M
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/attrCmd.lean.expected.out b/tests/lean/attrCmd.lean.expected.out
index 5c402508af..814c35d447 100644
--- a/tests/lean/attrCmd.lean.expected.out
+++ b/tests/lean/attrCmd.lean.expected.out
@@ -1,2 +1,3 @@
-attrCmd.lean:6:0-6:6: error: failed to synthesize instance
+attrCmd.lean:6:0-6:6: error: failed to synthesize
   Pure M
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out
index 4c0e353dc6..2ac5779a74 100644
--- a/tests/lean/calcErrors.lean.expected.out
+++ b/tests/lean/calcErrors.lean.expected.out
@@ -12,6 +12,7 @@ calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
   p a
 calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
+use `set_option diagnostics true` to get diagnostic information
 calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
   γ : Sort u_1
 previous right-hand-side is
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index 5a744d0f9e..8bb2e82879 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/tests/lean/defInst.lean.expected.out
@@ -1,6 +1,7 @@
 [4, 5, 6]
-defInst.lean:8:26-8:32: error: failed to synthesize instance
+defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
+use `set_option diagnostics true` to get diagnostic information
 fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
diff --git a/tests/lean/defaultInstance.lean.expected.out b/tests/lean/defaultInstance.lean.expected.out
index 786f08a893..8612de8a01 100644
--- a/tests/lean/defaultInstance.lean.expected.out
+++ b/tests/lean/defaultInstance.lean.expected.out
@@ -1,4 +1,5 @@
-defaultInstance.lean:20:20-20:23: error: failed to synthesize instance
+defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
+use `set_option diagnostics true` to get diagnostic information
 defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
   Foo Bool (?m x)
diff --git a/tests/lean/eagerUnfoldingIssue.lean.expected.out b/tests/lean/eagerUnfoldingIssue.lean.expected.out
index e116b6dd13..ff3e277fa7 100644
--- a/tests/lean/eagerUnfoldingIssue.lean.expected.out
+++ b/tests/lean/eagerUnfoldingIssue.lean.expected.out
@@ -1,4 +1,6 @@
-eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize instance
+eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
   MonadLog (StateM Nat)
-eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize instance
+use `set_option diagnostics true` to get diagnostic information
+eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
   MonadLog (StateM Nat)
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/eraseInsts.lean.expected.out b/tests/lean/eraseInsts.lean.expected.out
index 7f0ce21b86..7fbc16acae 100644
--- a/tests/lean/eraseInsts.lean.expected.out
+++ b/tests/lean/eraseInsts.lean.expected.out
@@ -1,2 +1,3 @@
-eraseInsts.lean:12:22-12:27: error: failed to synthesize instance
+eraseInsts.lean:12:22-12:27: error: failed to synthesize
   HAdd Foo Foo ?m
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out
index f115441e1f..860344f9ea 100644
--- a/tests/lean/forErrors.lean.expected.out
+++ b/tests/lean/forErrors.lean.expected.out
@@ -1,2 +1,3 @@
-forErrors.lean:3:29-3:30: error: failed to synthesize instance
+forErrors.lean:3:29-3:30: error: failed to synthesize
   ToStream α ?m
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/kernelMVarBug.lean.expected.out b/tests/lean/kernelMVarBug.lean.expected.out
index cb26e365b3..19feec3023 100644
--- a/tests/lean/kernelMVarBug.lean.expected.out
+++ b/tests/lean/kernelMVarBug.lean.expected.out
@@ -1,2 +1,3 @@
-kernelMVarBug.lean:5:15-5:20: error: failed to synthesize instance
+kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 5852b673fc..f044792348 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -9,8 +9,9 @@ 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 instance
+macroStack.lean:17:0-17:6: error: failed to synthesize
   HAdd Nat String ?m
+use `set_option diagnostics true` to get diagnostic information
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
 while expanding
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index 3ee7f64c07..a5f6b79cda 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/tests/lean/macroSwizzle.lean.expected.out
@@ -1,5 +1,6 @@
-macroSwizzle.lean:4:7-4:23: error: failed to synthesize instance
+macroSwizzle.lean:4:7-4:23: error: failed to synthesize
   HAdd Bool String ?m
+use `set_option diagnostics true` to get diagnostic information
 macroSwizzle.lean:6:7-6:10: error: application type mismatch
   Nat.succ "x"
 argument
diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out
index b44c5cfebe..f2449eb935 100644
--- a/tests/lean/openScoped.lean.expected.out
+++ b/tests/lean/openScoped.lean.expected.out
@@ -1,6 +1,7 @@
 openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon'
-openScoped.lean:4:2-4:24: error: failed to synthesize instance
+openScoped.lean:4:2-4:24: error: failed to synthesize
   Decidable (f = g)
+use `set_option diagnostics true` to get diagnostic information
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon'
 openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon'
diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out
index f175e7d2fd..c069a518e7 100644
--- a/tests/lean/prvCtor.lean.expected.out
+++ b/tests/lean/prvCtor.lean.expected.out
@@ -4,8 +4,9 @@ prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.E
 prvCtor.lean:23:0-25:61: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
-  failed to synthesize instance
+  failed to synthesize
     EmptyCollection (Name "hello")
+  use `set_option diagnostics true` to get diagnostic information
   
   invalid {...} notation, constructor for `Name` is marked as private
 prvCtor.lean:31:25-31:34: error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private
diff --git a/tests/lean/run/3313.lean b/tests/lean/run/3313.lean
new file mode 100644
index 0000000000..3b3874b557
--- /dev/null
+++ b/tests/lean/run/3313.lean
@@ -0,0 +1,49 @@
+class Zero (α : Type) where
+  zero : α
+
+class AddCommGroup (α : Type) extends Zero α where
+
+class Ring (α : Type) extends Zero α, AddCommGroup α
+
+class Module (R : Type) (M : Type) [Zero R] [Zero M] where
+
+instance (R : Type) [Zero R] : Module R R := ⟨⟩
+
+structure Submodule (R : Type) (M : Type) [Zero R] [Zero M] [Module R M] : Type where
+
+class HasQuotient (A : outParam <| Type) (B : Type) where
+  quotient' : B → Type
+
+instance Submodule.hasQuotient {R : Type} {M : Type} [Ring R] [AddCommGroup M]
+  [Module R M]: HasQuotient M (Submodule R M) := ⟨fun _ => M⟩
+
+def Synonym (M : Type) [Zero M] := M
+
+instance Synonym.zero {G : Type} [Zero G] : Zero (Synonym G) := ⟨(Zero.zero : G)⟩
+
+instance Synonym.addCommGroup {G : Type} [AddCommGroup G] : AddCommGroup (Synonym G) :=
+  { Synonym.zero with }
+
+instance Synonym.module (M : Type) {R : Type} [Zero R] [Zero M] [Module R M] :
+    Module R (Synonym M) := { }
+
+variable (R : Type) [Ring R]
+
+
+set_option maxSynthPendingDepth 2 in
+#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- works
+
+/--
+info: [type_class] max synth pending failures (maxSynthPendingDepth: 1), use `set_option maxSynthPendingDepth <limit>`
+    AddCommGroup Ruse `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+---
+error: failed to synthesize
+  HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+set_option diagnostics true in
+#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- fails
+
+set_option maxSynthPendingDepth 2 in
+#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- still works
diff --git a/tests/lean/run/3996.lean b/tests/lean/run/3996.lean
index 65bae07a33..cd2592851c 100644
--- a/tests/lean/run/3996.lean
+++ b/tests/lean/run/3996.lean
@@ -17,6 +17,7 @@ instance instB10000 : B 10000 where
 /--
 error: failed to synthesize
   A
+use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs in
 #synth A -- should fail quickly
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
index e85f273f63..d9399c65cf 100644
--- a/tests/lean/run/guard_msgs.lean
+++ b/tests/lean/run/guard_msgs.lean
@@ -46,8 +46,9 @@ example : α := x
 
 #guard_msgs in
 /--
-error: failed to synthesize instance
+error: failed to synthesize
   OfNat α 22
+use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs(error) in
 example : α := 22
@@ -100,13 +101,19 @@ run_meta Lean.logInfo "foo ⏎\nbar"
 Lax whitespace
 -/
 
-/-- error: failed to synthesize DecidableEq (Nat → Nat) -/
+/--
+error: failed to synthesize
+  DecidableEq (Nat → Nat)
+use `set_option diagnostics true` to get diagnostic information
+-/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
 
-/-- error: failed to synthesize
-
-DecidableEq (Nat → Nat) -/
+/--
+error: failed to synthesize
+  DecidableEq (Nat → Nat)
+use `set_option diagnostics true` to get diagnostic information
+-/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
 
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 8a0da14088..0e2eeb68d6 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -8,6 +8,7 @@ sanitychecks.lean:4:8-5:10: error: 'partial' theorems are not allowed, 'partial'
 sanitychecks.lean:7:7-8:10: error: 'unsafe' theorems are not allowed
 sanitychecks.lean:10:0-10:23: error: failed to synthesize
   Inhabited False
+use `set_option diagnostics true` to get diagnostic information
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False
 sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty
diff --git a/tests/lean/scopedLocalInsts.lean.expected.out b/tests/lean/scopedLocalInsts.lean.expected.out
index dbf148427f..9a3ab1cac8 100644
--- a/tests/lean/scopedLocalInsts.lean.expected.out
+++ b/tests/lean/scopedLocalInsts.lean.expected.out
@@ -1,9 +1,12 @@
-scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize instance
+scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize
   ToString A
+use `set_option diagnostics true` to get diagnostic information
 "A.mk 10 20"
-scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize instance
+scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize
   ToString A
+use `set_option diagnostics true` to get diagnostic information
 "{ x := 10, y := 20 }"
-scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize instance
+scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize
   ToString A
+use `set_option diagnostics true` to get diagnostic information
 "A.mk 10 20"
diff --git a/tests/lean/semicolonOrLinebreak.lean.expected.out b/tests/lean/semicolonOrLinebreak.lean.expected.out
index 1a0522add0..2383a4e139 100644
--- a/tests/lean/semicolonOrLinebreak.lean.expected.out
+++ b/tests/lean/semicolonOrLinebreak.lean.expected.out
@@ -5,5 +5,6 @@ semicolonOrLinebreak.lean:20:4-20:7: error: function expected at
   x
 term has type
   Nat
-semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize instance
+semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize
   Singleton ?m Point
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/setLit.lean.expected.out b/tests/lean/setLit.lean.expected.out
index a761f07149..1f63e7cc4c 100644
--- a/tests/lean/setLit.lean.expected.out
+++ b/tests/lean/setLit.lean.expected.out
@@ -1,10 +1,12 @@
 setLit.lean:22:19-22:21: error: overloaded, errors 
-  failed to synthesize instance
+  failed to synthesize
     EmptyCollection String
+  use `set_option diagnostics true` to get diagnostic information
   
   fields missing: 'data'
 setLit.lean:24:31-24:38: error: overloaded, errors 
-  failed to synthesize instance
+  failed to synthesize
     Singleton Nat String
+  use `set_option diagnostics true` to get diagnostic information
   
   24:33 'val' is not a field of structure 'String'
diff --git a/tests/lean/tcloop.lean.expected.out b/tests/lean/tcloop.lean.expected.out
index ca7a0fb613..4b0a694e9a 100644
--- a/tests/lean/tcloop.lean.expected.out
+++ b/tests/lean/tcloop.lean.expected.out
@@ -3,3 +3,4 @@ tcloop.lean:14:2-14:15: error: failed to synthesize
 (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
 use `set_option synthInstance.maxHeartbeats <num>` to set the limit
 use `set_option diagnostics true` to get diagnostic information
+use `set_option diagnostics true` to get diagnostic information
diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out
index 12b0b73d8f..65329e1845 100644
--- a/tests/lean/typeOf.lean.expected.out
+++ b/tests/lean/typeOf.lean.expected.out
@@ -1,7 +1,9 @@
-typeOf.lean:11:22-11:25: error: failed to synthesize instance
+typeOf.lean:11:22-11:25: error: failed to synthesize
   HAdd Nat Nat Bool
-typeOf.lean:12:0-12:5: error: failed to synthesize instance
+use `set_option diagnostics true` to get diagnostic information
+typeOf.lean:12:0-12:5: error: failed to synthesize
   HAdd Bool Nat Nat
+use `set_option diagnostics true` to get diagnostic information
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool : Type
 but is expected to have type