Skip to content

Commit 808f99f

Browse files
Khaclaude
Kha
and
claude
committed
perf: normalize free variables in metavariable-laden cache keys
This PR lets an instance query whose class has output parameters share a cache entry with structurally identical queries in other local contexts, and persist across commands, as queries without metavariables already do. The free-variable normalization ran only on `.noMVars` queries, so every other key kept the free variables of the context that created it and could never be shared. Run it on all queries: metavariable identities are left exactly as they are, so only the free variables are canonicalized. The wildcard that `preprocess` puts in output-parameter positions is left alone, being a marker rather than a variable of the local context. The gate on persistence tested `.noMVars`, which is a proxy for what it actually requires: a key without metavariables. Test that directly. An `.mvarsOutputParams` key has its output parameters replaced by a wildcard, so it is metavariable-free whenever every metavariable sits in an output parameter, and is then as context-free as a `.noMVars` key: the wildcard stands for a value the input parameters determine, and a hit re-derives it by unifying the cached result against the query. On `Mathlib.Algebra.Group.Basic` the misses drop from 1230 to 944 and the heartbeats spent inside missed searches by 45%. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent e934e9b commit 808f99f

3 files changed

Lines changed: 21 additions & 176 deletions

File tree

‎src/Lean/Meta/SynthInstance.lean‎

