XL-2: a binder is read as a name; an unread parameter slot refuses instead of leaving the domain

[gunbai-bot]

XL-2: the last route of RFM lowering_accessor_collapses_a_sequence_operand, the binder chain. The plan was approved by quiet-seal-543, including the name-reader refinement. Depends on #12779 (reify witness specimen): this PR touches body_lowering_fold, so the floor plans reify_operand_refusal, whose specimen #12420 made stale. It merges main once #12779 lands.

Why the binder reader reads a name, not an operand

body_lower_param_binding_atom_optional fell back to the operand reader and mapped OperandRefRefused to Absent. Every binder position the grammar writes is an identifier, possibly under shells whose value is that one atom:

• a parameter and a record field;
• a named argument's label and a let key;
• a type parameter and a projection's member.

The operand reader refuses only on an operator expression. So OperandRefRefused at a binder position requires ungrammatical input, and the earliest wrong link was calling the operand reader at all.

The reader now reads a name (body_lower_binder_name_behind_shell_optional). It peels only shells whose value is the one atom (a production's captured child, an optional element, a sequence with an empty right projection) and answers Absent otherwise. Every caller already refuses located on Absent. The reader never calls the operand reader, so it has no refusal arm to collapse.

That meets the retirement condition by construction: no caller of OperandRefRead maps Refused to Absent. Every OperandRefRefused site in the compiler propagates. The one non-propagating arm left, stated plainly, is the complexity_accumulator_copy lens: it reads a refused operand as its raw capture, whole, which #12615 wrote deliberately. It is never a part and never Absent.

The real silent drop: parameter slots filtered out of the domain

body_lower_collect_typed_params, lowering's view, filtered out a slot it could not read, so a declaration was Accepted with that parameter missing from its Arrow domain. Now:

• each slot is read or refused (body_lower_typed_param_slot → body_lowering_reason_parameter_unlowered, located at the slot);
• the lowering view and the occurrence-role binder view are one view, which carries the first refusal and never filters;
• the refusal is carried through body_lower_param_list, body_lower_declared_domain_from_param_list and body_lower_fn_signature_optional, now Outcome<Optional<..>>, where Absent is still the declared retained-shell frontier, to the fn declaration;
• body_lower_typed_param_from_comma_seq reads its parameter by position (the right element of seq(,, param)). It no longer tries the right element and then the left one, the , token.

Evidence (local gunbc run, same binary; the only variable is main's body_lowering_fold.dag against head's)

Witness v2.test.claim.body_lowering.parameter_slot_refusal, at body_lower_fn_decl_to_arrow with a supplied declaration. fn psr_f(psr_a: Int, psr_b: Int) is parsed, and its first slot is replaced by an atom that is not a typed parameter. A few probes found no parameter shape that parses and then fails to read, so the input is supplied. The unmodified declaration is the control. The claims are enrolled warm.

claim	main	head
an_unread_parameter_slot_refuses_the_declaration	FAIL (Accepted, psr_a dropped from the domain)	PASS
a_declaration_whose_every_slot_reads_lowers (control)	PASS	PASS

The other witnesses on this head pass: wildcard_pattern_form and wildcard_arm_resolve 9/9, else_arm_nested_if 5/5, parameter_slot_refusal 2/2.

Census: pinned sample, running; results will follow in a comment.

Carriers

• RFM lowering_accessor_collapses_a_sequence_operand: trigger met, receipt added, rung structurally guaranteed on the lowering routes, and the lens arm stated.
• New cause row body_lowering_reason_parameter_unlowered: a wall with no measured population.
• For compiler_frontend_program_status (not edited here): binders are read as names; an unread parameter slot refuses the declaration; no lowering reader collapses a refused operand read.

🤖 Generated with Claude Code

[gunbai-bot]

CI red at 396755a: the only blocker is a wet-lane witness that really executes on the runner host, test.claim.machine_intake.mtcollins1_kvm_observer_protocol_wet_witness.an_unreadable_process_state_never_skips_the_kill_of_an_unpublished_child (expected passed, observed failed). This PR changes body lowering, which that host-process witness does not reach, and its sibling claim in the same module passed in the same run. I reran the failed jobs to see whether it is intermittent. If it is red again I will take it to the witness's owner rather than work around it here. — sent from sharp-carp-336

[gunbai-bot]

Correction to my earlier comment: the wet-lane witness was not the whole story. On the rerun, 9 real claims failed on 396755a:

• the 7 v2.test.claim.body_lowering.statement_let_bind claims;
• 2 test.claim.parse_test_fn_decl_return_clause claims.

The first run's wet-lane refusal had stopped the floor before it reported them.

Cause, mine: the slot walk answered a capture that is neither a parameter nor a pair with a refusing slot, so an empty parameter list (fn f() -> ..) refused parameter_unlowered.

Fixed in 6d6b66f: an empty capture has no slots; any other unread capture still refuses. Locally all 9 claims pass, and parameter_slot_refusal still holds (2/2). The census I had started measured the broken head, so its results are void; it is re-running on 6d6b66f.

— sent from sharp-carp-336

[gunbai-bot]

Census on the fixed head, from completed waves only. Setup: reference_conservation_stratified_sample_paths, 316 paths; base fbdfd65, head 6d6b66f (the merge 5069baf adds main only). One gunbc process per path, with a child cgroup memory.max per batch.

• Pairing: all 316 paths paired.
• Verdicts: 0 refusal changes.
• Atoms: 0 recovered, 0 newly absent. Totals are identical (authored 29403, conserved 16632, dropped 2137).

Why the zero is readable: every parameter, field, named-argument label, let key, type parameter and projection member in the sample now goes through the name reader rather than the operand fallback. Main shows the same conservation, so the name reader reads every real binder exactly as before. The slot refusal fires only on supplied input, which parameter_slot_refusal pins.

Local run on the merge: parameter_slot_refusal 2/2, statement_let_bind plus parse_test_fn_decl_return_clause 9/9 (the claims the empty-list regression broke), reify_operand_refusal 4/4 (after #12779), else_arm_nested_if 5/5, wildcard 9/9.

— sent from sharp-carp-336

[briansrls]

APPROVE-MERGE at exact head 5069baf.

No findings. The binder route is repaired at the earliest wrong link: binder positions are read as names through value-preserving shells and no longer consult OperandRefRead. The parameter walk is now slot-preserving and fail-closed: every non-empty slot is read or refuses with body_lowering_reason_parameter_unlowered, and that Outcome propagates through the shared domain/binder view to both fn-declaration lowering routes. The empty-parameter-list regression from the intermediate head is fixed by treating the empty capture as zero slots; exact-head floor and the disclosed sibling controls pass. The 316/316 paired census is neutral, as expected for real grammar-produced binders.

Merge queue only. All applicable exact-head checks and the actual merge_group candidate must pass against then-current main; no direct merge and no check bypass.