v2: typed cast node (Transform[coerce, e] + <cast-target>) retires the as-cast refusal

[gunbai-bot]

Contains #12308 (the as-cast refusal) and the quick-dove-780-shared-marker-rule commit (v2.std.node PositionalPlusOneNamedEdges + v2.std.type_binder <cast-target>). Until #12308 lands, the diff against main includes both.

What

e as T lowers to the typed cast node, Transform[coerce, e] plus the unauthorable <cast-target> edge to T. That node is carried through lowering, resolve, infer, translate and eval. This is the restoration trigger of gunbc.recurring_failure_mode as_cast_has_no_lowered_form, and it retires #12308's refusal.

• Lowering (v2.compiler.body_lowering_fold):
  • A cast is a step of the postfix chain (PostfixCast), so a.b as T, (x as T).f, x as A as B and g(v: x) as T fold as one chain. body_lower_cast_node builds the node.
  • A chain that carries a cast never declines. Declining is how the cast was dropped: the arms behind the door read only the head. Measured before this change: g(v: x) as Int was accepted with no cast node.
  • A target type the lowering can't read refuses type_annotation_not_carried at that type.
• Resolve (v2.compiler.resolve). This PR builds the type-role frame, per the parent ruling, and lively-newt-275 rebases their let-annotation carrier onto it.
  • ResolveContext gains type_scope, which carries a fn's <T> over the whole Arrow and never a value binder.
  • resolve_type_role_target is the one type-role entry. An undeclared T refuses unbound at T.
  • T in a value position now refuses resolve_reason_type_parameter_in_value_position instead of unbound_symbol, as neat-boar-16 ruled. The no-shadowing refusal is kept, and an Arrow's own binders are checked from the outer context.
• Infer (v2.compiler.infer infer_transform_cast_optional):
  • A crossing is admitted only when v2.std.coercion coercion_cast_crossing finds an exact structural witness from the operand's derived type to T. That is coercion's own procedure over the singleton {T} with UniqueOnly.
  • Any other crossing refuses with coercion's typed mismatch. An operand whose type isn't derived leaves the cast on the counted frontier.
  • std.coercion dag_cast_rules is not consulted (coercion_two_algebras_answer_one_question_stall; its join is untouched).
• Target model (v2.std.compilers.target_model):
  • New CanonicalOperation variant CoercionCrossing { homomorphism_rule }, grounded by v2.std.coercion's rule symbol. It is a Symbol because coercion imports target_model. The wire, equality, decode and roster sites are all updated.
  • The dag canonicalization maps kw_as to it.
  • New TargetOperatorShape variant OperandUnchanged: how v1's emit_typed_cast_shared spells a representation-preserving crossing, not Rust as. Rust and TypeScript each get a realization row.
  • Translate projects a cast as a one-operand primitive apply.
• Eval: the v2 evaluator realizes the coercion as its operand's value, and any other arity refuses.
• Reader census (brief item 3): named-edge fixes in application_positional_targets (the cast target is passed over; any other named edge still refuses), body_lower_reify_transform_edge, and the complexity lens's port and combiner readers.
  • Eval needed no change. eval_edge_is_runtime_argument admits only positional edges.
  • I measured the fold with an atom target and with an Arrow target. Neither is refused when folding the named type node, so the eval edits I had made were reverted.

Census (brief item 5)

Instrument: v2.compiler.reference_conservation_census reference_conservation_census_for_paths, which measures through resolve. Each arm ran from its own worktree, batched 8 paths per process, with the same interpreter binary. Batches whose process died were re-run until every readable path was measured.

The 68 of #12308, before 620ecb0a50f vs this branch at ac97ef3711a:

• 67 are back to refused=0. Conserved went up on 58 and was equal on 9, with no decreases. Cast targets now reach the collector.
• dag/extdeps/uri.dag refuses at this head, but not because of this change. It refuses body_lowering_reason_call_argument_unread at the lambda cp => uri_percent_encode_scalar_outcome(cp: cp). Current main (a1d5db9518a) refuses that lambda identically, with or without a cast in the body; I checked the same shape on the pilot route on both trees. That is lambda_has_no_lowered_function_value_form, which landed on main after 620ecb0a50f: base drift, not a regression here.
• docker/hub.dag and tools/id.dag have conserved=0 in both arms, so v2 body lowering: an as-cast's target type refuses (type_annotation_not_carried, at T) instead of being dropped #12308's "each had conserved>0" was imprecise for those two.

"Nothing new may refuse": the 315 reference_conservation_stratified_sample_paths, main a1d5db9518a vs this branch at dfeb1228274 (which contains that main):

