LCNF simplifier scales super-linearly

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following Claude-produced MWE exhibits superlinear scaling:

import Lean

/-!
MWE: super-linear LCNF compile time on a sequential monadic do-block.

For each size N, `body_N` is `do <N copies of `if let some r ← step then return r`>;
return 0`. The elaborated term grows linearly in N, but `compilation (LCNF base)` is
super-linear — at N=64 it takes ~3.5 s.

The cost is essentially all in `pass simp` (`src/Lean/Compiler/LCNF/Simp.lean`).
`Decl.simp` is a fixpoint loop; iteration 1 dominates, and within it the
`# visited` counter (recursive `simp` calls) grows super-linearly:

  N=4 → 8 → 16 → 32 :  visited/size ratio = 10 → 12 → 15 → 22

`# inline local` (local function / join-point inlines) is exactly linear (one per
do-statement), so what's super-linear is *visits per inline*. Hypothesized
mechanism: monadic `if let some` desugars to a chain of N nested `__do_jp` join
points. Each JP inline copies the JP body into its call site, and the parent
`simp` re-traverses the copy. With N nested JPs of size O(N), total work is O(N²).

The choice of monad matters for the *severity*: deeper transformer stacks
(here `ReaderT Nat (StateRefT Nat MetaM)`) compound the inlining cost. Plain
`IO` shows the same shape but at smaller absolute numbers.

Measurements (stage1 lean 4.31.0-pre, commit 7df0bef7):

  N    LCNF base    pass simp    ratio vs N/2
  4    6.6 ms       ~6 ms        —
  8    21 ms        ~20 ms       3.2×
  16   55 ms        ~54 ms       2.6×
  32   270 ms       ~265 ms      4.9×
  64   3.52 s       ~3.5 s       13×

Run from the worktree root:

  build/release/stage1/bin/lean --root=. lcnf_simp_scaling_mwe.lean \
    2>&1 | grep -E '^(=====|compilation \(LCNF base\))'

To re-do per-pass attribution, instrument `runPassManagerPart` in
`src/Lean/Compiler/LCNF/Main.lean` by wrapping `pass.run` in
`profileitM Exception s!"pass {pass.name}" (← getOptions) ...`.
-/

open Lean Elab

abbrev MyM := ReaderT Nat (StateRefT Nat Lean.MetaM)

@[noinline] opaque step : MyM (Option Nat)

elab "mkBody " n:num : term => do
  let n := n.getNat
  let mut stmts : Array (TSyntax `Lean.Parser.Term.doSeqItem) := #[]
  for _ in [:n] do
    stmts := stmts.push (← `(Lean.Parser.Term.doSeqItem| if let some r ← step then return r))
  stmts := stmts.push (← `(Lean.Parser.Term.doSeqItem| return 0))
  let stx ← `(do $[$stmts]*)
  Term.elabTerm stx none

set_option profiler true
set_option profiler.threshold 100

set_option backward.do.legacy false -- to test with the new do elaborator (old reproduces the same)

#eval IO.eprintln "===== body_2 ====="
set_option trace.Elab.do true in
def body_2 : MyM Nat := mkBody 2
#eval IO.eprintln "===== body_30 ====="
def body_30 : MyM Nat := mkBody 30
#eval IO.eprintln "===== body_60 ====="
def body_60 : MyM Nat := mkBody 60
#eval IO.eprintln "===== body_80 ====="
def body_90 : MyM Nat := mkBody 90

Steps to Reproduce

Elaborate the file.

Expected behavior: Elaboration time for mkBody n scales linearly in n

Actual behavior: Elaboration time for mkBody n scales super-linearly in n

Versions

Lean 4.31.0, commit
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the provided lcnf_simp_scaling_mwe.lean command from the worktree root and inspect pass simp in src/Lean/Compiler/LCNF/Simp.lean. Use the suggested runPassManagerPart instrumentation in src/Lean/Compiler/LCNF/Main.lean to confirm the attribution; done means the reproducer's elaboration and simp work no longer scale super-linearly, with a regression test if the project provides an appropriate location.