perf: bound type class cache entry reuse by relative synthPending depth

Instead of a single depth-invariant class, each shared type class resolution cache entry now records the maximal `synthPendingDepth` (relative to the query) at which a `synthPending` decision was reached during synthesis, and is reused at any depth at which no such decision can reach the `maxSynthPendingDepth` give-up threshold. Only results whose synthesis actually hit the threshold remain keyed to their exact depth.

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

Author: Kha

src/Lean/Meta/Basic.lean

@@ -329,14 +329,17 @@ structure SynthInstanceCacheKey where
   localInsts        : LocalInstances
   type              : Expr
   /--
-  Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized,
-  or `none` if the result is depth-invariant.
+  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` decision was reached while synthesizing an instance,
-  the result is valid at every depth and is stored with `synthPendingDepth := none`.
+  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 : Option Nat
   deriving Hashable, BEq
@@ -351,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
@@ -466,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.
 -/
@@ -507,13 +534,14 @@ structure Context where
   -/
   synthPendingDepth : Nat                  := 0
   /--
-  When set, the reference is set to `true` as soon as a `synthPending` decision is reached,
-  i.e. behavior that may depend on `synthPendingDepth`. The type class resolution cache uses
-  this to decide whether a result is depth-invariant; see `SynthInstanceCacheKey.synthPendingDepth`.
+  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 Bool) := none
+  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
@@ -885,23 +888,46 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
     let synthPendingDepth := (← read).synthPendingDepth
     let depthSuffix : MessageData :=
       if synthPendingDepth == 0 then m!"" else m!" (synthPendingDepth := {synthPendingDepth})"
-    let applyCached (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
+    -- 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 abstResult?
+      let result? ← applyCachedAbstractResult? type entry.result
       trace[Meta.synthInstance] "result {result?} (cached)"
       return result?
-    let invariantKey : SynthInstanceCacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := none }
-    let depthKey := { invariantKey with synthPendingDepth := some synthPendingDepth }
-    if let some abstResult? := (← get).cache.synthInstance.find? invariantKey then
-      applyCached abstResult?
-    else if let some abstResult? := (← get).cache.synthInstance.find? depthKey then
-      -- Reusing a depth-sensitive entry makes the enclosing query depth-sensitive as well.
-      if let some ref := (← read).synthPendingActivityRef? then
-        ref.set true
-      applyCached abstResult?
+    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 false
+      let activityRef ← IO.mkRef {}
       let abstResult? ← withReader (fun ctx => { ctx with synthPendingActivityRef? := some activityRef }) do
         withNewMCtxDepth (allowLevelAssignments := true) do
         match kind with
@@ -930,12 +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?}"
-      let depthSensitive ← activityRef.get
-      if depthSensitive then
-        -- Propagate depth sensitivity to the enclosing query, if any.
-        if let some ref := (← read).synthPendingActivityRef? then
-          ref.set true
-      cacheResult (if depthSensitive then depthKey else invariantKey) 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
@@ -974,12 +1000,15 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
     | none   =>
       return false
     | some _ =>
-      -- From here on, behavior depends on `synthPendingDepth`; mark the enclosing type
-      -- class query (if any) as depth-sensitive for caching purposes.
+      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.set true
+        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

@@ -5,9 +5,11 @@ 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 did reach one
-(including giving up at `maxSynthPendingDepth`) remain keyed by their exact depth,
-preserving the fix for issue #2522.
+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
@@ -82,8 +84,11 @@ run_meta withTCTrace do
 
 /-!
 A local instance of type `Root (LeafT.T (Wr Nat) ?hP)` forces `synthPending ?hP` *inside*
-the search for the rigid goal `Root Nat`, so the entry is depth-sensitive: the depth-0
-entry is reused at depth 0 but not at depth 1.
+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
@@ -92,7 +97,8 @@ trace: [Meta.synthInstance.cache] new: Root Nat
 [Meta.synthPending] synthPending ?m.1
 [Meta.synthInstance.cache] cached (synthPendingDepth := 1): LeafT (Wr Nat)
 [Meta.synthInstance.cache] cached: Root Nat
-[Meta.synthInstance.cache] new (synthPendingDepth := 1): Root Nat
+[Meta.synthInstance.cache] cached (synthPendingDepth := 1): Root Nat
+[Meta.synthInstance.cache] new (synthPendingDepth := 2): Root Nat
 -/
 #guard_msgs in
 run_meta do
@@ -101,6 +107,7 @@ run_meta 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`)