• 309 are measured in both arms. Newly refused: none.
• Newly accepted: 3, all of them v2 body lowering: an as-cast's target type refuses (type_annotation_not_carried, at T) instead of being dropped #12308's cast specimens: dag/gunbc/host/host_resource.dag, dag/test/claim/data_reference_kind_from_resolved_node_witness_test.dag, dag/test/claim/extdeps/apt_package_of_witness_test.dag.
• Refusing: 42 on main, 39 here. Conserved went up on 60 and down on 0. No unmeasured value changed.
• The other 6 paths are dag/gunbc/namespace/transition_admission/* files that no longer exist in either tree.

Controls

v2.test.claim.body_cast_node replaces body_cast_target_refusal and has 17 claims, all green locally:

• A declared T is carried on tail, let value, call argument, if arm, match arm and call operand.
• An undeclared Q refuses at Q.
• In a generic fn, T binds <T>, and a value binder never answers for a type.
• Infer admits Int to Int and refuses Int to Bool. The Bool cast was admitted before the infer rule.
• Rust emits the operand. The mutant that drops the cast target is refused (transform_shape_invalid).
• Eval yields the operand's value, and 8 differs from 7.
• The named edge's position doesn't move the content hash.
• The residue below is asserted: 1 as Pos refuses at infer with coercion's NoTargetCandidate, located at the operand, and x as Int from Pos is admitted.
• an_as_cast_operand_resolves flips the cav row.

Residue, stated

A cast into a refinement ("lit" as NonEmptyStr, where NonEmptyStr = String where non_empty) is not structural equality, so it refuses at infer wherever the operand's type is derived. This was measured on a fixture type Pos = Int where positive: 1 as Pos refuses and x as Int from Pos is admitted. No route runs infer over the census modules today, so the census verdict is unaffected, but the 44 data-row modules would re-refuse at infer. So the census measures those 44 modules through resolve only; they are not Accepted end to end. The rung is stated on as_cast_has_no_lowered_form. Its next-rung trigger names the capability: v2.std.coercion deciding a refinement's predicate on the cast operand, literal first. That follow-up is filed as work item node://adhoc-032c89dc-138. Note: this PR had already left draft when the parent's conditions arrived, so the item was filed after the flip, not before.

🤖 Generated with Claude Code

[gunbai-bot]

Review 71387: confirmed. The five btar_* rows were a merge artifact from #12308's branch, which added rows main already had. The second copy is removed, and the roster now has no duplicate identities (checked with sort | uniq -d). Fixed in adb6dd3.

[gunbai-bot]

Review 71396: agreed and fixed. Bind is back to PositionalEdges with exactly 3 children in both behavior_edges_conform and behavior_edge_discipline, so the shape check no longer admits a named edge that nothing produces and type_binder_labels_conform refuses. PositionalPlusOneNamedEdges now applies to Transform only, where cast_target_edge is its producer. The let-annotation carrier widens Bind in the same change that lands its producer; the comments in v2.std.node and v2.std.type_binder now say so.

The same push fixes the floor cost refusal. Four body_cast_node claims were over the new-witness step budget, so their emit and infer outcomes are now nullary producers enrolled in floor_pure_producer_share. It also merges main, resolving the conflicts in type_binder and in body_lowering_fold's import. The 17 claims are green locally on the merged tree. Fixed in 444a4f7.

[gunbai-bot]

Review 71406: the finding stands and is fixed in ab4480a. The mechanism turned out to be different from the one proposed. Measured on the pilot route:

• x as Bool with x: Pos refuses at infer with NoTargetCandidate, so a Pos parameter's type IS derived. x as Int was therefore judged by coercion_cast_crossing, not passed over on the frontier.
• It is admitted because infer grounds a refinement-typed value as its carrier: the derived type is structurally Int.
• The consequence the row missed: x as Pos with x: Pos refuses. Every cast whose target names a refinement refuses, identity included.

Changes:

• The coercion_cast_crossing comment and the as_cast_has_no_lowered_form row now say exactly this, instead of "into or out of refuses" in one place and "out of is admitted" in the other.
• bcn_cast_out_of_a_refinement_admits now asserts the route through its partner: the same operand cast to Bool must refuse with coercion's mismatch.
• New bcn_identity_cast_into_a_refinement_refuses_at_infer pins the sharpest form of the residue.

The follow-up work item (refinement predicates in v2.std.coercion) owns flipping it. All 18 claims are green locally.

[gunbai-bot]

Blocking finding from neat-boar-16 (side chat): confirmed and fixed in 6366e59. type_binder_node_conforms sent every computation node through computation_named_labels_conform, which refuses any named edge on a behavior with no type-binder marker. A Loop's required bound edge and optional carrier edge (owned by v2.std.node loop_behavior_edges_conform) therefore failed the resolver's well_formed && type_binder_labels_conform gate. The label rule now applies to Transform only; every other behavior's named edges belong to its own edge discipline, as they did before this PR.

New controls in v2.test.claim.body_cast_node:

• bcn_a_loop_passes_the_resolver_gate runs the resolver's gate predicate over the real producer's Loop (v2.test.claim.fold_lowering lowered_fixture_loop: a parsed fold desugared by the real fold lowering). It was red at 4f4b67e and is green now.
• bcn_a_foreign_label_on_a_transform_refuses keeps the wrong-Transform-label refusal.

lowered_fixture_loop is enrolled as a shared producer. All 20 claims are green locally. The census was unaffected: its fold loops refuse at lowering, on the lambda step argument, before this gate.