chore: fix tests

This commit also adds supports for tracking `synthPending` failures when using
`set_option diagnostics true`.

It also increases limit 2.

closes #3313
closes #3927

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
@@ -251,7 +253,7 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     throw <| Exception.error .missing "elaboration interrupted"
 
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at `{moduleName}`, 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 at `{moduleName}`, 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

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.

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

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

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"

src/Lean/Meta/SynthInstance.lean

@@ -640,7 +640,7 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
            action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {}
        catch 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
 
@@ -735,7 +735,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
@@ -782,7 +783,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?
 
 /--
@@ -793,14 +794,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
@@ -814,9 +818,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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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'

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

tests/lean/run/3313.lean

@@ -0,0 +1,47 @@
+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]
+
+#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 maxSynthPendingDepth 1 in
+set_option diagnostics true in
+#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- fails
+
+#synth HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R))) -- works

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

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)
 

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

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"

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

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'

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

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