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

dag/gunbc/recurring_failure_mode/as_cast_has_no_lowered_form.dag

@@ -11,11 +11,34 @@ data as_cast_has_no_lowered_form: RecurringFailureMode = RecurringFailureMode {
     "no lowered form for an `as` cast `e as T` in v2 body lowering: `as` is not an operator of the precedence tower `v2.compiler.body_lowering_fold` `body_lower_read_operator_expression` reads, and no other reader lowers the cast. As an operator operand -- usually parenthesised, `(e as T) == ..` -- it refuses as `body_lowering_reason_operator_operand_unread`; on the value route the target type `T` does not reach the reference-site collector.",
     "SPECIMENS AND PINNED LOCUS: `dag/test/claim/extdeps/apt_package_of_witness_test.dag` `apt_installed_bin_path_is_apt_bin_dir_plus_the_binary_name` (`(apt_installed_bin_path(..) as String) == ..`), `dag/gunbc/host/host_resource.dag` (`(left.host as T)`), `dag/test/claim/data_reference_kind_from_resolved_node_witness_test.dag` (`(gigabyte.legal_name as T)`); each refuses at the parenthesised operand. A parenthesised CALL operand without a cast is read (control: `a_parenthesised_call_operand_resolves`), so the group is not the cause.",
     "EXPOSED, NOT INTRODUCED: the parent of gunbc#12145 (2de78893dfe) accepted this shape only by SILENT NARROWING -- the operand reader answered a sequence with its left element -- so the refusal on main after gunbc#12173 is a pre-existing defect made visible, not a new regression. Found by the XL-2 three-baseline identity census on gunbc#12194 (321 paths: 18 refusing at 2de78893dfe, 167 at ada85b9452, 101 after gunbc#12173).",
-    "RUNG FOUND AT: mitigated on the operator route; below the floor on the value route (the cast's type is dropped). CEILING: structurally guaranteed -- a cast lowers to a value carrying its operand and its target type, or refuses. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: v2 body lowering has a lowered form for `e as T` on every route, whose operand and target type both reach the reference-site collector.",
+    "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 -- including the identity cast `x as Pos` from `x: Pos`, because infer grounds a refinement-typed value as its carrier and no carrier is structurally the refinement. A cast from a refinement-typed value to its carrier (`x as Int` from `x: Pos`) is admitted by that same judged crossing, carrier to carrier, not left on the frontier. 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: [
-    DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "an_as_cast_operand_refuses_at_normalize", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_tail_cast_carries_its_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_let_value_cast_carries_its_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_call_argument_cast_carries_its_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_if_arm_cast_carries_its_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_match_arm_cast_carries_its_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_call_operand_cast_carries_its_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_undeclared_target_refuses_at_q", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_generic_target_binds_the_type_parameter", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_value_binder_does_not_answer_the_target", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_infer_admits_int_to_int", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_infer_refuses_int_to_bool", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_rust_realizes_the_cast_as_its_operand", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_without_its_target_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_eval_realizes_the_operand_value", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_cast_target_order_does_not_move_the_hash", field: WholeDeclaration },
+    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_admits", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.body_cast_node", decl_name: "bcn_identity_cast_into_a_refinement_refuses_at_infer", 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 },
     DeclarationRef { module_path: "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal", decl_name: "an_undeclared_name_in_a_parenthesised_call_operand_refuses_at_resolve_at_its_atom", field: WholeDeclaration },
   ],

dag/gunbc/recurring_failure_mode/behavior_named_edge_label_validated_not_constructed.dag

