fix(infer): return types were never checked — 13 false accepts

[Ch4s3]

The oracle was never checking function return types

fn f(n : Int) : String do n end — march rejects it. We accepted it.

inferModule''s .dfn arm honoured parameter annotations and discarded retAnnot entirely, so every return-position type error was invisible to the oracle. Independent type checking is milestone A1/A2's entire purpose, and half of function type-checking has been absent since then — through five milestones, 334 corpus files, and several reviews.

Found by an adversarial hunt targeting Infer.lean (1,525 lines) on the grounds that it had received far less scrutiny than CapCheck.lean (4,168 lines) while judging the majority of non-capability files.

~76 probes. 13 confirmed false accepts, ZERO false rejects. 12 fixed, 1 deliberately left.

Findings

#	Probe	march rejects because	before	after
1	fn f(n : Int) : String do n end	expected String, got Int	accept	reject
2	fn f(n : Int) : () do n end	expected (), got Int	accept	reject
3	fn f() : Float do 1 end	expected Float, got Int	accept	reject
4	fn f() : Int do 1.5 end	expected Int, got Float	accept	reject
5	record field returned at wrong type	expected String, got Int	accept	reject
6	type Age = Int; fn f(x:Int) : Age do x end	aliases are nominal to march	accept	reject
7	fn g() : String do fact(3) end	expected String, got Int	accept	reject
8	same, inside a nested mod	expected Bool, got Int	accept	reject
9	no_panic: match n do 0; 1 end (Int)	non-exhaustive	accept	reject
10	same on String	non-exhaustive	accept	reject
11	same on Float	non-exhaustive	accept	reject
12	match b do true -> 1 end (Bool)	non-exhaustive	accept	reject
13	(true,true) over (Bool,Bool)	non-exhaustive	accept	accept — left

1–8 are the one root cause. 9–12 are a second: Pattern.lit isn't a modeled shape, so the exhaustiveness safety net short-circuited before reading the scrutinee type, and Bool isn't in builtinCtors.

Finding 6 is worth flagging on its own — march treats type Age = Int nominally, so an Int is not an Age. Easy to assume structural.

Why both fixes are safe

Neither depends on an input the checker reconstructs — the governing rule adopted after slice (c)'s four failed exhaustiveness rounds:

• retAnnot is some only when fully in-fragment, so tyToMTy cannot throw on it.
• find_missing_mc decides infinite-domain scrutinees (Int/Float/String/Char/Atom) and Bool outright, consulting neither the constructor universe nor the or-expansion policy — the two reconstructed inputs that caused trouble before.

Validated against all 246 march-accepted files in specs/**/accept, examples/, and stdlib/: zero rejects. Plus explicit near-misses — catch-alls, k as m, true | false, guarded arms, and unit/generic/Cap returns. 13 fixtures added.

Builtin signature audit

Every registered builtin checked against march's effective type (not just its table entry — the println bug was a table entry that turned out to be dead code).

• println is the only prelude-shadowed name. Grepped stdlib/prelude.march for all 17 registered builtins.
• The other 16 match march's table exactly (print, print_int/float, *_to_string, string_length/concat, ++, %, +. -. *. /., && || not, Num/Ord/Eq operators, root_cap, cap_narrow), each probed at a wrong argument type — all 8 such probes agree.
• Unregistered builtins (to_string, head, int_*, float_*, record_*) throw SKIP: unbound variable → exit 2. Safe, but a real coverage hole.

Conformance

total files: 334   MATCH 86   MISMATCH 0   ERROR 0
SKIP 246 (145 accept / 101 reject)   SKIP-LEDGER OK   RESULT PASS

Unchanged from before the fix — the corpus does not exercise a single one of these 13 shapes. Fourth time this pattern has held; the fixtures are the only coverage.

Left unfixed, deliberately

• ci: repin to march 7c1d701c, re-baseline skip ledger at 242 files #13, nested tuple patterns — needs the real Maranget matrix, not a constructor-name set. Attempting it with the current machinery is exactly what cost four rounds in slice (c).
• Mutual recursion always hits SKIP: unbound variable: inferModule' folds decls in order, so forward references never resolve. Safe, but it removes a common shape from coverage — including one where march rejects on a wrong return type. A pre-pass binding top-level dfn names to fresh metavars would close it.

The pattern worth noting

retAnnot was decoded, threaded into Decl.dfn, scanned by CapCheck, and even had a hand-written #eval exercising the unify — and the one site that mattered dropped it behind a rationalising comment.

That is the same shape as the println bug (an authoritative-looking builtin table that was dead code) and the ELet bug (a docstring asserting march "never produces ELet here", false on two counts). Three defects, one mechanism: a plausible comment standing in for a check that wasn't there. Every remaining decoded-but-unconsumed field deserves an audit.