perf: synthetic-mvar resumption loop is quadratic in chained pending TC instances (100ms/command at 16 chained literals)

Description

Elab.synthesizeSyntheticMVars' 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²) synthInstance attempts, each an expensive underdetermined (mvar-headed) search. Numeral-dense statements (chained arithmetic, BitVec/Fin literals, polynomial coefficients) pay this on every command, on the elaboration critical path.

Reproduction

Generate 200 theorems 7 + 7 + … = 7 + 7 + … (k sevens per side, term-mode rfl, no imports):

python3 - <<'EOF'
for k in [1,2,4,8,16]:
    expr=" + ".join(["7"]*k)
    open(f'scale_{k}.lean','w').write("\n".join(
        f"theorem s{i} : {expr} = {expr} := rfl" for i in range(200))+"\n")
EOF
for k in 1 2 4 8 16; do time lean scale_$k.lean; done

Per-command elaboration cost on master (25ba8c3d, nightly-2026-07-19, 16-core linux, best of 5):

Controls that isolate the mechanism:

• the same expressions as def d{i} : Nat := 7 + … + 7 (expected type known, no postponement): linear (0.95 s total at k=16 vs 20.4 s for the theorem form);
• theorems over variables (n + n + …, no literals): linear (0.99 s).

The quadratic requires literals (pending OfNat/HAdd default-instance mvars) and an unknown expected type (the equality's implicit type argument) — i.e. the postpone-until-defaulting path.

Proposed fix

Memoize, per pending .typeClass 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 — pending mvars stay pending, and resolution happens exactly when the goal actually changes. O(k²) cheap instantiate-and-compare checks remain; O(k) expensive synth calls replace the former O(k²).

Evidence with the fix, measured on this branch rebased onto 25ba8c3d
(PR to follow; gated behind Elab.tcSkipUnchanged, default off, for evaluation):

• microbench per-command: k=4 7.38 → 3.41 ms, k=16 100.8 → 21.4 ms (4.7×) — quadratic term gone;
• real numeral-dense module (Mathlib.NumberTheory.PythagoreanTriples, measured on a 4.34.0-pre fork): module wall 2.40 → 2.22 s (−7.4 %);
• honest scoping: modules whose numerals are isolated literals (Mathlib.Data.Nat.Log, Mathlib.Data.Nat.Choose.Sum) are neutral — the win is specific to the chained-literal regime;
• soundness: broken proofs error identically; oleans byte-identical with the option on vs off (verified on the rebased master build, and previously on Batteries.Data.List.Lemmas + PythagoreanTriples on the 4.34.0-pre fork); ON-vs-ON deterministic; Batteries corpus builds clean.

Context

Found while profiling where per-command main-thread elaboration time goes. A remaining (separate, smaller) superlinearity after this fix is the .coe/defaulting round structure (one default instance applied per full pass); happy to file separately if useful.

Versions

Lean 4.34.0-nightly-2026-07-19 (25ba8c3d), reproduced identically on 4.34.0-pre (4f53dd7). Linux x86_64, 16 cores.

Start at Elab.synthesizeSyntheticMVars and inspect how pending .typeClass metavariables are retried, then trace the relevant Term.State handling. Use the supplied scale_k.lean reproduction to measure the chained-literal case. Done means avoiding unchanged pending-goal retries while preserving the reported proof behavior, determinism, and corpus-build results.