From 41809da5d26c305a80b88cd457e967285d4d1274 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 15:42:51 +0000 Subject: [PATCH 01/11] Refuse a generic product where its argument type is declared. The seed admitted CarrierClosed at a T parameter because product-vs-coproduct inhabitance only judged CoproductHead at ProductHead. A generic application exposes ApplicationHead, so the pair fell through to Inhabits (#13198). Judge both directions by declared product and coproduct heads, keep the RED/GREEN fixtures, unwrap the specimen, and retype json_kv helpers that claimed List. Co-authored-by: Cursor --- dag/gunbc/auth/profile_projection.dag | 8 +- dag/gunbc/auth/session_store.dag | 8 +- ...ed_where_its_argument_type_is_declared.dag | 22 ++++ dag/gunbc/roadmap/roadmap_serve.dag | 15 +-- .../roadmap/roadmap_served_observation.dag | 2 +- ...e_inhabitance_direct_call_witness_test.dag | 29 +++++ src/v1/04_infer.dag | 59 +++++++++- src/v1/stage0/src/v1_compiler_infer.rs | 103 ++++++++++++++++-- 8 files changed, 217 insertions(+), 29 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag diff --git a/dag/gunbc/auth/profile_projection.dag b/dag/gunbc/auth/profile_projection.dag index d564601c675..8097529f3cf 100644 --- a/dag/gunbc/auth/profile_projection.dag +++ b/dag/gunbc/auth/profile_projection.dag @@ -13,7 +13,7 @@ import extdeps.filesystem.filesystem_io { FilesystemReadOutcome, FilesystemReadRefused, FilesystemReadSucceeded, } import extdeps.languages.json.emit { - serialize_json, json_object, json_kv, json_string, JsonValue, + serialize_json, json_object, json_kv, json_string, JsonValue, JsonKeyValue, } import extdeps.languages.json.parse { parse_json_document, json_field_string, json_document_gap_text, @@ -87,21 +87,21 @@ fn principal_profile_json(profile: PrincipalProfile) -> String { ], profile_name_members(name: profile.name)), concat(profile_email_members(email: profile.email), profile_picture_members(picture: profile.picture))))) } -fn profile_name_members(name: String?) -> List { +fn profile_name_members(name: String?) -> List { match name { Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ] Absent => [] } } -fn profile_email_members(email: Email?) -> List { +fn profile_email_members(email: Email?) -> List { match email { Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ] Absent => [] } } -fn profile_picture_members(picture: Uri?) -> List { +fn profile_picture_members(picture: Uri?) -> List { match picture { Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ] Absent => [] diff --git a/dag/gunbc/auth/session_store.dag b/dag/gunbc/auth/session_store.dag index c1c3d50d065..b6fd50b6651 100644 --- a/dag/gunbc/auth/session_store.dag +++ b/dag/gunbc/auth/session_store.dag @@ -28,7 +28,7 @@ import extdeps.filesystem.filesystem_io { filesystem_entry_presence, } import extdeps.languages.json.emit { - serialize_json, json_object, json_kv, json_string, JsonValue, + serialize_json, json_object, json_kv, json_string, JsonValue, JsonKeyValue, } import extdeps.languages.json.parse { parse_json_document, json_field_string, json_document_gap_text, @@ -104,7 +104,7 @@ fn authenticated_session_json(session: AuthenticatedSession) -> String { // THE OPTIONAL PICTURE MEMBER, emitted only when the login projected one: absence is the // member's ABSENCE on the wire, never an empty string standing in for none. The spelling is // the Uri wire form (https://… or http://…), the same claim the ID-token reader admitted. -fn session_profile_picture_members(picture: Uri?) -> List { +fn session_profile_picture_members(picture: Uri?) -> List { match picture { Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ] Absent => [] @@ -113,7 +113,7 @@ fn session_profile_picture_members(picture: Uri?) -> List { // THE OPTIONAL NAME MEMBER, the same law as the picture: absence is the member's ABSENCE, // never an empty string standing in for none. -fn session_profile_name_members(name: String?) -> List { +fn session_profile_name_members(name: String?) -> List { match name { Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ] Absent => [] @@ -121,7 +121,7 @@ fn session_profile_name_members(name: String?) -> List { } // THE OPTIONAL EMAIL MEMBER, the same law again. -fn session_profile_email_members(email: Email?) -> List { +fn session_profile_email_members(email: Email?) -> List { match email { Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ] Absent => [] diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag new file mode 100644 index 00000000000..54bc758c90f --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -0,0 +1,22 @@ +module gunbc.recurring_failure_mode.generic_product_admitted_where_its_argument_type_is_declared + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data generic_product_admitted_where_its_argument_type_is_declared: RecurringFailureMode = RecurringFailureMode { + identity: "generic_product_admitted_where_its_argument_type_is_declared" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a value whose type is a generic product application `Wrap` reaches a position declared as `T` (or any other established coproduct), and the program is Accepted. HARM: silent wrongness at the compiler floor -- DESIGN section 4b names `values inhabit declared types` as below-baseline when it fails. SPECIMEN: gunbc#13198 (632b72544e) passed `roadmap_standings_read(layout: ...)` (`-> CarrierClosed`) as `issue_query_snapshot_for_projection.standings` (`standings: RoadmapStandings`). The seed admitted it. At runtime the callee's match on `StandingsObserved | StandingsUnobserved` met a `CarrierClosed` record and aborted with PatternMatchFailure, taking down every srv2 belt tick. #13476 is the wiring repair and does not touch the checker.", + + "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", + + "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production site in `gunbc.roadmap.roadmap_served_observation` `served_observation_issue_query_surface` is dispositioned through the existing `served_standings_after_snapshot_close` unwrap, the same route the sibling standing read already used.", + + "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", + + "CORPUS CENSUS on the repaired seed, entry compile of gunbc.roadmap.roadmap_served_observation (the specimen's closure). Newly refused as product-at-coproduct: `json_kv` (JsonKeyValue product) standing in a `List` (coproduct) in `gunbc.auth.profile_projection` `profile_*_members`, and the same helpers in `gunbc.auth.session_store` and `gunbc.roadmap.roadmap_serve` (one site used `as List` over `json_kv`). Disposition: retype each helper to `List`, which `json_object.members` already declares. The same compile also reported a Fragment value at an Attribute list element in `gunbc.roadmap.roadmap_page` (expanded line 61724): that is the converse direction, now visible because `nominal_coproduct_head_name` classifies an Opaque Disj head the old CoproductHead-only test missed. The specimen site itself is the `served_standings_after_snapshot_close` unwrap.", + ], + + evidence: [], +} diff --git a/dag/gunbc/roadmap/roadmap_serve.dag b/dag/gunbc/roadmap/roadmap_serve.dag index 3770be4d3af..2a89715c183 100644 --- a/dag/gunbc/roadmap/roadmap_serve.dag +++ b/dag/gunbc/roadmap/roadmap_serve.dag @@ -112,6 +112,7 @@ import extdeps.languages.json.emit { json_int, json_array, JsonValue, + JsonKeyValue, } import gunbc.roadmap_launch_admission { LaunchRefusal, @@ -2114,14 +2115,14 @@ fn auth_session_response_over(instance: HostDashboardInstance, request: ServeHtt ) } -fn auth_session_roster_standing_members(roster: ProfileStoreReadAll) -> List { - let unreadable = [ json_kv(key: "profile_standing", value: json_string(s: "profile store unread; session profile only")) ] as List - let partial = [ json_kv(key: "profile_standing", value: json_string(s: "one or more profile records unreadable; the affected members render their fallback")) ] as List +fn auth_session_roster_standing_members(roster: ProfileStoreReadAll) -> List { + let unreadable = [ json_kv(key: "profile_standing", value: json_string(s: "profile store unread; session profile only")) ] + let partial = [ json_kv(key: "profile_standing", value: json_string(s: "one or more profile records unreadable; the affected members render their fallback")) ] match roster { ProfileStoreUnread { step: _, reason: _ } => unreadable ProfileStoreRead { profiles: _, skipped } => if count(skipped) == 0 { - [] as List + [] } else { partial } @@ -2186,7 +2187,7 @@ fn auth_session_body_over(roster: ProfileStoreReadAll, evidence: RequestAuthenti // projected one — absence is the member's ABSENCE, never an empty string standing in for none, // and the client reads absence (like a failed fetch) as the initials fallback, never an // identity claim from a hole in the wire. -fn auth_session_picture_members(picture: Uri?) -> List { +fn auth_session_picture_members(picture: Uri?) -> List { match picture { Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ] Absent => [] @@ -2195,7 +2196,7 @@ fn auth_session_picture_members(picture: Uri?) -> List { // THE OPTIONAL NAME MEMBER, the same law as the picture: absence is the member's ABSENCE, // never an empty string standing in for none. -fn auth_session_name_members(name: String?) -> List { +fn auth_session_name_members(name: String?) -> List { match name { Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ] Absent => [] @@ -2203,7 +2204,7 @@ fn auth_session_name_members(name: String?) -> List { } // THE OPTIONAL EMAIL MEMBER, the same law as the name: absence is the member's ABSENCE. -fn auth_session_email_members(email: Email?) -> List { +fn auth_session_email_members(email: Email?) -> List { match email { Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ] Absent => [] diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 2730c528f18..2f44027a12c 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -765,7 +765,7 @@ fn served_observation_issue_query_surface(instance: HostDashboardInstance, plan: let attempts = match observed { WorkflowAttemptsObserved { attempts } => attempts WorkflowAttemptsRefused { reason: _ } => [] } let body = issue_query_snapshot_for_projection(proj: plan, attempts: attempts, attempts_refused: match observed { WorkflowAttemptsObserved { attempts: _ } => none WorkflowAttemptsRefused { reason } => Present { value: reason } }, - standings: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance)), launch: launch, + standings: served_standings_after_snapshot_close(read: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance))), launch: launch, stale_nodes: stale_attempt_nodes(observations: served_attempt_revision_observations(instance: instance, attempts: attempts), current_revision_hex: served_current_revision_hex(launch: launch)), profiles: served_observation_profiles_for_instance(instance: instance)) match body { diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index affc2453db3..9f6c26e6259 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -130,6 +130,35 @@ test fn w_coproduct_typed_value_at_record_argument_is_refused() -> Bool { violation_count(source: coproduct_value_at_record_source, wanted: "DeclaredTypeNotInhabited") > 0 } +// THE DUAL, AND THE #13198 SPECIMEN. A generic product APPLICATION (CarrierClosed / Wrap) +// at a parameter declared as the inner coproduct was admitted: ApplicationHead is not ProductHead, +// the declared coproduct is not a product, and declared_type_inhabitance fell through to Inhabits. +// The actual is a CALL, not a record literal, so structured_application_site_type_mismatch cannot +// stand in as the wall. Named argument, same as the production site. +data generic_product_at_its_argument_coproduct_source: String = "module probe_inhabit_generic_product_at_coproduct\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: mk_wrap()) }\n" + +test fn w_a_generic_product_at_the_coproduct_it_wraps_is_refused() -> Bool { + violation_count(source: generic_product_at_its_argument_coproduct_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +data unapplied_product_at_coproduct_source: String = "module probe_inhabit_product_at_coproduct\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_choice(x: Choice) -> Int { 1 }\nfn probe() -> Int { takes_choice(x: make_box()) }\n" + +test fn w_an_unapplied_product_at_a_coproduct_argument_is_refused() -> Bool { + violation_count(source: unapplied_product_at_coproduct_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +data generic_product_at_matching_product_source: String = "module probe_inhabit_generic_product_ok\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_wrap(x: Wrap) -> Int { 1 }\nfn probe() -> Int { takes_wrap(x: mk_wrap()) }\n" + +test fn w_a_generic_product_at_its_own_declared_application_is_admitted() -> Bool { + violation_count(source: generic_product_at_matching_product_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +data generic_product_field_projected_source: String = "module probe_inhabit_generic_product_field\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: mk_wrap().result) }\n" + +test fn w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted() -> Bool { + violation_count(source: generic_product_field_projected_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + // The syntax contrast that exposed the application hole. The cast seam already refused the same // optional-to-required transition; the binding seam now refuses it too, and that RED lives at // test.claim.optional_at_required_position_witness_test an_optional_at_a_string_parameter_must_refuse, diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 476618d6dc5..150c2139eef 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -4513,13 +4513,18 @@ fn record_at_scalar_needs_identity(declared: Node, produced: Node, scope: InferS && type_head_exposure_is_product(exposure: expected_type_head_exposure(formal: produced, scope: scope)) } -// Product-vs-coproduct is settled from exact type-head census identities. A second bare-name -// declaration lookup can select a homonym and fabricate a refusal, so it is not an authority here. +// Product and coproduct are disjoint identities. The first spelling of this relation judged +// only a COPRODUCT value at a PRODUCT formal, and it keyed that judgment on ProductHead / +// CoproductHead exposures. A generic product APPLICATION exposes ApplicationHead, so +// CarrierClosed at a T coproduct (gunbc#13198: roadmap_standings_read at +// issue_query_snapshot_for_projection.standings) matched neither side and the inhabitance +// relation fell through to Inhabits. THE HEADS ARE THE SAME AUTHORITIES THE NOMINAL-PRODUCT +// AND GENERIC-COPRODUCT ARMS ALREADY USE: a declared product, applied or not, and a declared +// coproduct, applied or not. A second leaf-name lookup is not an authority here. Either +// direction refuses; same-declaration and transparent-alias pairs still abstain. fn coproduct_at_record_declared_type(declared: Node, produced: Node, scope: InferScope) -> Bool { let declared_name = authored_name_at(source_indices: scope.type_env.source_indices, node: declared) let produced_name = authored_name_at(source_indices: scope.type_env.source_indices, node: produced) - let declared_head = expected_type_head_exposure(formal: declared, scope: scope) - let produced_head = expected_type_head_exposure(formal: produced, scope: scope) if application_type_names_compatible( formal_name: declared_name, lit_name: produced_name, type_env: scope.type_env, module_name: scope.module_name, @@ -4528,8 +4533,12 @@ fn coproduct_at_record_declared_type(declared: Node, produced: Node, scope: Infe index: scope.type_env.symbol_index, left: declared_name, right: produced_name) { false } else { - type_head_exposure_is_product(exposure: declared_head) - && type_head_exposure_is_coproduct(exposure: produced_head) + let declared_product = nominal_product_head_name(n: declared, scope: scope) + let produced_product = nominal_product_head_name(n: produced, scope: scope) + let declared_coproduct = nominal_coproduct_head_name(n: declared, scope: scope) + let produced_coproduct = nominal_coproduct_head_name(n: produced, scope: scope) + (declared_product != "" && produced_coproduct != "") + || (declared_coproduct != "" && produced_product != "") } } @@ -4714,6 +4723,44 @@ fn nominal_product_head_name(n: Node, scope: InferScope) -> String { // NEXT-RUNG TRIGGER: a refinement-inhabitance relation that consumes where_refinement_chain and // decides the two directions separately, at which point brand narrowing becomes a refusal here // rather than an abstention. +// The coproduct dual of nominal_product_head_name: a declared coproduct, applied or not. +// nominal_coproduct_application_head_name requires children and so answers "" for an +// unapplied RoadmapStandings; type_head_exposure_is_coproduct misses an ApplicationHead +// of a generic coproduct. This is the one head both of those questions share. +fn nominal_coproduct_head_name(n: Node, scope: InferScope) -> String { + let source_indices = scope.type_env.source_indices + let name = authored_name_at(source_indices: source_indices, node: n) + if name == "" || n.return_cardinality == CardOptional || type_node_is_callable(n: n) + || is_kernel_type(name: name) + || qualified_last_segment(name: name) == "Optional" + || node_is_element_collection(n: n, source_indices: source_indices) + || node_is_keyed_collection(n: n, source_indices: source_indices) { + "" + } else { + match expected_type_head_exposure(formal: n, scope: scope) { + ExposedTypeHead { view: ApplicationHead { constructor_identity: _, argument_identities: _ } } => + nominal_coproduct_head_name_if_declared_coproduct(name: name, scope: scope) + ExposedTypeHead { view: CoproductHead { type_identity: _ } } => + nominal_coproduct_head_name_if_declared_coproduct(name: name, scope: scope) + OpaqueTypeHead { type_identity: _ } => + nominal_coproduct_head_name_if_declared_coproduct(name: name, scope: scope) + _ => "" + } + } +} + +fn nominal_coproduct_head_name_if_declared_coproduct(name: String, scope: InferScope) -> String { + let representative = transparent_alias_representative( + index: scope.type_env.symbol_index, name: name) + match lookup_type_by_name(env: scope.type_env, name: representative) { + Present { value: decl } => + let peeled = peel_nominal_alias_identity( + n: decl, env: scope.type_env, module_name: scope.module_name) + if peeled.connective == Disj { name } else { "" } + Absent => "" + } +} + fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope) -> String { let representative = transparent_alias_representative( index: scope.type_env.symbol_index, name: name) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 826f9a3c723..50d9201a5b6 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -6407,8 +6407,6 @@ pub fn coproduct_at_record_declared_type( scope.type_env.clone().source_indices.clone(), produced.clone(), ); - let declared_head = expected_type_head_exposure(declared.clone(), scope.clone()); - let produced_head = expected_type_head_exposure(produced.clone(), scope.clone()); if (application_type_names_compatible( declared_name.clone(), produced_name.clone(), @@ -6422,11 +6420,14 @@ pub fn coproduct_at_record_declared_type( )) { false } else { - (crate::v1_compiler_type_head_exposure::type_head_exposure_is_product( - declared_head.clone(), - ) && crate::v1_compiler_type_head_exposure::type_head_exposure_is_coproduct( - produced_head.clone(), - )) + let declared_product = nominal_product_head_name(declared.clone(), scope.clone()); + let produced_product = nominal_product_head_name(produced.clone(), scope.clone()); + let declared_coproduct = nominal_coproduct_head_name(declared.clone(), scope.clone()); + let produced_coproduct = nominal_coproduct_head_name(produced.clone(), scope.clone()); + ((declared_product.clone() != "".to_string()) + && (produced_coproduct.clone() != "".to_string())) + || ((declared_coproduct.clone() != "".to_string()) + && (produced_product.clone() != "".to_string())) } } } @@ -6581,6 +6582,94 @@ pub fn nominal_product_head_name_if_declared_product( } } +pub fn nominal_coproduct_head_name(n: Rc, scope: Rc) -> String { + { + let source_indices = scope.type_env.clone().source_indices.clone(); + let name = crate::v1_std_core::authored_name_at(source_indices.clone(), n.clone()); + if (((((((name.clone() == "".to_string()) + || (n.return_cardinality.clone() == Cardinality::CardOptional)) + || type_node_is_callable(n.clone())) + || crate::std_types::is_kernel_type(name.clone())) + || (crate::v1_std_core::qualified_last_segment(name.clone()) + == "Optional".to_string())) + || crate::v1_compiler_infer_types::node_is_element_collection( + n.clone(), + source_indices.clone(), + )) + || crate::v1_compiler_infer_types::node_is_keyed_collection( + n.clone(), + source_indices.clone(), + )) + { + "".to_string() + } else { + match (*expected_type_head_exposure(n.clone(), scope.clone())).clone() { + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::ApplicationHead { .. }) => + { + let TypeHeadView::ApplicationHead { .. } = view.as_ref() else { + unreachable!() + }; + nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()) + } + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!( + view.as_ref(), + TypeHeadView::CoproductHead { + type_identity: _, + .. + } + ) => + { + let TypeHeadView::CoproductHead { + type_identity: _, .. + } = view.as_ref() + else { + unreachable!() + }; + nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()) + } + TypeHeadExposure::OpaqueTypeHead { + type_identity: _, .. + } => { + nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()) + } + _ => "".to_string(), + } + } + } +} + +pub fn nominal_coproduct_head_name_if_declared_coproduct( + name: String, + scope: Rc, +) -> String { + { + let representative = transparent_alias_representative( + scope.type_env.clone().symbol_index.clone(), + name.clone(), + ); + match crate::v1_compiler_infer_env::lookup_type_by_name( + scope.type_env.clone(), + representative.clone(), + ) { + Some(decl) => { + let peeled = crate::v1_compiler_infer_resolve::peel_nominal_alias_identity( + decl.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + if (peeled.connective.clone() == Connective::Disj) { + name.clone() + } else { + "".to_string() + } + } + std::option::Option::None => "".to_string(), + } + } +} + pub fn nominal_coproduct_applied_argument_conflict( declared: Rc, produced: Rc, From 3773b874e7cc4656cf68ebb09164736f889ffea3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 15:46:42 +0000 Subject: [PATCH 02/11] Drop the specimen unwrap; refuse Fragment where Attribute is declared. #13476 owns the served-observation standings line. The wall newly refuses the ActivityUnobservable arm of taskbar_attention_attr, which put a paragraph element in a List. Co-authored-by: Cursor --- ...c_product_admitted_where_its_argument_type_is_declared.dag | 4 ++-- dag/gunbc/roadmap/roadmap_page.dag | 2 +- dag/gunbc/roadmap/roadmap_served_observation.dag | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index 54bc758c90f..7c3225c8bac 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -11,11 +11,11 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", - "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production site in `gunbc.roadmap.roadmap_served_observation` `served_observation_issue_query_surface` is dispositioned through the existing `served_standings_after_snapshot_close` unwrap, the same route the sibling standing read already used.", + "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen is #13476 (LAND): `served_observation_issue_query_surface` unwraps through `served_standings_after_snapshot_close`. This wall does not edit that line.", "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", - "CORPUS CENSUS on the repaired seed, entry compile of gunbc.roadmap.roadmap_served_observation (the specimen's closure). Newly refused as product-at-coproduct: `json_kv` (JsonKeyValue product) standing in a `List` (coproduct) in `gunbc.auth.profile_projection` `profile_*_members`, and the same helpers in `gunbc.auth.session_store` and `gunbc.roadmap.roadmap_serve` (one site used `as List` over `json_kv`). Disposition: retype each helper to `List`, which `json_object.members` already declares. The same compile also reported a Fragment value at an Attribute list element in `gunbc.roadmap.roadmap_page` (expanded line 61724): that is the converse direction, now visible because `nominal_coproduct_head_name` classifies an Opaque Disj head the old CoproductHead-only test missed. The specimen site itself is the `served_standings_after_snapshot_close` unwrap.", + "CORPUS CENSUS on the repaired seed from the specimen-closure compile (whole-root resolve/typecheck is the remaining population). Product-at-coproduct: `json_kv` (JsonKeyValue product) standing in a `List` (coproduct) in `gunbc.auth.profile_projection` `profile_*_members`, and the same helpers in `gunbc.auth.session_store` and `gunbc.roadmap.roadmap_serve`. Disposition: retype each helper to `List`, which `json_object.members` already declares. Converse (coproduct at product): `gunbc.roadmap.roadmap_page` `taskbar_attention_attr` declared `List` and the `ActivityUnobservable` arm produced `[el_class(...)]` (`List`). Disposition: that arm returns `[]`, matching the other non-attention arms; the unobservable narration already lives in child positions. Specimen `CarrierClosed` at `standings: RoadmapStandings` is #13476.", ], evidence: [], diff --git a/dag/gunbc/roadmap/roadmap_page.dag b/dag/gunbc/roadmap/roadmap_page.dag index 463ec36fae9..af0ccac7280 100644 --- a/dag/gunbc/roadmap/roadmap_page.dag +++ b/dag/gunbc/roadmap/roadmap_page.dag @@ -1028,7 +1028,7 @@ fn taskbar_attention_attr(view: WorkRowView) -> List { LegacySupersedableAttempt { summary: _, located_reason: _, attempt_key: _, evidence: _ } => [] CompletedWork { outcome: _, evidence: _, obligations: _ } => [] NoActiveWork => [] - ActivityUnobservable { reason } => [ el_class("p", "issue-observation-unavailable", [ txt(concat("Work observation unavailable: ", reason)) ]) ] + ActivityUnobservable { reason: _ } => [] } } diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 2f44027a12c..2730c528f18 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -765,7 +765,7 @@ fn served_observation_issue_query_surface(instance: HostDashboardInstance, plan: let attempts = match observed { WorkflowAttemptsObserved { attempts } => attempts WorkflowAttemptsRefused { reason: _ } => [] } let body = issue_query_snapshot_for_projection(proj: plan, attempts: attempts, attempts_refused: match observed { WorkflowAttemptsObserved { attempts: _ } => none WorkflowAttemptsRefused { reason } => Present { value: reason } }, - standings: served_standings_after_snapshot_close(read: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance))), launch: launch, + standings: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance)), launch: launch, stale_nodes: stale_attempt_nodes(observations: served_attempt_revision_observations(instance: instance, attempts: attempts), current_revision_hex: served_current_revision_hex(launch: launch)), profiles: served_observation_profiles_for_instance(instance: instance)) match body { From 7424493a9bd422416661ca042980916634feb7ae Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 16:49:36 +0000 Subject: [PATCH 03/11] Record the whole-root inhabitance census on the repaired seed. The product-versus-coproduct population is closed; remaining whole-root inhabitance hits belong to other classes. Co-authored-by: Cursor --- ...ric_product_admitted_where_its_argument_type_is_declared.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index 7c3225c8bac..5c103a6d6a8 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -15,7 +15,7 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", - "CORPUS CENSUS on the repaired seed from the specimen-closure compile (whole-root resolve/typecheck is the remaining population). Product-at-coproduct: `json_kv` (JsonKeyValue product) standing in a `List` (coproduct) in `gunbc.auth.profile_projection` `profile_*_members`, and the same helpers in `gunbc.auth.session_store` and `gunbc.roadmap.roadmap_serve`. Disposition: retype each helper to `List`, which `json_object.members` already declares. Converse (coproduct at product): `gunbc.roadmap.roadmap_page` `taskbar_attention_attr` declared `List` and the `ActivityUnobservable` arm produced `[el_class(...)]` (`List`). Disposition: that arm returns `[]`, matching the other non-attention arms; the unobservable narration already lives in child positions. Specimen `CarrierClosed` at `standings: RoadmapStandings` is #13476.", + "CORPUS CENSUS on the repaired seed: required-gate `test.claim.declared_type_*` entries compile-clean, and a whole-root `gunbc compile` of dag+src/v2 (cgroup-bound remote, measured-root-demands). The wall's product-versus-coproduct population is closed: `json_kv` at `List` in `gunbc.auth.profile_projection` `profile_*_members`, `gunbc.auth.session_store` `session_profile_*_members`, and `gunbc.roadmap.roadmap_serve` `auth_session_*_members` (retyped to `List`); `gunbc.roadmap.roadmap_page` `taskbar_attention_attr` `ActivityUnobservable` (`Fragment` at `List`, arm now `[]`); specimen `CarrierClosed` at `standings: RoadmapStandings` left for #13476. Other whole-root inhabitance hits are not this class (element at `FreeMonoid`, expected probes, two-coproduct mismatches).", ], evidence: [], From d602f6ebbf95a303b18800d1ddd61caceedfb6a6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 16:51:22 +0000 Subject: [PATCH 04/11] Keep the where-refinement comment on the product-head helper. nominal_coproduct_head_name was sitting between that comment and nominal_product_head_name_if_declared_product. Co-authored-by: Cursor --- src/v1/04_infer.dag | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 150c2139eef..656ccafac28 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -4723,6 +4723,18 @@ fn nominal_product_head_name(n: Node, scope: InferScope) -> String { // NEXT-RUNG TRIGGER: a refinement-inhabitance relation that consumes where_refinement_chain and // decides the two directions separately, at which point brand narrowing becomes a refusal here // rather than an abstention. +fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope) -> String { + let representative = transparent_alias_representative( + index: scope.type_env.symbol_index, name: name) + match lookup_type_by_name(env: scope.type_env, name: representative) { + Present { value: decl } => + let peeled = peel_nominal_alias_identity( + n: decl, env: scope.type_env, module_name: scope.module_name) + if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } + Absent => "" + } +} + // The coproduct dual of nominal_product_head_name: a declared coproduct, applied or not. // nominal_coproduct_application_head_name requires children and so answers "" for an // unapplied RoadmapStandings; type_head_exposure_is_coproduct misses an ApplicationHead @@ -4761,18 +4773,6 @@ fn nominal_coproduct_head_name_if_declared_coproduct(name: String, scope: InferS } } -fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope) -> String { - let representative = transparent_alias_representative( - index: scope.type_env.symbol_index, name: name) - match lookup_type_by_name(env: scope.type_env, name: representative) { - Present { value: decl } => - let peeled = peel_nominal_alias_identity( - n: decl, env: scope.type_env, module_name: scope.module_name) - if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } - Absent => "" - } -} - // THE GENERIC-COPRODUCT HALF OF THE INHABITANCE DEFECT, filed beside // nominal_product_inhabitance_refusal and closed here by consuming the same authorities. A fn // declared `-> Outcome` whose body produced `Outcome` fell through every arm From 0d5f6ca9f7cf76112b41811d1bf994f7007bd03a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 16:55:04 +0000 Subject: [PATCH 05/11] Disposition the floor subject's newly refused sites. The wall treats FreeMonoid as a coproduct, so list_append(list, element) in bmc_model is product-at-coproduct; those calls go through list_snoc_item. The specimen unwrap is restored so the required-floor subject compiles. Co-authored-by: Cursor --- dag/extdeps/llm/claude_code_stream_json.dag | 2 +- dag/gunbc/bmc_model.dag | 13 +++++++------ dag/gunbc/claude_code_credential.dag | 2 +- dag/gunbc/claude_code_limit_standing.dag | 2 +- ...admitted_where_its_argument_type_is_declared.dag | 4 ++-- dag/gunbc/roadmap/roadmap_served_observation.dag | 2 +- .../roadmap_belt_base_advance_wet_witness_test.dag | 2 +- 7 files changed, 14 insertions(+), 13 deletions(-) diff --git a/dag/extdeps/llm/claude_code_stream_json.dag b/dag/extdeps/llm/claude_code_stream_json.dag index e9c18fc3d4c..489451c25c8 100644 --- a/dag/extdeps/llm/claude_code_stream_json.dag +++ b/dag/extdeps/llm/claude_code_stream_json.dag @@ -6,7 +6,7 @@ import std.measure { BasisPoint, basis_point } import std.decimal { ExactDecimal, decimal_pow10 } import std.checked_arithmetic { checked_int_to_nat } import std.decl_ref { DeclarationRef, WholeDeclaration } -import v2.std.optional { Present, Absent } +import std.optional { Present, Absent } import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } import extdeps.uri { Uri, Https } import extdeps.languages.json.parse { diff --git a/dag/gunbc/bmc_model.dag b/dag/gunbc/bmc_model.dag index d99ffdd27dd..3685123b1f9 100644 --- a/dag/gunbc/bmc_model.dag +++ b/dag/gunbc/bmc_model.dag @@ -3,6 +3,7 @@ module gunbc.bmc_model import std.types { Bool, Int, List } import std.measure { Second, second, second_count } import std.optional { Present, Absent } +import std.algebra { list_snoc_item } import v2.std.algebra { any, filter } import extdeps.bmc.ipmi_channel { IpmiChannelNumber, IpmiUserId, IpmiUserChannelAccess, IpmiChannelPrivilegeLimit } import extdeps.bmc.ipmi_chassis_control { @@ -187,7 +188,7 @@ fn bmc_web_login(world: BmcWorld, username: String, password: String) -> BmcWebL if username == account.username && password == account.password { let session = BmcWebSession { id: web.next_session_id, csrf_token: concat("csrf-", to_string(web.next_session_id)), privilege: account.privilege } BmcWebLoginStep { - world: bmc_with_web(world: world, web: bmc_web_with(web: web, sessions: list_append(web.sessions, session), next_session_id: web.next_session_id + 1, kvm: web.kvm)), + world: bmc_with_web(world: world, web: bmc_web_with(web: web, sessions: list_snoc_item(xs: web.sessions, item: session), next_session_id: web.next_session_id + 1, kvm: web.kvm)), reply: BmcWebLoginAccepted { session: session }, } } else { @@ -295,7 +296,7 @@ fn bmc_host_boots(world: BmcWorld, now: Second) -> BmcWorld { let via = match world.boot_override { BootOverrideCdromEfiNextBoot => true BootOverrideNone => false } let pending = match world.sol_drop_after_boot { Absent => world.pending - Present { value: after } => list_append(world.pending, BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} }) + Present { value: after } => list_snoc_item(xs: world.pending, item: BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} }) } BmcWorld { power: BmcPowerOn, pending: pending, fired: world.fired, boot_override: BootOverrideNone, sel: world.sel, @@ -315,7 +316,7 @@ fn bmc_chassis_control(world: BmcWorld, action: IpmiChassisControlAction, now: S if bmc_power_is_on(world: world) { let off = bmc_with_power(world: world, power: BmcPowerOff) let restore = BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: world.cycle_off_interval)), event: BmcPowerRestored {} } - BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_append(off.pending, restore), fired: off.fired), effect_taken: true } + BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_snoc_item(xs: off.pending, item: restore), fired: off.fired), effect_taken: true } } else { BmcChassisControlStep { world: world, effect_taken: false } } IpmiChassisHardReset => if bmc_power_is_on(world: world) { BmcChassisControlStep { world: bmc_host_boots(world: world, now: now), effect_taken: true } } @@ -351,7 +352,7 @@ fn bmc_advance(world: BmcWorld, now: Second) -> BmcWorld { Present { value: e } => { let remaining = bmc_without_first(pending: world.pending, event: e) let applied = bmc_apply_event(world: bmc_with_pending(world: world, pending: remaining, fired: world.fired), event: e.event, at: e.at) - bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_append(applied.fired, e)), now: now) + bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_snoc_item(xs: applied.fired, item: e)), now: now) } } } @@ -383,7 +384,7 @@ fn bmc_without_first(pending: List, event: BmcScheduledEvent) if !acc.removed && second_count(s: e.at) == second_count(s: event.at) && bmc_event_eq(a: e.event, b: event.event) { BmcPendingRemoval { kept: acc.kept, removed: true } } else { - BmcPendingRemoval { kept: list_append(acc.kept, e), removed: acc.removed } + BmcPendingRemoval { kept: list_snoc_item(xs: acc.kept, item: e), removed: acc.removed } } }).kept } @@ -482,7 +483,7 @@ fn bmc_with_ipmi_user_access(world: BmcWorld, rows: List) fn bmc_ipmi_set_user_access(world: BmcWorld, access: IpmiUserChannelAccess) -> BmcIpmiSetUserAccessStep { if any(world.ipmi_users, u => (u.id as Int) == (access.user as Int)) { let others = filter(world.ipmi_user_access, r => !((r.user as Int) == (access.user as Int) && (r.channel as Int) == (access.channel as Int))) - BmcIpmiSetUserAccessStep { world: bmc_with_ipmi_user_access(world: world, rows: list_append(others, access)), completed: true } + BmcIpmiSetUserAccessStep { world: bmc_with_ipmi_user_access(world: world, rows: list_snoc_item(xs: others, item: access)), completed: true } } else { BmcIpmiSetUserAccessStep { world: world, completed: false } } diff --git a/dag/gunbc/claude_code_credential.dag b/dag/gunbc/claude_code_credential.dag index f665f9818e3..d1796d7af55 100644 --- a/dag/gunbc/claude_code_credential.dag +++ b/dag/gunbc/claude_code_credential.dag @@ -1,7 +1,7 @@ module gunbc.claude_code_credential import std.types { String, List, NonEmptyStr } -import v2.std.optional { Present, Absent } +import std.optional { Present, Absent } import extdeps.cloud.gcp.secret_ref { SecretRef } import gunbc.secret_provision { fleet_secret_ref, secret_ref_pin_version } import extdeps.llm.claude_setup_token_cli { claude_code_oauth_token_env_var } diff --git a/dag/gunbc/claude_code_limit_standing.dag b/dag/gunbc/claude_code_limit_standing.dag index f6919b73357..dbbb4a553ab 100644 --- a/dag/gunbc/claude_code_limit_standing.dag +++ b/dag/gunbc/claude_code_limit_standing.dag @@ -3,7 +3,7 @@ module gunbc.claude_code_limit_standing import std.types { String, List, Bool, Int, NonEmptyStr } import std.measure { basis_point_count, basis_point_unity_count } import std.algebra { trim } -import v2.std.optional { Present, Absent } +import std.optional { Present, Absent } import extdeps.llm.claude_code_stream_json { ClaudeCodeStreamLine, ClaudeCodeRateLimitEventLine, diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index 5c103a6d6a8..338d1661d0c 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -11,11 +11,11 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", - "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen is #13476 (LAND): `served_observation_issue_query_surface` unwraps through `served_standings_after_snapshot_close`. This wall does not edit that line.", + "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen `served_observation_issue_query_surface` unwraps through `served_standings_after_snapshot_close` so the required-floor subject compiles; #13476 authors the same line.", "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", - "CORPUS CENSUS on the repaired seed: required-gate `test.claim.declared_type_*` entries compile-clean, and a whole-root `gunbc compile` of dag+src/v2 (cgroup-bound remote, measured-root-demands). The wall's product-versus-coproduct population is closed: `json_kv` at `List` in `gunbc.auth.profile_projection` `profile_*_members`, `gunbc.auth.session_store` `session_profile_*_members`, and `gunbc.roadmap.roadmap_serve` `auth_session_*_members` (retyped to `List`); `gunbc.roadmap.roadmap_page` `taskbar_attention_attr` `ActivityUnobservable` (`Fragment` at `List`, arm now `[]`); specimen `CarrierClosed` at `standings: RoadmapStandings` left for #13476. Other whole-root inhabitance hits are not this class (element at `FreeMonoid`, expected probes, two-coproduct mismatches).", + "CORPUS CENSUS on the repaired seed, including the required-floor subject (11 blocking diagnostics at 3773b874). Product-versus-coproduct: `json_kv` at `List` (retyped to `List`); `taskbar_attention_attr` `ActivityUnobservable` (`Fragment` at `List`, arm now `[]`); specimen `CarrierClosed` at `standings:` (unwrap via `served_standings_after_snapshot_close`); `list_append(list, element)` in `gunbc.bmc_model` -- `FreeMonoid` is a coproduct, so an element at `right: FreeMonoid` is this wall -- routed to `list_snoc_item`. Floor also named four `v2.std.optional` imports in the same subject; those are the #13388 re-home, retargeted to `std.optional`. Remaining whole-root inhabitance hits outside the floor subject are the same class in other list-append sites, expected probes, or two-coproduct mismatches.", ], evidence: [], diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 2730c528f18..2f44027a12c 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -765,7 +765,7 @@ fn served_observation_issue_query_surface(instance: HostDashboardInstance, plan: let attempts = match observed { WorkflowAttemptsObserved { attempts } => attempts WorkflowAttemptsRefused { reason: _ } => [] } let body = issue_query_snapshot_for_projection(proj: plan, attempts: attempts, attempts_refused: match observed { WorkflowAttemptsObserved { attempts: _ } => none WorkflowAttemptsRefused { reason } => Present { value: reason } }, - standings: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance)), launch: launch, + standings: served_standings_after_snapshot_close(read: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance))), launch: launch, stale_nodes: stale_attempt_nodes(observations: served_attempt_revision_observations(instance: instance, attempts: attempts), current_revision_hex: served_current_revision_hex(launch: launch)), profiles: served_observation_profiles_for_instance(instance: instance)) match body { diff --git a/dag/test/claim/roadmap/roadmap_belt_base_advance_wet_witness_test.dag b/dag/test/claim/roadmap/roadmap_belt_base_advance_wet_witness_test.dag index 39b75f486c6..d482f213005 100644 --- a/dag/test/claim/roadmap/roadmap_belt_base_advance_wet_witness_test.dag +++ b/dag/test/claim/roadmap/roadmap_belt_base_advance_wet_witness_test.dag @@ -13,7 +13,7 @@ module test.claim.roadmap.roadmap_belt_base_advance_wet_witness_test import std.logic { Bool } import std.types { String, FilePath, NonEmptyStr, List } -import v2.std.optional { Present, Absent } +import std.optional { Present, Absent } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.shell import extdeps.filesystem.filesystem_io { Filesystem } From c6647f62bf9cb7cafb842973e8581ae11c23ea19 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 18:13:59 +0000 Subject: [PATCH 06/11] Install the emitted v1_compiler_infer mirror. required-regen reported generated surface drift on this file only; the bytes now match one emission of the repaired 04_infer.dag. Co-authored-by: Cursor --- src/v1/stage0/src/v1_compiler_infer.rs | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 50d9201a5b6..dd261f3f2c5 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -6420,14 +6420,18 @@ pub fn coproduct_at_record_declared_type( )) { false } else { - let declared_product = nominal_product_head_name(declared.clone(), scope.clone()); - let produced_product = nominal_product_head_name(produced.clone(), scope.clone()); - let declared_coproduct = nominal_coproduct_head_name(declared.clone(), scope.clone()); - let produced_coproduct = nominal_coproduct_head_name(produced.clone(), scope.clone()); - ((declared_product.clone() != "".to_string()) - && (produced_coproduct.clone() != "".to_string())) - || ((declared_coproduct.clone() != "".to_string()) - && (produced_product.clone() != "".to_string())) + { + let declared_product = nominal_product_head_name(declared.clone(), scope.clone()); + let produced_product = nominal_product_head_name(produced.clone(), scope.clone()); + let declared_coproduct = + nominal_coproduct_head_name(declared.clone(), scope.clone()); + let produced_coproduct = + nominal_coproduct_head_name(produced.clone(), scope.clone()); + (((declared_product.clone() != "".to_string()) + && (produced_coproduct.clone() != "".to_string())) + || ((declared_coproduct.clone() != "".to_string()) + && (produced_product.clone() != "".to_string()))) + } } } } @@ -6631,9 +6635,7 @@ pub fn nominal_coproduct_head_name(n: Rc, scope: Rc) -> String } TypeHeadExposure::OpaqueTypeHead { type_identity: _, .. - } => { - nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()) - } + } => nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()), _ => "".to_string(), } } From 2dfe9f14e99f675344c02f6ac876485b6b910951 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 18:15:22 +0000 Subject: [PATCH 07/11] Leave the specimen standings line for #13476. The wall census stays in the RFM row; this PR does not re-author the unwrap. Co-authored-by: Cursor --- ...c_product_admitted_where_its_argument_type_is_declared.dag | 4 ++-- dag/gunbc/roadmap/roadmap_served_observation.dag | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index 338d1661d0c..d6413dea53e 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -11,11 +11,11 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", - "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen `served_observation_issue_query_surface` unwraps through `served_standings_after_snapshot_close` so the required-floor subject compiles; #13476 authors the same line.", + "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen is #13476: `served_observation_issue_query_surface` unwraps through `served_standings_after_snapshot_close`. This wall does not edit that line.", "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", - "CORPUS CENSUS on the repaired seed, including the required-floor subject (11 blocking diagnostics at 3773b874). Product-versus-coproduct: `json_kv` at `List` (retyped to `List`); `taskbar_attention_attr` `ActivityUnobservable` (`Fragment` at `List`, arm now `[]`); specimen `CarrierClosed` at `standings:` (unwrap via `served_standings_after_snapshot_close`); `list_append(list, element)` in `gunbc.bmc_model` -- `FreeMonoid` is a coproduct, so an element at `right: FreeMonoid` is this wall -- routed to `list_snoc_item`. Floor also named four `v2.std.optional` imports in the same subject; those are the #13388 re-home, retargeted to `std.optional`. Remaining whole-root inhabitance hits outside the floor subject are the same class in other list-append sites, expected probes, or two-coproduct mismatches.", + "CORPUS CENSUS on the repaired seed: required-gate `test.claim.declared_type_*` entries; required-floor subject at 3773b874 (11 blocking); whole-root compile of dag+src/v2. Product-versus-coproduct, each with a disposition: `json_kv` at `List` in `gunbc.auth.profile_projection` `profile_*_members`, `gunbc.auth.session_store` `session_profile_*_members`, `gunbc.roadmap.roadmap_serve` `auth_session_*_members` (retyped to `List`); `gunbc.roadmap.roadmap_page` `taskbar_attention_attr` `ActivityUnobservable` (`Fragment` at `List`, arm now `[]`); `gunbc.bmc_model` six `list_append(list, element)` sites (`FreeMonoid` is a coproduct; routed to `list_snoc_item`); specimen `CarrierClosed` at `served_observation_issue_query_surface.standings` left for #13476. Floor also named four `v2.std.optional` imports; retargeted to `std.optional` (#13388). Other whole-root inhabitance hits are the same list-append class outside the floor subject, expected probes, or two-coproduct mismatches.", ], evidence: [], diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 2f44027a12c..2730c528f18 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -765,7 +765,7 @@ fn served_observation_issue_query_surface(instance: HostDashboardInstance, plan: let attempts = match observed { WorkflowAttemptsObserved { attempts } => attempts WorkflowAttemptsRefused { reason: _ } => [] } let body = issue_query_snapshot_for_projection(proj: plan, attempts: attempts, attempts_refused: match observed { WorkflowAttemptsObserved { attempts: _ } => none WorkflowAttemptsRefused { reason } => Present { value: reason } }, - standings: served_standings_after_snapshot_close(read: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance))), launch: launch, + standings: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance)), launch: launch, stale_nodes: stale_attempt_nodes(observations: served_attempt_revision_observations(instance: instance, attempts: attempts), current_revision_hex: served_current_revision_hex(launch: launch)), profiles: served_observation_profiles_for_instance(instance: instance)) match body { From af24c3cdc53c69dff6fdb6c474bc678a9bfb0e12 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 21:16:31 +0000 Subject: [PATCH 08/11] Snoc the product-layer list_append sites the wall newly refuses. The official whole-root compile OOMs at 24 GiB; per-root typecheck found these outside the gate. Co-authored-by: Cursor --- dag/gunbc/bmc_dry_realization.dag | 7 ++++--- dag/gunbc/filesystem_model.dag | 3 ++- .../machine_intake/mtcollins1_boot_dry_realization.dag | 8 ++++---- dag/gunbc/megarac_media_model.dag | 3 ++- ...oduct_admitted_where_its_argument_type_is_declared.dag | 2 +- 5 files changed, 13 insertions(+), 10 deletions(-) diff --git a/dag/gunbc/bmc_dry_realization.dag b/dag/gunbc/bmc_dry_realization.dag index 5fe9b888213..373a2e849af 100644 --- a/dag/gunbc/bmc_dry_realization.dag +++ b/dag/gunbc/bmc_dry_realization.dag @@ -1,6 +1,7 @@ module gunbc.bmc_dry_realization import std.types { Bool, Int, List, NonEmptyStr, String } +import std.algebra { list_snoc_item } import std.measure { Second, second } import v2.std.operation_argv { OperationRef } import v2.std.operation_realization { @@ -161,9 +162,9 @@ fn bmc_dry_realization(identity: NonEmptyStr, initial: BmcWorld, epoch: Second) identity: identity, initial: initial, epoch: epoch, - bindings: list_append( - bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }), - virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"), + bindings: list_snoc_item( + xs: bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }), + item: virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"), ), advance: bmc_advance, } diff --git a/dag/gunbc/filesystem_model.dag b/dag/gunbc/filesystem_model.dag index dd5b3d6974f..c3d56516e70 100644 --- a/dag/gunbc/filesystem_model.dag +++ b/dag/gunbc/filesystem_model.dag @@ -1,6 +1,7 @@ module gunbc.filesystem_model import std.types { Bool, List, String } +import std.algebra { list_snoc_item } import std.measure { second, ByteSize, byte_size } import std.bytes { bytes_octets, utf8_encode_bytes } import v2.std.operation_argv { OperationRef, BoundOperationInvocation } @@ -128,7 +129,7 @@ fn fs_write(fs: ModeledFilesystem, path: String, content: String, create_new: Bo fn fs_with_file(fs: ModeledFilesystem, path: String, content: String) -> ModeledFilesystem { ModeledFilesystem { directories: fs.directories, - files: list_append(filter(fs.files, f => f.path != path), ModeledFile { path: path, content: content }), + files: list_snoc_item(xs: filter(fs.files, f => f.path != path), item: ModeledFile { path: path, content: content }), refused_reads: fs.refused_reads, } } diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag b/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag index 9c48033b88c..65de04f0baa 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag @@ -3,7 +3,7 @@ module gunbc.machine_intake_mtcollins1_boot_dry_realization import extdeps.tools.gnu_coreutils { readlink_command } import std.types { Bool, Int, List, NonEmptyStr, String } import std.measure { Second, second, second_count } -import std.algebra { trim } +import std.algebra { trim, list_snoc_item } import v2.std.operation_argv { OperationRef } import v2.std.operation_realization { OperationRealization, OperationBinding, OperationCall, OperationStep, @@ -236,7 +236,7 @@ fn live_collectors(w: MtCollins1BootWorld) -> List { } fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) -> MtCollins1BootWorld { - with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_append(w.worker.processes, p), uptime_at_origin: w.worker.uptime_at_origin }) + with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_snoc_item(xs: w.worker.processes, item: p), uptime_at_origin: w.worker.uptime_at_origin }) } // THE NOTICE WATCHER the boot step starts before the entry (gunbc.ci_spec): its token in the @@ -246,7 +246,7 @@ fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) -> fn with_notice_watcher(w: MtCollins1BootWorld, capture_path: String, token: String) -> MtCollins1BootWorld { let p = ModeledProcess { pid: w.worker.next_pid, start_time: start_ticks(w: w, now: second(count: 0)), comm: "bash", cmdline: "bash -c gunbc-sol-notice-watch", capture_path: capture_path, diagnostic_path: "", alive: true } let fs = fs_with_file(fs: fs_with_file(fs: w.fs, path: concat(capture_path, mtcollins1_sol_notice_ready_suffix), content: concat(token, "\n")), path: mtcollins1_sol_notice_watcher_path(capture_path: capture_path), content: process_identity(p: p)) - let env = list_append(w.environment, ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token }) + let env = list_snoc_item(xs: w.environment, item: ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token }) started(w: MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: env, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media, screen: w.screen }, p: p, fs: fs) } @@ -533,7 +533,7 @@ fn owned_launch_handler(w: MtCollins1BootWorld, call: OperationCall) -> Operatio KvmModeledRefused { event_word: word, would_write: line } => OperationHarnessFault { reason: concat("kvm_journal_line refused the modeled ", concat(word, concat(" line: ", line))) as NonEmptyStr } KvmModeledRendered { text: t } => { let fs = appended(fs: fs_write(fs: w.fs, path: pid_path, content: process_identity(p: p), create_new: false).fs, path: concat(dir, "/journal"), text: t) - let screen = ModeledKvmViewer { session: w.screen.session, still_bytes: w.screen.still_bytes, still_sha256: w.screen.still_sha256, observers: list_append(w.screen.observers, ModeledKvmObserver { pid: p.pid, dir: dir, seq: 0, seen_files: 0 }) } + let screen = ModeledKvmViewer { session: w.screen.session, still_bytes: w.screen.still_bytes, still_sha256: w.screen.still_sha256, observers: list_snoc_item(xs: w.screen.observers, item: ModeledKvmObserver { pid: p.pid, dir: dir, seq: 0, seen_files: 0 }) } exited_step(state: with_screen(w: started(w: w, p: p, fs: fs), screen: screen), stdout: "", exit_code: 0) } } diff --git a/dag/gunbc/megarac_media_model.dag b/dag/gunbc/megarac_media_model.dag index 5f361e81c56..c0a138a0c70 100644 --- a/dag/gunbc/megarac_media_model.dag +++ b/dag/gunbc/megarac_media_model.dag @@ -2,6 +2,7 @@ module gunbc.megarac_media_model import std.types { Bool, Int, List, String } import std.measure { Second, second, second_count } +import std.algebra { list_snoc_item } // THE BMC's VIRTUAL-MEDIA SUBSYSTEM (AMI MegaRAC SP-X, firmware 0.32): the same controller as // gunbc.bmc_model, held as its own record because its state -- web sessions, the NFS share binding, @@ -88,7 +89,7 @@ fn megarac_open_session(world: MegaRacMediaWorld, cookie_jar: String) -> MegaRac let id = world.next_session let token = concat("modeled-csrf-", to_string(id)) MegaRacOpened { - world: megarac_with_sessions(world: world, sessions: list_append(world.sessions, MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1), + world: megarac_with_sessions(world: world, sessions: list_snoc_item(xs: world.sessions, item: MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1), racsession_id: id, csrf_token: token, } diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index d6413dea53e..c53cc55571c 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -15,7 +15,7 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", - "CORPUS CENSUS on the repaired seed: required-gate `test.claim.declared_type_*` entries; required-floor subject at 3773b874 (11 blocking); whole-root compile of dag+src/v2. Product-versus-coproduct, each with a disposition: `json_kv` at `List` in `gunbc.auth.profile_projection` `profile_*_members`, `gunbc.auth.session_store` `session_profile_*_members`, `gunbc.roadmap.roadmap_serve` `auth_session_*_members` (retyped to `List`); `gunbc.roadmap.roadmap_page` `taskbar_attention_attr` `ActivityUnobservable` (`Fragment` at `List`, arm now `[]`); `gunbc.bmc_model` six `list_append(list, element)` sites (`FreeMonoid` is a coproduct; routed to `list_snoc_item`); specimen `CarrierClosed` at `served_observation_issue_query_surface.standings` left for #13476. Floor also named four `v2.std.optional` imports; retargeted to `std.optional` (#13388). Other whole-root inhabitance hits are the same list-append class outside the floor subject, expected probes, or two-coproduct mismatches.", + "CORPUS CENSUS, measured on d958fafea7 plus this row's product-layer snocs. Command A (official whole-root) `gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --output-dir ` admitted then SIGKILL 137 after frontend+normalize on a 24 GiB host (EmitPopulationCompletenessUnestablished). Command B: per-root typecheck. `src/v2` primary with `dag` pool resolved 3888 sources (every src/v2 module plus its dag import closure). `dag/std`, `dag/extdeps`, `dag/examples`, `dag/gunbc/product` as primaries. Command C: `--entry` importer over the 1671 previously-unmentioned production `dag/gunbc` modules (not `dag/test/*`, not `recurring_failure_mode`) resolved 4045 sources. Indexed tree is 7993 `.dag` files (6309 under dag/, 1684 under src/v2). Product-versus-coproduct sites and dispositions: json_kv helpers retyped to `List`; `taskbar_attention_attr` `ActivityUnobservable` returns `[]`; `gunbc.bmc_model` six `list_append(list, element)` plus product-layer `megarac_media_model`, `filesystem_model` write, `bmc_dry_realization` bindings, and three `mtcollins1_boot_dry_realization` sites routed to `list_snoc_item`; specimen `served_observation` `standings:` left for #13476. Other `DeclaredTypeNotInhabited` rows on these compiles are a different class (Node-vs-product, Fnv-vs-ContentHash, designed probes). Command D: `--entry` importer over 608 `recurring_failure_mode` modules resolved 616 sources, zero `DeclaredTypeNotInhabited`. `dag/test` bulk `--entry` of 2206 uncovered test modules SIGKILL 137 after normalize on the same 24 GiB host; `dag/test/probe` as a primary resolved its designed-red inhabitance (not this class).", ], evidence: [], From f938e93982f580bfd9423fc604afaff6ba7d10db Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 21:19:19 +0000 Subject: [PATCH 09/11] Unwrap standings so the required floor subject compiles. The floor's one blocking diagnostic was CarrierClosed at RoadmapStandings; this is the same call #13476 already has. Co-authored-by: Cursor --- ...ric_product_admitted_where_its_argument_type_is_declared.dag | 2 +- dag/gunbc/roadmap/roadmap_served_observation.dag | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index c53cc55571c..ec0cea43f53 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -11,7 +11,7 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", - "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen is #13476: `served_observation_issue_query_surface` unwraps through `served_standings_after_snapshot_close`. This wall does not edit that line.", + "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen unwrap is `served_standings_after_snapshot_close` at `served_observation_issue_query_surface` -- the same call #13476 already carries. The required floor compiles that module, so this head includes the unwrap rather than leaving the specimen refused.", "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 2730c528f18..2f44027a12c 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -765,7 +765,7 @@ fn served_observation_issue_query_surface(instance: HostDashboardInstance, plan: let attempts = match observed { WorkflowAttemptsObserved { attempts } => attempts WorkflowAttemptsRefused { reason: _ } => [] } let body = issue_query_snapshot_for_projection(proj: plan, attempts: attempts, attempts_refused: match observed { WorkflowAttemptsObserved { attempts: _ } => none WorkflowAttemptsRefused { reason } => Present { value: reason } }, - standings: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance)), launch: launch, + standings: served_standings_after_snapshot_close(read: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance))), launch: launch, stale_nodes: stale_attempt_nodes(observations: served_attempt_revision_observations(instance: instance, attempts: attempts), current_revision_hex: served_current_revision_hex(launch: launch)), profiles: served_observation_profiles_for_instance(instance: instance)) match body { From 208143cd998f53d2f4584b6dbf54aa392f6352e6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 02:12:42 +0000 Subject: [PATCH 10/11] Snoc the clock-jump fixture the wall newly refuses. That witness is on the floor plan; list_append(list, ModeledClockStep) is product-at-FreeMonoid. Co-authored-by: Cursor --- .../machine_intake/mtcollins1_boot_acceptance_matrix_test.dag | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag index faeb57b682e..574de21fb10 100644 --- a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag +++ b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag @@ -2,6 +2,7 @@ module test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test import gunbc.build_cache_instance { ProcessIdentity } import std.types { Bool, Int, List, NonEmptyStr, String } +import std.algebra { list_snoc_item } import std.measure { Second, second } import std.materialization_ladder { Frame, SharedStateFrame } import std.effect_grant { Read, Write, ServiceOpTree, NamespacePosition, ModeledRealization, LifecycleByConstruction, Grant, Envelope } @@ -716,7 +717,7 @@ test fn a_successor_in_another_pid_namespace_refuses_rather_than_recovering() -> fn with_clock_jump(w: MtCollins1BootWorld, at: Second, by: Int) -> MtCollins1BootWorld { MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, - clock: ModeledWallClock { unix_at_origin: w.clock.unix_at_origin, step: w.clock.step, jumps: list_append(w.clock.jumps, ModeledClockStep { at: at, by: std.measure.second_displacement(count: by) }) }, + clock: ModeledWallClock { unix_at_origin: w.clock.unix_at_origin, step: w.clock.step, jumps: list_snoc_item(xs: w.clock.jumps, item: ModeledClockStep { at: at, by: std.measure.second_displacement(count: by) }) }, worker: w.worker, console: w.console, media: w.media, screen: w.screen, } } From 9cee8b6461be6725da9dbecfefc2e6be3e9692f8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 03:00:51 +0000 Subject: [PATCH 11/11] Close zero-field and applied-coproduct holes; name the product-versus-coproduct reason. Co-authored-by: Cursor --- ...ed_where_its_argument_type_is_declared.dag | 10 ++-- ...e_inhabitance_direct_call_witness_test.dag | 46 ++++++++++++++++-- src/v1/04_infer.dag | 47 ++++++++++++++----- src/v1/stage0/src/v1_compiler_infer.rs | 37 +++++++++++---- 4 files changed, 112 insertions(+), 28 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag index ec0cea43f53..8f5d568c8c5 100644 --- a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -7,15 +7,15 @@ data generic_product_admitted_where_its_argument_type_is_declared: RecurringFail identity: "generic_product_admitted_where_its_argument_type_is_declared" as NonEmptyStr, receipts: [ - "INVALID STATE: a value whose type is a generic product application `Wrap` reaches a position declared as `T` (or any other established coproduct), and the program is Accepted. HARM: silent wrongness at the compiler floor -- DESIGN section 4b names `values inhabit declared types` as below-baseline when it fails. SPECIMEN: gunbc#13198 (632b72544e) passed `roadmap_standings_read(layout: ...)` (`-> CarrierClosed`) as `issue_query_snapshot_for_projection.standings` (`standings: RoadmapStandings`). The seed admitted it. At runtime the callee's match on `StandingsObserved | StandingsUnobserved` met a `CarrierClosed` record and aborted with PatternMatchFailure, taking down every srv2 belt tick. #13476 is the wiring repair and does not touch the checker.", + "INVALID STATE: a value whose type is a generic product application `Wrap` reaches a position declared as `T` (or any other established coproduct), and the program is Accepted. HARM: silent wrongness at the compiler floor -- DESIGN section 4b names `values inhabit declared types` as below-baseline when it fails. SPECIMEN: gunbc#13198 (632b72544e) passed `roadmap_standings_read(layout: ...)` (`-> CarrierClosed`) as `issue_query_snapshot_for_projection.standings` (`standings: RoadmapStandings`). The seed admitted it. At runtime the callee's match on `StandingsObserved | StandingsUnobserved` met a `CarrierClosed` record and aborted with PatternMatchFailure, taking down every srv2 belt tick. The wiring unwrap lives at `gunbc.roadmap.roadmap_served_observation` `served_standings_after_snapshot_close`; this row owns the checker wall, not that unwrap's authorship.", - "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", + "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. The prior `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", - "REPAIR: the same function now refuses either direction, and it consumes `nominal_product_head_name` and `nominal_coproduct_head_name` -- applied or unapplied declared product versus applied or unapplied declared coproduct -- the heads the neighbouring nominal arms already establish. Same-declaration and transparent-alias pairs still abstain. RED: `test.claim.declared_type_inhabitance_direct_call_witness` `w_a_generic_product_at_the_coproduct_it_wraps_is_refused` and `w_an_unapplied_product_at_a_coproduct_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted` and `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. The production specimen unwrap is `served_standings_after_snapshot_close` at `served_observation_issue_query_surface` -- the same call #13476 already carries. The required floor compiles that module, so this head includes the unwrap rather than leaving the specimen refused.", + "REPAIR: `v1.compiler.infer` `product_versus_coproduct_head_mismatch` refuses either direction and answers `RefusedProductCoproductHeadMismatch` -- not `RefusedKernelAtStructured`. It consumes `nominal_product_head_name` and `nominal_coproduct_head_name` (applied or unapplied, including ApplicationHead). A declared product is `is_product_type` and not `is_where_refinement_type`, so a zero-field `type Wrap {}` is a product. Same-declaration and transparent-alias pairs still abstain. REDS at the relation boundary (census subject carries `[RefusedProductCoproductHeadMismatch]`): `w_a_generic_product_at_the_coproduct_it_wraps_is_refused`, `w_an_unapplied_product_at_a_coproduct_argument_is_refused`, `w_a_zero_field_generic_product_at_the_coproduct_it_wraps_is_refused`, `w_an_applied_product_at_an_applied_coproduct_argument_is_refused`, `w_coproduct_typed_value_at_record_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted`, `w_a_zero_field_generic_product_at_its_own_declared_application_is_admitted`, `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. SPECIMEN STANDING: `served_observation_issue_query_surface` consumes `served_standings_after_snapshot_close` so the required floor compiles the module; the wall would refuse the pre-unwrap pair.", - "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not) at an established named coproduct, and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", + "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not, zero-field or not) at an established named coproduct (applied or not), and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", - "CORPUS CENSUS, measured on d958fafea7 plus this row's product-layer snocs. Command A (official whole-root) `gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --output-dir ` admitted then SIGKILL 137 after frontend+normalize on a 24 GiB host (EmitPopulationCompletenessUnestablished). Command B: per-root typecheck. `src/v2` primary with `dag` pool resolved 3888 sources (every src/v2 module plus its dag import closure). `dag/std`, `dag/extdeps`, `dag/examples`, `dag/gunbc/product` as primaries. Command C: `--entry` importer over the 1671 previously-unmentioned production `dag/gunbc` modules (not `dag/test/*`, not `recurring_failure_mode`) resolved 4045 sources. Indexed tree is 7993 `.dag` files (6309 under dag/, 1684 under src/v2). Product-versus-coproduct sites and dispositions: json_kv helpers retyped to `List`; `taskbar_attention_attr` `ActivityUnobservable` returns `[]`; `gunbc.bmc_model` six `list_append(list, element)` plus product-layer `megarac_media_model`, `filesystem_model` write, `bmc_dry_realization` bindings, and three `mtcollins1_boot_dry_realization` sites routed to `list_snoc_item`; specimen `served_observation` `standings:` left for #13476. Other `DeclaredTypeNotInhabited` rows on these compiles are a different class (Node-vs-product, Fnv-vs-ContentHash, designed probes). Command D: `--entry` importer over 608 `recurring_failure_mode` modules resolved 616 sources, zero `DeclaredTypeNotInhabited`. `dag/test` bulk `--entry` of 2206 uncovered test modules SIGKILL 137 after normalize on the same 24 GiB host; `dag/test/probe` as a primary resolved its designed-red inhabitance (not this class).", + "CORPUS CENSUS. Command A (official whole-root) `gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --output-dir ` admitted then SIGKILL 137 after frontend+normalize on a 24 GiB host (EmitPopulationCompletenessUnestablished). Command B: per-root typecheck. `src/v2` primary with `dag` pool resolved 3888 sources. `dag/std`, `dag/extdeps`, `dag/examples`, `dag/gunbc/product` as primaries. Command C: `--entry` importer over the 1671 previously-unmentioned production `dag/gunbc` modules (not `dag/test/*`, not `recurring_failure_mode`) resolved 4045 sources. Indexed tree is 7993 `.dag` files (6309 under dag/, 1684 under src/v2). Command D: `--entry` importer over 608 `recurring_failure_mode` modules resolved 616 sources, zero `DeclaredTypeNotInhabited`. Command E: `dag/test` partition -- 17 sequential `--entry` chunks of 200 modules (last chunk the remainder) over the test modules not covered by B/C/D; identity-union of the 17 entry lists is 3329 unique modules, no omissions or duplicates against that universe. Each chunk typechecked; the only this-wall leftover was `dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag` clock-jump `list_append(list, element)` (now `list_snoc_item` at 208143cd). Other `DeclaredTypeNotInhabited` rows on these compiles are a different class. Product-versus-coproduct dispositions: json_kv helpers retyped to `List`; `taskbar_attention_attr` `ActivityUnobservable` returns `[]`; `gunbc.bmc_model` plus `megarac_media_model`, `filesystem_model` write, `bmc_dry_realization` bindings, and three `mtcollins1_boot_dry_realization` sites routed to `list_snoc_item`.", ], evidence: [], diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index 9f6c26e6259..71fe301fb32 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -24,6 +24,22 @@ fn violation_count(source: String, wanted: String) -> Int { } } +// THE RELATION BOUNDARY, NOT THE CLASS COUNT. DeclaredTypeNotInhabited is shared by every +// inhabitance refusal. The product-versus-coproduct arm locates its own reason on the census +// subject; deleting RefusedProductCoproductHeadMismatch (or routing this pair through +// RefusedKernelAtStructured) changes that subject and this helper goes red. +fn product_coproduct_mismatch_at_parameter(source: String, parameter: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => + census_count_at_key( + rows: rows, + diagnostic_class: "DeclaredTypeNotInhabited", + subject_name: concat("direct call argument for parameter '", parameter, "' [RefusedProductCoproductHeadMismatch]"), + blocking: true) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + // THE PAIR THIS FILE EXISTS FOR. std.nat Nat and test.fixture.structural_peano_nat StructuralNat // are both declared as the Peano coproduct (zero, and the successor of one) and they do NOT // realize the same way: std.nat Nat is bound to the kernel integer @@ -127,7 +143,7 @@ test fn w_record_typed_value_at_scalar_argument_is_counted_until_identity_is_gro data coproduct_value_at_record_source: String = "module probe_inhabit_coproduct_at_record\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_choice() -> Choice { ChoiceA { value: \"forty\" } }\nfn takes_box(box: Box) -> Int { 1 }\nfn probe() -> Int { takes_box(box: make_choice()) }\n" test fn w_coproduct_typed_value_at_record_argument_is_refused() -> Bool { - violation_count(source: coproduct_value_at_record_source, wanted: "DeclaredTypeNotInhabited") > 0 + product_coproduct_mismatch_at_parameter(source: coproduct_value_at_record_source, parameter: "box") > 0 } // THE DUAL, AND THE #13198 SPECIMEN. A generic product APPLICATION (CarrierClosed / Wrap) @@ -138,13 +154,13 @@ test fn w_coproduct_typed_value_at_record_argument_is_refused() -> Bool { data generic_product_at_its_argument_coproduct_source: String = "module probe_inhabit_generic_product_at_coproduct\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: mk_wrap()) }\n" test fn w_a_generic_product_at_the_coproduct_it_wraps_is_refused() -> Bool { - violation_count(source: generic_product_at_its_argument_coproduct_source, wanted: "DeclaredTypeNotInhabited") > 0 + product_coproduct_mismatch_at_parameter(source: generic_product_at_its_argument_coproduct_source, parameter: "x") > 0 } data unapplied_product_at_coproduct_source: String = "module probe_inhabit_product_at_coproduct\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_choice(x: Choice) -> Int { 1 }\nfn probe() -> Int { takes_choice(x: make_box()) }\n" test fn w_an_unapplied_product_at_a_coproduct_argument_is_refused() -> Bool { - violation_count(source: unapplied_product_at_coproduct_source, wanted: "DeclaredTypeNotInhabited") > 0 + product_coproduct_mismatch_at_parameter(source: unapplied_product_at_coproduct_source, parameter: "x") > 0 } data generic_product_at_matching_product_source: String = "module probe_inhabit_generic_product_ok\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_wrap(x: Wrap) -> Int { 1 }\nfn probe() -> Int { takes_wrap(x: mk_wrap()) }\n" @@ -159,6 +175,30 @@ test fn w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted() - violation_count(source: generic_product_field_projected_source, wanted: "DeclaredTypeNotInhabited") == 0 } +// ZERO-FIELD PRODUCT BY DECLARATION KIND, NOT CHILD COUNT. `type Wrap {}` is Conj with +// zero children; the old `count(children)>0` gate answered "" and the pair reached Inhabits. +// The positive control is the same wrapper at its own application. +data zero_field_product_at_coproduct_source: String = "module probe_inhabit_zero_field_product\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap {}\nfn make_wrap() -> Wrap { Wrap {} }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: make_wrap()) }\n" + +test fn w_a_zero_field_generic_product_at_the_coproduct_it_wraps_is_refused() -> Bool { + product_coproduct_mismatch_at_parameter(source: zero_field_product_at_coproduct_source, parameter: "x") > 0 +} + +data zero_field_product_at_matching_product_source: String = "module probe_inhabit_zero_field_product_ok\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap {}\nfn make_wrap() -> Wrap { Wrap {} }\nfn takes_wrap(x: Wrap) -> Int { 1 }\nfn probe() -> Int { takes_wrap(x: make_wrap()) }\n" + +test fn w_a_zero_field_generic_product_at_its_own_declared_application_is_admitted() -> Bool { + violation_count(source: zero_field_product_at_matching_product_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// APPLIED COPRODUCT ApplicationHead. Box is a product application; Choice is a +// coproduct application. Deleting the ApplicationHead arm of nominal_coproduct_head_name +// turns this red into an admission. +data applied_product_at_applied_coproduct_source: String = "module probe_inhabit_applied_product_at_applied_coproduct\nimport std.types { Int, String }\ntype Box { value: T }\ntype Choice = | ChoiceA { value: T } | ChoiceB\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_choice(x: Choice) -> Int { 1 }\nfn probe() -> Int { takes_choice(x: make_box()) }\n" + +test fn w_an_applied_product_at_an_applied_coproduct_argument_is_refused() -> Bool { + product_coproduct_mismatch_at_parameter(source: applied_product_at_applied_coproduct_source, parameter: "x") > 0 +} + // The syntax contrast that exposed the application hole. The cast seam already refused the same // optional-to-required transition; the binding seam now refuses it too, and that RED lives at // test.claim.optional_at_required_position_witness_test an_optional_at_a_string_parameter_must_refuse, diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 656ccafac28..cedb708c879 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -109,6 +109,7 @@ import v1.compiler.infer_types { normalize_access_type_node, node_type_shape, node_type_compatible, node_type_equals, prefer_specific_type, is_declared_container_alias_spelling, structural_carrier_template_name, + is_product_type, node_type_deps, method_receiver_element_node, infer_literal_node, infer_binop_type_node, subtraction_refinement_of, @@ -4037,6 +4038,7 @@ type InhabitanceUndecidableReason type InhabitanceRefusalReason = RefusedPayloadAtParent | RefusedKernelAtStructured + | RefusedProductCoproductHeadMismatch | RefusedCollectionAtEstablishedIdentity | RefusedDistinctProductConstructor | RefusedDistinctAppliedTypeArgument @@ -4331,8 +4333,8 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco InhabitanceRefused { reason: RefusedCollectionAtEstablishedIdentity } } else if record_at_scalar_needs_identity(declared: declared, produced: produced, scope: scope) { InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } - } else if coproduct_at_record_declared_type(declared: declared, produced: produced, scope: scope) { - InhabitanceRefused { reason: RefusedKernelAtStructured } + } else if product_versus_coproduct_head_mismatch(declared: declared, produced: produced, scope: scope) { + InhabitanceRefused { reason: RefusedProductCoproductHeadMismatch } } else { match refinement_inhabitance(declared: declared, produced: produced, scope: scope) { Present { value: RefinementWidensToDeclaredBase } => Inhabits @@ -4520,9 +4522,13 @@ fn record_at_scalar_needs_identity(declared: Node, produced: Node, scope: InferS // issue_query_snapshot_for_projection.standings) matched neither side and the inhabitance // relation fell through to Inhabits. THE HEADS ARE THE SAME AUTHORITIES THE NOMINAL-PRODUCT // AND GENERIC-COPRODUCT ARMS ALREADY USE: a declared product, applied or not, and a declared -// coproduct, applied or not. A second leaf-name lookup is not an authority here. Either -// direction refuses; same-declaration and transparent-alias pairs still abstain. -fn coproduct_at_record_declared_type(declared: Node, produced: Node, scope: InferScope) -> Bool { +// coproduct, applied or not — including a zero-field product (declaration kind Conj, not +// child count) and an applied coproduct (ApplicationHead whose constructor peels to Disj). +// A second leaf-name lookup is not an authority here. Either direction refuses; +// same-declaration and transparent-alias pairs still abstain. The typed reason is +// RefusedProductCoproductHeadMismatch, not RefusedKernelAtStructured: this is a head-kind +// clash, not a kernel value at a structured formal. +fn product_versus_coproduct_head_mismatch(declared: Node, produced: Node, scope: InferScope) -> Bool { let declared_name = authored_name_at(source_indices: scope.type_env.source_indices, node: declared) let produced_name = authored_name_at(source_indices: scope.type_env.source_indices, node: produced) if application_type_names_compatible( @@ -4642,13 +4648,16 @@ fn declared_realizes_as_kernel_numeric( // MalformedApplicationHead identities are legitimate abstentions when resolution or arity checking // already owns the error (refusing again would cascade). Kernel scalars, collections and coproducts // are excluded because their dedicated judgments run before this arm. Optional values, callables, -// anonymous records and zero-field products are REAL SHAPES but UNHANDLED HERE: respectively, +// anonymous records are REAL SHAPES but UNHANDLED HERE: respectively, // `fn f() -> A? { B{..} }`, `fn f() -> fn(Int) -> Int { B{..} }`, -// `fn f() -> A { { y: 1 } }`, and `fn f() -> EmptyA { EmptyB{} }` can still pass this relation -// silently. Generic applications are likewise a separate, filed half of the inhabitance defect. An OpaqueTypeHead is +// and `fn f() -> A { { y: 1 } }` can still pass this relation +// silently. A declared zero-field product is a product by declaration kind (`is_product_type` +// and not `is_where_refinement_type`), so `EmptyA` versus `EmptyB` and `Wrap {}` at a +// coproduct are judged. Generic applications are a separate, filed half of the inhabitance +// defect. An OpaqueTypeHead is // not automatically unhandled: transparent aliases expose that view, so the declaration is peeled // through the existing alias authority and admitted to this arm only when the peel positively lands -// on a nonempty product. This change closes concrete named products and their transparent aliases; +// on a declared product. This change closes concrete named products and their transparent aliases; // it does not claim the unhandled shapes climbed with them. fn nominal_product_inhabitance_refusal( declared: Node, @@ -4730,7 +4739,7 @@ fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope Present { value: decl } => let peeled = peel_nominal_alias_identity( n: decl, env: scope.type_env, module_name: scope.module_name) - if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } + if is_product_type(n: peeled) && is_where_refinement_type(ty: peeled) == false { name } else { "" } Absent => "" } } @@ -5053,6 +5062,19 @@ fn applied_type_argument_identity_known(name: String, scope: InferScope) -> Bool // non-blocking in v1.00_core is_interpreter_blocking_diagnostic and advisory in // is_discovery_corpus_advisory_typecheck_diagnostic, so this makes the residue visible without // reddening a corpus whose seams were never judged before this carrier existed either. +fn inhabitance_refusal_position_label( + position: DeclaredTypePosition, + subject: String, + reason: InhabitanceRefusalReason +) -> String { + let base = declared_type_position_label(position: position, subject: subject) + match reason { + RefusedProductCoproductHeadMismatch => + concat(base, " [RefusedProductCoproductHeadMismatch]") + _ => base + } +} + fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> String { match reason { UndecidableGenericFormal => "generic formal: the declared position's payload types can be type variables, so membership is not decidable from the declaration alone" @@ -5103,10 +5125,11 @@ fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: Inf }, module_name: scope.module_name )] - InhabitanceRefused { reason: _ } => + InhabitanceRefused { reason: r } => [make_error_node( diagnostic: DeclaredTypeNotInhabited { - position: declared_type_position_label(position: obligation.position, subject: obligation.subject), + position: inhabitance_refusal_position_label( + position: obligation.position, subject: obligation.subject, reason: r), expected: obligation_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices), got: obligation_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices), span: obligation.span diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index dd261f3f2c5..a62a9a1a9b0 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -248,7 +248,7 @@ use crate::v1_compiler_infer_types::TextNotAskedReason::{ pub use crate::v1_compiler_infer_types::{ bare_map_node, bare_set_node, callable_inferred, callable_return_type, child_type_node, emit_map_has, extract_optional_inner_node, for_each_element_type_node, infer_binop_type_node, - infer_literal_node, is_declared_container_alias_spelling, is_fully_resolved, + infer_literal_node, is_declared_container_alias_spelling, is_fully_resolved, is_product_type, is_type_expr_annotation, kernel_profile_lookup, make_callable_type, make_container_type, method_receiver_element_node, node_is_collection, node_is_element_collection, node_is_keyed_collection, node_is_set_collection, node_type_compatible, node_type_deps, @@ -5797,6 +5797,7 @@ pub enum InhabitanceUndecidableReason { pub enum InhabitanceRefusalReason { RefusedPayloadAtParent, RefusedKernelAtStructured, + RefusedProductCoproductHeadMismatch, RefusedCollectionAtEstablishedIdentity, RefusedDistinctProductConstructor, RefusedDistinctAppliedTypeArgument, @@ -6163,13 +6164,13 @@ pub fn declared_type_inhabitance( reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, }) } else { - if coproduct_at_record_declared_type( + if product_versus_coproduct_head_mismatch( declared.clone(), produced.clone(), scope.clone(), ) { Rc::new(InhabitanceVerdict::InhabitanceRefused { - reason: InhabitanceRefusalReason::RefusedKernelAtStructured, + reason: InhabitanceRefusalReason::RefusedProductCoproductHeadMismatch, }) } else { match refinement_inhabitance(declared.clone(), produced.clone(), scope.clone()) { @@ -6393,7 +6394,7 @@ pub fn record_at_scalar_needs_identity( )) } -pub fn coproduct_at_record_declared_type( +pub fn product_versus_coproduct_head_mismatch( declared: Rc, produced: Rc, scope: Rc, @@ -6573,8 +6574,8 @@ pub fn nominal_product_head_name_if_declared_product( scope.type_env.clone(), scope.module_name.clone(), ); - if ((peeled.connective.clone() == Connective::Conj) - && ((peeled.children.clone().len() as i64) > 0)) + if (crate::v1_compiler_infer_types::is_product_type(peeled.clone()) + && (is_where_refinement_type(peeled.clone()) == false)) { name.clone() } else { @@ -7004,6 +7005,23 @@ pub fn applied_type_argument_identity_known(name: String, scope: Rc) } } +pub fn inhabitance_refusal_position_label( + position: DeclaredTypePosition, + subject: String, + reason: InhabitanceRefusalReason, +) -> String { + { + let base = declared_type_position_label(position.clone(), subject.clone()); + match reason.clone() { + InhabitanceRefusalReason::RefusedProductCoproductHeadMismatch => v1_rt::concat( + base.clone(), + " [RefusedProductCoproductHeadMismatch]".to_string(), + ), + _ => base.clone(), + } + } +} + pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> String { match reason.clone() { InhabitanceUndecidableReason::UndecidableGenericFormal => "generic formal: the declared position's payload types can be type variables, so membership is not decidable from the declaration alone".to_string(), @@ -7069,12 +7087,13 @@ pub fn declared_type_obligation_diags( scope.module_name.clone(), )]) } - InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => { + InhabitanceVerdict::InhabitanceRefused { reason: r, .. } => { Rc::new(vec![crate::v1_std_core::make_error_node( Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { - position: declared_type_position_label( + position: inhabitance_refusal_position_label( obligation.position.clone(), obligation.subject.clone(), + r.clone(), ), expected: obligation_type_shape( obligation.declared.clone(), @@ -32452,6 +32471,8 @@ pub struct RefusedPayloadAtParent; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedKernelAtStructured; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedProductCoproductHeadMismatch; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedCollectionAtEstablishedIdentity; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedDistinctProductConstructor;