fix: only persist context-free type class resolution cache entries

Results with abstracted metavariables are only valid relative to the elaboration context that created them: degrees of freedom not determined by the cache key (e.g. universe metavariables of intermediate instances, cf. `Small`) are resolved by ambient unification constraints. Persisting such entries and reusing them in a different context (a later command, or a different elaboration phase of the same declaration) produces incorrectly instantiated terms: in `Mathlib.Condensed.Discrete.Module`, a cached `(sheafToPresheaf _ _).IsRightAdjoint` result was reused with universe instantiations from the wrong context, yielding kernel-rejected declarations.

The cache is now split into two tiers: the persistent environment extension only receives entries with a metavariable-free key and a closed result, which are context-free (free universe parameters and fvar references are pinned by the key). All other entries go to a reintroduced transient `Meta.Cache.synthInstance` tier with the previous per-`Meta.State` lifetime and semantics, the scope for which such sharing was originally designed.

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

Author: Kha

src/Lean/Meta/Basic.lean

@@ -410,14 +410,18 @@ We should also investigate the impact on memory consumption.
 abbrev DefEqCache := PersistentHashMap DefEqCacheKey Bool
 
 /--
-Cache datastructures for type inference, whnf, and definitional equality.
+Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
 
-The type class resolution cache is not part of this structure; it is stored in an environment
-extension so that it persists across commands (see `synthInstanceCacheExt`).
+The `synthInstance` field is only the *transient* tier of the type class resolution cache: it
+holds context-sensitive entries (keys containing metavariables, or results with abstracted
+metavariables), whose validity is tied to the current elaboration context. Context-free entries
+are stored in an environment extension instead so that they persist across commands (see
+`synthInstanceCacheExt`).
 -/
 structure Cache where
   inferType      : InferTypeCache := {}
   funInfo        : FunInfoCache := {}
+  synthInstance  : SynthInstanceCache := {}
   whnf           : WhnfCache := {}
   defEqTrans     : DefEqCache := {} -- transient cache for terms containing mvars or using nonstandard configuration options, it is frequently reset.
   defEqPerm      : DefEqCache := {} -- permanent cache for terms not containing mvars and using standard configuration options
@@ -681,13 +685,13 @@ def resetCache : MetaM Unit :=
   modifyCache fun _ => {}
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨ic, c1, c2, c3, c4⟩ => ⟨f ic, c1, c2, c3, c4⟩
+  modifyCache fun ⟨ic, c1, c2, c3, c4, c5⟩ => ⟨f ic, c1, c2, c3, c4, c5⟩
 
 @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, defeqTrans, c4⟩ => ⟨c1, c2, c3, f defeqTrans, c4⟩
+  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5⟩
 
 @[inline] def modifyDefEqPermCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, defeqPerm⟩ => ⟨c1, c2, c3, c4, f defeqPerm⟩
+  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm⟩
 
 def mkExprConfigCacheKey (expr : Expr) : MetaM ExprConfigCacheKey :=
   return { expr, configKey := (← read).configKey }

src/Lean/Meta/Instances.lean

@@ -115,9 +115,13 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
   }
 
 /--
-Cache for `synthInstance` results; see `Lean.Meta.SynthInstance`. It is stored in an environment
-extension so that it persists across commands; it is not stored in `.olean` files. It is
-registered in this module so that `addInstance` can invalidate it.
+Persistent tier of the `synthInstance` result cache; see `Lean.Meta.SynthInstance`. It is stored
+in an environment extension so that it persists across commands; it is not stored in `.olean`
+files. It is registered in this module so that `addInstance` can invalidate it.
+
+Only *context-free* entries are stored here: keys without metavariables and closed results.
+Context-sensitive entries (whose validity depends on the ambient metavariable context) live in
+the transient `Meta.Cache.synthInstance` tier instead.
 
 The cache map is stored behind an `IO.Ref` (`none` only as an unreachable `Inhabited` fallback):
 cache *fills* mutate the ref and thus survive elaborator backtracking, like the `Meta.Cache`
@@ -127,8 +131,8 @@ environment is rolled back, e.g. when a speculatively added instance is discarde
 the cache entries that were computed with it.
 
 Note that environment values derived from the same environment share the ref and thus the cache;
