v2: lower the where-refined head so resolve binds it; ResolvedTree.resolved_declarations (base for #12407)

dag/gunbc/recurring_failure_mode/declaration_body_type_shell_preserved_unresolved.dag

@@ -0,0 +1,18 @@
+module gunbc.recurring_failure_mode.declaration_body_type_shell_preserved_unresolved
+
+import std.types { NonEmptyStr }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data declaration_body_type_shell_preserved_unresolved: RecurringFailureMode = RecurringFailureMode {
+  identity: "declaration_body_type_shell_preserved_unresolved" as NonEmptyStr,
+  receipts: [
+    "INVALID STATE: a type reference inside a type DECLARATION's body reaches v2 resolve as an unlowered dag_surface_qualified_name parse shell, and resolve preserves that shell UNCHANGED as module metadata (`v2.extdeps.languages.dag` `dag_resolve_preserve_module_metadata_subtree`), so the declaration names its type in a vocabulary no stage resolved. HARM: a carrier nothing declares is accepted silently, and a consumer comparing the declaration's type with a resolved type sees two vocabularies for one type: the Widened refinement-to-carrier cast (gunbc#12407) refused `x as Int` from `x: Pos` once main lowered kernel spellings by declaration.",
+    "DISTINGUISHING FACT, MEASURED: on the resolved tree, a where-refined head that body lowering hands resolve as a plain type atom IS resolved (`Int` becomes the kernel binding); the same head left as the parse shell is not. So the boundary is LOWERING, not resolve: every declaration-body type position must be lowered before resolve, and resolve then binds it through its one producer, `v2.compiler.resolve` `resolved_reference_node` (a `std.decl_ref` `DeclarationRef`-carrying declaration reference for a corpus type, the kernel atom for a kernel spelling).",
+    "RUNG FOUND AT: silent on every declaration-body type position. RUNG NOW: structurally guaranteed for the where-refined head only: `v2.compiler.body_lowering_fold` `body_lower_type_variant` lowers it through `body_lower_type_expr_lowered_optional`, an unreadable head refuses at the head, and resolve binds it (RED: `v2.test.claim.declaration_graft_assemble` `declaration_graft_where_alias_over_an_undeclared_carrier_refuses`; control: `declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations`, read through `v2.compiler.resolve` `ResolvedTree` `resolved_declarations`). Step-0 census before the change: every where-refined head in the corpus is a plain type name, so none regressed. DECLARED FRONTIER: the alias right-hand side, record field types and variant payload types are the same defect and remain unresolved. CEILING: structurally guaranteed (a decidable, fully modeled class). NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: every declaration-body type position is lowered before resolve, so resolve binds each one and `resolved_declarations` carries it resolved. SIBLING: quiet-hawk-702's v1 cause 1b (gunbc#12612: v1 `Node.declaration`, written by v1 resolve for declaration-field references), the same identity type on the frozen v1 layer, not a second mechanism."
+  ],
+  evidence: [
+    DeclarationRef { module_path: "v2.test.claim.declaration_graft_assemble", decl_name: "declaration_graft_where_alias_over_an_undeclared_carrier_refuses", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.declaration_graft_assemble", decl_name: "declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations", field: WholeDeclaration },
+  ],
+}

src/v2/compiler/00_compile.dag

@@ -91,6 +91,7 @@ import v2.compiler.resolve {
   ResolveWalkAccepted,
   ResolveWalkRefused,
   resolve,
+  resolved_tree_of,
   ResolvedTree
 }
 import v2.compiler.tokenize { tokenize }
@@ -3141,7 +3142,7 @@ fn native_module_resolve_verdict(
         ResolveWalkAccepted { value: resolved, diagnostics: _ } =>
           match context.resolution {
             Accepted { value: shared, diagnostics: _ } =>
-              NativeModuleResolveAccepted { resolved: ResolvedTree { root: resolved, symbol_index: shared.symbol_index } }
+              NativeModuleResolveAccepted { resolved: resolved_tree_of(root: resolved, symbol_index: shared.symbol_index) }
             Rejected { diagnostics: r } =>
               NativeModuleResolveRefused {
                 first: r,

src/v2/compiler/03_ingest.dag

@@ -318,7 +318,7 @@ fn parse_tree_to_target_model_bridge(parse_tree: ParseTree, source_model: Target
     o: parse_tree_to_emitted_node(parse_tree: parse_tree, source_model: source_model),
     f: fn(emitted) {
       bind_outcome(
-        o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index() }),
+        o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index() }),
         f: fn(inferred) {
           bind_outcome(
             o: coerce_grounded_node(source: emitted, tree: inferred, target: source_model),
@@ -343,7 +343,7 @@ fn cross_language_compile(
         o: neutralize_core_for_target(core: core, target: target_model),
         f: fn(neutralized) {
           bind_outcome(
-            o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index() }),
+            o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index() }),
             f: fn(inferred) {
               emit(tree: inferred, target: target_model)
             }

src/v2/compiler/03_resolve.dag

@@ -74,6 +74,7 @@ import v2.std.resolution_policy {
   NamespaceOnlyY,
   default_name_resolution_policy
 }
+import v2.compiler.symbol_index_fill { symbol_index_fill_module_declarations }
 import v2.std.symbol_index {
   LexicalAmbiguous,
   LexicalBindingCandidate,
@@ -137,13 +138,35 @@ import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId }
 // the Namespace.symbol_index the walk ran under, minted beside the root on the Accepted arm only, so
 // a refusal carries no index and no stage can read one for a tree that did not resolve.
 // CONSUMERS: .root is read by every stage after resolve (infer's gather reads it at its entry).
-// .symbol_index is a DECLARED FRONTIER in this change: its consumer is gunbc#12407, which stacks on
-// it -- v2.compiler.infer refinement_declaration asks symbol_index_lookup for a refinement
-// declaration a cast operand's type references (the declared-carrier widening), replacing an
-// infer-private walk over the tree.
+// .symbol_index is the table resolve resolves against; no later stage reads it. A later stage that needs
+// a declaration reads .resolved_declarations below: v2.compiler.infer refinement_declaration (gunbc#12407,
+// stacked on this change) asks symbol_index_lookup there for the refinement declaration a cast
+// operand's type references, replacing an infer-private walk over the tree.
+// TWO INDEXES OVER THE SAME DECLARATIONS AT DIFFERENT PHASES, NEVER ONE QUESTION TWICE.
+// symbol_index is THE INDEX RESOLUTION CONSULTED: declarations as authored, before resolve, the table
+// resolve looks references up in. resolved_declarations is DECLARATIONS WITH RESOLVED BODIES: the same
+// module fold (v2.compiler.symbol_index_fill symbol_index_fill_module_declarations) run over the
+// RESOLVED root, so a declaration's body carries the identities resolve bound in it -- a where-refined
+// carrier `Int` is the kernel binding, a carrier naming a corpus type is its declaration reference. A
+// reader that needs a body's resolved type reads resolved_declarations; nothing reads symbol_index for
+// a body type (neat-boar-16 ruling), so the two never answer the same question.
 type ResolvedTree {
   root: Node
   symbol_index: SymbolIndex
+  resolved_declarations: SymbolIndex
+}
+
+// The resolved root's declarations, by the same module fold the pre-resolve index uses: the module's
+// qualified name is read from the root's own header, so a declaration is keyed at its full path (p.Pos).
+// A root whose module name cannot be read yields the empty index -- every lookup through it refuses.
+fn resolved_declarations_of(root: Node) -> SymbolIndex {
+  symbol_index_fill_module_declarations(index: empty_symbol_index(), root: root, record_declarations: Empty)
+}
+
+// THE ONE CONSTRUCTOR of an accepted resolution's carrier: the root, the index it was resolved
+// against, and its declarations as resolved.
+fn resolved_tree_of(root: Node, symbol_index: SymbolIndex) -> ResolvedTree {
+  ResolvedTree { root: root, symbol_index: symbol_index, resolved_declarations: resolved_declarations_of(root: root) }
 }
 
 // `test_code`, `declared_in` and `imported_origins` exist for one decision: whether a reference binds
@@ -1249,7 +1272,7 @@ fn resolve_walk_outcome(w: ResolveNodeWalk) -> Outcome<Node> {
 fn resolved_tree_outcome(w: ResolveNodeWalk, symbol_index: SymbolIndex) -> Outcome<ResolvedTree> {
   match w {
     ResolveWalkAccepted { value: v, diagnostics: d } =>
-      Accepted { value: ResolvedTree { root: v, symbol_index: symbol_index }, diagnostics: d }
+      Accepted { value: resolved_tree_of(root: v, symbol_index: symbol_index), diagnostics: d }
     ResolveWalkRefused { first: f, rest: _, observation: _ } => Rejected { diagnostics: f }
   }
 }

src/v2/compiler/body_lowering_fold.dag

@@ -966,6 +966,15 @@ fn body_lower_fielded_type_variant(shell: Node, head: Node, payload_shell: Node)
   }
 }
 
+// A WHERE-REFINED HEAD IS A TYPE, LOWERED BY THE ONE TYPE-EXPRESSION LOWERING that signatures and
+// cast targets use (body_lower_type_expr_lowered_optional), so resolve binds the carrier in type role
+// like any other type. Carried as the raw parse sequence, the head reached resolve as a
+// dag_surface_qualified_name shell, which v2.compiler.resolve preserves UNCHANGED as module metadata
+// (v2.extdeps.languages.dag dag_resolve_preserve_module_metadata_subtree): the declaration named its
+// carrier in a vocabulary no stage resolved. A head the lowering cannot read refuses at the head, as an
+// unreadable annotation does. The other declaration-body type positions (alias right-hand side, field
+// and payload types) are the same defect and a declared frontier
+// (gunbc.recurring_failure_mode declaration_body_type_shell_preserved_unresolved).
 // A variant shell is seq(type_expr, seq(optional(where), optional(payload))). A bare head is left
 // as parsed: whether `type T = U` names an alias or a one-variant sum is decided where the
 // alternatives are counted (v2.std.compilers.sugar sugar_fold_coproduct_pipe_chain, the seed's
@@ -1001,17 +1010,24 @@ fn body_lower_type_variant(shell: Node) -> Outcome<Node> {
                     Absent => outcome_accepted(value: shell)
                     Present { value: suffix_id } =>
                       if suffix_id == ^dag_surface_where_refinement_clause {
-                        outcome_accepted(
-                          value: node_with_occurrence_id(
-                            kind: TypeNode { connective: Conj },
-                            children: body_lower_type_variant_children_with_where(
-                              base: pair.left,
-                              where_clause: suffixes.left,
-                              fields: suffixes.right
-                            ),
-                            occurrence_id: shell.occurrence_id
-                          )
-                        )
+                        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 } =>
+                            outcome_accepted(
+                              value: node_with_occurrence_id(
+                                kind: TypeNode { connective: Conj },
+                                children: body_lower_type_variant_children_with_where(
+                                  base: carrier,
+                                  where_clause: suffixes.left,
+                                  fields: suffixes.right
+                                ),
+                                occurrence_id: shell.occurrence_id
+                              )
+                            )
+                        }
                       } else {
                         outcome_accepted(value: shell)
                       }

src/v2/test/claim/declaration_graft_assemble_test.dag

@@ -1,6 +1,9 @@
 module v2.test.claim.declaration_graft_assemble
 
 import v2.compiler.resolve { ResolvedTree }
+import v2.std.symbol_index { symbol_index_lookup }
+import v2.std.node_query { find_named_child }
+import v2.std.optional { Absent, Present }
 import extdeps.communication.medium { Lossless, Medium }
 import v2.compiler.name_resolve {
   Admission,
@@ -120,13 +123,14 @@ fn declaration_graft_atom_present(root: Node, lexeme: String) -> Bool {
 // fn-only, type-only, where-alias-only) are the containment-spine controls (gunbc#11694)
 // and stay separate, as do the three record sources (once refusing; now the Named controls of
 // the record spelling, see the bottom of this module).
-data src_combined: String = "module p\n\nimport v2.std.logic { Bool }\n\ntype Flag = On | Off\ntype Name = String where brand(\"Name\")\nfn f(x: Int) -> Int { x }\nfn dag_user(x: Int) -> Int { x }\nfn g(q: Flag) -> Flag { q }\nfn h() -> Flag { On }\nfn flip(q: Flag) -> Flag { match q { On => Off } }\nfn b() -> Bool { true }\n"
-data src_alias_spelled_as_emitted_id: String = "module p\n\ntype dag_surface_type_expr = String where brand(\"N\")\nfn f(x: Int) -> Int { x }\n"
-data src_alias_spelled_as_production_name: String = "module p\n\ntype dag_production_type_decl = String where brand(\"N\")\nfn f(x: Int) -> Int { x }\n"
+data src_combined: String = "module p\n\nimport v2.std.logic { Bool }\n\ntype Flag = On | Off\ntype Name = Int where brand(\"Name\")\nfn f(x: Int) -> Int { x }\nfn dag_user(x: Int) -> Int { x }\nfn g(q: Flag) -> Flag { q }\nfn h() -> Flag { On }\nfn flip(q: Flag) -> Flag { match q { On => Off } }\nfn b() -> Bool { true }\n"
+data src_alias_spelled_as_emitted_id: String = "module p\n\ntype dag_surface_type_expr = Int where brand(\"N\")\nfn f(x: Int) -> Int { x }\n"
+data src_alias_spelled_as_production_name: String = "module p\n\ntype dag_production_type_decl = Int where brand(\"N\")\nfn f(x: Int) -> Int { x }\n"
 data src_empty: String = "module p\n"
 data src_fn_only: String = "module p\n\nfn f(x: Int) -> Int { x }\n"
 data src_type_only: String = "module p\n\ntype Flag = On | Off\n"
-data src_where_alias_only: String = "module p\n\ntype Name = String where brand(\"Name\")\n"
+data src_where_alias_only: String = "module p\n\ntype Name = Int where brand(\"Name\")\n"
+data src_where_alias_undeclared_carrier: String = "module p\n\ntype Name = Undeclared where brand(\"Name\")\n"
 data src_record_construct: String = "module p\n\ntype Rec { n: Int }\nfn mk() -> Rec { Rec { n: 1 } }\n"
 data src_record_type_only: String = "module p\n\ntype Rec { n: Int }\n"
 data src_flag_and_rec: String = "module p\n\ntype Flag = On | Off\ntype Rec { n: Int }\n"
@@ -138,6 +142,8 @@ fn declaration_graft_empty_assembled() -> Outcome<ResolvedTree> { declaration_gr
 fn declaration_graft_fn_only_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_fn_only) }
 fn declaration_graft_type_only_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_type_only) }
 fn declaration_graft_where_alias_only_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_where_alias_only) }
