fix(infer): judge forward references; gate the tail-call false accept it revealed

[Ch4s3]

Stacked on #20 (→ #19). Merges the sibling branch in, so this contains the decoder gate and Check 6 too.

Forward references were never judged — and closing that revealed a live false accept

Compare.inferModule' folds declarations in order, so any forward reference hit SKIP: unbound variable and the whole file exited 2. The gap was not just mutual recursion: a plain fn a calling a later fn b skipped identically. Self-recursion already worked.

What march actually does (not textbook HM)

All in lib/typecheck/typecheck.ml:

1. Pass-1 placeholders (:11210-11235): every top-level DFn → Mono (fresh_var 1), one shared monomorphic var per name, conditional on the name not already being bound (:11232).
2. Dependency reordering (reorder_decls :8988, dependency_order_dfn_run :8533): each maximal contiguous DFn run is permuted into callee-before-caller DFS post-order. Cycles are tolerated, not analysed.
3. check_fn (:6842): fresh monomorphic self-ref, generalize at the outer level (:7139).
4. Reconciliation (:7189-7192): unify placeholder with inferred type only if Mono.

No recursive group, no group generalization. A non-cyclic forward reference is fully let-polymorphic; only cyclic edges see the monomorphic placeholder. The ordering is observable — inserting one top-level let between two functions splits the run, blocks reordering, and march then rejects a program it otherwise accepts.

Polymorphic recursion: probed, not assumed — march rejects it (sz((x,x)) → exit 1, annotated and unannotated alike).

What this implements

A ground-signature pass-1 pre-pass: a dfn whose parameters and return are all ground-annotated has a scheme provably fixed by its signature, so it is published before any body is inferred. For that class march's reordering is provably unobservable. reorder_decls is not reconstructed; everything else keeps the old skip.

Two looser designs were built and discarded because both produced live false rejects — the bare-metavar pre-pass, and the ground pre-pass made visible everywhere (march's placeholder is unsound at fresh_var 1, yielding h : ∀p. p, and accepts what we then rejected).

The part that matters more: a false accept this revealed

Making mutual recursion inferable immediately started ACCEPTing programs march REJECTS on tail-call grounds — enforce_tail_calls_in_decls (:10902), an ERROR-level check with no counterpart here.

The blind spot was not created by this change. Self-recursion had been false-accepting the same check all along; the exposing shapes just skipped for unrelated reasons. Removing a skip converts a hidden non-verdict into a visible wrong verdict.

Discriminator that makes this easy to miss: march warns (exit 0) on non-tail recursion it can prove structurally decreasing (pong(n - 1) + 1), but errors when it cannot (b(n + 1) + 1). Probing only the warning case makes the whole issue look like agreement.

The gate

nonTailRecursionGate (Compare.lean) declines to answer — it renders no opinion on tail-call legality. Scoping mirrors march (:10917-10966): call graph over top-level DFn names, recursive iff SCC size > 1 or a direct self-call, checked set = the whole SCC. REJECT stays reachable: a genuine modeled type error still rejects regardless of tail position.

The whitelist (so fib survives)

The gate alone cost grammar/parse/p15_multi_head_fn_merge.march — i.e. fib — because fib(n-1) + fib(n-2) is non-tail but decreasing, so march only warns. A deliberately tiny structural-decrease recogniser restores it: an argument p - k with p a bare variable in the decrease base and k a positive integer literal, mirroring march's List.exists (:10743).

Conservative on the ungate side by construction — anything unrecognised stays gated. Every divergence from march over-gates: march also accepts v - <anything>, v / <anything>, pattern sub-components, list accessors and nullary constructors; none implemented.

A discovery that turned out to be load-bearing: a multi-head fn fib(0)/fib(1)/fib(n) desugars into one clause with a synthetic __arg0 parameter and a match, so in fib(n - 1) n is not a parameter at all — it is an arm-bound pattern variable. The base therefore has to grow at match arms exactly as march's smaller does (:10812-10824). Without that, fib stays skipped and the reason is invisible.

Probe table (abridged)

shape	march	before	after
mutual pair, well typed / type error	0 / 1	2 / 2	0 / 1
mutual pair, wrong return annotation	1	2	1
three-way cycle a→b→c→a, ok / error	0 / 1	2 / 2	0 / 1
plain forward reference / wrong arity	0 / 1	2 / 2	0 / 1
fib(n-1) + fib(n-2) (p15)	0	0	0
n * fact(n-1); pong(n-1) + 1	0	0	0
loopy(n+1) + 1	1	0 ← pre-existing false accept	2
mutual b(n+1) + 1; dbl(n*2); walk(q,q); h(idf(n))	1	0 or 2	2
polymorphic recursion	1	2	2

Every reject row still rejects. No march=1 row is accepted anywhere. Over-gated edges (all safe): z(n - 0), a shadowed parameter, non-literal g(n - m, m).

Verification

decoder coverage: 0 undeclared, 0 drift, PASS
harness: 334 files   MATCH 87   MISMATCH 0   ERROR 0
         SKIP 245 (145 accept / 100 reject)   SKIP-LEDGER OK   RESULT PASS

395-file sweep: accept 34/213/28, reject 2/30/88 — identical to pre-branch, zero files changed.

Also included

ecb56f3 retracts a false claim the author had written into the pre-pass docstring — that every dfn reaching inference has ground parameter types. Desugared multi-head fns falsify it (FPNamed with "ty": null). No behaviour depended on it, but it was an unchecked assertion propping up a soundness argument.

Open, not closed

march's tail-call enforcement is gated, not modeled. The over-gate class (non-tail recursion whose decrease we cannot recognise syntactically) skips rather than being judged. Separating it properly needs march's real decrease analysis, which was deliberately not reconstructed.