feat(tailcall): model march's Pass 3 tail-call enforcement

[Ch4s3]

Closes a live FALSE ACCEPT class. march ERRORs on truly unbounded non-tail recursion (enforce_tail_calls_in_decls, typecheck.ml:11367 → check_recursion_safety, :10715) and nothing here modelled it.

probe	before	after	march
loopy — loopy(n + 1) + 1	0	1	1
go — same shape	0	1	1
mutual — walk/helper SCC	2	1	1
nested_mod_flat	0	1	1
fact — fact(n - 1) * n, structural	0	0	0
11 other clean probes	—	not-1	0

mutual flipped without waiting for af6fece (still unmerged on claude/mutual-recursion), because the pass runs pre-gate.

Design

MarchLean/TailCall.lean ports the analysis 1:1 from march's own code: the extern-name subtraction, the scope-threaded shadowing discipline, and is_structurally_smaller verbatim. Getting that last one too narrow is what manufactures false rejects — march merely WARNS on structural recursion and allows it, so fact(n - 1) * n must keep passing.

It reads the raw JSON envelope, not the decoded Module — the only pass here that does. Elab is lossy in exactly the four places Pass 3 is structural: it drops fn.attrs (so @[no_warn_recursion], live in march's own stdlib, would be invisible), and collapses ECond/ELetQ/ELetFn to Term.opaque_, erasing the tail positions and binders the analysis is made of. Reading the envelope needs no change to Syntax.lean or Elab.lean, so no existing verdict can be perturbed by construction.

Placement: pre-gate, beside CapCheck, mirroring march (its capability checks at typecheck.ml:11351 precede Pass 3 at :11367). TailResult has no skip case — the pass returns reject-or-silence and never licenses an accept.

Bail rule: an unrecognised expression or pattern kind anywhere in a function body abandons that function. Bail beats error, since an unmodelled block sibling could have been an ELet shadowing the recursive name.

Two findings that came from probes, not from reading the source

march's Pass 3 does not fire inside a nested mod. enforce_tail_calls_in_decls has a DMod arm that recurses into inner decls and looks entirely load-bearing. It is dead in the --check path. Confirmed two ways: no error, and no structural-recursion warning either — so it is Pass 3 as a whole that finds nothing inside, not just its error path. Following the source here would have been a false reject.

Root cause, traced upstream after this branch was written: Desugar.qualify_module_refs rewrites bare intra-module call sites inside every nested DMod to Prefix.name (EVar "boom" → EVar "Inner.boom") and leaves the declaration name bare. Pass 3 built fn_names from the bare declaration name, so it searched a post-desugar body for a pre-desugar name and matched nothing. The DMod arm does run — it just never matches.

That is a march bug, now fixed upstream on fix/tailcall-nested-mod-qualified-names. When this repo re-pins to a march carrying that fix, nested_mod flips from clean to tailcall and the pass must model the prefix. That probe going red is the intended signal — it is the whole reason march is modelled as it behaves rather than as its source reads.

Correction to an earlier revision of this description: it also claimed a type error inside a nested mod goes unreported. That was wrong — the measurement piped march through head and read $?, which is head's status. Nested mod bodies are typechecked normally. The Pass 3 findings used grep -c on the output and are unaffected.

The probe runner must not use pipefail. march exits 1 on --emit-core-ast for a rejected file, which masks march-lean-check's own exit — turning every false accept in the suite into a spurious "ok". This bit on the suite's first run.

Verification

Every clean probe was mutation-tested — break the guard it protects, confirm it goes red. That caught three probes passing for the wrong reason:

• cond_tail recursed as spin(n - 1), which is structurally smaller and therefore allowed whether or not the arm body is tail position. It tested nothing. Rewritten to spin(dec(n)).
• The shadow_* trio guarded only the walk, leaving the call graph unguarded → added shadow_edge_*.
• Nothing guarded calls treating ELam/ELetFn bodies as new scopes → added lambda_edge, letfn_edge.

The full guard → probe table is in §8 of the design doc.

• 22 probes (scripts/tailcall-probes.sh), wired into CI before the harness so a false reject fails fast.
• 3 native_decide guards over real emitter envelopes — a regression breaks the build, no march binary required.
• Corpus: unchanged — MATCH 86 / MISMATCH 0 / SKIP 246 (145 + 101) / KNOWN_LIMITATION 2 / PASS, identical to baseline. It moved not one file, exactly as expected: the corpus contains no unbounded non-tail recursion. It proves no regression and nothing more.
• Stdlib sweep (one-time; CI's sparse checkout excludes stdlib/): every march-accepted file under march's stdlib/ and examples/ — 124 files, 0 tail-call rejects. Since march accepts them all, any reject would be a false reject by definition. Exercises real @[no_warn_recursion] uses in hamt.march and dataframe.march.
• Performance is a non-issue: dataframe.march (3520 lines, 4 MB envelope) checks in 0.12 s.

Design doc: specs/plans/2026-08-09-tail-call-enforcement-design.md.

[Ch4s3]

Upstream fix for the nested-mod finding in §5.5: march-language/march#239.

That PR makes march reject nested-mod non-tail recursion, so when this repo re-pins to a march carrying it, scripts/tailcall-probes/nested_mod.march flips from clean to tailcall and TailCall.lean must model the qualifying prefix. The probe going red is the intended signal, not a regression — it is why march is modelled as it behaves rather than as its source reads.

Root cause, for the record: Desugar.qualify_module_refs rewrites bare intra-module call sites inside every nested DMod to Prefix.name and leaves the declaration name bare, so Pass 3 searched a post-desugar body for a pre-desugar name. The DMod arm does run — it just never matched. #239 also closes a second, nesting-free instance of the same blind spot (a self-qualified call in a dependency module), which this repo does not currently probe.