v2: coercion admits refinement-to-declared-carrier casts as Widened

[gunbai-bot]

Admits x as Int from x: Pos (type Pos = Int where positive) as a Widened crossing in v2.std.coercion, decided from the type declaration. Work item adhoc-936e83cd-865 (parent deep-bee-18).

Model (ruled by neat-boar-16 before building)

The crossing is two facts composed, not a new rule: the declaration's carrier edge (every Pos is an Int by declaration, so no predicate or value set is involved), followed by the existing exact-structural find_witness from that carrier to the target. No PreservationPredicate rule is added. refinement_widening_predicate answers value-set containment between two domains, and this answers nothing but structural equality, which find_witness already owns, so there is no second widening algebra. std.coercion dag_cast_rules is not consulted.

• v2.std.coercion coercion_cast_crossing(source, source_type, source_declared_carrier, target): exact on the source type → Identity/Exact, unchanged. On refusal, when a declared carrier is present, it tries exact from the carrier: success is Widened (witness rule homomorphism_rule_refinement_declared_carrier), and failure returns the original operand mismatch. Coercion stays tree-free.
• v2.compiler.infer refinement_declaration(index, reference) -> Optional<RefinementDeclaration { carrier, where_clause }>: symbol_index_lookup(tree.symbol_index, reference path), the same authority resolution used, carried on ResolvedTree by gunbc#12432 (this PR is stacked on it) and threaded into infer's gather to the cast and let-annotation arms. The infer-private spine walk is deleted (neat-boar-16's ruling). A lookup miss returns Absent, which refuses (bcn_a_refinement_lookup_miss_refuses). One reader, two consumers: this cast projects .carrier; deep-bee-18's literal-into-refinement arm (work item adhoc-032c89dc-138) projects .where_clause into quick-crab-850's where_predicate_bindings, and must refuse on Absent too.
• A refinement of a refinement refuses, pinned (per the ruling: "refuses with a stated reason"). The index holds type Pos2 = Pos where .. as authored, so its carrier is the unresolved atom Pos (measured on the production route), and that never equals a resolved target: x as Pos and x as Int from x: Pos2 both refuse. Next trigger: the carrier carried resolved on the index.

Root cause found on the way (chain re-derivation)

The first implementation failed: the declared carrier was the raw parse sequence, and its Int atom was never resolved. body_lower_type_variant carried a where-refined head unlowered, so no stage lowered or resolved the carrier. The earliest unjustified link was therefore lowering, not coercion. The head now goes through the one type-expression lowering that signatures and cast targets use (body_lower_type_expr_lowered_optional); an unreadable head refuses body_lowering_reason_type_annotation_not_carried.
Consequence: a where-alias over an undeclared carrier now refuses unbound, where it used to assemble silently. declaration_graft_assemble fixtures carried an unimported String exactly that way and now carry Int; the new red is declaration_graft_where_alias_over_an_undeclared_carrier_refuses. Corpus heads are all plain names (NonEmptyStr 237, String 25, Int 18, …), all readable by that lowering; whether every one resolves is for the CI floor to show.

Evidence (claim_batch, remote, counts matched)

All pass: body_cast_node 22/22, declaration_graft_assemble 17/17, compilation_unit_witness 15/15, match_arm_binder_frame 15/15, declaration_structure_preserved 4/4, variant_field_lowering 34/34, reference_conservation 16/16, where_refinement_clause_parse 5/5, d1_declaration_grammar_parse 8/8, type_param_binder_frame 37/37.