@@ -0,0 +1,20 @@
+module gunbc.recurring_failure_mode.behavior_named_edge_label_validated_not_constructed
+
+import std.types { NonEmptyStr }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data behavior_named_edge_label_validated_not_constructed: RecurringFailureMode = RecurringFailureMode {
+  identity: "behavior_named_edge_label_validated_not_constructed" as NonEmptyStr,
+
+  receipts: [
+    "INVALID STATE: a behavior node carrying a Named edge whose label is not the marker that behavior admits -- a Transform with a Named edge other than `v2.std.type_binder` `<cast-target>`, or (once the let-annotation carrier lands) a Bind with a Named edge other than its annotation marker. `v2.std.node` states only the SHAPE (`PositionalPlusOneNamedEdges`: at most one Named edge beside the positional children) and cannot intern the marker lexemes, so the LABEL is checked by a second function, `v2.std.type_binder` `type_binder_labels_conform`, over any Node. HARM if it were not checked: a foreign Named edge on a Transform would be carried as a cast target nobody authored, or skipped by readers that pass the marker over.",
+    "RUNG FOUND AT: structurally guaranteed (rung 3), not impossible. The mislabelled node is CONSTRUCTIBLE -- Edge.label is an open `Named { name: Symbol }` -- but no Accepted program contains one: `v2.compiler.resolve` gates the tree on `well_formed(n) && type_binder_labels_conform(root: n)` before resolving, and refuses a mislabelled tree as malformed. Discriminating evidence: `v2.test.claim.body_cast_node` `bcn_a_foreign_label_on_a_transform_refuses` (a Transform carrying a non-marker Named edge fails the gate predicate) with its positive partner `bcn_a_loop_passes_the_resolver_gate` (a real fold-lowered Loop, whose Named edges belong to its own edge discipline, passes it); the Bind arm's control is `v2.test.claim.body_let_annotation` `bla_bind_admits_only_its_annotation_label`, landing with the let-annotation carrier (gunbc#12322), which adds its DeclarationRef here. Ruled by neat-boar-16 on review 71525 (gunbc#12322).",
+    "CEILING: structurally impossible -- which label a behavior's Named edge may carry is decidable and fully modeled, so the invalid state need not have a constructor. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: edge labels on behavior nodes become a closed coproduct owned by `v2.std.node`, so a Transform's or Bind's Named edge can only be constructed as the marker that behavior admits and a foreign label has no constructor; `type_binder_labels_conform`'s label arm for behaviors then dissolves, its discriminating red kept as the evidence. It must be ONE authority with the edge-discipline coproduct gentle-koi-724's lane is building, not a second one beside it.",
+  ],
+
+  evidence: [
+    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_a_loop_passes_the_resolver_gate", field: WholeDeclaration },
+  ],
+}

src/v2/compiler/03_resolve.dag

@@ -109,7 +109,7 @@ import v2.std.node {
   node_with_occurrence_id,
   well_formed,
 }