-in contexts that should not share the cache with their surroundings (e.g. async elaboration
-branches or incremental reuse across edits), it may need to be replaced explicitly in the future.
+this is sound for context-free entries, but e.g. incremental reuse across edits may require
+replacing the ref explicitly in the future.
 -/
 builtin_initialize synthInstanceCacheExt : EnvExtension (Option (IO.Ref SynthInstanceCache)) ←
   registerEnvExtension (some <$> IO.mkRef {}) (asyncMode := .local)  -- mere cache, keep local

src/Lean/Meta/SynthInstance.lean

@@ -879,20 +879,38 @@ private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVa
   check result
   return some result
 
-/-- Returns the type class resolution cache entry for `key`; see `synthInstanceCacheExt`. -/
+/--
+Returns the type class resolution cache entry for `key` from the transient
+(`Meta.Cache.synthInstance`) or persistent (`synthInstanceCacheExt`) tier.
+-/
 private def findCachedResult? (key : SynthInstanceCacheKey) :
     MetaM (Option (Option AbstractMVarsResult)) := do
+  if let some result? := (← get).cache.synthInstance.find? key then
+    return some result?
   let some ref := synthInstanceCacheExt.getState (← getEnv) | return none
   return (← ref.get).find? key
 
 /--
-Inserts a result into the type class resolution cache. The insertion mutates the cache ref
-instead of the environment, so it survives environment rollbacks; see `synthInstanceCacheExt`.
+Inserts a result into the type class resolution cache: into the persistent tier if `persist` is
+true, and otherwise into the transient `Meta.Cache.synthInstance` tier, which has the lifetime of
+the current `Meta.State`.
+
+Only context-free entries may be persisted: the key must not contain metavariables and the result
+must be closed. Results with abstracted metavariables are only valid relative to the elaboration
+context that created them: their degrees of freedom (e.g. universe metavariables not determined
+by the key, cf. `Small`) are resolved by ambient constraints, so reusing them in a different
+context can produce incorrectly instantiated terms.
+
+Persistent insertions mutate the cache ref instead of the environment, so they survive
+environment rollbacks; see `synthInstanceCacheExt`.
 -/
-private def insertCachedResult (key : SynthInstanceCacheKey) (result? : Option AbstractMVarsResult) :
-    MetaM Unit := do
-  let some ref := synthInstanceCacheExt.getState (← getEnv) | return ()
-  ref.modify (·.insert key result?)
+private def insertCachedResult (key : SynthInstanceCacheKey) (result? : Option AbstractMVarsResult)
+    (persist : Bool) : MetaM Unit := do
+  if persist then
+    let some ref := synthInstanceCacheExt.getState (← getEnv) | return ()
+    ref.modify (·.insert key result?)
+  else
+    modifyCache fun c => { c with synthInstance := c.synthInstance.insert key result? }
 
 /--
 Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthInstance.main` into an `Expr`.
@@ -914,19 +932,21 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr
 
 /-- 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.
-  match abstResult? with
-  | none => insertCachedResult cacheKey none
-  | some abstResult =>
-    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then
-      match result? with
-      | none => insertCachedResult cacheKey none
-      | some result =>
-        -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
-        -- we don't need to perform extra checks again when reusing result.
-        insertCachedResult cacheKey (some { expr := result, paramNames := #[], mvars := #[] })
-    else
-      insertCachedResult cacheKey (some abstResult)
+  -- The stored value: for a closed result we store the concrete `result` expr with an empty
+  -- `AbstractMVarsResult` so that `applyCachedAbstractResult?` can skip re-`check`ing it.
+  let value? :=
+    match abstResult? with
+    | none => none
+    | some abstResult =>
+      if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then
+        result?.map fun result => { expr := result, paramNames := #[], mvars := #[] }
+      else
+        some abstResult
+  -- Only context-free entries may be persisted: mvar-free key (`.noMVars`) and a closed value
+  -- (no abstracted metavariables); see `insertCachedResult`.
+  let persist := kind matches .noMVars &&
+    (value?.all fun r => r.numMVars == 0 && r.paramNames.isEmpty)
+  insertCachedResult cacheKey value? (persist := persist)
 
 def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
   let opts ← getOptions