The #55 cutover (plan 0121, Task 4) is blocked: deleting
ParamMode::Implicit activates the strict linearity check universally,
but the migrated corpus does not pass cleanly. #56 (spec 0063) closed
two false-positive classes; universal activation surfaces three more
plus one genuine corpus over-consume. This spec is the "#56 part 2"
hardening, sibling to 0063, landing before the irreversible variant
deletion. It does NOT patch a fifth phase onto plan 0121 (project
rule: 2+ blocking classes = spec defect).
Four additive fixes, no schema/hash/codegen change, check stays
diagnostic-only:
- Type table teed from the typecheck pass (synth Let arm at lib.rs:3808
computes the binder type then discards it) into (def,binder)->Type,
threaded to linearity. The "stop discarding known information" fix,
not a re-run of inference in the walk (ruled out by aaa70d4 / 0063).
- Class 3 (value-typed let-binder): is_value seeded from the table,
extending 0063's per-binder flag to the let site it deferred.
- Class 1 (local function-typed binder): BinderState.fn_param_modes;
callee_arg_modes consults local binders (params/lam from signature,
let from the table) before the global table.
- Class 2 (let-alias of a borrowed value): an alias REDIRECT (not a
state clone -- a clone would miss a real double-consume), root-
resolved in use_var. Closes the contract 0008:340 carve-out.
- Class 4 (partition_eithers): genuine double-consume, body rewrite
(destructure rest once); check unchanged, must-stay-RED fixture pins
it.
Design call (user delegated): the binder->type table is the chosen
mechanism over local/shallow derivation -- the type is known and
discarded, and 0063's deferral of exactly this class is what produced
#57; a local-only patch re-creates the latent class. All five fenced
ail fixtures parse and reach the linearity stage with the recorded
exit codes (parse-every-block gate fired). Grounding-check PASS: every
load-bearing assumption ratified by a green in-source test or a live
RED trace.
refs #57
