perf: normalize free variables in the type class resolution cache key

.github/workflows/build-template.yml

@@ -270,7 +270,9 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: matrix.test
+        # `skip-tests`: label for experimental PRs with known-failing tests, so CI still produces
+        # the `pr-release` toolchain (e.g. for Mathlib benchmarking)
+        if: matrix.test && !contains(github.event.pull_request.labels.*.name, 'skip-tests')
       # copy failed tests' output into the `<failure>` elements shown by the test summary
       - name: Embed Test Output
         run: |

src/Lean/Elab/Command.lean

@@ -1054,11 +1054,13 @@ such as `open` and `namespace` commands,
 only have an effect for the remainder of the `CommandElabM` computation passed here,
 and do not affect subsequent commands.
 
-*Warning:* when using this from `MetaM` monads, the caches are *not* reset.
-If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache`
-to reset the instance cache.
+*Warning:* when using this from `MetaM` monads, the `Meta.Cache` caches are *not* reset.
 While the `modifyEnv` function for `MetaM` clears its caches entirely,
 `liftCommandElabM` has no way to reset these caches.
+In particular, if the command may affect typeclass resolution (e.g. by adding instances or
+changing reducibility attributes), you should call `Lean.Meta.resetSynthInstanceCache`
+afterwards: the cache resets performed inside the command cannot clear the calling `MetaM`'s
+transient tier, which also holds context-free entries such as cached failures.
 -/
 def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : CoreM α := do
   -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.

src/Lean/Meta/Basic.lean

@@ -355,10 +355,58 @@ structure SynthInstanceCacheKey where
   localInsts        : LocalInstances
   type              : Expr
   /--
+  For a normalized (`.noMVars`, fvar-typed) query, the canonical types of the free variables
+  referenced by `type`/`localInsts`, indexed by their canonical position (see the fvar
+  normalization in `SynthInstance.lean`). Free variables in `type` and `localInsts` are renamed
+  to positional canonical identifiers, so structurally identical queries in different local
+  contexts share a cache entry. Empty for non-normalized (raw) keys.
+  -/
+  normFVarTypes     : Array Expr := #[]
+  /--
+  For each closure position, the canonical value of that free variable if it is let-bound, and
+  `none` otherwise. A let-bound variable's value is visible to definitional unfolding, so contexts
+  that agree on the types but not the values are not interchangeable. Empty for raw keys.
+  -/
+  normFVarValues    : Array (Option Expr) := #[]
+  /--
   Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
   See issue #2522.
   -/
   synthPendingDepth : Nat
+  /--
+  Namespaces with scoped instances that are currently activated (e.g. via `open`), in canonical
+  order. Keying the cache by this set keeps entries from outside a scope valid after the scope
+  ends, e.g. for the `open Classical in` expansion of `by_cases`.
+  -/
+  activeScopedInsts : Array Name
+  /--
+  Instances currently added with the `local` attribute kind (`Instances.localInstanceNames`).
+  Like `activeScopedInsts`, keying the cache by this set keeps entries from outside a scope
+  containing `attribute [local instance]` valid after the scope ends, and prevents entries
+  computed with the local instance from leaking out of the scope.
+  -/
+  localAttrInsts    : Array Name
+  /--
+  Effective maximum result size (`synthInstance.maxSize` unless overridden by the caller).
+  The cache persists across commands, so results (in particular failures) obtained under a
+  different size limit must not be reused.
+  -/
+  maxResultSize     : Nat
+  /-- Value of `backward.synthInstance.canonInstances`. -/
+  canonInstances    : Bool
+  /--
+  Values of `backward.isDefEq.respectTransparency` and `backward.isDefEq.respectTransparency.types`.
+  They control whether `isDefEq` bumps the transparency when assigning a metavariable, and hence
+  which of several definitionally equal terms an instance's implicit arguments are assigned. The
+  cache persists across commands, which may set them differently.
+  -/
+  respectTransparency      : Bool
+  respectTransparencyTypes : Bool
+  /--
+  Value of `Environment.isExporting`: in the exporting state, fewer definitions can be unfolded,
+  which can change the result of typeclass resolution.
+  -/
+  isExporting       : Bool
   deriving Hashable, BEq
 
 /-- Resulting type for `abstractMVars` -/
@@ -409,8 +457,46 @@ We should also investigate the impact on memory consumption.
 -/
 abbrev DefEqCache := PersistentHashMap DefEqCacheKey Bool
 
+/--
+The free-variable normalization of a local instance context: the canonical position of every free
+variable reachable from the local instances (transitively via their types), that variable's
+recursively normalized type, and the local instances themselves over the canonical variables. See
+the normalization in `SynthInstance.lean`.
+-/
+structure SynthNormClosure where
+  fmap            : PersistentHashMap FVarId Nat
+  order           : Array FVarId
+  types           : Array Expr
+  /-- The canonical value of each let-bound closure variable; `none` for the others. -/
+  values          : Array (Option Expr)
+  canonLocalInsts : LocalInstances
+
+/--
+`SynthNormClosure` memoized for the local instances it was computed from. The closure does not
+depend on the query, so every type class query made under the same local instances shares it;
+recomputing it per query dominates the cost of building a cache key.
+-/
+structure SynthNormClosureMemo where
+  /-- The local instances the closure was computed for. -/
+  localInsts : LocalInstances
+  /--
+  The closure variables whose raw `LocalDecl` type or let-value mentions a metavariable, with the
+  instantiation the closure was built from (`true` = the value, `false` = the type). A `LocalDecl`
+  is immutable, so only these can change: a metavariable may be assigned, or an assignment reverted
+  by backtracking.
+  -/
+  mvarTyped : Array (FVarId × Bool × Expr)
+  /-- `none` if the local instance context cannot be soundly normalized. -/
+  closure? : Option SynthNormClosure
+
 /--
 Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
+
+The `synthInstance` field is the *transient* tier of the type class resolution cache: it has
+the lifetime of the current `Meta.State` and holds all entries, including context-sensitive ones
+(keys containing metavariables, or results with abstracted metavariables) whose validity is tied
+to the current elaboration context. Context-free entries are additionally stored in an
+environment extension so that they persist across commands (see `synthInstanceCacheExt`).
 -/
 structure Cache where
   inferType      : InferTypeCache := {}
@@ -419,6 +505,12 @@ structure Cache where
   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
+  /--
+  One-slot memo for the free-variable normalization of the local instance context; see
+  `SynthNormClosureMemo`. One slot suffices because the local instances change rarely relative to
+  the number of type class queries made under them.
+  -/
+  synthNormClosure : Option SynthNormClosureMemo := none
   deriving Inhabited
 
 /--
@@ -683,13 +775,13 @@ def resetCache : MetaM Unit :=
   modifyCache fun _ => {}
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨ic, c1, c2, c3, c4, c5⟩ => ⟨f ic, c1, c2, c3, c4, c5⟩
+  modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
 
 @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5⟩
+  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5, c6⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5, c6⟩
 
 @[inline] def modifyDefEqPermCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm⟩
+  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm, c6⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm, c6⟩
 
 def mkExprConfigCacheKey (expr : Expr) : MetaM ExprConfigCacheKey :=
   return { expr, configKey := (← read).configKey }
@@ -707,9 +799,6 @@ def mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey :=
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
 
-@[inline] def resetSynthInstanceCache : MetaM Unit :=
-  modifyCache fun c => {c with synthInstance := {}}
-
 @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }

src/Lean/Meta/Instances.lean

@@ -77,15 +77,28 @@ structure Instances where
   discrTree     : InstanceTree := DiscrTree.empty
   instanceNames : PHashMap Name InstanceEntry := {}
   erased        : PHashSet Name := {}
+  /--
+  Names of instances added with the `local` attribute kind into this state, in insertion order.
+  Local instances are delimited by their surrounding scope, which restores the previous
+  `Instances` state (and thereby the previous value of this field) when it is closed. The field
+  is part of the type class resolution cache key (`SynthInstanceCacheKey.localAttrInsts`), so
+  cache entries never leak into or out of scopes with local instances.
+  -/
+  localInstanceNames : Array Name := #[]
   deriving Inhabited
 
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
+  let d := if e.attrKind matches .local then
+    { d with localInstanceNames := d.localInstanceNames.push (e.globalName?.getD .anonymous) }
+  else
+    d
   match e.globalName? with
   | some n => { d with discrTree := d.discrTree.insertKeyValue e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
   | none   => { d with discrTree := d.discrTree.insertKeyValue e.keys e }
 
 def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
-  { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName }
+  { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName,
+           localInstanceNames := d.localInstanceNames.filter (· != declName) }
 
 def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do
   unless d.instanceNames.contains declName do
@@ -101,6 +114,50 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
       else ⟨none, none, some e⟩
   }
 
+/--
+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.
+
+Both fills and invalidation are plain (branch-local) environment modifications: an entry is
+only ever observable in environments derived from the one it was filled in, so rolling back the
+environment (e.g. discarding a speculatively added instance) also rolls back the entries that
+were computed with it, and parallel elaboration branches never observe each other's fills.
+Entries persisted within a rolled-back region are lost with it; within a single command the
+transient tier compensates, as `Meta.Cache` is deliberately not restored by
+`Meta.SavedState.restore` (see `Lean.Meta.SynthInstance.insertCachedResult`).
+-/
+builtin_initialize synthInstanceCacheExt : EnvExtension SynthInstanceCache ←
+  registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep local
+
+/--
+Resets the persistent tier of the type class resolution cache. Use `resetSynthInstanceCache`
+instead from `MetaM`, which also clears the transient `Meta.Cache.synthInstance` tier;
+context-free entries are written to both tiers (see `Lean.Meta.SynthInstance.insertCachedResult`).
+-/
+def resetSynthInstanceCacheCore : CoreM Unit :=
+  modify fun s => { s with env := synthInstanceCacheExt.setState s.env {} }
+
+/--
+Resets the type class resolution cache (both the persistent tier and the transient
+`Meta.Cache.synthInstance` tier).
+
+The cache is reset automatically when an instance is added via `addInstance` or erased, and
+activation of scoped instances is accounted for in the cache key
+(`SynthInstanceCacheKey.activeScopedInsts`). Other changes that may affect typeclass resolution
+require calling this function explicitly, e.g. closing a section containing local instances,
+changing the reducibility status of a pre-existing declaration, or adding instances through an
+environment modification the current `Meta.State` cannot observe, such as running a command via
+`liftCommandElabM` (which threads the environment back but cannot clear `Meta.Cache`).
+-/
+def resetSynthInstanceCache : MetaM Unit := do
+  resetSynthInstanceCacheCore
+  modifyCache fun c => { c with synthInstance := {} }
+
 private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
   let type ← inferType e
   withNewMCtxDepth do
@@ -302,6 +359,7 @@ this warning can be disabled with `set_option warn.classDefReducibility false`."
   let projInfo? ← getProjectionFnInfo? declName
   let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
+  resetSynthInstanceCache
 
 /-
 Adds instance **and** marks it with reducibility status `@[instance_reducible]`. We use this function
@@ -351,6 +409,7 @@ builtin_initialize
       let s := instanceExtension.getState (← getEnv)
       let s ← s.erase declName
       modifyEnv fun env => instanceExtension.modifyState env fun _ => s
+      resetSynthInstanceCacheCore
   }
 
 def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=