From 8607fedfed97e6255c95c97f2330d33128f3533f Mon Sep 17 00:00:00 2001 From: grandchildrice Date: Sun, 19 Jul 2026 18:54:26 +0900 Subject: [PATCH] perf: avoid quadratic re-attempts of pending TC mvars in synthesizeSyntheticMVars The resumption loop re-attempts every pending `.typeClass` synthetic metavariable whenever any single one makes progress. In statements whose literals/operators create a chain of interdependent default-instance mvars (each assignment unlocks the next), k pending instances cost k+(k-1)+... = O(k^2) synthInstance attempts, each an expensive underdetermined (mvar-headed) search. Microbench (200 theorems `7 + ... + 7 = 7 + ... + 7`, k per side, term-mode rfl), per-command elaboration cost on master (25ba8c3): 1.64 / 3.22 / 8.43 / 27.6 / 101.4 ms for k = 1/2/4/8/16 (x3.3-3.7 per doubling => quadratic). Controls: the same expressions in defs (known expected type) and theorems over variables are both linear. Fix: memoize per pending mvar the instantiated goal type at its last failed attempt (one MVarIdMap Expr in Term.State); skip the re-attempt when the instantiated goal is unchanged. synthInstance is deterministic in the instantiated goal for a fixed env/local-instance context, so the skip elides only attempts whose outcome is already known. With the fix the k=16 case drops ~4.7x and oleans are byte-identical. Gated behind `Elab.tcSkipUnchanged` (default false) for evaluation. --- src/Lean/Elab/SyntheticMVars.lean | 11 +++++++++++ src/Lean/Elab/Term/TermElabM.lean | 5 +++++ 2 files changed, 16 insertions(+) diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 7b7f039bfa57..56a1d9b4150e 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -76,8 +76,19 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId /-- Similar to `synthesizeInstMVarCore`, but makes sure that `instMVar` local context and instances are used. It also logs any error message produced. -/ +register_builtin_option Elab.tcSkipUnchanged : Bool := { + defValue := false + descr := "skip re-attempting a pending typeclass metavariable whose instantiated goal type is unchanged since its last failed attempt (the outcome is deterministic in the goal, so re-attempting is wasted work; the resumption loop is otherwise quadratic in the number of chained pending instances)" +} + private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Option MessageData := none): TermElabM Bool := instMVar.withContext do + if Elab.tcSkipUnchanged.get (← getOptions) then + let type ← instantiateMVars (← instMVar.getType) + if let some prev := (← get).tcSynthAttempt.get? instMVar then + if prev == type then + return false + modify fun s => { s with tcSynthAttempt := s.tcSynthAttempt.insert instMVar type } try synthesizeInstMVarCore instMVar (extraErrorMsg? := extraErrorMsg?) catch diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index 4d848e0860a2..dc0c25bfcb4e 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -181,6 +181,11 @@ structure State where levelNames : List Name := [] syntheticMVars : MVarIdMap SyntheticMVarDecl := {} pendingMVars : List MVarId := {} + /-- Last instantiated goal type per still-pending `.typeClass` mvar whose synthesis + attempt failed; used (option `Elab.tcSkipUnchanged`) to skip re-attempts when the + goal is unchanged — the resumption loop otherwise re-tries every pending TC mvar + after each single success, which is quadratic in chained-literal statements. -/ + tcSynthAttempt : MVarIdMap Expr := {} /-- List of errors associated to a metavariable that are shown to the user if the metavariable could not be fully instantiated -/ mvarErrorInfos : List MVarErrorInfo := [] /-- List of data to be able to localize universe level metavariable errors to particular expressions. -/