Lines changed: 18 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -984,15 +984,22 @@ private def cacheResult (cacheKey : SynthInstanceCacheKey) (kind : PreprocessKin
984984
result?.map fun result => { expr := result, paramNames := #[], mvars := #[] }
985985
else
986986
some abstResult
987-
-- Only context-free entries may be persisted: a mvar-free key (`.noMVars`), a key that does not
987+
-- Only context-free entries may be persisted: a key without metavariables, a key that does not
988988
-- depend on the identity of any free variable, and a closed value (no abstracted metavariables,
989989
-- no free variables); see `insertCachedResult`.
990990
--
991+
-- The key is tested for metavariables directly rather than through `.noMVars`. An
992+
-- `.mvarsOutputParams` query has its output parameters replaced by a wildcard in the key, so the
993+
-- key is metavariable-free whenever every metavariable sits in an output parameter, even though
994+
-- the query itself is not. Such an entry is as context-free as a `.noMVars` one: the wildcard
995+
-- stands for a value the input parameters determine, and a hit re-derives it by unifying the
996+
-- cached result against the query (`assignOutParams`).
997+
--
991998
-- A `normalized` key names its free variables by canonical position and records their types in
992999
-- `normFVarTypes`, so it is context-free even though it mentions free variables. A raw key is
9931000
-- context-free only if it mentions none: an `FVarId` identifies a variable only within the
9941001
-- `NameGenerator` that created it, and the cache outlives any of them.
995-
let persist := kind matches .noMVars &&
1002+
let persist := !cacheKey.type.hasMVar &&
9961003
(normalized || (cacheKey.localInsts.isEmpty && !cacheKey.type.hasFVar)) &&
9971004
(value?.all fun r => r.numMVars == 0 && r.paramNames.isEmpty && !r.expr.hasFVar)
9981005
insertCachedResult cacheKey value? (persist := persist)
@@ -1053,6 +1060,9 @@ private partial def normExpr (e : Expr) : M Expr := do
10531060
| .fvar id =>
10541061
if let some i := (← get).fmap.find? id then
10551062
return .fvar (canonFVarId i)
1063+
-- `preprocess` puts this marker in output-parameter positions; it is a constant, not a
1064+
-- variable of the local context, and must not be renamed (nor bail the normalization).
1065+
if id.name == `__wild__ then return e
10561066
match (← read).find? id with
10571067
| none =>
10581068
modify fun s => { s with bail := true }
@@ -1214,9 +1224,12 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
12141224
let localInsts ← getLocalInstances
12151225
let type ← instantiateMVars type
12161226
let { type, cacheKeyType, kind } ← preprocess type
1217-
-- For `.noMVars` queries, normalize the free variables of the key and result so that
1218-
-- structurally identical queries in different local contexts share a cache entry.
1219-
let normCtx? ← if kind matches .noMVars then SynthNorm.normalizeContext? cacheKeyType localInsts else pure none
1227+
-- Normalize the free variables of the key and result so that structurally identical queries in
1228+
-- different local contexts share a cache entry. Metavariables are left exactly as they are, so
1229+
-- this applies to metavariable-laden queries as well: their keys are otherwise context-specific
1230+
-- and can never be shared. `.mvarsOutputParams` keys have their output parameters replaced by a
1231+
-- wildcard already, so they are usually metavariable-free apart from it.
1232+
let normCtx? ← SynthNorm.normalizeContext? cacheKeyType localInsts
12201233
let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth,
12211234
activeScopedInsts := instanceExtension.getActiveScopesWithEntries (← getEnv),
12221235
localAttrInsts := instanceExtension.getState (← getEnv) |>.localInstanceNames,

‎tests/elab/synth1.lean.out.expected‎

Lines changed: 2 additions & 164 deletions
Original file line numberDiff line numberDiff line change
@@ -101,88 +101,7 @@
101101
[Meta.synthInstance] result coerceTrans
102102
[Meta.synthInstance] coerceTrans Nat Bool Prop coerceBoolToProp coerceNatToBool
103103
[Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
104-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM Elab.Command.CommandElabM
105-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
106-
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
107-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
108-
[Meta.synthInstance] ✅️ new goal MonadEval _tc.1 Elab.Command.CommandElabM
109-
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
110-
[Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
111-
Elab.Command.CommandElabM
112-
[Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
113-
[Meta.synthInstance.resume] ✅️ propagating MonadEval Elab.TermElabM
114-
Elab.Command.CommandElabM to subgoal MonadEval Elab.TermElabM
115-
Elab.Command.CommandElabM of MonadEvalT MetaM Elab.Command.CommandElabM
116-
[Meta.synthInstance.resume] size: 1
117-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM Elab.TermElabM
118-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
119-
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
120-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
121-
[Meta.synthInstance] ✅️ new goal MonadEval _tc.1 Elab.TermElabM
122-
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
123-
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
124-
[Meta.synthInstance] ✅️ new goal MonadLift _tc.1 Elab.TermElabM
125-
[Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
126-
[Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
127-
(StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
128-
[Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
129-
[Meta.synthInstance.resume] ✅️ propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
130-
(ReaderT Elab.Term.Context
131-
(StateRefT' IO.RealWorld Elab.Term.State
132-
MetaM)) to subgoal MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
133-
Elab.TermElabM of MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
134-
[Meta.synthInstance.resume] size: 1
135-
[Meta.synthInstance.answer] ✅️ MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
136-
[Meta.synthInstance.resume] ✅️ propagating MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM)
137-
Elab.TermElabM to subgoal MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM)
138-
Elab.TermElabM of MonadEvalT MetaM Elab.TermElabM
139-
[Meta.synthInstance.resume] size: 2
140-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
141-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
142-
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
143-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
144-
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
145-
[Meta.synthInstance] ✅️ new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
146-
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
147-
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
148-
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
149-
[Meta.synthInstance] ✅️ new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
150-
[Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
151-
[Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
152-
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
153-
[Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
154-
[Meta.synthInstance.resume] ✅️ propagating MonadLift MetaM
155-
(StateRefT' IO.RealWorld Elab.Term.State
156-
MetaM) to subgoal MonadLift MetaM
157-
(StateRefT' IO.RealWorld Elab.Term.State
158-
MetaM) of MonadEval MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
159-
[Meta.synthInstance.resume] size: 1
160-
[Meta.synthInstance.answer] ✅️ MonadEval MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
161-
[Meta.synthInstance.resume] ✅️ propagating MonadEval MetaM
162-
(StateRefT' IO.RealWorld Elab.Term.State
163-
MetaM) to subgoal MonadEval MetaM
164-
(StateRefT' IO.RealWorld Elab.Term.State
165-
MetaM) of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
166-
[Meta.synthInstance.resume] size: 2
167-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM MetaM
168-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
169-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
170-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
171-
[Meta.synthInstance.resume] ✅️ propagating MonadEvalT MetaM
172-
MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
173-
[Meta.synthInstance.resume] size: 3
174-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
175-
[Meta.synthInstance.resume] ✅️ propagating MonadEvalT MetaM
176-
(StateRefT' IO.RealWorld Elab.Term.State
177-
MetaM) to subgoal MonadEvalT MetaM
178-
(StateRefT' IO.RealWorld Elab.Term.State MetaM) of MonadEvalT MetaM Elab.TermElabM
179-
[Meta.synthInstance.resume] size: 6
180-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM Elab.TermElabM
181-
[Meta.synthInstance.resume] ✅️ propagating MonadEvalT MetaM
182-
Elab.TermElabM to subgoal MonadEvalT MetaM Elab.TermElabM of MonadEvalT MetaM Elab.Command.CommandElabM
183-
[Meta.synthInstance.resume] size: 8
184-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
185-
[Meta.synthInstance] result instMonadEvalTOfMonadEval MetaM Elab.TermElabM Elab.Command.CommandElabM
104+
[Meta.synthInstance] result instMonadEvalTOfMonadEval MetaM Elab.TermElabM Elab.Command.CommandElabM (cached)
186105
[Meta.synthInstance] ✅️ Bind IO
187106
[Meta.synthInstance] ✅️ new goal Bind IO
188107
[Meta.synthInstance.instances] #[@Monad.toBind]
@@ -197,88 +116,7 @@
197116
[Meta.synthInstance] result instMonadEIO.toBind
198117
[Meta.synthInstance] Monad.toBind.{0, 0} IO (instMonadEIO IO.Error)
199118
[Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
200-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM Elab.Command.CommandElabM
201-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
202-
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
203-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
204-
[Meta.synthInstance] ✅️ new goal MonadEval _tc.1 Elab.Command.CommandElabM
205-
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
206-
[Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
207-
Elab.Command.CommandElabM
208-
[Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
209-
[Meta.synthInstance.resume] ✅️ propagating MonadEval Elab.TermElabM
210-
Elab.Command.CommandElabM to subgoal MonadEval Elab.TermElabM
211-
Elab.Command.CommandElabM of MonadEvalT MetaM Elab.Command.CommandElabM
212-
[Meta.synthInstance.resume] size: 1
213-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM Elab.TermElabM
214-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
215-
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
216-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
217-
[Meta.synthInstance] ✅️ new goal MonadEval _tc.1 Elab.TermElabM
218-
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
219-
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
220-
[Meta.synthInstance] ✅️ new goal MonadLift _tc.1 Elab.TermElabM
221-
[Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
222-
[Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
223-
(StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
224-
[Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
225-
[Meta.synthInstance.resume] ✅️ propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
226-
(ReaderT Elab.Term.Context
227-
(StateRefT' IO.RealWorld Elab.Term.State
228-
MetaM)) to subgoal MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
229-
Elab.TermElabM of MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
230-
[Meta.synthInstance.resume] size: 1
231-
[Meta.synthInstance.answer] ✅️ MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
232-
[Meta.synthInstance.resume] ✅️ propagating MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM)
233-
Elab.TermElabM to subgoal MonadEval (StateRefT' IO.RealWorld Elab.Term.State MetaM)
234-
Elab.TermElabM of MonadEvalT MetaM Elab.TermElabM
235-
[Meta.synthInstance.resume] size: 2
236-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
237-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
238-
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
239-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
240-
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
241-
[Meta.synthInstance] ✅️ new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
242-
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
243-
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
244-
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
245-
[Meta.synthInstance] ✅️ new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
246-
[Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
247-
[Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
248-
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
249-
[Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
250-
[Meta.synthInstance.resume] ✅️ propagating MonadLift MetaM
251-
(StateRefT' IO.RealWorld Elab.Term.State
252-
MetaM) to subgoal MonadLift MetaM
253-
(StateRefT' IO.RealWorld Elab.Term.State
254-
MetaM) of MonadEval MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
255-
[Meta.synthInstance.resume] size: 1
256-
[Meta.synthInstance.answer] ✅️ MonadEval MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
257-
[Meta.synthInstance.resume] ✅️ propagating MonadEval MetaM
258-
(StateRefT' IO.RealWorld Elab.Term.State
259-
MetaM) to subgoal MonadEval MetaM
260-
(StateRefT' IO.RealWorld Elab.Term.State
261-
MetaM) of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
262-
[Meta.synthInstance.resume] size: 2
263-
[Meta.synthInstance] ✅️ new goal MonadEvalT MetaM MetaM
264-
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
265-
[Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
266-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
267-
[Meta.synthInstance.resume] ✅️ propagating MonadEvalT MetaM
268-
MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
269-
[Meta.synthInstance.resume] size: 3
270-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
271-
[Meta.synthInstance.resume] ✅️ propagating MonadEvalT MetaM
272-
(StateRefT' IO.RealWorld Elab.Term.State
273-
MetaM) to subgoal MonadEvalT MetaM
274-
(StateRefT' IO.RealWorld Elab.Term.State MetaM) of MonadEvalT MetaM Elab.TermElabM
275-
[Meta.synthInstance.resume] size: 6
276-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM Elab.TermElabM
277-
[Meta.synthInstance.resume] ✅️ propagating MonadEvalT MetaM
278-
Elab.TermElabM to subgoal MonadEvalT MetaM Elab.TermElabM of MonadEvalT MetaM Elab.Command.CommandElabM
279-
[Meta.synthInstance.resume] size: 8
280-
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
281-
[Meta.synthInstance] result instMonadEvalTOfMonadEval MetaM Elab.TermElabM Elab.Command.CommandElabM
119+
[Meta.synthInstance] result instMonadEvalTOfMonadEval MetaM Elab.TermElabM Elab.Command.CommandElabM (cached)
282120
[Meta.synthInstance] ✅️ BEq Nat
283121
[Meta.synthInstance] ✅️ new goal BEq Nat
284122
[Meta.synthInstance.instances] #[@instBEqOfDecidableEq, @Std.PreorderPackage.toBEq]

‎tests/elab/trace_synth.lean‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,7 @@ error: failed to synthesize instance of type class
2222
Foo "two"
2323
---
2424
trace: [Meta.synthInstance] ❌️ Foo "two"
25-
[Meta.synthInstance] ✅️ new goal Foo "two"
26-
[Meta.synthInstance.instances] #[@instFoo_1]
27-
[Meta.synthInstance.apply] ✅️ apply @instFoo_1 to Foo "two"
28-
[Meta.synthInstance.tryResolve] ✅️ Foo "two" ≟ Foo "two"
29-
[Meta.synthInstance] ✅️ no instances for Foo "three"
30-
[Meta.synthInstance.instances] #[]
31-
[Meta.synthInstance] result <not-available>
25+
[Meta.synthInstance] result <not-available> (cached)
3226
[Meta.synthInstance] ❌️ Foo "two"
3327
[Meta.synthInstance] result <not-available> (cached)
3428
-/

0 commit comments

Comments
 (0)