v2: a parameter's type may carry a where refinement; it parses and the fn refuses at the clause until a carrier exists

[gunbai-bot]

XL-2, per quiet-seal-543's ruling on class H: v2 parse refusals, one class per PR, with v1 as the reference.

The defect

gunbc.auth.optional_impersonation writes lifetime_seconds: Int where range(min: 1, max: 3600) = 3600 and refused at range. v2's typed parameter was name : type_expr, with no refinement. v1 02_parse parse_param reads a where clause on a parameter type.

Lowering does NOT read a where clause on a parameter type, so this is not grammar-only

The one where-clause reader, v2.compiler.body_lowering_fold body_lower_kept_where_clause, serves a type variant. A parameter's type is read by body_lower_type_expr_lowered_optional, whose sequence fallback keeps the base type and drops the clause. So per the ruling: the grammar admits it, and lowering refuses, typed and located.

The change

• Grammar (dag_grammar_typed_param_expr): a choice whose first arm is name : type_expr where_refinement_clause, with the clause required, so it is taken only where a refinement is written. An unrefined parameter falls to the second arm, the original name : type_expr, so every existing parameter keeps an identical parse tree.
• Lowering: body_lower_param_refinement_refusal_optional refuses the fn, located at the where_refinement_clause, with the new reason body_lowering_reason_parameter_refinement_unmodeled. It searches only inside the declaration's own param_list, and is asked before anything is read on both arms through body_lower_first_signature_refusal_optional (after the pattern-form wall, before the uses check), so the sequence fallback is never reached.
• Ownership: a new unique FatalGrain row in v2.workflow.compile_door_cause_ownership known_frontier_causes.
• Failure mode: new gunbc.recurring_failure_mode parameter_refinement_has_no_carrier. Rung: mitigated. Ceiling: structurally impossible. Trigger, naming the capability: a parameter's lowered type carries its where-clause refinement, read through the one where-clause reader type variants use rather than a second one.

Controls (v2.test.claim.parse.parameter_refinement, nullary values enrolled warm by module family)

• a_refined_parameter_parses_holds. Red on main.
• a_refined_parameter_refuses_at_its_clause_holds: the reason, with the NodeLocus anchor being the where_refinement_clause shell. Red on main.
• an_unrefined_parameter_still_normalizes_holds: passes on main and on this branch.

Evidence (claim_batch, 30 GB BuildBuddy runner)

• Main with only the test added: both new claims FAIL.
• This branch: 3/3 PASS. Also passing: compile_door_ledger_ownership, native_frontier_ratchet (29), parse_test_fn_decl_return_clause (15), uses_clause, reference_conservation.
• Neighbour control: the parse-tree content hashes of 10 forms are identical on main 96744f2f8be and this branch's merged head 011b8bad622, both built from the same main. The 10 forms are a module with typed-parameter fns, a record, record literals, named and positional calls, ==, let / annotated let / let..in, field access and match.

Effect on the corpus file

gunbc.auth.optional_impersonation:7 also writes a parameter default (= 3600), class G, which lands next. With this PR it parses past the refinement and stops at the default. Once G lands it parses, and the fn refuses at the refinement.

Land only via the merge queue.

🤖 Generated with Claude Code

[briansrls]

APPROVE-MERGE at exact GitHub head 3e82cf4c4c29d55186f95fde63623105fc06ce6a.

The SHA supplied in the request (3e82cf424d73b11d8a497c0dd2a0d6b17ab4adae) does not exist in this repository; this review is deliberately anchored to the PR's actual current head above.

No findings. v1 parse_param reads the base type and then try_where_clause, so the source form is authoritative. The v2 grammar's refined arm requires an actual where_refinement_clause, while the original unrefined arm remains intact. Lowering checks the declaration's own parameter list before either full or census Arrow reading, and rejects at the clause with body_lowering_reason_parameter_refinement_unmodeled, preventing the type-expression sequence fallback from silently retaining only the base type. The new fatal cause has one ownership row, and the RFM's retirement trigger names one shared refinement reader rather than a second representation.

The controls discriminate parse admission, exact located refusal, and unchanged unrefined normalization. Exact-head floor, generated, emit-build, and witnesses all pass.

Merge-queue landing only: the actual merge_group candidate must pass against then-current main; no direct merge or check bypass.