diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 93fcded72d2..493bf2f6bf1 100644 --- a/src/v2/compiler/04_infer.dag +++ b/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 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`) 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 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 { + 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 diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag new file mode 100644 index 00000000000..a87b764c309 --- /dev/null +++ b/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) 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) 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 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> { + module_roots_from_source_root_ingest(ingest: gbo_ingest, lm: dag_language_model()) +} + +fn gbo_resolve_subject(subject: String) -> Outcome { + 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 { 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) +} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 28d3129de9e..d3833dade50 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -821,7 +821,19 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // 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 { + 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: [