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

dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag

@@ -14,7 +14,7 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode {
     "RUNG FOUND AT: mitigated on the operator route; below the floor on the value route (the cast's type was dropped, so `x as Q` was Accepted with `Q` declared nowhere). CEILING: structurally guaranteed -- a cast lowers to a value carrying its operand and its target type, or refuses.",
     "RUNG NOW: mitigated on EVERY route. `v2.compiler.body_lowering_fold` `body_lower_postfix_expr` refuses a postfix chain carrying an as-suffix with `body_lowering_reason_type_annotation_not_carried` located at the authored target type -- the one reason for a type the lowering cannot carry, shared with the let annotation -- and `body_lower_arm_operand_resolved_optional` declines a cast so a let value or an arm reaches that refusal instead of answering the operand. A declared target refuses too: nothing is carried, so nothing is accepted. As an operator operand the cast now refuses with the same reason, because the postfix is folded before the operator reader sees it. CENSUS: the v2-route identity census over the 321-path population (`v2.compiler.reference_conservation_census` `reference_conservation_stratified_sample_paths` plus six) re-derived by `reference_conservation_census_for_paths` over each arm (pair 620ecb0a50f / 4c9f8d326d3): the modules that newly refuse are data rows casting a literal to a refinement and fn bodies casting to String, each refusing whole, and each returns when the trigger below lands.",
     "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY (the one the refusal above was retired by): a TYPED CAST NODE -- `e as T` lowers to Transform[coerce, e] with `v2.std.type_binder` `<cast-target>` -> T beside its positional children, and that node is SUFFICIENT FOR: resolve binding T in type role through the shared type-role frame (an undeclared T refusing at T); infer admitting the crossing through `v2.std.coercion` (not `std.coercion` `dag_cast_rules`, which is v1's side of `coercion_two_algebras_answer_one_question_stall`) or refusing typed; and translate and eval realizing it or refusing typed -- on every route, for every cast the refusal now stops.",
-    "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's <T> over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its carrier (`x as Int` from `x: Pos`) REFUSES, loud and typed at the operand, until `v2.std.coercion` admits a refinement-to-declared-carrier crossing as Widened from the type declaration (its existing widening fold needs per-domain integer value sets); it previously admitted only because an unscoped parameter walk bound x to an unrelated `fn positive(x: Int)`. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.",
+    "RUNG NOW, AFTER THE TRIGGER: structurally guaranteed on the lowering and resolve routes -- the postfix chain read carries a cast as a step (`v2.compiler.body_lowering_fold` `PostfixCast`) and the chain fold builds `body_lower_cast_node`, so no reader answers `x as T` with `x`; a target type the lowering cannot read refuses `body_lowering_reason_type_annotation_not_carried` at it; `v2.compiler.resolve` `resolve_type_role_target` binds T in the type-role frame (`ResolveContext` `type_scope`, which carries a fn's <T> over its whole Arrow and never a value binder) and an undeclared T refuses unbound at T. Infer (`v2.compiler.infer` `infer_transform_cast_optional`) admits a crossing only when `v2.std.coercion` `coercion_cast_crossing` finds an exact structural witness from the operand's derived type to T, and refuses with coercion's typed mismatch otherwise; an operand whose type is not derived leaves the cast on the counted frontier. Translate projects the cast as a one-operand primitive apply of the coercion `CanonicalOperation` (`CoercionCrossing`) and the rust and typescript extdeps realize it `OperandUnchanged`, as v1's emitter spells a representation-preserving crossing; the v2 evaluator realizes it as the operand's value. RESIDUE, STATED ON THE RUNG: a cast INTO a refinement (`lit as NonEmptyStr` for a string literal `lit`, `NonEmptyStr = String where non_empty`) is not an exact structural crossing, so on the infer path it REFUSES, loud and typed (coercion's NoTargetCandidate, located at the operand), wherever the operand's type is derived . The identity cast `x as Pos` from `x: Pos` is ADMITTED: infer binds a parameter by its enclosing Arrow (`v2.compiler.infer` `infer_parameter_type_in_scope`), so x grounds as the Pos declaration-reference and the crossing is exact. A cast from a refinement-typed value to its DECLARED carrier (`x as Int` from `x: Pos`, `type Pos = Int where positive`) is ADMITTED as Widened: `v2.compiler.infer` `refinement_declaration` reads the carrier from the declaration the reference's path reaches, and `v2.std.coercion` `coercion_cast_crossing` composes that carrier edge with the same exact-structural find_witness -- no preservation rule is added and no predicate is evaluated. Only the DECLARED carrier widens, one step: `x as Bool` from x: Pos and `x as Neg` between two refinements of Int REFUSE at the operand; for a refinement of a refinement (`type Pos2 = Pos where ..`) `x as Pos` is Widened and `x as Int` REFUSES (the carrier edge is not walked). The declaration is read through `v2.std.symbol_index` `symbol_index_lookup` on `v2.compiler.resolve` `ResolvedTree` `resolved_declarations` (gunbc#12629: declarations with resolved bodies, so a carrier is the identity resolve bound), and a lookup miss refuses (`bcn_a_refinement_lookup_miss_refuses`). Residue on that arm: the lowered cast's operator names `CoercionCrossing` by the exact rule (`v2.std.compilers.target_model` `canonical_operation_op_coerce`), fixed at lowering, so a Widened crossing is realized under that identity; both are representation-preserving (`OperandUnchanged`), so no emitted program differs. The 44 data-row census modules casting a literal into `NonEmptyStr` are therefore measured Accepted through RESOLVE ONLY (the census instrument's reach), not end to end. NEXT-RUNG TRIGGER FOR THAT PATH, NAMING THE CAPABILITY: v2.std.coercion deciding a refinement's predicate on the cast operand (a literal first), so a crossing into a refinement is admitted exactly when the predicate holds and refused located when it does not.",
   ],
 
   evidence: [
@@ -36,7 +36,11 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode {
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_loop_passes_the_resolver_gate", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_foreign_label_on_a_transform_refuses", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_into_a_refinement_refuses_at_infer", field: WholeDeclaration },
-    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_refuses_until_carrier_widening", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_its_declared_carrier_widens", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_out_of_a_refinement_to_a_non_carrier_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_between_sibling_refinements_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_a_refinement_lookup_miss_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_refinement_of_a_refinement_widens_one_step", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_identity_cast_into_a_refinement_admits", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "an_as_cast_operand_resolves", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "a_parenthesised_call_operand_resolves", field: WholeDeclaration },