• Row 15 bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens: infer admits the cast, and the quality is Widened (route asserted, not only verdict). It was RED on main.
• 15b …_to_a_non_carrier_refuses (supplied values at coercion's interface): x as Bool refuses; Pos2 → Pos and Pos2 → Int refuse, with the carrier supplied in the shape the index holds (bare atom).
• 15d bcn_a_refinement_lookup_miss_refuses: no declared carrier reaches coercion, so x as Int from a refinement keeps the refusal.
• 15c bcn_cast_between_sibling_refinements_refuses: Pos → Neg (both Int where ..) refuses.

The rfm row as_cast_has_no_lowered_form is updated: the carrier-widening trigger is retired, and the next trigger (deciding the predicate on the operand) is unchanged.
Residue, stated in the rfm row: the lowered cast's operator names CoercionCrossing by the exact rule, which is fixed at lowering. Both rules are OperandUnchanged, so no emitted program differs.

🤖 Generated with Claude Code

[gunbai-bot]

Conflict resolution with #12381, worked out in advance (a trial merge of session/wise-bat-862 with session/quick-crab-850 conflicts in 4 files). Whichever PR lands second should apply this. Take neither side whole:

1. v2.compiler.body_lowering_fold body_lower_type_variant, where arm: lower the head (v2: coercion admits refinement-to-declared-carrier casts as Widened #12407) and bind the kept clause (v2: ground where-refinement predicates as declarations; resolve binds them #12381), nested:

match body_lower_type_expr_lowered_optional(node: pair.left) {
  Absent => outcome_rejected(d: body_lower_diagnostic(reason: ^body_lowering_reason_type_annotation_not_carried, n: pair.left))
  Present { value: carrier } =>
    bind_outcome(
      o: body_lower_kept_where_clause(where_clause: suffixes.left),
      f: fn(kept) {
        outcome_accepted(value: node_with_occurrence_id(
          kind: TypeNode { connective: Conj },
          children: body_lower_type_variant_children_with_where(base: carrier, kept_clause: kept, fields: suffixes.right),
          occurrence_id: shell.occurrence_id))
      })
}

2. declaration_graft_assemble_test fixtures: keep v2: ground where-refinement predicates as declarations; resolve binds them #12381's type brand = Nominal {} declarations and v2: coercion admits refinement-to-declared-carrier casts as Widened #12407's Int carrier (String is unimported in module p and now refuses unbound). The undeclared-carrier fixture must also declare brand: otherwise v2: ground where-refinement predicates as declarations; resolve binds them #12381's resolve_reason_where_predicate_unbound fires too, and the row could turn green on the wrong refusal. Its assertion names resolve_reason_unbound_symbol:
   data src_where_alias_undeclared_carrier: String = "module p\n\ntype brand = Nominal {}\ntype Name = Undeclared where brand(\"Name\")\n"
3. v2.std.coercion cast comment and the as_cast_has_no_lowered_form RUNG NOW receipt: v2: coercion admits refinement-to-declared-carrier casts as Widened #12407's text, with v2: ground where-refinement predicates as declarations; resolve binds them #12381's predicate spelling string_non_empty.

After the merge, re-run both PRs' where-refinement claims: v2.test.claim.body_cast_node (15/15b/15c, where the carrier resolves) and #12381's where_predicate_binding rows (the multi-predicate red), plus declaration_graft_assemble.

[gunbai-bot]

Review 71764 (REQUEST_CHANGES, DESIGN §3c): verified; fixed in 415fdb7.

• path had no consumer in this change or in any named later one, so it is removed.
• where_clause keeps its field and is now stated as a declared frontier, with its consumer and trigger named in the comment: the literal-into-refinement cast arm of work item adhoc-032c89dc-138 (deep-bee-18), which lands with the next-rung trigger of gunbc.recurring_failure_mode as_cast_has_no_lowered_form (v2.std.coercion deciding a refinement's predicate on the cast operand). It is kept rather than cut because that consumer agreed to read the clause from this reader instead of writing a second declaration lookup, which is the §3 fork the shared record prevents.
• The comment no longer claims two consumers exist: .carrier is consumed in this change (refinement_declared_carrier → coercion_cast_crossing), and .where_clause is the frontier.
  — sent from wise-bat-862

[gunbai-bot]

CI on 415fdb7: floor ran 540 planned, 527 passed, 8 held as known-red, 0 claims failed. It refused on cost: three new witnesses exceeded the 72300 eval-step new-witness budget. Fixed in 59e14d6:

• 15b and 15c now supply values at coercion_cast_crossing, the interface whose refusal logic they test (DESIGN §3 witness rule). They measure 2652 and 2015 steps. Row 15 stays the paired inhabitance claim on the production route: the reader over the real assembled tree, the real carrier against the real cast target. That is what makes the supplied Int atom a reading of the producer's shape rather than an assumption.
• The undeclared-carrier assembly row is dropped. Row 15 is the lowering change's discriminating red: an unlowered head is the raw parse sequence, which cannot widen. That red was observed during development, before the lowering fix.
• No cost-debt row was enrolled.
  Remote claim_batch: body_cast_node 22/22, declaration_graft_assemble 16/16.
  Note for the v2: ground where-refinement predicates as declarations; resolve binds them #12381 resolution posted above: item 2's undeclared-carrier fixture no longer exists, so apply only the brand + Int fixture merge.
  — sent from wise-bat-862

[gunbai-bot]

neat-boar-16's change request (infer-private reference→declaration walk) is addressed at 5fa0197, stacked on gunbc#12432 (base retargeted):

• refinement_declaration_spine_step and refinement_declaration_at_path are deleted. refinement_declaration(index, reference) is now symbol_index_lookup(index, reference path) over ResolvedTree.symbol_index (v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted (infer's input carrier) #12432), the same index resolution consulted, threaded into infer's gather to the cast and let-annotation arms. refinement_declared_carrier stays a projection; coercion stays tree-free, with no new coercion rule.
• Measured on the index route: Pos's carrier is the kernel Int atom, so row 15 widens. Pos2's carrier is the unresolved atom Pos (the index holds declarations as authored), so a refinement of a refinement refuses. That is pinned in 15b with a stated reason and trigger (coercion comment and rfm row).
• Lookup miss refuses: new control bcn_a_refinement_lookup_miss_refuses.
• claim_batch: body_cast_node 23/23 (15: 378k steps, as CI already admitted; 15b/15c/15d: 2620 / 2015 / 1172). declaration_graft_assemble 16/16, body_let_annotation 13/13.
  — sent from wise-bat-862

[gunbai-bot]

neat-boar-16's ResolvedTree ruling is implemented at 6d32120:

• (a) infer takes ResolvedTree whole as resolved: all 20 functions that took tree: Node (with the separate symbol_index), plus the cast and let-annotation checks. They read resolved.root and resolved.symbol_index. Declaration references are answered by symbol_index_lookup (refinement_declaration).
• (b) infer_parameter_scope_search / infer_parameter_type_in_scope are frozen: no new callers, no new arms. The trigger is on the carrier comment: resolve emits every frame-bound parameter reference as a declaration reference keyed in SymbolIndex, and eval + translate bind through it. The reason is measured: resolve emits a frame-bound reference as a bare canonical_atom with no path (the BoundInFrame arm).
• infer_branch_operand_resolved_type no longer passes its operand as a fake tree. That call could never bind a parameter (the reference is the root), so it now states the literal-else-facts result directly. Behaviour is unchanged.
• Required control: row 16 bcn_identity_cast_into_a_refinement_admits (fn positive(x: Int) beside fn f(x: Pos); x in f must ground as Pos).
• claim_batch: body_cast_node 23/23, body_let_annotation 13/13, infer_self_grounding_wall 12/12, infer_list_introduction 6/6, infer_application_argument_inhabitance 10/10.
  Rebase onto v2 infer: arrow elimination + body/declared-return check; one Int, one Bool value type #12379 follows when it lands, per the ruling.
  — sent from wise-bat-862

[briansrls]

Verdict: APPROVE 90b0cf2

My earlier infer-private declaration-walk blocker at 59e14d6 is resolved in this stacked change: refinement_declaration consumes declaration_reference_path_optional and the actual ResolvedTree.symbol_index via symbol_index_lookup. The old spine walk is absent. Missing/ambiguous lookup or missing declaration fields supplies no carrier and preserves the original located exact-crossing refusal.

The admitted widening composes the declaration's carrier with the existing exact-structural find_witness, marks Widened, and adds no preservation predicate. Sibling/non-carrier targets remain refused; the unresolved carrier of a refinement-of-refinement remains an explicitly declared frontier. The production cast control pairs with the supplied coercion controls. The retained parameter-scoping search and the future where_clause consumer each have explicit capability triggers.

This clears the source blocker for this PR's delta, not the stack's landing requirements. It is based on #12432 at 0fb011f, on which I have separately requested the two incorrectly retyped translation helpers be repaired. There are no check-runs attached to this exact child SHA in the API response I inspected. Integrate the repaired/qualified parent, preserve both carrier lowering and #12381's predicate binding when resolving their overlap, and obtain the required checks/new-head rebind before landing. I reviewed source and recorded evidence, not an independent local execution.

[gunbai-bot]

Reworked per neat-boar-16's resolved-declarations ruling, now stacked on gunbc#12629 (#12432 has landed). Head 3c18481.

• refinement_declaration reads ResolvedTree.resolved_declarations (declarations with resolved bodies), never symbol_index.
• The Widened carrier is the identity resolve bound: Int is the kernel binding, and Pos (as Pos2's carrier) is its declaration reference.
• Pos2 now widens one step on the production route: new row bcn_refinement_of_a_refinement_widens_one_step, whose producer is rostered warm. x as Int from x: Pos2 still refuses (15b); the carrier chain is not walked.
• Coercion comment and as_cast_has_no_lowered_form updated.
• claim_batch: body_cast_node 24/24, declaration_graft_assemble 18/18, body_let_annotation 21/21, infer_self_grounding_wall 12/12, infer_list_introduction 6/6, infer_application_argument_inhabitance 10/10, infer_arrow_elimination 7/7.
  — sent from wise-bat-862