+// Rostered warm in v2.workflow.floor_pure_producer_share: one front end is more than one claim's budget.
+fn declaration_graft_where_alias_undeclared_carrier_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_where_alias_undeclared_carrier) }
 fn declaration_graft_record_construct_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_record_construct) }
 fn declaration_graft_record_type_only_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_record_type_only) }
 fn declaration_graft_flag_and_rec_assembled() -> Outcome<ResolvedTree> { declaration_graft_assemble_for(src: src_flag_and_rec) }
@@ -185,6 +191,44 @@ test fn declaration_graft_where_alias_accepts() -> Bool {
   declaration_graft_accepts(out: declaration_graft_where_alias_only_assembled())
 }
 
+// A WHERE-ALIAS'S CARRIER IS A RESOLVED TYPE. Body lowering lowers the refined head as a type
+// (v2.compiler.body_lowering_fold body_lower_type_variant), so resolve binds it and a carrier nothing
+// declares refuses unbound, located at the carrier. RED BEFORE: the head reached resolve as an
+// unlowered dag_surface_qualified_name shell, which resolve preserves unchanged as module metadata,
+// so `Undeclared where ..` ASSEMBLED with its carrier never checked (and this module's fixtures
+// carried an unimported `String` that way; they now carry Int).
+// THE RESOLVED CARRIER IS READ FROM resolved_declarations (v2.compiler.resolve ResolvedTree): the
+// where-alias's declaration, as resolved, holds its carrier as the kernel Int binding. RED if the head
+// reached resolve unlowered (a preserved qualified-name shell) or were read from symbol_index, which
+// holds the declaration as authored (the bare spelling Int).
+test fn declaration_graft_where_alias_carrier_is_resolved_in_resolved_declarations() -> Bool {
+  match declaration_graft_where_alias_only_assembled() {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: tree, diagnostics: _ } =>
+      match symbol_index_lookup(index: tree.resolved_declarations, qualified_path: Cons { head: ^p, tail: Cons { head: ^Name, tail: Empty } }) {
+        Absent => false
+        Present { value: decl } =>
+          match find_named_child(root: decl, name: ^dag_surface_type_expr) {
+            Accepted { value: carrier, diagnostics: _ } =>
+              match carrier.kind {
+                TypeNode { connective: Atom { identity: id } } => id == ^dag_binding_type_int
+                _ => false
+              }
+            Rejected { diagnostics: _ } => false
+          }
+      }
+  }
+}
+
+test fn declaration_graft_where_alias_over_an_undeclared_carrier_refuses() -> Bool {
+  match declaration_graft_where_alias_undeclared_carrier_assembled() {
+    Accepted { value: _, diagnostics: _ } => false
+    Rejected { diagnostics: d } =>
+      (d.head.reason == ^resolve_reason_unbound_symbol)
+        || fold(d.tail, init: false, f: fn(acc, x) { acc || (x.reason == ^resolve_reason_unbound_symbol) })
+  }
+}
+
 test fn declaration_graft_combined_accepts() -> Bool {
   declaration_graft_accepts(out: declaration_graft_combined_assembled())
 }

src/v2/test/lens_common/infer_fixture.dag

@@ -19,7 +19,7 @@ import v2.std.witness { Holds, StructuralPropertyWitness, Witness, witness_from_
 // resolution consulted; a supplied tree was never resolved, so it carries an index holding NO
 // declarations -- the name says so, and a declaration lookup through it finds nothing and refuses.
 fn claim_resolved_tree_without_declarations(root: Node) -> ResolvedTree {
-  ResolvedTree { root: root, symbol_index: empty_symbol_index() }
+  ResolvedTree { root: root, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index() }
 }
 
 fn claim_atom_node(s: Symbol) -> Node {