perf: skip redundant typeclass synthesis retries in synthesizeSyntheticMVarsStep

This PR adds dependency tracking to `synthesizeSyntheticMVarsStep` to avoid
redundant typeclass synthesis retries. When synthesis returns `.undef` (stuck),
the instantiated type is cached in `MetavarContext.synthInstDeps`. Before
retrying, the type is re-instantiated and compared; if unchanged, the retry is
skipped since it would produce the same result. The cache is cleared after
`synthesizeUsingDefault` applies default instances.

This reduces the NestedLetAdditions benchmark (N=256) from ~12.5s to ~6.3s by
turning O(N²) total synthesis attempts into O(N) for dependency chains of the
form `let x₁ := 1; let x₂ := x₁ + x₁; ...`.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Elab/SyntheticMVars.lean

@@ -569,7 +569,9 @@ mutual
           return false
   /--
     Try to synthesize the current list of pending synthetic metavariables.
-    Return `true` if at least one of them was synthesized. -/
+    Return `true` if at least one of them was synthesized.
+    Uses `MetavarContext.synthInstCache` to cache the instantiated type of stuck TC mvars,
+    skipping retries when the type hasn't changed. -/
   private partial def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do
     let ctx ← read
     traceAtCmdPos `Elab.resume fun _ =>
@@ -584,8 +586,24 @@ mutual
     let remainingPendingMVars ← pendingMVars.filterRevM fun mvarId => do
        -- We use `traceM` because we want to make sure the metavar local context is used to trace the message
        traceM `Elab.postpone (mvarId.withContext do addMessageContext m!"resuming {mkMVar mvarId}")
+       -- Skip TC mvars whose instantiated type is unchanged since last failed synthesis
+       if let some lastType := (← getMCtx).synthInstCache.find? mvarId then
+         unless (← mvarId.isAssignedOrDelayedAssigned) do
+           let type ← instantiateMVars (← mvarId.getDecl).type
+           if type == lastType then
+             trace[Elab.postpone] "skipping: TC type unchanged"
+             return true  -- keep pending, don't retry
+         modifyMCtx fun mctx => { mctx with synthInstCache := mctx.synthInstCache.erase mvarId }
        let succeeded ← synthesizeSyntheticMVar mvarId postponeOnError runTactics
        if succeeded then markAsResolved mvarId
+       else
+         -- Record instantiated type for stuck TC mvars to skip redundant retries
+         if let some decl ← getSyntheticMVarDecl? mvarId then
+           match decl.kind with
+           | .typeClass _ =>
+             let type ← instantiateMVars (← mvarId.getDecl).type
+             modifyMCtx fun mctx => { mctx with synthInstCache := mctx.synthInstCache.insert mvarId type }
+           | _ => pure ()
        trace[Elab.postpone] if succeeded then format "succeeded" else format "not ready yet"
        pure !succeeded
     -- Merge new synthetic metavariables with `remainingPendingMVars`, i.e., metavariables that still couldn't be synthesized
@@ -633,6 +651,9 @@ mutual
             if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := true) (runTactics := false) then
               loop ()
             else if ← synthesizeUsingDefault then
+              -- Clear stale dependency info after default instance application, since
+              -- defaults may assign mvars that indirectly affect TC synthesis.
+              modifyMCtx fun mctx => { mctx with synthInstCache := {} }
               loop ()
             else if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then
               loop ()

src/Lean/MetavarContext.lean

@@ -354,6 +354,10 @@ structure MetavarContext where
   /-- Assignment table for delayed abstraction metavariables.
   For more information about delayed abstraction, see the docstring for `DelayedMetavarAssignment`. -/
   dAssignment    : PersistentHashMap MVarId DelayedMetavarAssignment := {}
+  /-- Tracks the instantiated type of pending TC mvars whose synthesis last returned `.undef`.
+  If the type hasn't changed since the last attempt, the mvar is skipped to avoid redundant retries
+  in `synthesizeSyntheticMVarsStep`. -/
+  synthInstCache  : PersistentHashMap MVarId Expr := {}
 
 instance : Inhabited MetavarContext := ⟨{}⟩
 

tests/elab/info_trees.lean

@@ -62,7 +62,7 @@ info: • [Command] @ ⟨79, 0⟩-⟨79, 40⟩ @ Lean.Elab.Command.elabDeclarati
                   ⊢ 0 ≤ n
                   after no goals
                   • [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
-                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.47.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.38.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
                       • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†

tests/server_interactive/completionPrefixIssue.lean.out.expected

@@ -3,7 +3,7 @@
 {"items":
  [{"label": "veryLongDefinitionName",
    "kind": 6,
-   "data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.51"]},
+   "data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.42"]},
   {"label": "veryLongDefinitionNameVeryLongDefinitionName",
    "kind": 21,
    "data":
@@ -17,7 +17,7 @@ Resolution of veryLongDefinitionName:
 {"label": "veryLongDefinitionName",
  "kind": 6,
  "detail": "Nat",
- "data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.51"]}
+ "data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.42"]}
 Resolution of veryLongDefinitionNameVeryLongDefinitionName:
 {"label": "veryLongDefinitionNameVeryLongDefinitionName",
  "kind": 21,