diff --git a/dag/gunbc/recurring_failure_mode/roster_membership_by_structural_equality.dag b/dag/gunbc/recurring_failure_mode/roster_membership_by_structural_equality.dag new file mode 100644 index 00000000000..2c8e4354c1f --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/roster_membership_by_structural_equality.dag @@ -0,0 +1,23 @@ +module gunbc.recurring_failure_mode.roster_membership_by_structural_equality + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data roster_membership_by_structural_equality: RecurringFailureMode = RecurringFailureMode { + identity: "roster_membership_by_structural_equality" as NonEmptyStr, + + receipts: [ + "**a node becomes a declared-inhabitant roster member because it is STRUCTURALLY EQUAL to some node inside a roster value, not because it denotes that roster entry.** (INVALID STATE: a bare synthetic childless Conj, which is parse residue or an empty product anywhere, is a TypeDenotationKind member of the dag roster. So `v2.compiler.infer` derives it a grounding by lookup, an ungrounded algebra ref, instead of GroundingNotDerived.) Consumers that demand grounding refuse at the wrong link (coercion at `infer_algebra_ref_ungrounded`, not `infer_grounding_demanded_not_derived`), and any frontier claim over such a node reads derived. `std.kind` `roster_kind_index` keys `Map` by the node value and entered every node reachable from the roster.", + "RECEIPT. gunbc#12625 (Program P, one Arrow encoding) rebuilt `v2.extdeps.languages.dag` `dag_fixture_emitted_add_fn` through `v2.std.arrow_signature` `anonymous_signature_arrow`. That added the declared-order edge, whose label list is a FreeMonoid ending in a synthetic childless Conj. Bisected on BuildBuddy (339be73493..c29acd041e, `product_introduction_leaves_childless_conj_on_the_frontier_holds`); first bad commit feadae7841. Five claims went silently red outside the required gate (gunbc#12860): infer_self_grounding_wall, translate_underived_refusal, type_param_binder_frame tpb_undeclared_t, infer_product_introduction childless_conj, and ingest_bridge refuses_source_absent. The cause was decided by execution, not by a facts-key collision: each claim's tree is one node, so infer's facts map holds one entry. A direct `infer_node_declared_in_language_inhabitants` probe answered Present for a bare childless Conj.", + "REPAIRED AT THE EARLIEST UNJUSTIFIED LINK: the roster index walked label metadata as if it were payload. `std.kind` `roster_member_nodes` skips an edge that `v2.std.node` `arrow_signature_order_edge` classifies as an Arrow's declared order. That is the same predicate infer's gather fold and product evidence ask, so there is one classification and no second label list. RESIDUAL, COUNTED: membership is STILL decided by structural equality with a node in the roster value, so any value-position node equal to a payload node of a roster member is still read as that member. RUNG: mechanically preventable, held by the claims below. CEILING: structurally guaranteed. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: roster membership is keyed by the DECLARED IDENTITY a node resolves to, not by its value. This is the namespace migration's end-state that `v2.compiler.infer` names, where the roster lookup is deleted in favour of consuming resolution output.", + ], + + evidence: [ + DeclarationRef { module_path: "v2.test.execution.infer_product_introduction", decl_name: "a_bare_childless_conj_is_not_a_roster_member_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.execution.infer_product_introduction", decl_name: "the_declared_order_label_list_is_not_a_roster_member_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.execution.infer_product_introduction", decl_name: "the_roster_add_fn_is_still_a_roster_member_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.execution.infer_product_introduction", decl_name: "the_add_fn_domain_through_a_payload_edge_is_a_roster_member_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.execution.infer_product_introduction", decl_name: "product_introduction_leaves_childless_conj_on_the_frontier_holds", field: WholeDeclaration }, + ], +} diff --git a/dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag b/dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag index b413fb57ff1..3e6f23d721e 100644 --- a/dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag +++ b/dag/gunbc/rung_drop_amendment/v2_test_family_reds_measured_outside_the_gate.dag @@ -13,5 +13,5 @@ data v2_test_family_reds_measured_outside_the_gate: RungDropAmendment = RungDrop later_event: "the srv1 probe of the withdrawn v2.test. family (neat-boar-16, scratch commit eff2d73b14 = main c95f906 plus the family, artifacts on branch artifact/v2-gate-probe) measured what this row's population holds for that family: 841 v2.test.* modules declaring 5,030 test fns at c29acd041e1 have no required route; with the family restored, 4,265 were planned, 4,192 passed, 17 reached no verdict (route gaps already rostered by v2.workflow.floor_route_gap), and 44 were red on main with no lane observing them. Preparation dominated, about 3,569 modules resolved and 3,096 s wall against about 101 s of claim evaluation, the shape of this row's 2026-09-19 nominal-roster cut, so the family stays out until the trigger below. One module, v2.test.claim.cargo_build_run_argv_witness, did not typecheck on main and refused the whole floor in strict preparation when the family was restored; gunbc#12860 repaired it" as NonEmptyStr, - bearing: "of the 44 measured red identities, those still red are named here with their owners, and each leaves this amendment's list when its fix lands, so restoring the family does not inherit them as silent reds. Owner gentle-koi-724 (MQ lane), fixed green by sharp-tern-39: v2.test.execution.data_decl_lowering_grounding.childless_conj_in_codomain_stays_on_the_frontier_holds (returned false). Owner deep-ferret-305 (floor lane), fixed by work item adhoc-e6c8990b-ccf: v2.test.claim.declaring_identity_spelling.production_ingest.matched_imported_kernel_type_position_is_absent_from_the_census_today (returned false); v2.test.claim.infer_self_grounding_wall.wall_conj_grounding_no_longer_returns_source_as_its_own_type (returned false); v2.test.claim.reference_derived_residency_reading.a_type_declaration_does_not_resolve_from_a_live_module_root_pending_11574 (returned false); v2.test.claim.translate_underived_refusal.translate_refuses_underived_conj_holds (returned false); v2.test.claim.type_param_binder_frame.tpb_undeclared_t_is_not_a_type_variable (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_holds_accepts (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_wrong_value_discriminates (returned false); v2.test.execution.infer_product_introduction.product_introduction_leaves_childless_conj_on_the_frontier_holds (returned false); v2.test.manual.ingest_bridge.ingest_identity_coercion_refuses_source_absent_from_authored_roster (returned false); v2.test.manual.program_assembly_multi_file.program_assembly_cross_file_import_assembles_holds (returned false); v2.test.manual.structured_body_dispatch.structured_body_produce_subsumes_add_table (returned false); v2.test.name_resolve.test_code_reference_wall.supplied_root_is_what_normalize_emits_holds (returned false); v2.test.parse.d5_expression_grammar_parse.cause_p_keyword_field_init_red_tokens_remain_holds (returned false); v2.test.parse.type_decl_modifier_g0_parse_probe.generic_param_publishes_the_generic_ident_class_holds (returned false). None is an expected-red row: that roster asserts the identity executes, and these do not while the family is outside the gate" as NonEmptyStr, + bearing: "of the 44 measured red identities, those still red are named here with their owners, and each leaves this amendment's list when its fix lands, so restoring the family does not inherit them as silent reds. Owner deep-ferret-305 (floor lane), fixed by work item adhoc-e6c8990b-ccf: v2.test.claim.declaring_identity_spelling.production_ingest.matched_imported_kernel_type_position_is_absent_from_the_census_today (returned false); v2.test.claim.reference_derived_residency_reading.a_type_declaration_does_not_resolve_from_a_live_module_root_pending_11574 (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_holds_accepts (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_wrong_value_discriminates (returned false); v2.test.manual.program_assembly_multi_file.program_assembly_cross_file_import_assembles_holds (returned false); v2.test.manual.structured_body_dispatch.structured_body_produce_subsumes_add_table (returned false); v2.test.name_resolve.test_code_reference_wall.supplied_root_is_what_normalize_emits_holds (returned false); v2.test.parse.d5_expression_grammar_parse.cause_p_keyword_field_init_red_tokens_remain_holds (returned false); v2.test.parse.type_decl_modifier_g0_parse_probe.generic_param_publishes_the_generic_ident_class_holds (returned false). Owner calm-hawk-793 (typing/identity lane), measured red on main on 2026-10-01 while fixing the rows above and missing from the srv1 list: v2.test.manual.ingest_bridge.ingest_identity_coercion_accepts_source_present_in_authored_roster (returned false); v2.test.execution.infer_product_introduction.product_introduction_derives_fully_evidenced_products_holds (returned false). None is an expected-red row: that roster asserts the identity executes, and these do not while the family is outside the gate" as NonEmptyStr, } diff --git a/dag/std/kind.dag b/dag/std/kind.dag index 9d5d481657a..4d6c9413e5c 100644 --- a/dag/std/kind.dag +++ b/dag/std/kind.dag @@ -4,7 +4,7 @@ import std.occurrence_identity { OccurrenceSynthetic } import v2.std.algebra { filter, fold_list, list_flat_map } import v2.std.collection { List, empty_map, map_insert, map_lookup } import std.types { Map } -import v2.std.node { Atom, Node, Symbol, TypeNode, node_subtree_nodes } +import v2.std.node { Atom, Node, Symbol, TypeNode, arrow_signature_order_edge } import v2.std.node_query { NamedChildAmbiguous, NamedChildFound, NamedChildMissing, named_child_lookup } import v2.std.optional { Optional } @@ -72,11 +72,31 @@ type RosterKindIndex { kinds: Map } +// A ROSTER'S MEMBERS ARE ITS VALUES, NOT ITS LABEL METADATA. An Arrow member built through +// v2.std.arrow_signature carries a declared-order edge whose subtree is the domain's binder labels +// (a FreeMonoid ending in a childless Conj), not a value the Arrow is built from; infer already +// carries that edge as metadata and derives nothing from it. Walking it entered those label nodes +// as TypeDenotationKind members, so every structurally equal node anywhere -- a bare childless +// Conj -- derived a kind by lookup (gunbc#12625 rebuilt dag_fixture_emitted_add_fn with the edge). +// The edge is classified by v2.std.node arrow_signature_order_edge, the one predicate infer asks. +// Membership is still decided by STRUCTURAL equality with a node in the roster value; keying it by +// declared identity is the namespace migration's end-state named in v2.compiler.infer +// (gunbc.recurring_failure_mode roster_membership_by_structural_equality). +fn roster_member_nodes(root: Node) -> List { + fold(root.children, init: [root], f: fn(acc, edge) { + if arrow_signature_order_edge(parent: root, edge: edge) { + acc + } else { + concat(acc, roster_member_nodes(root: edge.target)) + } + }) +} + fn kind_record_fact_nodes(record: Node, subject_field: Symbol) -> List { match named_child_lookup(root: record, name: subject_field) { NamedChildFound { target: subject } => filter( - xs: node_subtree_nodes(root: record), + xs: roster_member_nodes(root: record), predicate: fn(member) { !(member == record) && !(member == subject) } ) NamedChildMissing => [] @@ -97,7 +117,7 @@ fn roster_kind_enter_one(kinds: Map, n: Node, kind: Kind) -> Map RosterKindIndex { - let members = node_subtree_nodes(root: roster) + let members = roster_member_nodes(root: roster) let denotations = roster_kind_enter(kinds: empty_map(), nodes: members, kind: TypeDenotationKind) RosterKindIndex { kinds: roster_kind_enter( diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 72a0fdc20f5..1b26857f207 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -106,7 +106,7 @@ Producer: `tools.emission_entry_instrument::measure_entry_emission` **RUNG DROP, DECLARED (2026-08-29, the CI bankruptcy, operator ruling in session neat-tern-658).** PREVIOUS RUNG: mechanically preventable for every class the required run carried -- eight phases over two lanes, the floor folding every discovered witness (11,996 on the last green run) through a whole-corpus strict preparation, plus v2-emission, emit-compile, partition-crates and generated-artifact drift. TEMPORARY RUNG: mechanically preventable ONLY for what the static gate names -- parse, namespace-wave-admission, regen, generated-artifact drift, and a floor over `v2.workflow.required_floor` `required_gate_prefixes` prepared as that roster's import closure -- and MITIGATABLE for everything else: those witnesses and phases are still runnable (the floor with the gate widened, `claim_executor --required-v2-emission`, `--required-emit-compile`; and -- CORRECTED 2026-08-31, re-verified against main AFTER the generated-artifact partial climb below, because a drop whose stated mitigation cannot be executed is not mitigated but a rung-honesty defect in the drop row itself, and one cited as coverage -- NOT `--required-partition-crates`, which is ABSENT from claim_executor's argument parser: that build is projected by `gunbc.repo.repo_self_build` `repo_self_build_partition_crates_command`. `--required-generated-artifact` is absent from that parser too, and the climb below restores the CHECK without restoring that spelling, so the generated-artifact projection is regenerated through the .dag entry point `tools.generated_artifact_gate` `main_wet_one`, invoked per artifact path via `gunbc run` on a gunbc BUILT FROM SOURCE -- the installed binary predates the section 4c annotation channel and cannot parse the corpus. Both flag spellings went with this cut's deleted phases and the prose naming them was not updated, so this sentence recited two remedies nobody could run) and their receipts are produced only when someone runs them, so a regression there is caught at the next manual run, not at merge. REASON: the last green run was 87 wall minutes (`gh run view 33140387402`), strict preparation alone 27 of them on one core, against ~50 squash-merges a day; main sat red for fifteen consecutive runs on two integration collisions no PR could have seen (#9662), and the CI-cost lane's change-denominated selection did not land in time to prevent it. A gate no merge can wait for validates nothing, which is a lower rung than a small gate that runs. POPULATION: every witness outside the roster (reported per run as `declined_outside_required_gate` in the disposition TSV), the three deleted required phases v2-emission, emit-compile, and partition-crates, and the v1-compiler lib tests that carry the `live-corpus` ignore reason -- enumerated by `cargo test -p v1-compiler --lib -- --ignored --list` -- each of which prepares or builds over the live tree and is run only by the receipts lane; AND -- POPULATION AMENDED 2026-09-02, because this row was cited as coverage for a member it did not name -- every module OUTSIDE THE REQUIRED FLOOR GATE CLOSURE, which no required phase compiles at all: the floor prepares the import closure of `required_gate_prefixes`, not the corpus, so a module that no rostered prefix transitively imports is never checked by any required run, and a green required run has therefore never entailed that the corpus holds the floor. That member is a FOURTH thing the original population sentence did not name -- not a witness outside the roster, not a deleted phase, not an ignored lib test -- while the RESTORATION TRIGGER below already covers it verbatim (the whole corpus as its universe). The omission was a rung-honesty defect in THIS ROW rather than a missing class, so it is amended here instead of filed as a second row: two rows behind one trigger is the same single-authority fork this project rejects in every other subject, and the more dangerous form when the row is quoted as evidence of what CI checks. the first-ever CI run of `cargo test -p v1-compiler --lib` (run 33238828500) was cancelled by its own 60-minute timeout with 204 of 682 tests finished, which is how that class was measured into existence. The workflow's two-lane shape, the aggregate context, and the per-claim cost receipt are unchanged, and the drop is countable from that receipt every run. RESTORATION TRIGGER: the CAPABILITY of a required run whose population is DERIVED from the change -- the roadmap's 'decide what matters before paying to prepare everything' -- executing on the required path with the whole corpus as its universe; a widening of the static roster does not retire this row, it only moves the population. Widening the roster is a wall-clock decision priced by the cost receipt and recorded on the roster's own header. GENERATED-ARTIFACT PARTIAL CLIMB (2026-08-31): restoring generated-artifact drift widens the static required roster by one exact class and does NOT retire this drop; the population-derived restoration trigger has not fired. INCIDENT RECEIPT (2026-08-31), recorded because a drop whose population has demonstrably fired ranks differently for restoration than one that never has: the generated-artifact drift member produced a real stale artifact on main -- two correct regens composed a `docs/design-ledgers.md` missing the frontier-receipts projection of `gunbc.self_host_compile_phase_frontier`, with no conflict and no author error -- detected only sideways by an adjacent-diff review question, and bounded to exactly one file by a dispatched whole-population `main_wet` regen on pristine main (repair and measurement: PR #9804). The window between drift landing and detection is the cost this row's REASON accepted, now materialized once. INCIDENT RECEIPT (2026-09-02), recorded on the same principle as the one above -- a population that has demonstrably fired ranks differently for restoration than one that never has: a whole-corpus compile over dag plus src/v2 found 11 NON-EXHAUSTIVE MATCH SITES STANDING ON GREEN MAIN, closed variants that do not eliminate exhaustively, which is the ordinary compiler floor this document names first; every one of them sits in a module the gate closure never compiles, so no required run has ever been able to see them. Measured as the BASELINE arm of the nested-pattern exhaustiveness checker in gunbc#10028 (whose own change additionally exposes a larger population of ordinary floor defects that the OLD checker could not see -- that population is counted by that PR and its repair program, deliberately NOT transcribed here, because a number copied into this row rots the moment the instrument that produced it is re-run; it is not evidence about this gate in any case, since those sites were invisible to the CHECKER rather than to CI, and only the 11 that main already carries under today's checker measure what the gate does not compile). Those 11 are the first number anyone has put on the gap between main is green and the corpus holds the floor, and they are exactly the population this amendment names. -AMENDED 2026-10-01: the srv1 probe of the withdrawn v2.test. family (neat-boar-16, scratch commit eff2d73b14 = main c95f906 plus the family, artifacts on branch artifact/v2-gate-probe) measured what this row's population holds for that family: 841 v2.test.* modules declaring 5,030 test fns at c29acd041e1 have no required route; with the family restored, 4,265 were planned, 4,192 passed, 17 reached no verdict (route gaps already rostered by v2.workflow.floor_route_gap), and 44 were red on main with no lane observing them. Preparation dominated, about 3,569 modules resolved and 3,096 s wall against about 101 s of claim evaluation, the shape of this row's 2026-09-19 nominal-roster cut, so the family stays out until the trigger below. One module, v2.test.claim.cargo_build_run_argv_witness, did not typecheck on main and refused the whole floor in strict preparation when the family was restored; gunbc#12860 repaired it; of the 44 measured red identities, those still red are named here with their owners, and each leaves this amendment's list when its fix lands, so restoring the family does not inherit them as silent reds. Owner gentle-koi-724 (MQ lane), fixed green by sharp-tern-39: v2.test.execution.data_decl_lowering_grounding.childless_conj_in_codomain_stays_on_the_frontier_holds (returned false). Owner deep-ferret-305 (floor lane), fixed by work item adhoc-e6c8990b-ccf: v2.test.claim.declaring_identity_spelling.production_ingest.matched_imported_kernel_type_position_is_absent_from_the_census_today (returned false); v2.test.claim.infer_self_grounding_wall.wall_conj_grounding_no_longer_returns_source_as_its_own_type (returned false); v2.test.claim.reference_derived_residency_reading.a_type_declaration_does_not_resolve_from_a_live_module_root_pending_11574 (returned false); v2.test.claim.translate_underived_refusal.translate_refuses_underived_conj_holds (returned false); v2.test.claim.type_param_binder_frame.tpb_undeclared_t_is_not_a_type_variable (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_holds_accepts (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_wrong_value_discriminates (returned false); v2.test.execution.infer_product_introduction.product_introduction_leaves_childless_conj_on_the_frontier_holds (returned false); v2.test.manual.ingest_bridge.ingest_identity_coercion_refuses_source_absent_from_authored_roster (returned false); v2.test.manual.program_assembly_multi_file.program_assembly_cross_file_import_assembles_holds (returned false); v2.test.manual.structured_body_dispatch.structured_body_produce_subsumes_add_table (returned false); v2.test.name_resolve.test_code_reference_wall.supplied_root_is_what_normalize_emits_holds (returned false); v2.test.parse.d5_expression_grammar_parse.cause_p_keyword_field_init_red_tokens_remain_holds (returned false); v2.test.parse.type_decl_modifier_g0_parse_probe.generic_param_publishes_the_generic_ident_class_holds (returned false). None is an expected-red row: that roster asserts the identity executes, and these do not while the family is outside the gate. The restoration trigger above stands whole. +AMENDED 2026-10-01: the srv1 probe of the withdrawn v2.test. family (neat-boar-16, scratch commit eff2d73b14 = main c95f906 plus the family, artifacts on branch artifact/v2-gate-probe) measured what this row's population holds for that family: 841 v2.test.* modules declaring 5,030 test fns at c29acd041e1 have no required route; with the family restored, 4,265 were planned, 4,192 passed, 17 reached no verdict (route gaps already rostered by v2.workflow.floor_route_gap), and 44 were red on main with no lane observing them. Preparation dominated, about 3,569 modules resolved and 3,096 s wall against about 101 s of claim evaluation, the shape of this row's 2026-09-19 nominal-roster cut, so the family stays out until the trigger below. One module, v2.test.claim.cargo_build_run_argv_witness, did not typecheck on main and refused the whole floor in strict preparation when the family was restored; gunbc#12860 repaired it; of the 44 measured red identities, those still red are named here with their owners, and each leaves this amendment's list when its fix lands, so restoring the family does not inherit them as silent reds. Owner deep-ferret-305 (floor lane), fixed by work item adhoc-e6c8990b-ccf: v2.test.claim.declaring_identity_spelling.production_ingest.matched_imported_kernel_type_position_is_absent_from_the_census_today (returned false); v2.test.claim.reference_derived_residency_reading.a_type_declaration_does_not_resolve_from_a_live_module_root_pending_11574 (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_holds_accepts (returned false); v2.test.emit.rust_variant_construct_emit.rust_variant_construct_emit_wrong_value_discriminates (returned false); v2.test.manual.program_assembly_multi_file.program_assembly_cross_file_import_assembles_holds (returned false); v2.test.manual.structured_body_dispatch.structured_body_produce_subsumes_add_table (returned false); v2.test.name_resolve.test_code_reference_wall.supplied_root_is_what_normalize_emits_holds (returned false); v2.test.parse.d5_expression_grammar_parse.cause_p_keyword_field_init_red_tokens_remain_holds (returned false); v2.test.parse.type_decl_modifier_g0_parse_probe.generic_param_publishes_the_generic_ident_class_holds (returned false). Owner calm-hawk-793 (typing/identity lane), measured red on main on 2026-10-01 while fixing the rows above and missing from the srv1 list: v2.test.manual.ingest_bridge.ingest_identity_coercion_accepts_source_present_in_authored_roster (returned false); v2.test.execution.infer_product_introduction.product_introduction_derives_fully_evidenced_products_holds (returned false). None is an expected-red row: that roster asserts the identity executes, and these do not while the family is outside the gate. The restoration trigger above stands whole. ### Non-literal kernel-String refusal at the structural text boundary — declared 2026-08-30 diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 6b7eae44f29..f7feef92ff2 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -63,7 +63,7 @@ import v2.std.optional { import v2.std.qualified_name { QualifiedName, declaration_reference_node, declaration_reference_path_optional, parameter_reference_path_optional } import v2.std.node_query { construct_field_edges, construct_tag_optional, declared_field_from_edge } 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.node { Ambiguous, Found, NotMarkedReference, arrow_body_target_lookup, arrow_signature_order_label, edge_label_of, match_arm_pattern_edge, resolved_reference_body_kind } +import v2.std.node { Ambiguous, Found, NotMarkedReference, arrow_body_target_lookup, arrow_signature_order_edge, match_arm_pattern_edge, resolved_reference_body_kind } import v2.std.list_introduction { list_introduction_elements_optional, list_introduction_head_path } import v2.std.arrow_signature { ApplicationBindingRefused, @@ -661,15 +661,15 @@ fn infer_roster_member_declared_type(n: Node) -> Optional { } // AN ARROW'S DECLARED ORDER IS ITS OWN EVIDENCE: the ^arrow_signature_order_edge's atoms are labels, -// not values, so the derived type carries that edge unchanged (see infer_arrow_signature_order_edge). +// not values, so the derived type carries that edge unchanged (v2.std.node arrow_signature_order_edge). fn infer_product_child_evidence_edges( - children: List, + node: Node, entries: List, ) -> Optional> { infer_formation_child_evidence_edges( - children: children, + children: node.children, entries: entries, - is_metadata: fn(edge) { edge_label_of(e: edge) == arrow_signature_order_label } + is_metadata: fn(edge) { arrow_signature_order_edge(parent: node, edge: edge) } ) } @@ -815,7 +815,7 @@ fn infer_product_facts_from_entries( Violates { diagnostic: d } => Rejected { diagnostics: diagnostics_singleton(d: d) } Holds { value: descent_proof } => - match infer_product_child_evidence_edges(children: node.children, entries: entries) { + match infer_product_child_evidence_edges(node: node, entries: entries) { Absent => bind_outcome_accepted( od: cd, @@ -3600,7 +3600,7 @@ fn infer_sum_nullary_payload_edge(parent: Node, edge: Edge) -> Bool { // declaration's binder Conj -- names the binder authority checks and resolve scopes, not values -- so // there is no type for its subtree to derive, and an EMPTY binder list is never a unit value. The // wrapper carries the edge unchanged as its own evidence, the same shape as the Arrow's declared order -// (infer_arrow_signature_order_edge). Asked through the view, never by the label alone, so the marker +// (v2.std.node arrow_signature_order_edge). Asked through the view, never by the label alone, so the marker // on an Arrow (a fn's type parameters) is not swept in. fn infer_declaration_binder_edge(parent: Node, edge: Edge) -> Bool { declaration_binder_edge(parent: parent, edge: edge) @@ -3622,15 +3622,10 @@ fn infer_disj_is_named_sum(n: Node) -> Bool { // the domain's binder LABELS (v2.std.arrow_signature signature_order_edge), not values: there // is no type for a label atom to derive, so walking it left every declared Arrow's order atoms on the // frontier (infer_grounding_not_derived) and the Arrow itself NotDerived. The Arrow carries the edge -// as its own evidence (infer_product_child_evidence_edges), and this step takes nothing from its subtree -- -// the same shape as infer_arrow_empty_domain_edge and the literal payload arm, where the parent's -// model, not the child's walk, says what the child is. -fn infer_arrow_signature_order_edge(parent: Node, edge: Edge) -> Bool { - match parent.kind { - TypeNode { connective: Arrow } => (edge_label_of(e: edge) == arrow_signature_order_label) - _ => false - } -} +// as its own evidence (infer_product_child_evidence_edges), and the gather step below takes nothing +// from its subtree -- the same shape as infer_arrow_empty_domain_edge and the literal payload arm, where +// the parent's model, not the child's walk, says what the child is. The edge is classified by +// v2.std.node arrow_signature_order_edge, the one predicate std.kind's roster index also asks. // A MATCH ARM'S PATTERN IS A BINDING FORM, NOT A VALUE, so this step carries its edge the way it // carries a declaration's binders (v2.std.node match_arm_pattern_edge). A fielded pattern is the @@ -3648,7 +3643,7 @@ fn infer_gather_fold_step( ) -> InferGatherFoldAcc { if acc.failed { acc - } else if infer_arrow_signature_order_edge(parent: acc.node, edge: edge) + } else if arrow_signature_order_edge(parent: acc.node, edge: edge) || infer_declaration_binder_edge(parent: acc.node, edge: edge) || match_arm_pattern_edge(parent: acc.node, edge: edge) || (resolved_reference_body_kind(target: acc.node) != NotMarkedReference) { diff --git a/src/v2/std/node.dag b/src/v2/std/node.dag index 48c15ad9984..d87395644e2 100644 --- a/src/v2/std/node.dag +++ b/src/v2/std/node.dag @@ -565,6 +565,17 @@ fn arrow_named_edge_is_non_binder(e: Edge) -> Bool { } } +// WHETHER AN EDGE IS AN ARROW'S DECLARED ORDER: label metadata (the domain's binder labels), not a value +// the Arrow is built from. The one classification every reader that walks values through an Arrow asks +// -- v2.compiler.infer (its gather fold and product evidence) and std.kind's roster-kind index -- so +// no reader keeps its own list of metadata labels. +fn arrow_signature_order_edge(parent: Node, edge: Edge) -> Bool { + match parent.kind { + TypeNode { connective: Arrow } => (edge_label_of(e: edge) == arrow_signature_order_label) + _ => false + } +} + fn arrow_signature_edges_conform(children: List) -> Bool { let binder_edges = fold(children, init: 0, f: fn(acc, e) { match e.label { diff --git a/src/v2/test/claim/execution/infer_product_introduction_test.dag b/src/v2/test/claim/execution/infer_product_introduction_test.dag index 4ed286ee446..362f8523446 100644 --- a/src/v2/test/claim/execution/infer_product_introduction_test.dag +++ b/src/v2/test/claim/execution/infer_product_introduction_test.dag @@ -3,12 +3,19 @@ module v2.test.execution.infer_product_introduction import v2.test.lens_common.infer_fixture { claim_resolved_tree_without_declarations } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } -import v2.compiler.infer { DerivedGrounding, GroundingNotDerived, InferredTree } +import v2.compiler.infer { + DerivedGrounding, + GroundingNotDerived, + InferredTree, + infer_language_inhabitants_kind_index, + infer_node_declared_in_language_inhabitants +} import v2.compiler.self_host.direct_rust_door_fixture { direct_rust_door_specimen_inferred } import std.kind { TypeDenotationKind, kind_node } import v2.extdeps.languages.dag { + dag_fixture_emitted_add_fn, dag_int_inhabitant_node } import v2.std.algebra { fold_list } @@ -26,9 +33,10 @@ import v2.std.node { Named, Node, TypeNode, + arrow_signature_order_edge, node_subtree_nodes } -import v2.std.optional { Absent, Present } +import v2.std.optional { Absent, Optional, Present, optional_present } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -256,3 +264,57 @@ test fn product_introduction_leaves_partially_evidenced_conj_on_the_frontier_hol && (product_introduction_hand_tree_grounding(tree: partial, n: frontier_child) == 1) && (product_introduction_hand_tree_grounding(tree: partial, n: partial) == 1) } + +// ROSTER MEMBERSHIP IS OVER THE ROSTER'S VALUES, NOT ITS LABEL METADATA (std.kind roster_member_nodes). +// gunbc#12625 rebuilt the dag roster's add fn through anonymous_signature_arrow, whose declared-order +// edge lists the domain's binder labels as a FreeMonoid ending in a synthetic childless Conj; the +// roster index walked that edge, so every bare childless Conj became a TypeDenotationKind member and +// derived a grounding by lookup (the red above, and four more rows of gunbc#12860). The order edge is +// classified by v2.std.node arrow_signature_order_edge, the predicate infer's gather fold asks. +fn ipi_is_roster_member(n: Node) -> Bool { + match infer_node_declared_in_language_inhabitants(kinds: infer_language_inhabitants_kind_index(), n: n) { + Present { value: _ } => true + Absent => false + } +} + +fn ipi_order_target_step(acc: Optional, e: Edge) -> Optional { + if arrow_signature_order_edge(parent: dag_fixture_emitted_add_fn, edge: e) { optional_present(value: e.target) } else { acc } +} + +fn ipi_add_fn_order_target() -> Optional { + fold_list( + xs: dag_fixture_emitted_add_fn.children, + empty: Absent, + cons: fn(acc, e) { ipi_order_target_step(acc: acc, e: e) } + ) +} + +// RED: a bare synthetic childless Conj is not a member of any closed-ingest-set roster. +test fn a_bare_childless_conj_is_not_a_roster_member_holds() -> Bool { + ipi_is_roster_member(n: Node { kind: TypeNode { connective: Conj }, children: [], occurrence_id: OccurrenceSynthetic }) == false +} + +// RED: the add fn's declared-order label list is metadata, not a member. +test fn the_declared_order_label_list_is_not_a_roster_member_holds() -> Bool { + match ipi_add_fn_order_target() { + Absent => false + Present { value: order } => ipi_is_roster_member(n: order) == false + } +} + +// CONTROL: a genuine roster member still derives its kind -- the add fn Arrow itself. +test fn the_roster_add_fn_is_still_a_roster_member_holds() -> Bool { + ipi_is_roster_member(n: dag_fixture_emitted_add_fn) +} + +// CONTROL: a payload edge into the roster is still walked -- the add fn's domain, reached only +// through the Arrow's value edge, is a member. +test fn the_add_fn_domain_through_a_payload_edge_is_a_roster_member_holds() -> Bool { + match list_at_optional(xs: dag_fixture_emitted_add_fn.children, index: 0) { + Absent => false + Present { value: domain_edge } => + (arrow_signature_order_edge(parent: dag_fixture_emitted_add_fn, edge: domain_edge) == false) + && ipi_is_roster_member(n: domain_edge.target) + } +} diff --git a/src/v2/test/claim/type_param_binder_frame_test.dag b/src/v2/test/claim/type_param_binder_frame_test.dag index 358c73e5de1..f9f0ed1cdac 100644 --- a/src/v2/test/claim/type_param_binder_frame_test.dag +++ b/src/v2/test/claim/type_param_binder_frame_test.dag @@ -330,16 +330,35 @@ test fn tpb_distinct_type_variables_do_not_alias() -> Bool { } } -// (12) The type variable is the callee's OWN: an Arrow declaring no `T` still judges `x: T` as the -// ordinary declared type, and the Int argument refuses. +// (12) The type variable is the callee's OWN: an Arrow declaring no `T` still judges `x: T` as an +// ordinary declared type, never instantiating it. RE-STATED 2026-10-01 against gunbc#12566 (bisected: +// green at its parent, red at it), which routes every declared position through +// infer_declared_position_undecidable_reason: a declared atom that denotes no value type and is not +// one of the callee's type variables is counted UndecidableFormalUnresolved on the Accepted path, +// "never refused for the spelling and never admitted silently". So `T` no longer refuses the Int as +// the structural atom `T`; the evidence that it was not taken as a type variable is that it was +// judged at all -- an instantiated variable carries no undecidable advisory (the twin below). test fn tpb_undeclared_t_is_not_a_type_variable() -> Bool { match infer(tree: claim_resolved_tree_without_declarations(root: tpb_apply( arrow: tpb_generic_arrow(type_params: [^U], formals: [tpb_formal(name: ^x, declared: ^T)]), args: [dag_int_literal_fixture_one()] ))) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: d } => - diagnostics_has_reason(d: Some { diagnostics: d }, reason: ^application_argument_does_not_inhabit) + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: d } => + diagnostics_has_reason(d: d, reason: ^inhabitance_undecidable_formal_unresolved) + } +} + +// THE TWIN THAT MAKES (12) DISCRIMINATE: the same application with `T` declared as the callee's type +// parameter instantiates it from the Int argument and carries no undecidable-formal advisory. +test fn tpb_declared_t_is_instantiated_not_judged_unresolved() -> Bool { + match infer(tree: claim_resolved_tree_without_declarations(root: tpb_apply( + arrow: tpb_generic_arrow(type_params: [^T], formals: [tpb_formal(name: ^x, declared: ^T)]), + args: [dag_int_literal_fixture_one()] + ))) { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: d } => + diagnostics_has_reason(d: d, reason: ^inhabitance_undecidable_formal_unresolved) == false } }