test: add typeclass synthesis scaling benchmarks

This PR adds 9 variable-size benchmarks for typeclass synthesis in
tests/elab_bench/, covering different instance graph shapes:

- synth_chain: linear chain of explicit instances
- synth_diamond_stack: stacked diamonds (exposes synthesis failure at depth 19)
- synth_hypercube: d-dimensional hypercube with conjunctive instances
- synth_ladder_rungs_first / synth_ladder_rails_first: ladder graphs
  testing whether instance declaration order affects performance
- synth_wide_extends: wide fan-in through accumulator chain
- synth_nat_indexed: Nat-parameterized recursive class
- synth_accum_param: accumulating typeclass parameters per level
- synth_nested_param: nested V-chain with P-chain consuming it

Each benchmark programmatically generates class hierarchies at multiple
sizes using command elaborators, times synthesis via Meta.synthInstance,
and emits per-size measurement lines.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

tests/elab_bench/synth_accum_param.lean

@@ -0,0 +1,80 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: accumulating typeclass parameters.
+
+Generates a chain where each successive class requires one more typeclass parameter:
+  `class V (i : Nat) (α : Type) where u : Unit := ()`
+  `instance : V i Nat := {}` for i = 1..n
+  `class P0 (α : Type) where u : Unit := ()`
+  `class P1 (α : Type) [V 1 α] where u : Unit := ()`
+  `class P2 (α : Type) [V 1 α] [V 2 α] where u : Unit := ()`
+  ...
+  `class Pk (α : Type) [V 1 α] [V 2 α] ... [V k α] where u : Unit := ()`
+  With instances: `instance : P0 Nat := {}`, `instance [V 1 α] [P0 α] : P1 α := {}`, etc.
+  Each Pk instance requires P{k-1} and V k.
+Synthesize: Pn Nat
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 4000000
+set_option synthInstance.maxSize 65536
+
+syntax (name := synthBenchAccumParam) "#synth_bench_accum_param" : command
+
+@[command_elab synthBenchAccumParam]
+def synthBenchAccumParamImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [5] [5, 25, 100, 500, 1000]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"AccumParam{n}")
+    elabCommand (← `(namespace $ns))
+    -- Generate V class (parameterized by Nat and Type)
+    let vId := mkIdent (Name.mkSimple "V")
+    let iId := mkIdent (Name.mkSimple "i")
+    let aId := mkIdent (Name.mkSimple "α")
+    elabCommand (← `(class $vId ($iId : Nat) ($aId : Type) where u : Unit := ()))
+    -- Generate V instances for Nat: V 1 Nat, V 2 Nat, ..., V n Nat
+    for i in List.range n do
+      let iLit := Syntax.mkNumLit s!"{i + 1}"
+      elabCommand (← `(instance : $vId $iLit Nat := {}))
+    -- Generate P classes and instances using a chain approach:
+    -- P0 has no V-params. Each Pi requires P{i-1} and V i.
+    -- P0 class and base instance
+    let p0 := mkIdent (Name.mkSimple "P0")
+    elabCommand (← `(class $p0 ($aId : Type) where u : Unit := ()))
+    elabCommand (← `(instance : $p0 Nat := {}))
+    -- Pi for i = 1..n: requires [P{i-1} α] and [V i α]
+    for i in List.range n do
+      let j := i + 1
+      let pj := mkIdent (Name.mkSimple s!"P{j}")
+      let pprev := mkIdent (Name.mkSimple s!"P{i}")
+      let jLit := Syntax.mkNumLit s!"{j}"
+      elabCommand (← `(class $pj ($aId : Type) where u : Unit := ()))
+      elabCommand (← `(instance [$pprev $aId] [$vId $jLit $aId] : $pj $aId := {}))
+    -- Synthesize Pn Nat and time it
+    let pn := mkIdent (Name.mkSimple s!"P{n}")
+    liftTermElabM do
+      let pnNat ← Term.elabTerm (← `($pn Nat)) none
+      let pnNat ← instantiateMVars pnNat
+      let ms ← timeSynth pnNat
+      emitMeasurement "accum_param" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_accum_param

