Join corpus Int and kernel Int at inhabitance (N7 g_tokenize_parse)

src/v2/compiler/04_infer.dag

@@ -40,6 +40,7 @@ import v2.extdeps.languages.dag {
   DagCanonicalStringLiteral,
   DagCanonicalLiteral,
   dag_binding_denotation,
+  dag_kernel_type_declaration_binding_optional,
   dag_canonical_literal_from_node,
   dag_declared_inhabitants_root,
   dag_declared_inhabitants_subject_field,
@@ -69,7 +70,7 @@ import std.optional {
   optional_absent,
   optional_present
 }
-import v2.std.qualified_name { QualifiedName, declaration_reference_node, declaration_reference_path_optional, qualified_name_to_dotted_string, lexical_reference_label_optional, parameter_reference_path_optional }
+import v2.std.qualified_name { QualifiedName, declaration_reference_node, declaration_reference_path_optional, qualified_name_last_segment, qualified_name_to_dotted_string, lexical_reference_label_optional, parameter_reference_path_optional }
 import v2.std.node_query { BinderParts, binder_node, binder_node_parts, construct_field_edges, construct_tag_optional, declared_field_from_edge, find_labeled_child }
 import v2.std.symbol_index { RecordTypePayload, SymbolIndex, VariantArmPayload, symbol_index_declared_payload_at, symbol_index_declared_type_params_at, symbol_index_lookup }
 import v2.std.grammar { node_atom_identity_optional }
@@ -146,6 +147,7 @@ import v2.std.diagnostic {
   outcome_accepted,
   rejected_with_pending
 }
+import v2.std.integer { integer_int_type_node }
 import v2.std.logic { bool_node }
 import v2.std.node {
   StructuralLabel,
@@ -3525,22 +3527,29 @@ fn infer_type_alias_unfolded(t: Node, declarations: SymbolIndex) -> Optional<Nod
 // declared and the produced type, so every declared position -- argument, return, record field, let annotation,
 // binder default -- and both the plain and the generic routes see one type per alias family (review 75435;
 // calm-boar-904, option 1). v2.std.inhabitance holds no index, so the reading is supplied by the producer,
-// exactly as produced_declared_carrier is.
+// exactly as produced_declared_carrier is. KERNEL RECOGNITION IS PART OF EVERY STEP
+// (infer_kernel_value_type_optional): checked before each alias unfolding and inside every Instantiation argument,
+// so `type Alias = v2.std.integer.Int` stops at the kernel atom exactly as a direct reference does, and the generic
+// formal match and the declared-type obligation read ONE normalized type, not two.
 fn infer_type_alias_normalized(t: Node, declarations: SymbolIndex) -> Node {
-  match infer_type_alias_unfolded(t: t, declarations: declarations) {
-    Present { value: unfolded } => infer_type_alias_normalized(t: unfolded, declarations: declarations)
+  match infer_kernel_value_type_optional(t: t) {
+    Present { value: k } => k
     Absent =>
-      match t.kind {
-        TypeNode { connective: Instantiation } =>
-          Node {
-            kind: t.kind,
-            children: fold(t.children, init: Empty, f: fn(acc, e) {
-              list_snoc_item(xs: acc, item: Edge { label: e.label, target: infer_type_alias_normalized(t: e.target, declarations: declarations) })
-            }),
-            occurrence_id: t.occurrence_id
+      match infer_type_alias_unfolded(t: t, declarations: declarations) {
+        Present { value: unfolded } => infer_type_alias_normalized(t: unfolded, declarations: declarations)
+        Absent =>
+          match t.kind {
+            TypeNode { connective: Instantiation } =>
+              Node {
+                kind: t.kind,
+                children: fold(t.children, init: Empty, f: fn(acc, e) {
+                  list_snoc_item(xs: acc, item: Edge { label: e.label, target: infer_type_alias_normalized(t: e.target, declarations: declarations) })
+                }),
+                occurrence_id: t.occurrence_id
+              }
+            TypeNode { connective: _ } => t
+            ComputationNode { behavior: _ } => t
           }
-        TypeNode { connective: _ } => t
-        ComputationNode { behavior: _ } => t
       }
   }
 }
@@ -3563,6 +3572,36 @@ fn infer_match_generic_formal_or_carrier(formal: Node, produced: Node, type_para
   }
 }
 
+// THE KERNEL VALUE TYPE AND THE CORPUS DECLARATION ARE ONE TYPE. `v2.std.integer.Int`
+// (`type Int = GroupCompletion<Nat>`) and the kernel atom `dag_binding_type_int`
+// (integer_int_type_node) answer the same value-type question. Alias-normalizing first unfolds
+// that alias to GroupCompletion<Nat> and then the judge compares that product to the kernel atom.
+// Recognition is BY AUTHORITY, NOT BY SPELLING: a declaration reference joins only when
+// dag_kernel_type_declaration_binding_optional admits the FULL path (the same roster resolve
+// uses). A last-segment `Int` would recapture a module's own `type Int = | Mine` and admit
+// `let y: Int = 1` (gunbc.recurring_failure_mode kernel_type_spelling_captured_a_module_declaration;
+// review 77259). An atom joins only through dag_binding_denotation (binding -> value type).
+fn infer_kernel_value_type_optional(t: Node) -> Optional<Node> {
+  if infer_type_equal_ignoring_provenance(a: t, b: integer_int_type_node()) {
+    optional_present(value: integer_int_type_node())
+  } else if infer_type_equal_ignoring_provenance(a: t, b: bool_node()) {
+    optional_present(value: bool_node())
+  } else {
+    match declaration_reference_path_optional(node: t) {
+      Present { value: path } =>
+        match dag_kernel_type_declaration_binding_optional(path: path) {
+          Present { value: binding } => dag_binding_denotation(sym: binding)
+          Absent => optional_absent()
+        }
+      Absent =>
+        match node_atom_identity_optional(node: t) {
+          Present { value: id } => dag_binding_denotation(sym: id)
+          Absent => optional_absent()
+        }
+    }
+  }
+}
+
 // THE ONE PRODUCER OF A DeclaredTypeObligation in infer: every obligation -- a call argument, a declared return, a
 // fold member or carrier, a generic formal -- is built here, so the ONE alias rule (infer_type_alias_normalized)
 // reaches every judgment: the declared type, the produced type and the produced type's refinement carrier are

src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag

@@ -0,0 +1,128 @@
+module v2.test.claim.compiler.generic_closure_outcome_construct_probe
+
+import v2.compiler.infer {
+  infer,
+  infer_kernel_value_type_optional,
+  infer_type_equal_ignoring_provenance
+}
+import v2.compiler.name_resolve {
+  Admission,
+  ResolutionSubject,
+  resolution_context,
+  resolve_in_context
+}
+import v2.compiler.normalized_tree { NormalizedTree }
+import v2.compiler.program_assembly { module_roots_from_source_root_ingest }
+import v2.compiler.resolve { ResolvedTree }
+import v2.compiler.source_authority { SourceRootIngest }
+import v2.extdeps.languages.dag { dag_language_model }
+import v2.std.cross_tree.resolution { source_root_index_empty }
+import v2.std.diagnostic { Accepted, None, Outcome, Rejected, Some, diagnostics_fatal_reason }
+import v2.std.integer { integer_int_type_node }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import std.occurrence_identity { OccurrenceSynthetic }
+import v2.std.node { Atom, Node, Symbol, TypeNode, node_synthetic }
+import std.optional { Absent, Present }
+import v2.std.qualified_name { declaration_reference_node, qualified_name_from_dotted_string }
+import v2.std.resolution_policy { default_name_resolution_policy }
+import v2.std.text { String }
+import std.algebra { Empty, FreeMonoid }
+import v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test {
+  rcf_member_accepted_and_decided,
+  rcf_read
+}
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+// SUBJECT: infer_declared_type_obligation's kernel-value join (infer_kernel_value_type_optional, applied at
+// every step of infer_type_alias_normalized). A position declared with the kernel Int (dag_binding_type_int)
+// and one declared with the corpus v2.std.integer.Int (type Int = GroupCompletion<Nat>) are one value type. The
+// join keys the kernel declaration roster (full path) and dag_binding_denotation, never a last-segment Int.
+//
+// SUPPLIED claims judge the join at its own interface. ONE claim runs the real ingest -> resolve -> infer route
+// (the alias claim). The negative side of the join is
+// supplied (gbo_a_bool_name_is_not_the_kernel_int_holds), not re-run end to end.
+//
+// DECLARED FRONTIER, NOT CLAIMED HERE: generic-variant constructs undecided. A direct generic-variant construct
+// (Acc { value: 1, n: 0 } at Out<Int>) is not accepted-and-decided on this base, with or without the join (measured
+// at 41afbbbb, BuildBuddy 36e48268). Owner: gunbc#13558 (payload binders over Outcome<T> via #13210's formal-payload
+// obligation), which carries the claim that turns it green.
+
+data gbo_integer_stub_source: String = "module v2.std.integer\n\ntype Nat = Zero | One\n\ntype Int = Nat\n"
+
+data gbo_alias_source: String = "module v2.test.gbo_alias\n\nimport v2.std.integer { Int }\n\ntype Alias = v2.std.integer.Int\n\nfn one() -> Alias {\n  1\n}\n"
+
+data gbo_ingest: SourceRootIngest = [
+  rcf_read(source: gbo_integer_stub_source, id: ^gbo_integer_stub_read, unit: ^gbo_integer_stub_cu, path: "src/v2/test/fixture/gbo/integer.dag"),
+  rcf_read(source: gbo_alias_source, id: ^gbo_alias_read, unit: ^gbo_alias_cu, path: "src/v2/test/fixture/gbo/alias.dag")
+]
+
+fn gbo_fixture_normalized() -> Outcome<FreeMonoid<NormalizedTree>> {
+  module_roots_from_source_root_ingest(ingest: gbo_ingest, lm: dag_language_model())
+}
+
+fn gbo_resolve_subject(subject: String) -> Outcome<ResolvedTree> {
+  match gbo_fixture_normalized() {
+    Rejected { diagnostics: d } => Rejected { diagnostics: d }
+    Accepted { value: roots, diagnostics: _ } =>
+      resolve_in_context(
+        context: resolution_context(lm: dag_language_model(), roots: roots, index: source_root_index_empty(), active_roots: Empty, policy: default_name_resolution_policy()),
+        admission: Admission {
+          subject: ResolutionSubject { name: qualified_name_from_dotted_string(dotted: subject) },
+          imports: Empty
+        }
+      ).resolved
+  }
+}
+
+fn gbo_resolved_alias() -> Outcome<ResolvedTree> { gbo_resolve_subject(subject: "v2.test.gbo_alias") }
+
+fn gbo_atom(id: Symbol) -> Node {
+  node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: [])
+}
+
+fn gbo_is_kernel_int(t: Node) -> Bool {
+  match infer_kernel_value_type_optional(t: t) {
+    Absent => false
+    Present { value: k } => infer_type_equal_ignoring_provenance(a: k, b: integer_int_type_node())
+  }
+}
+
+test fn gbo_an_int_spelling_atom_is_not_the_kernel_int_holds() -> Bool {
+  !gbo_is_kernel_int(t: gbo_atom(id: ^Int))
+}
+
+test fn gbo_a_module_int_declaration_is_not_the_kernel_int_holds() -> Bool {
+  !gbo_is_kernel_int(
+    t: declaration_reference_node(
+      qn: qualified_name_from_dotted_string(dotted: "v2.test.gbo_shadow.Int"),
+      occurrence_id: OccurrenceSynthetic
+    )
+  )
+}
+
+test fn gbo_the_integer_int_declaration_is_the_kernel_int_holds() -> Bool {
+  gbo_is_kernel_int(
+    t: declaration_reference_node(
+      qn: qualified_name_from_dotted_string(dotted: "v2.std.integer.Int"),
+      occurrence_id: OccurrenceSynthetic
+    )
+  )
+}
+
+test fn gbo_a_kernel_int_atom_is_the_kernel_int_holds() -> Bool {
+  gbo_is_kernel_int(t: gbo_atom(id: ^dag_binding_type_int))
+}
+
+test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool {
+  !gbo_is_kernel_int(t: gbo_atom(id: ^Bool))
+}
+
+// THE ROUTE: a kernel Int literal returned at a declared `Alias` of the corpus Int (`fn one() -> Alias { 1 }`),
+// on the real ingest -> resolve -> infer path, ACCEPTED AND DECIDED. The literal is the kernel atom; the declared
+// side reaches the kernel atom only through the join, and only if recognition re-enters after the alias step. So it
+// goes red both when the join is deleted (Alias unfolds to its right-hand side) and when recognition happens only at
+// the input -- the integration and the regression in one claim (BuildBuddy 50c58a76 and 2002ea86).
+test fn gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds() -> Bool {
+  rcf_member_accepted_and_decided(resolved: gbo_resolved_alias(), member: ^one)
+}

src/v2/workflow/floor_pure_producer_share.dag

@@ -821,7 +821,19 @@ fn floor_single_claim_fill_debt_active_claims() -> List<String> {
 // pipeline's per-claim fixed cost of assembling and inferring a one-module fixture, not the test's own work.
 // Trigger: assemble plus infer of a one-module fixture runs under the per-claim budget
 // (gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame).
+// gunbc#13511 (kernel-value join): the ONE real-path inhabitance of v2.test.claim.compiler.generic_closure_outcome_construct_probe,
+// gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (red with the join deleted and with input-only recognition). Its own-frame eval steps are
+// re-derived by claim_batch --hermetic --entry src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag
+// --functions gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (receipt: BuildBuddy a63835e8, pinned
+// 46da0c8fa0; red with the join deleted, BuildBuddy 50c58a76, and with input-only recognition, BuildBuddy 2002ea86).
+// Trigger: shared_precondition_re_derived_once_per_claim_frame, as above.
 data floor_single_claim_fill_debt: List<SingleClaimFillDebtModule> = [
+  SingleClaimFillDebtModule {
+    module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe",
+    claims: [
+      SingleClaimFillDebtClaim { claim: "gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds", standing: ActiveFillDebt }
+    ]
+  },
   SingleClaimFillDebtModule {
     module: "v2.test.claim.body_lowering.fold_operand_structure",
     claims: [