perf: key type class resolution cache by query only

Kha · claude · Kha · commit 8b0a880a2033 · 2026-07-08T15:10:15.000Z
Drop `synthPendingDepth` from the type class resolution cache key: an entry now pairs an optional shared result (bounded by its relative `synthPending` activity depth) with an optional depth-exact result (from syntheses that hit the `maxSynthPendingDepth` give-up). Each query thus performs a single cache lookup, and both kinds of result for the same query can coexist without evicting each other.

Co-Authored-By: Claude Fable 5 &lt;noreply@anthropic.com&gt;
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
@@ -326,22 +326,8 @@ instance : Hashable InfoCacheKey where
 
 -- Remark: we don't need to store `Config.toKey` because typeclass resolution uses a fixed configuration.
 structure SynthInstanceCacheKey where
-  localInsts        : LocalInstances
-  type              : Expr
-  /--
-  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 : Option Nat
+  localInsts : LocalInstances
+  type       : Expr
   deriving Hashable, BEq
 
 /-- Resulting type for `abstractMVars` -/
@@ -354,18 +340,32 @@ structure AbstractMVarsResult where
 def AbstractMVarsResult.numMVars (r : AbstractMVarsResult) : Nat :=
   r.mvars.size
 
-/-- Entry of the type class resolution cache. -/
+/--
+Entry of the type class resolution cache. In both fields, a `none`
+`AbstractMVarsResult` records that the synthesis failed.
+
+`synthPendingDepth` can influence the result of a query because `synthPending` gives up
+when `synthPendingDepth > maxSynthPendingDepth` (see issue #2522) — and this is the *only*
+way the depth can influence a query. Each field's validity condition ensures that every
+`synthPending` decision reached during the stored synthesis comes out the same way for the
+reusing query, so the synthesis would behave identically at its depth.
+-/
 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`.
+  Result shared across `synthPendingDepth` values, together with the maximum
+  `synthPendingDepth` at which a `synthPending` decision was reached during its synthesis,
+  relative to the query's own depth (`none` if no decision was reached). It may be reused
+  by a query at depth `d` iff the bound is `none` or `d + bound` does not exceed
+  `maxSynthPendingDepth`: under that condition, no `synthPending` invocation can reach the
+  give-up threshold.
+  -/
+  shared? : Option (Option Nat × Option AbstractMVarsResult) := none
+  /--
+  Result of a synthesis during which some `synthPending` invocation gave up because of
+  `maxSynthPendingDepth`, together with the exact `synthPendingDepth` it was computed at;
+  it may only be reused at that exact depth.
   -/
-  relSynthPendingDepth : Option Nat := none
-  result               : Option AbstractMVarsResult
+  exact?  : Option (Nat × Option AbstractMVarsResult) := none
 
 abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey SynthInstanceCacheEntry
 
@@ -485,7 +485,7 @@ register_builtin_option maxSynthPendingDepth : Nat := {
 /--
 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`.
+See `SynthInstanceCacheEntry`.
 -/
 structure SynthPendingActivity where
   /-- Maximum `synthPendingDepth` at which a `synthPending` decision was reached. -/
@@ -537,7 +537,7 @@ structure Context where
   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`.
+  `SynthInstanceCacheEntry`.
   The reference is intentionally not part of the backtrackable state: a `synthPending`
   invocation in a discarded search branch still influenced the search outcome.
   -/
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
@@ -856,11 +856,24 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr
     applyAbstractResult? type abstResult?
 
 /-- Helper function for caching synthesized type class instances. -/
-private def cacheResult (cacheKey : SynthInstanceCacheKey) (relSynthPendingDepth : Option Nat)
-    (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
+private def cacheResult (cacheKey : SynthInstanceCacheKey) (synthPendingDepth : Nat)
+    (activity : SynthPendingActivity) (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 } }
+    modify fun s => { s with cache.synthInstance :=
+      -- Merge into the existing entry (if any) so that shared and depth-exact results for
+      -- the same key can coexist. Re-reading the entry here is required for correctness:
+      -- nested queries during the search may have stored results for the same key.
+      let entry := s.cache.synthInstance.find? cacheKey |>.getD {}
+      let entry :=
+        if activity.guardHit then
+          -- The synthesis hit the `maxSynthPendingDepth` give-up, so the result is only
+          -- valid at the exact depth; all others are shared, bounded by their relative
+          -- activity depth.
+          { entry with exact? := some (synthPendingDepth, result) }
+        else
+          { entry with shared? := some (activity.maxDepth.map (· - synthPendingDepth), result) }
+      s.cache.synthInstance.insert cacheKey entry }
   match abstResult? with
   | none => insert none
   | some abstResult =>
@@ -874,6 +887,10 @@ private def cacheResult (cacheKey : SynthInstanceCacheKey) (relSynthPendingDepth
     else
       insert (some abstResult)
 
+/-- Trace-message suffix showing a nonzero `synthPendingDepth`. -/
+private def depthSuffix (synthPendingDepth : Nat) : MessageData :=
+  if synthPendingDepth == 0 then m!"" else m!" (synthPendingDepth := {synthPendingDepth})"
+
 def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
@@ -886,8 +903,6 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
     let type ← instantiateMVars type
     let { type, cacheKeyType, kind } ← preprocess type
     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
@@ -898,71 +913,64 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
               | 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
+    let applyCached (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
+      trace[Meta.synthInstance.cache] "cached{depthSuffix synthPendingDepth}: {type}"
+      let result? ← applyCachedAbstractResult? type abstResult?
       trace[Meta.synthInstance] "result {result?} (cached)"
       return result?
-    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 =>
-          /-
-          **Note**: The expensive `preprocessOutParam` step is morally **not** needed here because
-          the output params should be uniquely determined by the input params. During type class
-          resolution, definitional equality only unfolds `[reducible]` and `[instance_reducible]`
-          declarations. This is a contract with our users to ensure performance is reasonable.
-          However, the same `OrderDual` declaration that creates problems for `assignOutParams`
-          also prevents us from using this optimization. As an example, suppose we are trying to
-          synthesize
-          ```
-          FunLike F (OrderDual α) (OrderDual β)
-          ```
-          where the last two arguments of `FunLike` are output parameters. This term has no
-          metavariables, and it seems natural to skip `preprocessOutParam`, which would replace
-          the last two arguments with metavariables. However, if we don't replace them,
-          TC resolution fails because it cannot unfold `OrderDual` since it is semireducible.
-
-          **Note**: We should remove `preprocessOutParam` from the following line as soon as
-          Mathlib refactors `OrderDual`.
-          -/
-          SynthInstance.main (← preprocessOutParam type) maxResultSize
-        | .mvarsNoOutputParams => SynthInstance.main type maxResultSize
-        | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize
-      let result? ← applyAbstractResult? type abstResult?
-      trace[Meta.synthInstance] "result {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?
+    let key : SynthInstanceCacheKey := { localInsts, type := cacheKeyType }
+    if let some entry := (← get).cache.synthInstance.find? key then
+      if let some (rel, abstResult?) := entry.shared? then
+        -- Valid iff no `synthPending` invocation can reach the give-up threshold at the
+        -- current depth; see `SynthInstanceCacheEntry.shared?`.
+        let valid ←
+          match rel with
+          | none     => pure true
+          | some rel => do pure (synthPendingDepth + rel ≤ maxSynthPendingDepth.get (← getOptions))
+        if valid then
+          -- Reusing the result re-enacts its `synthPending` decisions at the current depth.
+          foldActivity { maxDepth := match rel with | none => none | some rel => some (synthPendingDepth + rel) }
+          return (← applyCached abstResult?)
+      if let some (depth, abstResult?) := entry.exact? then
+        if depth == synthPendingDepth then
+          -- The result's synthesis hit the `maxSynthPendingDepth` give-up, so reusing it
+          -- keeps the enclosing query depth-exact as well.
+          foldActivity { maxDepth := some synthPendingDepth, guardHit := true }
+          return (← applyCached abstResult?)
+    trace[Meta.synthInstance.cache] "new{depthSuffix synthPendingDepth}: {type}"
+    let activityRef ← IO.mkRef {}
+    let abstResult? ← withReader (fun ctx => { ctx with synthPendingActivityRef? := some activityRef }) do
+      withNewMCtxDepth (allowLevelAssignments := true) do
+      match kind with
+      | .noMVars =>
+        /-
+        **Note**: The expensive `preprocessOutParam` step is morally **not** needed here because
+        the output params should be uniquely determined by the input params. During type class
+        resolution, definitional equality only unfolds `[reducible]` and `[instance_reducible]`
+        declarations. This is a contract with our users to ensure performance is reasonable.
+        However, the same `OrderDual` declaration that creates problems for `assignOutParams`
+        also prevents us from using this optimization. As an example, suppose we are trying to
+        synthesize
+        ```
+        FunLike F (OrderDual α) (OrderDual β)
+        ```
+        where the last two arguments of `FunLike` are output parameters. This term has no
+        metavariables, and it seems natural to skip `preprocessOutParam`, which would replace
+        the last two arguments with metavariables. However, if we don't replace them,
+        TC resolution fails because it cannot unfold `OrderDual` since it is semireducible.
+
+        **Note**: We should remove `preprocessOutParam` from the following line as soon as
+        Mathlib refactors `OrderDual`.
+        -/
+        SynthInstance.main (← preprocessOutParam type) maxResultSize
+      | .mvarsNoOutputParams => SynthInstance.main type maxResultSize
+      | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize
+    let result? ← applyAbstractResult? type abstResult?
+    trace[Meta.synthInstance] "result {result?}"
+    let activity ← activityRef.get
+    foldActivity activity
+    cacheResult key synthPendingDepth activity 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
   synthInstanceCore? type maxResultSize?
