feat: add maxSynthPendingDepth

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

It also increases limit 2.

closes #3313
closes #3927

Author: leodemoura

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

@@ -283,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
 
 /--
@@ -306,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.
 -/
@@ -321,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`.
@@ -480,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
 
@@ -794,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
@@ -815,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/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