tests/elab_bench/synth_chain.lean

@@ -0,0 +1,60 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: linear chain.
+
+Generates a chain of n classes with explicit instances:
+  `instance : C₀`, `instance [C₀] : C₁`, ..., `instance [Cₙ₋₁] : Cₙ`
+Then synthesizes `Cₙ`. The solver must walk backwards: expected O(n).
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 8000000
+set_option synthInstance.maxSize 200000
+
+syntax (name := synthBenchChain) "#synth_bench_chain" : command
+
+@[command_elab synthBenchChain]
+def synthBenchChainImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [50] [200, 400, 600, 800, 1000]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"Chain{n}")
+    elabCommand (← `(namespace $ns))
+    -- Generate n+1 classes: C0, C1, ..., Cn
+    for i in List.range (n + 1) do
+      let ci := mkIdent (Name.mkSimple s!"C{i}")
+      elabCommand (← `(class $ci where u : Unit := ()))
+    -- Generate instances: C0 base, [Ci] : C{i+1} for i=0..n-1
+    let c0 := mkIdent (Name.mkSimple "C0")
+    elabCommand (← `(instance : $c0 := {}))
+    for i in List.range n do
+      let ci := mkIdent (Name.mkSimple s!"C{i}")
+      let ci1 := mkIdent (Name.mkSimple s!"C{i + 1}")
+      elabCommand (← `(instance [$ci] : $ci1 := {}))
+    -- Synthesize Cn and time it
+    let cn := mkIdent (Name.mkSimple s!"C{n}")
+    liftTermElabM do
+      let cnExpr ← Term.elabTerm (← `($cn)) none
+      let cnExpr ← instantiateMVars cnExpr
+      let ms ← timeSynth cnExpr
+      emitMeasurement "chain" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_chain

tests/elab_bench/synth_diamond_stack.lean

@@ -0,0 +1,73 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: stacked diamonds.
+
+Generates a stack of n diamond shapes:
+  T0 → L0, T0 → R0, L0 ∧ R0 → T1, T1 → L1, T1 → R1, L1 ∧ R1 → T2, ...
+Base instance: T0. Synthesize: Tn.
+Tabled resolution finds the answer in O(n) time, but the constructed proof term
+has no sharing: both Li and Ri independently embed the full Ti proof, causing 2^n
+blowup in solution size. This causes synthesis to silently fail once the proof term
+exceeds `synthInstance.maxSize`. See https://github.com/leanprover/lean4/issues/13085
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 80000000
+set_option synthInstance.maxSize 2000000
+
+syntax (name := synthBenchDiamondStack) "#synth_bench_diamond_stack" : command
+
+@[command_elab synthBenchDiamondStack]
+def synthBenchDiamondStackImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [5] [1, 2, 4, 6, 8, 10, 12, 14, 15]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"DiamondStack{n}")
+    elabCommand (← `(namespace $ns))
+    -- Generate base class T0
+    let t0 := mkIdent (Name.mkSimple "T0")
+    elabCommand (← `(class $t0 where u : Unit := ()))
+    elabCommand (← `(instance : $t0 := {}))
+    -- Generate diamond levels
+    for i in List.range n do
+      let ti := mkIdent (Name.mkSimple s!"T{i}")
+      let li := mkIdent (Name.mkSimple s!"L{i}")
+      let ri := mkIdent (Name.mkSimple s!"R{i}")
+      let ti1 := mkIdent (Name.mkSimple s!"T{i + 1}")
+      -- Left and right classes
+      elabCommand (← `(class $li where u : Unit := ()))
+      elabCommand (← `(class $ri where u : Unit := ()))
+      -- Ti → Li, Ti → Ri
+      elabCommand (← `(instance [$ti] : $li := {}))
+      elabCommand (← `(instance [$ti] : $ri := {}))
+      -- Next top class
+      elabCommand (← `(class $ti1 where u : Unit := ()))
+      -- Li ∧ Ri → T{i+1}
+      elabCommand (← `(instance [$li] [$ri] : $ti1 := {}))
+    -- Synthesize Tn and time it
+    let tn := mkIdent (Name.mkSimple s!"T{n}")
+    liftTermElabM do
+      let tnExpr ← Term.elabTerm (← `($tn)) none
+      let tnExpr ← instantiateMVars tnExpr
+      let ms ← timeSynth tnExpr
+      emitMeasurement "diamond_stack" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_diamond_stack

tests/elab_bench/synth_hypercube.lean

@@ -0,0 +1,103 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: d-dimensional hypercube.
+
+Generates 2^d vertex classes V0..V_{2^d-1} arranged as a d-dimensional hypercube.
+For each vertex k with popcount > 0, instances encode the requirement that all
+vertices obtained by flipping each 1-bit to 0 must be synthesized:
+  - popcount 1: single instance `[V_{k flip bit}] : Vk`
+  - popcount > 1: chain through accumulators to aggregate all predecessors
+Base: V0
+Synthesize: V_{2^d - 1}
+
+Fails at d=10 due to exponential proof term size (same root cause as diamond_stack).
+See https://github.com/leanprover/lean4/issues/13085
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 80000000
+set_option synthInstance.maxSize 2000000
+
+/-- Get the list of bit positions that are 1 in `k`, for bits 0..d-1. -/
+private def oneBits (k d : Nat) : List Nat := Id.run do
+  let mut result := []
+  for i in List.range d do
+    if k &&& (1 <<< i) != 0 then
+      result := i :: result
+  result.reverse
+
+syntax (name := synthBenchHypercube) "#synth_bench_hypercube" : command
+
+@[command_elab synthBenchHypercube]
+def synthBenchHypercubeImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [3] [1, 2, 3, 4, 5, 6, 7, 8]
+  for d in sizes do
+    let numVertices := 1 <<< d
+    let ns := mkIdent (Name.mkSimple s!"Hypercube{d}")
+    elabCommand (← `(namespace $ns))
+    -- Generate 2^d classes
+    for k in List.range numVertices do
+      let vk := mkIdent (Name.mkSimple s!"V{k}")
+      elabCommand (← `(class $vk where u : Unit := ()))
+    -- Base instance: V0
+    let v0 := mkIdent (Name.mkSimple "V0")
+    elabCommand (← `(instance : $v0 := {}))
+    -- For each vertex k with popcount > 0, generate a conjunctive instance.
+    -- We build the instance command using Syntax directly to handle variable arity.
+    for k in List.range numVertices do
+      let bits := oneBits k d
+      if bits.isEmpty then continue
+      -- For vertices with popcount = 1, use a simple single-binder instance.
+      -- For vertices with popcount > 1, chain through intermediate accumulator classes.
+      if bits.length == 1 then
+        let predK := k ^^^ (1 <<< bits.head!)
+        let vpred := mkIdent (Name.mkSimple s!"V{predK}")
+        let vk := mkIdent (Name.mkSimple s!"V{k}")
+        elabCommand (← `(instance [$vpred] : $vk := {}))
+      else
+        -- Create intermediate accumulator classes: Acc_k_1, Acc_k_2, ..., Acc_k_{m-1}
+        -- Then chain: [V_{pred0}] : Acc_k_1, [Acc_k_1] [V_{pred1}] : Acc_k_2, etc.
+        let preds := bits.map fun i => k ^^^ (1 <<< i)
+        let firstPred := mkIdent (Name.mkSimple s!"V{preds.head!}")
+        let acc1 := mkIdent (Name.mkSimple s!"Acc{k}x1")
+        elabCommand (← `(class $acc1 where u : Unit := ()))
+        elabCommand (← `(instance [$firstPred] : $acc1 := {}))
+        for j in List.range (preds.length - 2) do
+          let accJ := mkIdent (Name.mkSimple s!"Acc{k}x{j + 1}")
+          let accJ1 := mkIdent (Name.mkSimple s!"Acc{k}x{j + 2}")
+          let predJ := mkIdent (Name.mkSimple s!"V{preds[j + 1]!}")
+          elabCommand (← `(class $accJ1 where u : Unit := ()))
+          elabCommand (← `(instance [$accJ] [$predJ] : $accJ1 := {}))
+        -- Final step: [Acc_{m-1}] [V_{last_pred}] : Vk
+        let lastAcc := mkIdent (Name.mkSimple s!"Acc{k}x{preds.length - 1}")
+        let lastPred := mkIdent (Name.mkSimple s!"V{preds.getLast!}")
+        let vk := mkIdent (Name.mkSimple s!"V{k}")
+        elabCommand (← `(instance [$lastAcc] [$lastPred] : $vk := {}))
+    -- Synthesize V_{2^d - 1} and time it
+    let target := mkIdent (Name.mkSimple s!"V{numVertices - 1}")
+    liftTermElabM do
+      let targetExpr ← Term.elabTerm (← `($target)) none
+      let targetExpr ← instantiateMVars targetExpr
+      let ms ← timeSynth targetExpr
+      emitMeasurement "hypercube" d ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_hypercube

tests/elab_bench/synth_ladder_rails_first.lean

@@ -0,0 +1,75 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: ladder graph, rails declared first.
+
+Same graph as synth_ladder_rungs_first but with reversed instance declaration order:
+  Classes: A0, B0, A1, B1, ..., An, Bn
+  Rail instances (declared first): [Ai] : A{i+1} and [Bi] : B{i+1} for all i
+  Rung instances (declared second): [Ai] : Bi for all i
+  Base: A0
+  Synthesize: Bn
+Instance declaration order affects search behavior.
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 4000000
+set_option synthInstance.maxSize 65536
+
+syntax (name := synthBenchLadderRailsFirst) "#synth_bench_ladder_rails_first" : command
+
+@[command_elab synthBenchLadderRailsFirst]
+def synthBenchLadderRailsFirstImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [50] [50, 100, 200, 400, 600]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"LadderRailsFirst{n}")
+    elabCommand (← `(namespace $ns))
+    -- Generate classes: A0, B0, A1, B1, ..., An, Bn
+    for i in List.range (n + 1) do
+      let ai := mkIdent (Name.mkSimple s!"A{i}")
+      let bi := mkIdent (Name.mkSimple s!"B{i}")
+      elabCommand (← `(class $ai where u : Unit := ()))
+      elabCommand (← `(class $bi where u : Unit := ()))
+    -- Base instance
+    let a0 := mkIdent (Name.mkSimple "A0")
+    elabCommand (← `(instance : $a0 := {}))
+    -- Rail instances FIRST: [Ai] : A{i+1} and [Bi] : B{i+1}
+    for i in List.range n do
+      let ai := mkIdent (Name.mkSimple s!"A{i}")
+      let ai1 := mkIdent (Name.mkSimple s!"A{i + 1}")
+      let bi := mkIdent (Name.mkSimple s!"B{i}")
+      let bi1 := mkIdent (Name.mkSimple s!"B{i + 1}")
+      elabCommand (← `(instance [$ai] : $ai1 := {}))
+      elabCommand (← `(instance [$bi] : $bi1 := {}))
+    -- Rung instances SECOND: [Ai] : Bi
+    for i in List.range (n + 1) do
+      let ai := mkIdent (Name.mkSimple s!"A{i}")
+      let bi := mkIdent (Name.mkSimple s!"B{i}")
+      elabCommand (← `(instance [$ai] : $bi := {}))
+    -- Synthesize Bn and time it
+    let bn := mkIdent (Name.mkSimple s!"B{n}")
+    liftTermElabM do
+      let bnExpr ← Term.elabTerm (← `($bn)) none
+      let bnExpr ← instantiateMVars bnExpr
+      let ms ← timeSynth bnExpr
+      emitMeasurement "ladder_rails_first" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_ladder_rails_first

tests/elab_bench/synth_ladder_rungs_first.lean

@@ -0,0 +1,75 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: ladder graph, rungs declared first.
+
+Generates a ladder graph with two rails (A-chain, B-chain) and rungs:
+  Classes: A0, B0, A1, B1, ..., An, Bn
+  Rung instances (declared first): [Ai] : Bi for all i
+  Rail instances (declared second): [Ai] : A{i+1} and [Bi] : B{i+1} for all i
+  Base: A0
+  Synthesize: Bn
+Instance declaration order affects search behavior.
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 4000000
+set_option synthInstance.maxSize 65536
+
+syntax (name := synthBenchLadderRungsFirst) "#synth_bench_ladder_rungs_first" : command
+
+@[command_elab synthBenchLadderRungsFirst]
+def synthBenchLadderRungsFirstImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [50] [50, 100, 200, 400, 600]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"LadderRungsFirst{n}")
+    elabCommand (← `(namespace $ns))
+    -- Generate classes: A0, B0, A1, B1, ..., An, Bn
+    for i in List.range (n + 1) do
+      let ai := mkIdent (Name.mkSimple s!"A{i}")
+      let bi := mkIdent (Name.mkSimple s!"B{i}")
+      elabCommand (← `(class $ai where u : Unit := ()))
+      elabCommand (← `(class $bi where u : Unit := ()))
+    -- Base instance
+    let a0 := mkIdent (Name.mkSimple "A0")
+    elabCommand (← `(instance : $a0 := {}))
+    -- Rung instances FIRST: [Ai] : Bi
+    for i in List.range (n + 1) do
+      let ai := mkIdent (Name.mkSimple s!"A{i}")
+      let bi := mkIdent (Name.mkSimple s!"B{i}")
+      elabCommand (← `(instance [$ai] : $bi := {}))
+    -- Rail instances SECOND: [Ai] : A{i+1} and [Bi] : B{i+1}
+    for i in List.range n do
+      let ai := mkIdent (Name.mkSimple s!"A{i}")
+      let ai1 := mkIdent (Name.mkSimple s!"A{i + 1}")
+      let bi := mkIdent (Name.mkSimple s!"B{i}")
+      let bi1 := mkIdent (Name.mkSimple s!"B{i + 1}")
+      elabCommand (← `(instance [$ai] : $ai1 := {}))
+      elabCommand (← `(instance [$bi] : $bi1 := {}))
+    -- Synthesize Bn and time it
+    let bn := mkIdent (Name.mkSimple s!"B{n}")
+    liftTermElabM do
+      let bnExpr ← Term.elabTerm (← `($bn)) none
+      let bnExpr ← instantiateMVars bnExpr
+      let ms ← timeSynth bnExpr
+      emitMeasurement "ladder_rungs_first" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_ladder_rungs_first

tests/elab_bench/synth_nat_indexed.lean

@@ -0,0 +1,59 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: Nat-parameterized chain.
+
+Generates a single class parameterized by Nat, with recursive instances:
+  `class C (n : Nat) where u : Unit := ()`
+  `instance : C 0 := {}`
+  `instance [C n] : C (n + 1) := {}`
+Then synthesizes `C <literal>` for various sizes using Expr-level construction.
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 4000000
+set_option synthInstance.maxSize 65536
+
+syntax (name := synthBenchNatIndexed) "#synth_bench_nat_indexed" : command
+
+@[command_elab synthBenchNatIndexed]
+def synthBenchNatIndexedImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [10] [10, 50, 200, 800, 1600]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"NatIndexed{n}")
+    elabCommand (← `(namespace $ns))
+    -- Declare the parameterized class and instances
+    let cId := mkIdent (Name.mkSimple "C")
+    let nId := mkIdent (Name.mkSimple "n")
+    elabCommand (← `(class $cId ($nId : Nat) where u : Unit := ()))
+    elabCommand (← `(instance : $cId 0 := {}))
+    elabCommand (← `(instance [$cId $nId] : $cId ($nId + 1) := {}))
+    -- Synthesize C n using Expr-level construction
+    liftTermElabM do
+      let cName ← resolveGlobalConstNoOverload (← `($cId))
+      let cInfo ← getConstInfo cName
+      let cExpr := mkConst cName (cInfo.levelParams.map fun _ => Level.zero)
+      let natLit := mkNatLit n
+      let goalType := mkApp cExpr natLit
+      let ms ← timeSynth goalType
+      emitMeasurement "nat_indexed" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_nat_indexed

