perf: share depth-invariant type class cache entries across synthPendingDepth

The type class resolution cache is keyed by `synthPendingDepth` (issue #2522), which partitions the whole cache by depth even though the depth can only influence a query through the `synthPending` give-up check. Track whether a query ever reached a `synthPending` decision (via a non-backtrackable `IO.Ref` in `Meta.Context`, so discarded search branches still count); results of queries that never did are now cached with `synthPendingDepth := none` and shared across all depths. Depth-sensitive results remain keyed by their exact depth as before. The `Meta.synthInstance.cache` trace now includes the depth when it is nonzero.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: Kha

src/Lean/Meta/Basic.lean

@@ -329,10 +329,19 @@ structure SynthInstanceCacheKey where
   localInsts        : LocalInstances
   type              : Expr
   /--
-  Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
-  See issue #2522.
+  Value of `synthPendingDepth` when the instance was synthesized or failed to be
+  synthesized, or `none` if the result can be reused at other depths.
+
+  `synthPendingDepth` can influence the result of a query because `synthPending` gives up
+  when `synthPendingDepth > maxSynthPendingDepth`, so a result may not be reused at a
+  different depth (see issue #2522). However, this is the *only* way the depth can influence
+  a query. Thus, if no `synthPending` invocation gave up while synthesizing an instance, the
+  result is valid at every depth at which the guard still cannot trigger, and is stored with
+  `synthPendingDepth := none` together with a validity bound in the cache entry (see
+  `SynthInstanceCacheEntry.relSynthPendingDepth`). Only results whose synthesis hit the
+  give-up threshold remain keyed by their exact depth.
   -/
-  synthPendingDepth : Nat
+  synthPendingDepth : Option Nat
   deriving Hashable, BEq
 
 /-- Resulting type for `abstractMVars` -/
@@ -345,7 +354,20 @@ structure AbstractMVarsResult where
 def AbstractMVarsResult.numMVars (r : AbstractMVarsResult) : Nat :=
   r.mvars.size
 
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
+/-- Entry of the type class resolution cache. -/
+structure SynthInstanceCacheEntry where
+  /--
+  Maximum `synthPendingDepth` at which a `synthPending` decision was reached during the
+  synthesis, relative to the query's own `synthPendingDepth`, or `none` if no such decision
+  was reached. An entry stored under `synthPendingDepth := none` may be reused by a query at
+  depth `d` iff `relSynthPendingDepth` is `none` or `d + relSynthPendingDepth` does not
+  exceed `maxSynthPendingDepth`: under that bound no `synthPending` invocation can reach the
+  give-up threshold, so the synthesis behaves identically at depth `d`.
+  -/
+  relSynthPendingDepth : Option Nat := none
+  result               : Option AbstractMVarsResult
+
+abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey SynthInstanceCacheEntry
 
 -- Key for `InferType` and `WHNF` caches
 structure ExprConfigCacheKey where
@@ -460,6 +482,17 @@ register_builtin_option maxSynthPendingDepth : Nat := {
   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."
 }
 
+/--
+Accumulated `synthPending` decisions of a type class query, used by the type class
+resolution cache to bound the `synthPendingDepth` values at which the result may be reused.
+See `SynthInstanceCacheEntry.relSynthPendingDepth`.
+-/
+structure SynthPendingActivity where
+  /-- Maximum `synthPendingDepth` at which a `synthPending` decision was reached. -/
+  maxDepth : Option Nat := none
+  /-- Whether some `synthPending` invocation gave up because of `maxSynthPendingDepth`. -/
+  guardHit : Bool       := false
+
 /--
   Contextual information for the `MetaM` monad.
 -/
@@ -500,6 +533,15 @@ structure Context where
     Remark: `synthPending` fails if `synthPendingDepth > maxSynthPendingDepth`.
   -/
   synthPendingDepth : Nat                  := 0
+  /--
+  When set, the reference accumulates the `synthPending` decisions reached during the
+  current type class query, i.e. behavior that may depend on `synthPendingDepth`. The type
+  class resolution cache uses this to decide at which depths a result may be reused; see
+  `SynthInstanceCacheKey.synthPendingDepth` and `SynthInstanceCacheEntry.relSynthPendingDepth`.
+  The reference is intentionally not part of the backtrackable state: a `synthPending`
+  invocation in a discarded search branch still influenced the search outcome.
+  -/
+  synthPendingActivityRef? : Option (IO.Ref SynthPendingActivity) := none
   /--
     A predicate to control whether a constant can be unfolded or not at `whnf`.
     Note that we do not cache results at `whnf` when `canUnfold?` is not `none`. -/

src/Lean/Meta/SynthInstance.lean

@@ -856,20 +856,23 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr
     applyAbstractResult? type abstResult?
 
 /-- Helper function for caching synthesized type class instances. -/
-private def cacheResult (cacheKey : SynthInstanceCacheKey) (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
-  -- **TODO**: simplify this function.
+private def cacheResult (cacheKey : SynthInstanceCacheKey) (relSynthPendingDepth : Option Nat)
+    (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
+  let insert (result : Option AbstractMVarsResult) : MetaM Unit :=
+    modify fun s => { s with
+      cache.synthInstance := s.cache.synthInstance.insert cacheKey { relSynthPendingDepth, result } }
   match abstResult? with
-  | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
+  | none => insert none
   | some abstResult =>
     if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then
       match result? with
-      | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
+      | none => insert none
       | some result =>
         -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
         -- we don't need to perform extra checks again when reusing result.
-        modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], mvars := #[] }) }
+        insert (some { expr := result, paramNames := #[], mvars := #[] })
     else
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
+      insert (some abstResult)
 
 def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
   let opts ← getOptions
@@ -882,16 +885,51 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let { type, cacheKeyType, kind } ← preprocess type
-    let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth }
-    match (← get).cache.synthInstance.find? cacheKey with
-    | some abstResult? =>
-      trace[Meta.synthInstance.cache] "cached: {type}"
-      let result? ← applyCachedAbstractResult? type abstResult?
+    let synthPendingDepth := (← read).synthPendingDepth
+    let depthSuffix : MessageData :=
+      if synthPendingDepth == 0 then m!"" else m!" (synthPendingDepth := {synthPendingDepth})"
+    -- Fold `synthPending` activity into the enclosing query's accumulator, if any.
+    let foldActivity (activity : SynthPendingActivity) : MetaM Unit := do
+      if activity.maxDepth.isSome || activity.guardHit then
+        if let some ref := (← read).synthPendingActivityRef? then
+          ref.modify fun a => {
+            maxDepth := match a.maxDepth, activity.maxDepth with
+              | some d₁, some d₂ => some (d₁.max d₂)
+              | some d, none | none, some d => some d
+              | none, none => none
+            guardHit := a.guardHit || activity.guardHit }
+    let applyCached (entry : SynthInstanceCacheEntry) : MetaM (Option Expr) := do
+      trace[Meta.synthInstance.cache] "cached{depthSuffix}: {type}"
+      let result? ← applyCachedAbstractResult? type entry.result
       trace[Meta.synthInstance] "result {result?} (cached)"
       return result?
-    | none =>
-      trace[Meta.synthInstance.cache] "new: {type}"
-      let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
+    let sharedKey : SynthInstanceCacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := none }
+    let depthKey := { sharedKey with synthPendingDepth := some synthPendingDepth }
+    let maxSynthPending := maxSynthPendingDepth.get (← getOptions)
+    let sharedEntry? :=
+      match (← get).cache.synthInstance.find? sharedKey with
+      | some entry =>
+        match entry.relSynthPendingDepth with
+        | none     => some entry
+        | some rel =>
+          -- Valid iff no `synthPending` invocation can reach the give-up threshold at the
+          -- current depth; see `SynthInstanceCacheEntry.relSynthPendingDepth`.
+          if synthPendingDepth + rel ≤ maxSynthPending then some entry else none
+      | none => none
+    if let some entry := sharedEntry? then
+      -- Reusing the entry re-enacts its `synthPending` decisions at the current depth.
+      foldActivity { maxDepth := entry.relSynthPendingDepth.map (synthPendingDepth + ·) }
+      applyCached entry
+    else if let some entry := (← get).cache.synthInstance.find? depthKey then
+      -- The entry's synthesis hit the `maxSynthPendingDepth` give-up, so reusing it keeps
+      -- the enclosing query depth-exact as well.
+      foldActivity { maxDepth := some synthPendingDepth, guardHit := true }
+      applyCached entry
+    else
+      trace[Meta.synthInstance.cache] "new{depthSuffix}: {type}"
+      let activityRef ← IO.mkRef {}
+      let abstResult? ← withReader (fun ctx => { ctx with synthPendingActivityRef? := some activityRef }) do
+        withNewMCtxDepth (allowLevelAssignments := true) do
         match kind with
         | .noMVars =>
           /-
@@ -918,7 +956,12 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
         | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize
       let result? ← applyAbstractResult? type abstResult?
       trace[Meta.synthInstance] "result {result?}"
-      cacheResult cacheKey kind abstResult? result?
+      let activity ← activityRef.get
+      foldActivity activity
+      -- Results whose synthesis hit the `maxSynthPendingDepth` give-up are only valid at
+      -- the exact depth; all others are shared, bounded by their relative activity depth.
+      let key := if activity.guardHit then depthKey else sharedKey
+      cacheResult key (activity.maxDepth.map (· - synthPendingDepth)) kind abstResult? result?
       return result?
 
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
@@ -957,8 +1000,15 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
     | none   =>
       return false
     | some _ =>
+      let depth := (← read).synthPendingDepth
+      -- Record the `synthPending` decision reached at `depth`; the enclosing type class
+      -- query's cache entry (if any) is only valid at depths where it comes out the same.
+      if let some ref := (← read).synthPendingActivityRef? then
+        ref.modify fun a => { a with maxDepth := some ((a.maxDepth.getD 0).max depth) }
       let max := maxSynthPendingDepth.get (← getOptions)
-      if (← read).synthPendingDepth > max then
+      if depth > max then
+        if let some ref := (← read).synthPendingActivityRef? then
+          ref.modify fun a => { a with guardHit := true }
         trace[Meta.synthPending] "too many nested synthPending invocations"
         recordSynthPendingFailure mvarDecl.type
         return false

tests/elab/tc_cache_synth_pending_depth.lean

@@ -0,0 +1,141 @@
+import Lean
+
+/-!
+Fine-grained `synthPendingDepth` handling in the type-class resolution cache
+(`SynthInstanceCacheKey.synthPendingDepth : Option Nat`).
+
+Cache entries whose synthesis never reached a `synthPending` decision are depth-invariant
+and shared across `synthPendingDepth` levels. Entries whose synthesis reached decisions up
+to relative depth `r` (without any giving up) are shared with queries at depth `d` as long
+as `d + r ≤ maxSynthPendingDepth`, i.e. as long as no decision can come out differently.
+Entries whose synthesis gave up at `maxSynthPendingDepth` remain keyed by their exact
+depth, preserving the fix for issue #2522.
+
+`Meta.synthPending` fires when unification is stuck on a pending instance metavariable,
+e.g. a class projection applied to an unassigned instance mvar. The tests below construct
+pending mvars by hand and simulate nested queries by setting `synthPendingDepth` directly.
+The taint tests use a *local* instance because local instances are candidates regardless
+of discrimination-tree keys, so a stuck projection in its type meets the rigid goal during
+`tryResolve`.
+-/
+
+open Lean Meta
+
+structure Wr (α : Type) : Type
+
+class LeafT (α : Type) where T : Type
+instance iLeafT : LeafT (Wr Nat) := ⟨Nat⟩
+
+class Out (α : Type) (β : outParam Type) where
+instance iOut : Out (Wr Nat) Nat := ⟨⟩
+
+class Root (α : Type) where
+
+def wrNat : Expr := mkApp (mkConst ``Wr) (mkConst ``Nat)
+def leafTWr : Expr := mkApp (mkConst ``LeafT) wrNat
+def projT (h : Expr) : Expr := mkApp2 (mkConst ``LeafT.T) wrNat h
+def rootNat : Expr := mkApp (mkConst ``Root) (mkConst ``Nat)
+
+def withTCTrace (x : MetaM α) : MetaM α :=
+  withOptions (fun o =>
+    (o.setBool `trace.Meta.synthInstance.cache true).setBool `trace.Meta.synthPending true) x
+
+def atDepth (d : Nat) (x : MetaM α) : MetaM α :=
+  withReader (fun ctx : Meta.Context => { ctx with synthPendingDepth := d }) x
+
+set_option maxSynthPendingDepth 1
+
+/-!
+`LeafT (Wr Nat)` synthesis never reaches a `synthPending` decision, so its cache entry is
+depth-invariant: computed at depth 0, it is reused at depths 1 and 2.
+-/
+/--
+trace: [Meta.synthInstance.cache] new: LeafT (Wr Nat)
+[Meta.synthInstance.cache] cached (synthPendingDepth := 1): LeafT (Wr Nat)
+[Meta.synthInstance.cache] cached (synthPendingDepth := 2): LeafT (Wr Nat)
+-/
+#guard_msgs in
+run_meta withTCTrace do
+  discard <| synthInstance? leafTWr
+  discard <| atDepth 1 do synthInstance? leafTWr
+  discard <| atDepth 2 do synthInstance? leafTWr
+
+/-!
+A query with a stuck projection in an `outParam` position: the search itself is
+depth-invariant (the out-param is replaced by a fresh mvar before the search), and the
+depth-sensitive `synthPending` happens while assigning the out-params to the caller's
+arguments, which is re-run on every cache hit. Hence the `Out` entry is shared with the
+depth-1 query, and the nested `LeafT (Wr Nat)` query (depth 1 first, then depth 2 on the
+cache hit) reuses the depth-invariant entry as well.
+-/
+/--
+trace: [Meta.synthInstance.cache] new: Out (Wr Nat) (LeafT.T (Wr Nat))
+[Meta.synthPending] synthPending ?m.1
+[Meta.synthInstance.cache] new (synthPendingDepth := 1): LeafT (Wr Nat)
+[Meta.synthInstance.cache] cached (synthPendingDepth := 1): Out (Wr Nat) (LeafT.T (Wr Nat))
+[Meta.synthPending] synthPending ?m.2
+[Meta.synthInstance.cache] cached (synthPendingDepth := 2): LeafT (Wr Nat)
+-/
+#guard_msgs in
+run_meta withTCTrace do
+  discard <| synthInstance? (mkApp2 (mkConst ``Out) wrNat (projT (← mkFreshExprMVar leafTWr)))
+  discard <| atDepth 1 do
+    synthInstance? (mkApp2 (mkConst ``Out) wrNat (projT (← mkFreshExprMVar leafTWr)))
+
+/-!
+A local instance of type `Root (LeafT.T (Wr Nat) ?hP)` forces `synthPending ?hP` *inside*
+the search for the rigid goal `Root Nat`. The `synthPending` decision is reached at
+relative depth 0 and does not give up, so the depth-0 entry is valid for depths `d` with
+`d + 0 ≤ maxSynthPendingDepth`: it is reused at depths 0 and 1, but not at depth 2. (The
+depth-2 recomputation finds `?hP` already assigned by the first query, so it performs no
+`synthPending` at all and its entry is unbounded.)
+-/
+/--
+trace: [Meta.synthInstance.cache] new: Root Nat
+[Meta.synthPending] synthPending ?m.1
+[Meta.synthInstance.cache] new (synthPendingDepth := 1): LeafT (Wr Nat)
+[Meta.synthPending] synthPending ?m.1
+[Meta.synthInstance.cache] cached (synthPendingDepth := 1): LeafT (Wr Nat)
+[Meta.synthInstance.cache] cached: Root Nat
+[Meta.synthInstance.cache] cached (synthPendingDepth := 1): Root Nat
+[Meta.synthInstance.cache] new (synthPendingDepth := 2): Root Nat
+-/
+#guard_msgs in
+run_meta do
+  let hP ← mkFreshExprMVar leafTWr
+  withLocalDecl `linst .instImplicit (mkApp (mkConst ``Root) (projT hP)) fun _ => withTCTrace do
+    discard <| synthInstance? rootNat
+    discard <| synthInstance? rootNat
+    discard <| atDepth 1 do synthInstance? rootNat
+    discard <| atDepth 2 do synthInstance? rootNat
+
+/-!
+Issue #2522: at depth 2, `synthPending` gives up (`synthPendingDepth > maxSynthPendingDepth`)
+and the query *fails*. Here the failure aborts the search with an `isDefEqStuck` exception,
+so nothing is cached at all (both depth-2 queries recompute), and in particular the depth-0
+query is unaffected by the depth-2 failures and succeeds.
+-/
+/--
+info: depth 2: failed
+---
+info: depth 0: synthesized
+---
+trace: [Meta.synthInstance.cache] new (synthPendingDepth := 2): Root Nat
+[Meta.synthPending] too many nested synthPending invocations
+[Meta.synthInstance.cache] new (synthPendingDepth := 2): Root Nat
+[Meta.synthPending] too many nested synthPending invocations
+[Meta.synthInstance.cache] new: Root Nat
+[Meta.synthPending] synthPending ?m.1
+[Meta.synthInstance.cache] new (synthPendingDepth := 1): LeafT (Wr Nat)
+[Meta.synthPending] synthPending ?m.1
+[Meta.synthInstance.cache] cached (synthPendingDepth := 1): LeafT (Wr Nat)
+-/
+#guard_msgs in
+run_meta do
+  let hP ← mkFreshExprMVar leafTWr
+  withLocalDecl `linst .instImplicit (mkApp (mkConst ``Root) (projT hP)) fun _ => withTCTrace do
+    let r2 ← atDepth 2 do trySynthInstance rootNat
+    let r2' ← atDepth 2 do trySynthInstance rootNat
+    logInfo m!"depth 2: {if r2.toOption.isSome || r2'.toOption.isSome then "synthesized" else "failed"}"
+    let r0 ← synthInstance? rootNat
+    logInfo m!"depth 0: {if r0.isSome then "synthesized" else "failed"}"