-import v2.std.type_binder { edge_is_type_params, type_binder_labels_conform, type_param_names }
+import v2.std.type_binder { edge_is_cast_target, edge_is_type_params, type_binder_labels_conform, type_param_names }
 import v2.std.node_query {
   construct_field_edges,
   construct_tag_optional,
@@ -139,8 +139,15 @@ type Scope
   = ScopeRoot { module: Namespace }
   | ScopeFrame { locals: Map<Symbol, Symbol>, outer: Scope }
 
+// type_scope IS THE TYPE-ROLE FRAME: the scope a name in a TYPE position resolves in. It is the
+// enclosing Arrows' type-parameter frames over the namespace root, and it never carries a value
+// binder (a parameter, a `let`, an arm binder), so a type position cannot bind a value and a value
+// position -- which resolves in `scope` -- cannot bind a type parameter. resolve_arrow_node opens a
+// fn's <T> on it over the WHOLE Arrow, signature and body; only type-role walks consult it
+// (resolve_type_role_target).
 type ResolveContext {
   scope: Scope
+  type_scope: Scope
   namespace: Namespace
   policy: NameResolutionPolicy
   position: QualifiedName
@@ -318,6 +325,7 @@ fn resolve_ctx_init(
 ) -> ResolveContext {
   ResolveContext {
     scope: scope_from_namespace(namespace: namespace),
+    type_scope: scope_from_namespace(namespace: namespace),
     namespace: namespace,
     policy: policy,
     position: namespace.module_qn,
@@ -329,6 +337,7 @@ fn resolve_ctx_init(
 fn resolve_ctx_with_scope(ctx: ResolveContext, scope: Scope) -> ResolveContext {
   ResolveContext {
     scope: scope,
+    type_scope: ctx.type_scope,
     namespace: ctx.namespace,
     policy: ctx.policy,
     position: ctx.position,
@@ -337,9 +346,30 @@ fn resolve_ctx_with_scope(ctx: ResolveContext, scope: Scope) -> ResolveContext {
   }
 }
 
+fn resolve_ctx_with_type_scope(ctx: ResolveContext, type_scope: Scope) -> ResolveContext {
+  ResolveContext {
+    scope: ctx.scope,
+    type_scope: type_scope,
+    namespace: ctx.namespace,
+    policy: ctx.policy,
+    position: ctx.position,
+    lm: ctx.lm,
+    under_module_root: ctx.under_module_root
+  }
+}
+
+// THE ONE TYPE-ROLE ENTRY. A type expression carried in a body -- a cast's target today
+// (v2.std.type_binder <cast-target>), a let annotation next -- resolves here: in the type-role
+// frame, so the enclosing fn's <T> binds it and no value binder can, and an undeclared name refuses
+// located at that name.
+fn resolve_type_role_target(ctx: ResolveContext, target: Node) -> ResolveNodeWalk {
+  resolve_node_walk(ctx: resolve_ctx_with_scope(ctx: ctx, scope: ctx.type_scope), n: target)
+}
+
 fn resolve_ctx_snoc_position(ctx: ResolveContext, segment: Symbol) -> ResolveContext {
   ResolveContext {
     scope: ctx.scope,
+    type_scope: ctx.type_scope,
     namespace: ctx.namespace,
     policy: ctx.policy,
     position: qualified_name_snoc(qn: ctx.position, segment: segment),
@@ -351,6 +381,7 @@ fn resolve_ctx_snoc_position(ctx: ResolveContext, segment: Symbol) -> ResolveCon
 fn resolve_ctx_with_under_module_root(ctx: ResolveContext, under_module_root: Bool) -> ResolveContext {
   ResolveContext {
     scope: ctx.scope,
+    type_scope: ctx.type_scope,
     namespace: ctx.namespace,
     policy: ctx.policy,
     position: ctx.position,
@@ -450,7 +481,30 @@ fn anonymous_parameter_referenced_diagnostic(n: Node) -> Diagnostic {
 // IT DISCRIMINATES THE TWO CAUSES, which is why the third arm exists rather than defaulting: a name
 // no module declares gets NO advisory, because the honest reading there is a typo or a deleted
 // declaration and pointing anywhere would be fabrication.
+// A TYPE PARAMETER NAMED IN A VALUE POSITION is not an unknown name: the type-role frame binds it,
+// and the value scope deliberately does not. It refuses with its own reason, located at the use.
+fn type_parameter_in_value_position_optional(ctx: ResolveContext, n: Node, name: Symbol) -> Optional<Diagnostic> {
+  match lookup_chain(s: ctx.type_scope, name: name) {
+    Accepted { value: BoundInFrame { canonical: _ }, diagnostics: _ } =>
+      optional_present(
+        value: Diagnostic {
+          reason: ^resolve_reason_type_parameter_in_value_position,
+          at: node_locus(node: n),
+          correction: Unavailable { reason: UserInputBoundary }
+        }
+      )
+    _ => optional_absent()
+  }
+}
+
 fn unbound_symbol_diagnostics(ctx: ResolveContext, n: Node, name: Symbol) -> NonEmptyDiagnostics {
+  match type_parameter_in_value_position_optional(ctx: ctx, n: n, name: name) {
+    Present { value: d } => NonEmptyDiagnostics { head: d, tail: [] }
+    Absent => unbound_symbol_diagnostics_of_value_name(ctx: ctx, n: n, name: name)
+  }
+}
+
+fn unbound_symbol_diagnostics_of_value_name(ctx: ResolveContext, n: Node, name: Symbol) -> NonEmptyDiagnostics {
   let fatal = unbound_symbol_diagnostic(n: n)
   match symbol_index_global_unique_lookup(index: ctx.namespace.symbol_index, name: name) {
     GlobalBareHit { node: _, path: path } =>
@@ -1190,7 +1244,12 @@ fn resolve_transform_children(
           } else {
             resolve_node_walk(ctx: ctx, n: e.target)
           }
-        _ => resolve_node_walk(ctx: ctx, n: e.target)
+        Named { name: _ } =>
+          if edge_is_cast_target(e: e) {
+            resolve_type_role_target(ctx: ctx, target: e.target)
+          } else {
+            resolve_node_walk(ctx: ctx, n: e.target)
+          }
       }
     )
   }))
@@ -1633,6 +1692,16 @@ fn resolve_type_params_conj(ctx: ResolveContext, conj: Node) -> ResolveNodeWalk
 // to RESOLVE a parameter's type still binds the parameter's name, and the codomain's scope is not
 // invented by that refusal.
 fn resolve_arrow_node(ctx: ResolveContext, n: Node) -> ResolveNodeWalk {
+  resolve_arrow_node_in(
+    outer_ctx: ctx,
+    ctx: resolve_ctx_with_type_scope(ctx: ctx, type_scope: resolve_type_param_frame(n: n, outer: ctx.type_scope)),
+    n: n
+  )
+}
+
+// The Arrow's own <T> binders are checked from the OUTER context: the frame they open must not
+// answer for them, or every binder would read as shadowing itself.
+fn resolve_arrow_node_in(outer_ctx: ResolveContext, ctx: ResolveContext, n: Node) -> ResolveNodeWalk {
   let scope_type = resolve_type_param_frame(n: n, outer: ctx.scope)
   let value_params = add_arrow_domain_named_params(n: n, acc: empty_map())
   let scope_codomain = ScopeFrame { locals: value_params, outer: scope_type }
@@ -1641,7 +1710,7 @@ fn resolve_arrow_node(ctx: ResolveContext, n: Node) -> ResolveNodeWalk {
     match e.label {
       Named { name: _ } =>
         if edge_is_type_params(e: e) {
-          child_walk_step(w: acc, e: e, r: resolve_type_params_conj(ctx: ctx, conj: e.target))
+          child_walk_step(w: acc, e: e, r: resolve_type_params_conj(ctx: outer_ctx, conj: e.target))
         } else {
           child_walk_step(
             w: acc,