tests/elab_bench/synth_nested_param.lean

@@ -0,0 +1,90 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: nested typeclass parameter chain.
+
+Generates a V chain with nested dependencies:
+  `class V1 (α : Type) where u : Unit := ()`
+  `class V2 (α : Type) [V1 α] where u : Unit := ()`
+  ...
+  `class Vk (α : Type) [V{k-1} α] where u : Unit := ()`
+V instances for Nat (each depends on the previous):
+  `instance : V1 Nat := {}`
+  `instance : V2 Nat := {}` (V1 Nat resolved automatically)
+  ...
+P chain: P0 has no V deps, Pk has [Vk α] (which transitively needs V1..V{k-1}):
+  `class P0 (α : Type) where u : Unit := ()`
+  `class P1 (α : Type) [V1 α] where u : Unit := ()`
+  ...
+  `class Pk (α : Type) [Vk α] where u : Unit := ()`
+P instances via chain: [P{k-1} α] [Vk α] : Pk α
+Synthesize: Pn Nat
+
+Fails around n=400 due to exponential proof term size from shared V-chain subgoals.
+See https://github.com/leanprover/lean4/issues/13085
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 4000000
+set_option synthInstance.maxSize 65536
+
+syntax (name := synthBenchNestedParam) "#synth_bench_nested_param" : command
+
+@[command_elab synthBenchNestedParam]
+def synthBenchNestedParamImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [2] [2, 20, 100, 200, 300]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"NestedParam{n}")
+    elabCommand (← `(namespace $ns))
+    -- V chain: V1, V2, ..., Vn are all standalone classes
+    let aId := mkIdent (Name.mkSimple "α")
+    for i in List.range n do
+      let vi := mkIdent (Name.mkSimple s!"V{i + 1}")
+      elabCommand (← `(class $vi ($aId : Type) where u : Unit := ()))
+    -- V instances for Nat: V1 Nat (base), then V{k} Nat requires [V{k-1} Nat]
+    let v1 := mkIdent (Name.mkSimple "V1")
+    elabCommand (← `(instance : $v1 Nat := {}))
+    for i in List.range (n - 1) do
+      let j := i + 2
+      let vj := mkIdent (Name.mkSimple s!"V{j}")
+      let vprev := mkIdent (Name.mkSimple s!"V{j - 1}")
+      elabCommand (← `(instance [$vprev Nat] : $vj Nat := {}))
+    -- P chain: P0 (no V deps)
+    let p0 := mkIdent (Name.mkSimple "P0")
+    elabCommand (← `(class $p0 ($aId : Type) where u : Unit := ()))
+    elabCommand (← `(instance : $p0 Nat := {}))
+    -- Pi for i = 1..n: requires [P{i-1} α] and [Vi α]
+    for i in List.range n do
+      let j := i + 1
+      let pj := mkIdent (Name.mkSimple s!"P{j}")
+      let pprev := mkIdent (Name.mkSimple s!"P{i}")
+      let vj := mkIdent (Name.mkSimple s!"V{j}")
+      elabCommand (← `(class $pj ($aId : Type) where u : Unit := ()))
+      elabCommand (← `(instance [$pprev $aId] [$vj $aId] : $pj $aId := {}))
+    -- Synthesize Pn Nat and time it
+    let pn := mkIdent (Name.mkSimple s!"P{n}")
+    liftTermElabM do
+      let pnNat ← Term.elabTerm (← `($pn Nat)) none
+      let pnNat ← instantiateMVars pnNat
+      let ms ← timeSynth pnNat
+      emitMeasurement "nested_param" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_nested_param

tests/elab_bench/synth_wide_extends.lean

@@ -0,0 +1,79 @@
+import Lean
+
+/-!
+Typeclass synthesis benchmark: wide fan-in.
+
+Generates a wide fan-in pattern:
+  Classes: Base, S1, S2, ..., Sn, T1, T2, ..., Tn (= Target)
+  Instances:
+    Base (base)
+    [Base] : Si for all i
+    [S1] : T1
+    [T{i-1}] [S{i}] : Ti for i = 2..n
+  Synthesize: Tn
+The fan-in is accumulated through a chain: Ti collects S1..Si.
+-/
+
+set_option Elab.async false
+
+open Lean Elab Meta
+open Elab.Command (CommandElab CommandElabM elabCommand liftTermElabM)
+
+def getBenchSizes (testSizes benchSizes : List Nat) : IO (List Nat) := do
+  if (← IO.getEnv "TEST_BENCH") == some "1" then return benchSizes
+  else return testSizes
+
+def timeSynth (goalType : Expr) : MetaM Float := do
+  let startTime ← IO.monoNanosNow
+  discard <| Meta.synthInstance goalType
+  let endTime ← IO.monoNanosNow
+  return (endTime - startTime).toFloat / 1000000.0
+
+def emitMeasurement (shape : String) (n : Nat) (ms : Float) : IO Unit :=
+  IO.println s!"measurement: {shape}_n{n} {ms / 1000.0} s"
+
+set_option synthInstance.maxHeartbeats 4000000
+set_option synthInstance.maxSize 65536
+
+syntax (name := synthBenchWideExtends) "#synth_bench_wide_extends" : command
+
+@[command_elab synthBenchWideExtends]
+def synthBenchWideExtendsImpl : CommandElab := fun _ => do
+  let sizes ← getBenchSizes [10] [10, 40, 160, 400, 800]
+  for n in sizes do
+    let ns := mkIdent (Name.mkSimple s!"WideExtends{n}")
+    elabCommand (← `(namespace $ns))
+    -- Base class
+    let base := mkIdent (Name.mkSimple "Base")
+    elabCommand (← `(class $base where u : Unit := ()))
+    elabCommand (← `(instance : $base := {}))
+    -- S1 .. Sn classes and instances: [Base] : Si
+    for i in List.range n do
+      let si := mkIdent (Name.mkSimple s!"S{i + 1}")
+      elabCommand (← `(class $si where u : Unit := ()))
+      elabCommand (← `(instance [$base] : $si := {}))
+    -- T1 .. Tn classes: accumulator chain
+    for i in List.range n do
+      let ti := mkIdent (Name.mkSimple s!"T{i + 1}")
+      elabCommand (← `(class $ti where u : Unit := ()))
+    -- T1 instance: [S1] : T1
+    let s1 := mkIdent (Name.mkSimple "S1")
+    let t1 := mkIdent (Name.mkSimple "T1")
+    elabCommand (← `(instance [$s1] : $t1 := {}))
+    -- Ti instance: [T{i-1}] [Si] : Ti for i = 2..n
+    for i in List.range (n - 1) do
+      let j := i + 2
+      let tprev := mkIdent (Name.mkSimple s!"T{j - 1}")
+      let sj := mkIdent (Name.mkSimple s!"S{j}")
+      let tj := mkIdent (Name.mkSimple s!"T{j}")
+      elabCommand (← `(instance [$tprev] [$sj] : $tj := {}))
+    -- Synthesize Tn and time it
+    let tn := mkIdent (Name.mkSimple s!"T{n}")
+    liftTermElabM do
+      let tnExpr ← Term.elabTerm (← `($tn)) none
+      let tnExpr ← instantiateMVars tnExpr
+      let ms ← timeSynth tnExpr
+      emitMeasurement "wide_extends" n ms
+    elabCommand (← `(end $ns))
+
+#synth_bench_wide_extends