From 3c509b67899a6ad42aad17431a1691b1d376fb95 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 01:56:06 +0000 Subject: [PATCH 01/27] WIP: declared-type inhabitance obligation carrier (UNVERIFIED, not for push) Carrier types, the single declared_type_inhabitance relation consuming #8876's coproduct_payload_where_parent_required, the DeclaredTypeNotInhabited diagnostic, and the list-element position wired. Mirrors NOT regenerated; the wall does not execute in any built artifact yet. Verification dispatch in flight. --- src/v1/00_core.dag | 4 ++ src/v1/04_infer.dag | 129 ++++++++++++++++++++++++++++++++++- src/v1/stage0/src/cli_run.rs | 2 + 3 files changed, 134 insertions(+), 1 deletion(-) diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index a1f7a76efd7..e09970b3713 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -187,6 +187,7 @@ type CompilerDiagnostic permitted_callers: List, span: SourceSpan } + | DeclaredTypeNotInhabited { position: String, expected: String, got: String, span: SourceSpan } | UnlistedImportUse { name: String, span: SourceSpan } | AmbiguousReference { name: String, candidates: List, span: SourceSpan } | CallArgumentNameUnknown { callee: String, argument: String, declared: List, span: SourceSpan } @@ -325,6 +326,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan { permitted_callers: _, span: s } => s + DeclaredTypeNotInhabited { position: _, expected: _, got: _, span: s } => s UnlistedImportUse { name: _, span: s } => s AmbiguousReference { name: _, candidates: _, span: s } => s CallArgumentNameUnknown { callee: _, argument: _, declared: _, span: s } => s @@ -396,6 +398,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String { join(permitted, separator: ", "), "]" ) + DeclaredTypeNotInhabited { position: pos, expected: e, got: g, span: _ } => + concat("value does not inhabit its declared type at the ", pos, ": declared '", e, "', produced '", g, "'") UnlistedImportUse { name: n, span: _ } => concat("unlisted import use '", n, "' (referenced but not in any import's name list)") AmbiguousReference { name: n, candidates: cs, span: _ } => concat("ambiguous reference '", n, "': ", to_string(value: cs |> count), " candidates: ", join(cs, separator: ", "), " — qualify by containment path, alias, or rename") CallArgumentNameUnknown { callee: c, argument: a, declared: ds, span: _ } => diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index b70b0458aba..bf861404809 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2070,6 +2070,118 @@ fn coproduct_variant_payload_admits_type_name( // makes "the actual is one of this coproduct's payload types" undecidable from the declaration // alone; refusing there would be a fabricated refusal, which DESIGN section 5 forbids exactly as it // forbids a fabricated success. +// ONE OBLIGATION, ONE AUTHORITY. The grammar has fourteen type positions and twelve of them +// can receive a source value. Before this carrier each position that judged anything judged it +// with its own local chain of else-if predicates, which is one rule in N representations: a +// position added later inherits nothing, and a rule fixed at one position stays broken at the +// rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was declared and WHAT +// was produced; declared_type_inhabitance is the single relation that decides; the position +// travels with the obligation so the diagnostic can locate the refusal without the decision +// procedure forking per position. +type DeclaredTypePosition + = PositionRecordLiteralField + | PositionListElement + | PositionMapValue + | PositionDataInitializer + | PositionDeclaredReturn + | PositionLetAnnotation + | PositionVariantPayload + | PositionGenericTypeArgument + | PositionCastTarget + | PositionParameterDefault + | PositionCallableReturn + | PositionDirectCallArgument + +type DeclaredTypeObligation { + position: DeclaredTypePosition + declared: Node + produced: Node + span: SourceSpan +} + +// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. Each reason names something the +// modeled facts genuinely cannot settle at this seam. A position that has not been wired yet is +// NOT undecidable -- it is a missing obligation producer, and it is absent from the census +// rather than present with a verdict. Reading "we did not look" as "it cannot be decided" is +// the rung inflation DESIGN 4b names, applied to this relation's own self-description. +type InhabitanceUndecidableReason + = UndecidableGenericFormal + | UndecidableOptionalCarrier + | UndecidableFormalUnresolved + | UndecidableProducedIdentityErased + +type InhabitanceRefusalReason + = RefusedPayloadAtParent + | RefusedKernelAtStructured + +type InhabitanceVerdict + = Inhabits + | InhabitanceRefused { reason: InhabitanceRefusalReason } + | InhabitanceUndecidable { reason: InhabitanceUndecidableReason } + +fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position { + PositionRecordLiteralField => "record literal field" + PositionListElement => "list element" + PositionMapValue => "map value" + PositionDataInitializer => "data initializer" + PositionDeclaredReturn => "declared return" + PositionLetAnnotation => "let annotation" + PositionVariantPayload => "variant payload" + PositionGenericTypeArgument => "generic type argument" + PositionCastTarget => "cast target" + PositionParameterDefault => "parameter default" + PositionCallableReturn => "callable return" + PositionDirectCallArgument => "direct call argument" + } +} + +// THE SINGLE DECISION PROCEDURE. It CONSUMES the established predicates rather than restating +// them: coproduct_payload_where_parent_required already peels transparent aliases through +// transparent_alias_identity_agrees, so alias identity is decided in exactly one place in the +// tree and this relation inherits it instead of re-deriving a second answer. +fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferScope) -> InhabitanceVerdict { + let declared = obligation.declared + let produced = obligation.produced + let source_indices = scope.type_env.source_indices + let declared_name = authored_name_at(source_indices: source_indices, node: declared) + let produced_name = authored_name_at(source_indices: source_indices, node: produced) + let either_optional = declared.return_cardinality == CardOptional || produced.return_cardinality == CardOptional + let declared_is_generic = (declared.params |> count) > 0 + if either_optional { + InhabitanceUndecidable { reason: UndecidableOptionalCarrier } + } else if declared_is_generic { + InhabitanceUndecidable { reason: UndecidableGenericFormal } + } else if declared_name == "" { + InhabitanceUndecidable { reason: UndecidableFormalUnresolved } + } else if produced_name == "" { + InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { + InhabitanceRefused { reason: RefusedPayloadAtParent } + } else { + Inhabits + } +} + +// The obligation carries its own position, so ONE emitter locates every refusal. A per-position +// diagnostic function would be the N-representation problem moved one layer down. +fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: InferScope) -> List { + match declared_type_inhabitance(obligation: obligation, scope: scope) { + Inhabits => [] + InhabitanceUndecidable { reason: _ } => [] + InhabitanceRefused { reason: _ } => + [make_error_node( + diagnostic: DeclaredTypeNotInhabited { + position: declared_type_position_label(position: obligation.position), + expected: node_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices), + got: node_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices), + span: obligation.span + }, + module_name: scope.module_name + )] + } +} + fn coproduct_payload_where_parent_required( formal: Node, actual: Node, @@ -4602,7 +4714,22 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu } let elem_results = elements |> map(e => infer_expr(texpr: e, scope: scope, expected: elem_expected)) let typed_elements = elem_results |> map(r => r.typed) - let elem_diags = flat_map(elem_results, r => r.diagnostics) + let elem_inhabitance_diags = match elem_expected { + Present { value: declared_elem } => + flat_map(typed_elements, te => + declared_type_obligation_diags( + obligation: DeclaredTypeObligation { + position: PositionListElement, + declared: declared_elem, + produced: resolved_type(n: te), + span: te.span + }, + scope: scope + ) + ) + Absent => [] + } + let elem_diags = concat(flat_map(elem_results, r => r.diagnostics), elem_inhabitance_diags) let elem_type_node = if count(elem_results) > 0 { match first(elem_results) { Present { value: r } => resolved_type(n: r.typed) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 351dc600c6f..d12db20b7b1 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -4738,6 +4738,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str CompilerDiagnostic::ConstructorCallAdmissionRefused { .. } => { "ConstructorCallAdmissionRefused" } + CompilerDiagnostic::DeclaredTypeNotInhabited { .. } => "DeclaredTypeNotInhabited", CompilerDiagnostic::UnlistedImportUse { .. } => "UnlistedImportUse", CompilerDiagnostic::AmbiguousReference { .. } => "AmbiguousReference", CompilerDiagnostic::CallArgumentNameUnknown { .. } => "CallArgumentNameUnknown", @@ -4783,6 +4784,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str constructor_decl_name, .. } => constructor_decl_name.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { position, .. } => position.clone(), CompilerDiagnostic::UnlistedImportUse { name, .. } => name.clone(), CompilerDiagnostic::AmbiguousReference { name, .. } => name.clone(), CompilerDiagnostic::CallArgumentNameUnknown { argument, .. } => argument.clone(), From fdde6fb435280e72652d6d77bdb351e38849d19b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 02:55:38 +0000 Subject: [PATCH 02/27] Wire the kernel-at-structured route and its witness (still unverified) --- ..._inhabitance_list_element_witness_test.dag | 101 ++++++++++++++++++ src/v1/04_infer.dag | 4 + 2 files changed, 105 insertions(+) create mode 100644 dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag new file mode 100644 index 00000000000..1ed96abeae2 --- /dev/null +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -0,0 +1,101 @@ +module test.claim.declared_type_inhabitance_list_element_witness + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CensusObserved, + CensusNotRunnable, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE FLOOR CLAUSE THIS GUARDS: a value accepted at a declared-type position inhabits that +// declared type. DESIGN names it as floor, so a breach is a below-baseline safety regression +// rather than a missing nicety, and it is not softened to mitigatable anywhere in this file. +// +// WHY ONE CARRIER AND NOT ONE CHECK PER POSITION. The grammar has fourteen type positions; +// twelve can receive a source value. Before the obligation carrier, each position that judged +// anything judged it with its own local chain of predicates -- one rule in N representations, +// where a position added later inherits nothing and a rule repaired at one position stays +// broken at the rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was +// declared and WHAT was produced; declared_type_inhabitance is the single relation that +// decides; the position rides along so the diagnostic can locate the refusal without the +// decision procedure forking. This file is the executing evidence for the FIRST position wired +// through that carrier, and its arms are the shape every later position reuses. +// +// THE RELATION CONSUMES, IT DOES NOT RE-DERIVE. Alias identity is decided once in the tree: +// coproduct_payload_where_parent_required peels transparent aliases through +// transparent_alias_identity_agrees, and the kernel arm defers to +// kernel_value_declared_type_mismatch. A second answer to either question authored here would +// be the nicknaming failure at the level of judgments. +// +// PATH SCOPE, per DESIGN 4b's rung-per-path rule: this asserts source -> .dag acceptance only. +// The refusal sits in inference, so nothing reaches emission with a non-inhabiting list +// element -- but that is a consequence of where the wall sits, not a second measurement, and +// it is not claimed as one. + +fn violation_count(source: String, wanted: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count(rows: census_rows_of_class(rows: rows, wanted: wanted)) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// RED ARM ONE -- the plain kernel at a structured declared type. This is the floor case, and it +// is in this file because the FIRST wiring of the carrier ACCEPTED it: the relation consulted +// only the payload-at-parent predicate, so RefusedKernelAtStructured was a declared verdict +// variant that no code path could produce. A variant nothing constructs is a decoration that +// reads as coverage, which is the rung inflation DESIGN 4b names. This arm exists so that +// deleting the kernel route from the relation goes red rather than quiet. +data kernel_at_structured_source: String = "module probe_inhabit_nega\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [7] }\n" + +test fn w_plain_kernel_at_declared_list_element_is_refused() -> Bool { + violation_count(source: kernel_at_structured_source, wanted: "DeclaredTypeNotInhabited") >= 1 +} + +// RED ARM TWO -- an arm's PAYLOAD type standing where the PARENT coproduct is declared. The +// shape gunbc#8865 recorded, measured here at the list-element position rather than inferred +// from the record-field one: two positions are two paths, and a wall proven at one says +// nothing about the other. +data payload_at_parent_source: String = "module probe_inhabit_negb\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk_inner() -> Inner { Inner { v: 1 } }\nfn probe() -> List { [mk_inner()] }\n" + +test fn w_arm_payload_where_parent_declared_is_refused() -> Bool { + violation_count(source: payload_at_parent_source, wanted: "DeclaredTypeNotInhabited") >= 1 +} + +// GREEN ARM -- the control that stops the wall being a wrecking ball. A genuine member of the +// declared coproduct must still compile and must raise NO inhabitance diagnostic. Without it, +// a relation that refused every list element would score identically on both red arms above, +// and the reds would establish nothing. +data inhabiting_member_source: String = "module probe_inhabit_pos\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [SameRev] }\n" + +test fn w_declared_coproduct_member_is_accepted() -> Bool { + violation_count(source: inhabiting_member_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// REACHABILITY -- an undefined name at the same position must refuse whether or not the +// inhabitance wall exists. This separates "the position is judged and the value was refused" +// from "the position is never reached at all", which the accepting arms above cannot +// distinguish on their own. It is asserted on a DIFFERENT class than the wall's, deliberately: +// keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. +data undefined_name_source: String = "module probe_inhabit_reach\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [nosuchname_zzz_probe] }\n" + +test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { + violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. An optional carrier at the +// declared position is genuinely undecidable at this seam -- optionality lives in +// return_cardinality while the produced value carries the nominal coproduct, so the two are +// not comparable here without peeling a representation this relation does not own. It must +// therefore NOT refuse. This arm is what keeps Undecidable honest: if the relation ever starts +// refusing optionals it goes red, and if a future author repurposes an Undecidable reason to +// mean "unimplemented" this is the arm that notices. +data optional_carrier_source: String = "module probe_inhabit_opt\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn maybe() -> Rel? { none }\nfn probe() -> List { [maybe()] }\n" + +test fn w_optional_carrier_is_undecidable_not_refused() -> Bool { + violation_count(source: optional_carrier_source, wanted: "DeclaredTypeNotInhabited") == 0 +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index bf861404809..c18d70c2223 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2156,6 +2156,10 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco InhabitanceUndecidable { reason: UndecidableFormalUnresolved } } else if produced_name == "" { InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if kernel_value_declared_type_mismatch( + formal: declared, actual: produced, + type_env: scope.type_env, source_indices: source_indices) { + InhabitanceRefused { reason: RefusedKernelAtStructured } } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { InhabitanceRefused { reason: RefusedPayloadAtParent } } else { From 8a3571570768fa29a9610b2399de22d226644f63 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 03:09:53 +0000 Subject: [PATCH 03/27] Install the emitted mirrors for the inhabitance carrier --- src/v1/stage0/src/v1_compiler_infer.rs | 243 ++++++++++++++++++++++++- src/v1/stage0/src/v1_std_core.rs | 8 + 2 files changed, 244 insertions(+), 7 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 250b7fafdc1..9d8e8d20fe5 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -1,7 +1,11 @@ // Generated by v1 compiler -- do not edit. // Source module: v1.compiler.infer +use self::DeclaredTypePosition::*; use self::DescentSizeExpr::*; +use self::InhabitanceRefusalReason::*; +use self::InhabitanceUndecidableReason::*; +use self::InhabitanceVerdict::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, }; @@ -3032,6 +3036,169 @@ pub fn coproduct_variant_payload_admits_type_name( } } +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum DeclaredTypePosition { + PositionRecordLiteralField, + PositionListElement, + PositionMapValue, + PositionDataInitializer, + PositionDeclaredReturn, + PositionLetAnnotation, + PositionVariantPayload, + PositionGenericTypeArgument, + PositionCastTarget, + PositionParameterDefault, + PositionCallableReturn, + PositionDirectCallArgument, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct DeclaredTypeObligation { + pub position: DeclaredTypePosition, + pub declared: Rc, + pub produced: Rc, + pub span: Rc, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceUndecidableReason { + UndecidableGenericFormal, + UndecidableOptionalCarrier, + UndecidableFormalUnresolved, + UndecidableProducedIdentityErased, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceRefusalReason { + RefusedPayloadAtParent, + RefusedKernelAtStructured, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum InhabitanceVerdict { + Inhabits, + InhabitanceRefused { + reason: InhabitanceRefusalReason, + }, + InhabitanceUndecidable { + reason: InhabitanceUndecidableReason, + }, +} + +pub fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position.clone() { + DeclaredTypePosition::PositionRecordLiteralField => "record literal field".to_string(), + DeclaredTypePosition::PositionListElement => "list element".to_string(), + DeclaredTypePosition::PositionMapValue => "map value".to_string(), + DeclaredTypePosition::PositionDataInitializer => "data initializer".to_string(), + DeclaredTypePosition::PositionDeclaredReturn => "declared return".to_string(), + DeclaredTypePosition::PositionLetAnnotation => "let annotation".to_string(), + DeclaredTypePosition::PositionVariantPayload => "variant payload".to_string(), + DeclaredTypePosition::PositionGenericTypeArgument => "generic type argument".to_string(), + DeclaredTypePosition::PositionCastTarget => "cast target".to_string(), + DeclaredTypePosition::PositionParameterDefault => "parameter default".to_string(), + DeclaredTypePosition::PositionCallableReturn => "callable return".to_string(), + DeclaredTypePosition::PositionDirectCallArgument => "direct call argument".to_string(), + } +} + +pub fn declared_type_inhabitance( + obligation: Rc, + scope: Rc, +) -> Rc { + { + let declared = obligation.declared.clone(); + let produced = obligation.produced.clone(); + let source_indices = scope.type_env.clone().source_indices.clone(); + let declared_name = authored_name_at(source_indices.clone(), declared.clone()); + let produced_name = authored_name_at(source_indices.clone(), produced.clone()); + let either_optional = ((declared.return_cardinality.clone() == Cardinality::CardOptional) + || (produced.return_cardinality.clone() == Cardinality::CardOptional)); + let declared_is_generic = ((declared.params.clone().len() as i64) > 0); + if either_optional.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableOptionalCarrier, + }) + } else { + if declared_is_generic.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableGenericFormal, + }) + } else { + if (declared_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableFormalUnresolved, + }) + } else { + if (produced_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, + }) + } else { + if kernel_value_declared_type_mismatch( + declared.clone(), + produced.clone(), + scope.type_env.clone(), + source_indices.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedKernelAtStructured, + }) + } else { + if coproduct_payload_where_parent_required( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedPayloadAtParent, + }) + } else { + Rc::new(InhabitanceVerdict::Inhabits) + } + } + } + } + } + } + } +} + +pub fn declared_type_obligation_diags( + obligation: Rc, + scope: Rc, +) -> Rc>> { + match (*declared_type_inhabitance(obligation.clone(), scope.clone())).clone() { + InhabitanceVerdict::Inhabits => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceUndecidable { reason: _, .. } => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { + position: declared_type_position_label(obligation.position.clone()), + expected: node_type_shape( + obligation.declared.clone(), + scope.type_env.clone().source_indices.clone(), + ), + got: node_type_shape( + obligation.produced.clone(), + scope.type_env.clone().source_indices.clone(), + ), + span: obligation.span.clone(), + }), + scope.module_name.clone(), + )]), + } +} + pub fn coproduct_payload_where_parent_required( formal: Rc, actual: Rc, @@ -8135,13 +8302,38 @@ if ((call_ambiguity_cands.clone().len() as i64) > 0) { } __result }); - let elem_diags = Rc::new({ - let mut __result = Vec::new(); - for r in elem_results.iter().cloned() { - __result.extend((*r.diagnostics.clone()).iter().cloned()); - } - __result - }); + let elem_inhabitance_diags = match elem_expected.clone() { + Some(declared_elem) => Rc::new({ + let mut __result = Vec::new(); + for te in typed_elements.iter().cloned() { + __result.extend( + (*declared_type_obligation_diags( + Rc::new(DeclaredTypeObligation { + position: DeclaredTypePosition::PositionListElement, + declared: declared_elem.clone(), + produced: resolved_type(te.clone()), + span: te.span.clone(), + }), + scope.clone(), + )) + .iter() + .cloned(), + ); + } + __result + }), + None => Rc::new(vec![]), + }; + let elem_diags = v1_rt::concat( + Rc::new({ + let mut __result = Vec::new(); + for r in elem_results.iter().cloned() { + __result.extend((*r.diagnostics.clone()).iter().cloned()); + } + __result + }), + elem_inhabitance_diags.clone(), + ); let elem_type_node = if ((elem_results.clone().len() as i64) > 0) { match elem_results.clone().first().cloned() { Some(r) => resolved_type(r.typed.clone()), @@ -21847,3 +22039,40 @@ pub fn reconcile_with_census_extra( }) } } + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionRecordLiteralField; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionListElement; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionMapValue; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDataInitializer; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDeclaredReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionLetAnnotation; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionVariantPayload; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionGenericTypeArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCastTarget; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionParameterDefault; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCallableReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDirectCallArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableGenericFormal; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableOptionalCarrier; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableFormalUnresolved; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableProducedIdentityErased; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedPayloadAtParent; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedKernelAtStructured; diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index b6accf4e9d1..ed59d3d9e43 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -510,6 +510,12 @@ pub enum CompilerDiagnostic { permitted_callers: Rc>, span: Rc, }, + DeclaredTypeNotInhabited { + position: String, + expected: String, + got: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -660,6 +666,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { annotation_attachment_refusal_origin(r.clone()) } CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::CallArgumentNameUnknown { span: s, .. } => s.clone(), @@ -708,6 +715,7 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::BareNoneNotAdmittedByFieldType { field: f, type_name: t, declared_type: dt, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("bare 'None' cannot inhabit field '".to_string(), f.clone()), "' of '".to_string()), t.clone()), "': declared type '".to_string()), dt.clone()), "' carries no absence — it is not optional and declares no 'None' variant".to_string()), CompilerDiagnostic::SourceAnnotationRefused { refusal: r, .. } => annotation_attachment_refusal_message(r.clone()), CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), + CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::CallArgumentNameUnknown { callee: c, argument: a, declared: ds, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("call shape mismatch calling '".to_string(), c.clone()), "': no parameter named '".to_string()), a.clone()), "' (declared: [".to_string()), ds.clone().join(&", ".to_string())), "])".to_string()), From 1509c316ce2552bb452b2414a9bc254d9a3a9dfc Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 03:55:43 +0000 Subject: [PATCH 04/27] Regenerate both mirrors from the merged authorities, not from a textual merge Git conflicted on v1_std_core.rs and AUTO-MERGED v1_compiler_infer.rs. Resolving only the file git complained about left the pair internally inconsistent: one mirror declared the roster variant and not the inhabitance one, while its sibling used both. That state is not something any emitter produces, and it does not compile. Generated files are projections of one authority and are only consistent as a SET, so both are replaced wholesale by a fresh emit from the merged .dag rather than merged file-by-file. Measured on that emit: both variants present in all three seed files, and all four inhabitance arms hold -- nega and negb refused at the list element, pos accepted, reach refused. Neither wall was eaten by the merge. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v1/stage0/src/v1_std_core.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index ef800cf006c..cf0d36f6381 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -527,6 +527,12 @@ pub enum CompilerDiagnostic { constructor_decl_name: String, span: Rc, }, + DeclaredTypeNotInhabited { + position: String, + expected: String, + got: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -678,6 +684,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { } CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::CallArgumentNameUnknown { span: s, .. } => s.clone(), @@ -727,6 +734,7 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::SourceAnnotationRefused { refusal: r, .. } => annotation_attachment_refusal_message(r.clone()), CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, .. } => v1_rt::concat(v1_rt::concat("admit_callers entry on '".to_string(), cn.clone()), "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored".to_string()), + CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::CallArgumentNameUnknown { callee: c, argument: a, declared: ds, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("call shape mismatch calling '".to_string(), c.clone()), "': no parameter named '".to_string()), a.clone()), "' (declared: [".to_string()), ds.clone().join(&", ".to_string())), "])".to_string()), From ba6ce3e1e211769b041a468c2481499b64508462 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 05:08:23 +0000 Subject: [PATCH 05/27] The wall's first landing found a real one: octet rows declared as bit-records The list-element inhabitance obligation refused six data rows in emit_on_demand_match_loop_fold_family_witness, 30 elements in all. It was right, and the annotation was wrong. data match_expected_octets: List = [0, 1, 0, 0, 0] Byte here resolves through v2.std.machine to std.bit's `type Byte { bits: List }` -- a product. A plain Int does not inhabit it. The values were never bit-records: their only consumer is `emit_host_octets_byte_string(octets: List)`, which takes the octets as numbers. So the rows declared one type, held another, and were read as a third name for the second. Nothing in the corpus noticed, because the direct-call argument position is exactly the one still exempted pending gunbc#8925 -- the value flowed into a List parameter unchecked. Corrected to List, which is what the consumer's signature already said, and dropped the now-unused Byte import rather than leave a name in scope that no longer means anything here. Verified on the committed tree, both directions, one remote dispatch: fixed exit=0 inhabit_errors=0 compiled: 149 files emitted control exit=1 inhabit_errors=30 30 hard diagnostic(s) The control restores the List annotation and nothing else, so the discriminator is the annotation itself and not the harness. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...mand_match_loop_fold_family_witness_test.dag | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag index b2e166c3811..964ee6bdf2a 100644 --- a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag +++ b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag @@ -1,7 +1,7 @@ module v2.test.execution.emit_on_demand_match_loop_fold_family_witness import std.logic { Bool } -import std.types { String } +import std.types { Int, String } import std.content_hash { ContentHash, Fnv1a64Structural } import std.measure { ByteSize, byte_size } import std.cache_interface { @@ -73,7 +73,6 @@ import v2.test.emit.fold_call_closure_fixture { fold_fixture_param_canonical_arrow, fold_fixture_param_wrong_arrow, } -import v2.std.machine { Byte } import v2.std.collection { List } @@ -122,12 +121,12 @@ fn family_cache_root_for(test_id: String) -> String { concat(family_cache_root, "/", test_id) } -data match_expected_octets: List = [0, 1, 0, 0, 0] -data match_alt_expected_octets: List = [0, 2, 0, 0, 0] -data loop_expected_octets: List = [0, 1, 0, 0, 0] -data loop_alt_expected_octets: List = [0, 2, 0, 0, 0] -data fold_expected_octets: List = [0, 7, 0, 0, 0] -data fold_alt_expected_octets: List = [0, 255, 255, 255, 255] +data match_expected_octets: List = [0, 1, 0, 0, 0] +data match_alt_expected_octets: List = [0, 2, 0, 0, 0] +data loop_expected_octets: List = [0, 1, 0, 0, 0] +data loop_alt_expected_octets: List = [0, 2, 0, 0, 0] +data fold_expected_octets: List = [0, 7, 0, 0, 0] +data fold_alt_expected_octets: List = [0, 255, 255, 255, 255] fn match_fixture_inputs() -> Inputs { inputs_for_emit_host( @@ -212,7 +211,7 @@ fn mlf_family_member_run( source: Medium, member_id: String, expect_compile_skipped: Bool, - expected_octets: List + expected_octets: List ) -> Bool { match run_emit_host_cached_with_run_args( workspace_dir: workspace, From f88b81701c218f4f2a67b7740c85bf67c237b37d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 06:06:34 +0000 Subject: [PATCH 06/27] A reachability control that asserted our own class at zero was measuring nothing Review 54993 caught a contradiction between this arm's prose and its assertion, and the prose was the honest half. The comment said the arm keys on a DIFFERENT class than the wall's, deliberately, because keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. The assertion was: violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 That is the wall's own class at zero, and it is satisfied identically by "the position is judged and our wall correctly stayed silent" and by "the position is never reached by anything" -- precisely the distinction the arm exists to draw. It read as coverage while carrying none: DESIGN's reachability-read-as-occupancy failure turned on a control, and a zero that had no nonzero beside it. The class was measured rather than guessed. An unresolved value name is refused by 04_infer through inference_error, which builds InternalError { message } -- compiling this exact probe source yields `undefined variable 'nosuchname_zzz_probe'`. The arm now demands that refusal. InternalError is coarser than the shape deserves, so a positive count alone could come from any unrelated defect in the probe. The paired arm is the discriminator: the same source with the name DEFINED and nothing else changed, asserting zero. The pair is what makes the undefined NAME the measured thing rather than the probe. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ..._inhabitance_list_element_witness_test.dag | 29 ++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag index 1ed96abeae2..9204c53e7ae 100644 --- a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -81,10 +81,37 @@ test fn w_declared_coproduct_member_is_accepted() -> Bool { // from "the position is never reached at all", which the accepting arms above cannot // distinguish on their own. It is asserted on a DIFFERENT class than the wall's, deliberately: // keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. +// +// THE ASSERTION MUST BE POSITIVE, AND AN EARLIER REVISION OF IT WAS NOT. This arm shipped +// asserting DeclaredTypeNotInhabited == 0 -- the wall's OWN class, at zero -- while the prose +// above claimed it keyed on a different one. That assertion is satisfied identically by "the +// position is judged and our wall correctly stayed silent" and by "the position is never +// reached by anything", which is precisely the distinction the arm exists to make, so it read +// as coverage while carrying none. It is DESIGN's reachability-read-as-occupancy failure +// turned on a control: a zero is only readable beside a nonzero. Corrected to demand the +// refusal it was named for (review 54993). +// +// WHY InternalError IS THE CLASS: an unresolved value name is refused by v1.compiler.04_infer +// through inference_error, which constructs InternalError { message } -- measured, not assumed +// ("undefined variable 'nosuchname_zzz_probe'" against this exact source). It is coarser than +// the shape deserves, and that coarseness is why the paired green arm below is not optional: +// alone, a positive InternalError count could be produced by any unrelated defect in the +// probe. The pair is what makes the undefined NAME the thing being measured. data undefined_name_source: String = "module probe_inhabit_reach\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [nosuchname_zzz_probe] }\n" +// The same source with the name DEFINED and nothing else changed. It is the discriminator for +// the arm above: if this also reported InternalError, the positive count there would be an +// artifact of the probe rather than evidence about the name. +data defined_name_source: String = "module probe_inhabit_reach_ok\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk() -> Rel { SameRev }\nfn probe() -> List { [mk()] }\n" + test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { - violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 + violation_count(source: undefined_name_source, wanted: "InternalError") > 0 + && violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +test fn w_reachability_control_discriminates_on_the_name() -> Bool { + violation_count(source: defined_name_source, wanted: "InternalError") == 0 + && violation_count(source: defined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 } // UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. An optional carrier at the From 08d7e6d41fe51a15d1bd05eaacbf80219aec45be Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 09:11:46 +0000 Subject: [PATCH 07/27] =?UTF-8?q?Wire=20the=20direct-call=20argument=20pos?= =?UTF-8?q?ition=20=E2=80=94=20MEASUREMENT=20FIRST,=20no=20repair=20in=20t?= =?UTF-8?q?his=20diff?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The list-element position landed in gunbc#8974. This attaches the same DeclaredTypeObligation at the direct-call argument seam, which is the position everything routes through and the one that has never judged inhabitance. WHAT THIS IS NOT: it does not touch module_skips_direct_call_arg_check. That exemption keeps its exact current meaning and population, and the 285k/67k residue behind it is not disturbed. gunbc#8925 landed the correction that deleting that arm is a NECESSARY condition someone had written as a sufficient one; this change sits beside the arm rather than removing it. WHY THE EXEMPTION'S REASON DOES NOT REACH THIS JUDGMENT. The arm exists for the TYPE judgment, whose false-positive classes are representation gaps -- brand aliases, optionality's two forms, anonymous literals, expansion depth. This relation refuses exactly two states, kernel-at-structured and payload-at-parent, and answers Undecidable for generic formals, optional carriers, unresolved formals and identity-erased produced types. All four representation classes are Undecidable or Inhabits under it. That is the same argument direct_call_shape_diags already makes in this file for sitting un-exempted at this very seam (direct_call_shape_wall_note): a label has no representation, so the exemption's reason does not reach it. The precedent is in the file, not built for this case. It attaches beside direct_call_structured_application_mismatch_diags, which is already un-exempted here and already reads app.formal_subst as declared and arg_value(n: ta) as produced -- the exact pair the obligation needs. HOISTED, NOT INLINE, AND THE REASON IS A TRAP WORTH RECORDING. Written inline at the seam it refused at regen: call shape mismatch calling function value 'resolved_type': named argument 'n' is not supported -- use positional arguments The seam binds a local `let resolved_type = match sig { ... }`, which shadows the top-level function of the same name, so the fold was calling a Node value as a function. The shadow is invisible to reading and the diagnostic names the call, not the binding five lines above it. Hoisting to a top-level fn beside the judgment it mirrors is both the fix and this file's existing convention. THE POPULATION IS NOT ASSERTED HERE. Two local attempts to measure it died: required-ci ran 116 minutes against CI's 44 for the same phases, and the whole-tree diagnostic histogram was OOM-killed on the runner (exit 137), whose empty output means the instrument died rather than that the corpus is clean. CI has the resources, so this branch exists to have CI produce the census -- by position, by declared-to-produced shape, by file -- before anything is repaired. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v1/04_infer.dag | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index ab59ce42ec8..ce860c4997d 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2492,6 +2492,30 @@ fn direct_call_structured_application_mismatch_diags( ) } +fn direct_call_argument_inhabitance_diags( + plan: List, + scope: InferScope +) -> List { + flat_map( + plan, + app => + match app.matched_arg { + Present { value: ta } => + let actual_expr = arg_value(n: ta) + declared_type_obligation_diags( + obligation: DeclaredTypeObligation { + position: PositionDirectCallArgument, + declared: app.formal_subst, + produced: resolved_type(n: actual_expr), + span: actual_expr.span + }, + scope: scope + ) + Absent => [] + } + ) +} + fn container_element_nominal_brand_mismatch( formal: Node, actual: Node, @@ -4053,6 +4077,10 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu plan: call_application_plan, scope: scope ) + let inhabitance_arg_diags = direct_call_argument_inhabitance_diags( + plan: call_application_plan, + scope: scope + ) InferResult { typed: make_named_expr_node( name: func_name, expr_data: ExprCall { call_semantics: Present { value: PlainCallSemantics }, descent_evidence: none }, @@ -4061,7 +4089,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu span: span, name_span: node_name_span(n: texpr) ), - diagnostics: concat(arg_diags, concat(arg_shape_diags, concat(arg_compat_diags, structured_arg_diags))) + diagnostics: concat(arg_diags, concat(arg_shape_diags, concat(arg_compat_diags, concat(structured_arg_diags, inhabitance_arg_diags)))) } } else { let first_arg_type = match typed_args |> first { From ba2f6e32b4cde7967858da1b853fc26db1d635f0 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 10:16:35 +0000 Subject: [PATCH 08/27] =?UTF-8?q?The=20seed=20mirror=20the=20.dag=20change?= =?UTF-8?q?=20requires=20=E2=80=94=20without=20it=20the=20floor=20measured?= =?UTF-8?q?=20nothing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first push of this branch carried the .dag wiring and not its regenerated mirror, so CI refused at the regen phase: required-regen: first_generation_equal=false ... FAIL generated surface drift: v1_compiler_infer.rs The floor phase therefore never ran, and the corpus reported ZERO DeclaredTypeNotInhabited diagnostics. That zero is not a measurement. It is the two-generation property doing exactly what it is supposed to: cargo builds the COMMITTED mirror, so a .dag edit is invisible until regen emits a new one, and a gate that stops before the floor produces an absence that looks identical to a clean corpus. This is the third instrument in a row on this question to fail toward zero -- a 116-minute buffered run I could not observe, an OOM-killed histogram that printed empty section headers under exit=137, and now a regen refusal that skipped the measuring phase entirely. All three would have supported the sentence "zero direct-call inhabitance defects corpus-wide", and all three would have been fabricating it. A zero is only readable beside a nonzero. The mirror was regenerated remotely and transported back verified rather than rebuilt by hand: exactly one file drifted (v1_compiler_infer.rs, confirmed by comparing every candidate file against its committed pair), and the decoded bytes match the candidate's sha256 07a3256ede2120bf9c65f4934fdc94f25fe258dcc2c7f4531d5db9a43d8d0fae. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v1/stage0/src/v1_compiler_infer.rs | 41 +++++++++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index ced4032c1ee..97151302b40 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -3661,6 +3661,37 @@ pub fn direct_call_structured_application_mismatch_diags( } } +pub fn direct_call_argument_inhabitance_diags( + plan: Rc>>, + scope: Rc, +) -> Rc>> { + Rc::new({ + let mut __result = Vec::new(); + for app in plan.iter().cloned() { + __result.extend( + (*match app.matched_arg.clone() { + Some(ta) => { + let actual_expr = arg_value(ta.clone()); + declared_type_obligation_diags( + Rc::new(DeclaredTypeObligation { + position: DeclaredTypePosition::PositionDirectCallArgument, + declared: app.formal_subst.clone(), + produced: resolved_type(actual_expr.clone()), + span: actual_expr.span.clone(), + }), + scope.clone(), + ) + } + None => Rc::new(vec![]), + }) + .iter() + .cloned(), + ); + } + __result + }) +} + pub fn container_element_nominal_brand_mismatch( formal: Rc, actual: Rc, @@ -6901,6 +6932,11 @@ pub fn infer_expr_body( call_application_plan.clone(), scope.clone(), ); + let inhabitance_arg_diags = + direct_call_argument_inhabitance_diags( + call_application_plan.clone(), + scope.clone(), + ); Rc::new(InferResult { typed: make_named_expr_node( func_name.clone(), @@ -6923,7 +6959,10 @@ pub fn infer_expr_body( arg_shape_diags.clone(), v1_rt::concat( arg_compat_diags.clone(), - structured_arg_diags.clone(), + v1_rt::concat( + structured_arg_diags.clone(), + inhabitance_arg_diags.clone(), + ), ), ), ), From 30ce9d2c07b4fd0601337ffedbd5cebc3d661669 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 10:38:17 +0000 Subject: [PATCH 09/27] The octet rows say why they are Int, and name the carrier that would replace them Review 55052 approved and asked, non-blocking, for a tracked pointer toward a proper octet carrier, on the ground that no Octet alias exists today. One does, and it changes the shape of the answer: extdeps.network.ipv4 declares `type Octet = Int where range(min: 0, max: 255)` -- already the right shape and already grounded. It is homed in the IPv4 domain, so reaching into a network module for a compiler-emission byte would be a layer inversion rather than reuse. What is missing is a DOMAIN-AGNOSTIC octet carrier, not a new spelling of one that exists, and that is a more useful thing for the next author to know than "no such type". The annotation records three facts a reader of these rows would otherwise have to re-derive: that Byte is a bit-record so the Int literals never inhabited it; that List is the consumer's own declared type rather than a weakened carrier; and that Int is nonetheless weaker than an octet deserves, with the replacement named and the order stated -- the parameter moves first, since the declaration follows its consumer. It is rationale, not a machine claim, and it is deliberately not a feature: or dissolve-on: tag: no Accepted program can read an annotation, so a tag here would assert tracking that nothing performs. When the carrier lands, the obligation belongs on it. Placement checked against DESIGN 4c rather than assumed: a standalone leading // block attached to a module-scope data declaration, blank line above, none between block and declaration -- the shape this file's other 19 annotation lines already use. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...nd_match_loop_fold_family_witness_test.dag | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag index 964ee6bdf2a..8c93523b661 100644 --- a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag +++ b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag @@ -121,6 +121,25 @@ fn family_cache_root_for(test_id: String) -> String { concat(family_cache_root, "/", test_id) } +// WHY List AND NOT List, AND WHAT WOULD REPLACE IT. These rows are octet +// values compared against emitted bytes. They were declared List while holding +// integers, which the list-element inhabitance obligation refused: std.bit's Byte is +// `type Byte { bits: List }`, a bit-record, so an Int literal never inhabited it. +// The consumer's signature already carried the right type -- v2.compiler.emit_host +// `emit_host_octets_byte_string(octets: List)` -- so this is the declaration +// agreeing with its single authority, not a carrier weakened to satisfy a wall. +// +// Int is nonetheless weaker than the values deserve: an octet is 0..255 and nothing +// here says so. The correctly shaped type already exists and is grounded -- +// extdeps.network.ipv4 `Octet`, declared as Int refined by range(min: 0, max: 255) -- +// but it is homed in the IPv4 domain, and reaching into a network module for a +// compiler-emission byte would be the layer inversion DESIGN 3 warns about rather +// than a reuse. What is missing is a domain-agnostic octet carrier, not a new +// spelling of one that exists. +// +// So the pointer, deliberately stated as rationale rather than a machine claim: when +// such a carrier lands, these rows and emit_host_octets_byte_string's parameter move +// to it together -- the parameter first, since the declaration follows its consumer. data match_expected_octets: List = [0, 1, 0, 0, 0] data match_alt_expected_octets: List = [0, 2, 0, 0, 0] data loop_expected_octets: List = [0, 1, 0, 0, 0] From a71096d01a78703058372cd64b160131d6d48655 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 11:02:45 +0000 Subject: [PATCH 10/27] =?UTF-8?q?The=20class=20was=20never=20undecidable?= =?UTF-8?q?=20=E2=80=94=20it=20was=20unconsulted?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The census refused 33 correct sites: a kernel integer at a parameter declared std.nat.Nat. Reading it structurally, that is kernel-at-structured, because std.nat declares `type Nat = CommutativeSemiring` and std.integer declares `type Int = AbelianGroup>` -- the canonical form of both is an algebraic STRUCTURE while their values are authored as kernel literals. The obvious reading is that this is undecidable and owed a counted advisory: dag/std/magnitude.dag is three lines with no body, so nothing there relates Magnitude to a kernel integer, and "40 is a Nat" looks like a convention the corpus relies on and never declares. That reading is wrong, and stopping at magnitude.dag is what makes it look right. v1.compiler.coercion numeric_realization_declaring_modules already records that dag/std/nat.dag and dag/std/integer.dag realize natively, and decl_file_realizes_natively answers it. So the relation was refusing on a question an authority in the tree already decides. Counting the residue would have recorded a deficit that does not exist and handed the next author a number to explain away. decl_file_realizes_natively is the surface used, and the choice is deliberate: it takes only decl_file. The neighbouring lookup_checkpoint takes a RenderTarget, so it would have made an EMISSION fact answer a SOURCE-level question -- fact in one carrier, operation governed by another, and the arrow between them invented. THREE PROPERTIES, EACH WITH AN ARM RATHER THAN AN INTENTION: It is a conjunction. The produced value must also be a kernel numeric, so a String at a natively-realized Nat stays refused -- without that arm, an implementation admitting anything at such a type would pass the positive arm. It fails closed on unknown identity. decl_file_realizes_natively answers false for the empty string, which is what an unestablished identity yields, and no fallback is added here that would undo it. It is keyed on the declaring module, never the spelling. std.nat.Nat realizes natively; v2.std.nat.Nat is the Peano coproduct Zero | Succ and must NOT. That last pair is enrolled as a permanent RED rather than argued in prose. A kernel integer at the Peano Nat must refuse, and if the discrimination ever decays to a spelling comparison that arm admits and goes green. DESIGN 4b(4) keeps a climb's evidence for exactly this reason. The witness declares SubstrateInputsOnly deliberately. A ReadsLiveTree witness is discovered, counted in declined_live, and never folded -- the sibling direct_call_argument_type_witness calls that state "enrolled and inert, the specification-without-execution state DESIGN 5 names, wearing the costume of a populated probe corpus". A regression control has to run. Acceptance test for the next measurement: cause 1 to 0 refused AND 0 counted; causes 2 and 3 unchanged at 16 and 1 sites. If either of those drops, the arm is too wide. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...e_inhabitance_direct_call_witness_test.dag | 79 +++++++++++++++++++ src/v1/04_infer.dag | 46 +++++++++++ 2 files changed, 125 insertions(+) create mode 100644 dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag 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 new file mode 100644 index 00000000000..a7f997b6a57 --- /dev/null +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -0,0 +1,79 @@ +module test.claim.declared_type_inhabitance_direct_call_witness + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CensusObserved, + CensusNotRunnable, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// SUBSTRATE-ONLY BY DELIBERATE CHOICE, AND THE SIBLING FILE EXPLAINS WHY IN ITS OWN VOICE. +// test.claim.direct_call_argument_type_witness records that an assertion authored in a +// ReadsLiveTree module is "enrolled and inert -- the specification-without-execution state +// DESIGN 5 names, wearing the costume of a populated probe corpus", because a ReadsLiveTree +// witness is discovered, counted in declined_live, and never folded. These arms are the +// regression control for a discrimination that must not decay, so they are authored where the +// floor actually folds them. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn violation_count(source: String, wanted: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count(rows: census_rows_of_class(rows: rows, wanted: wanted)) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// THE PAIR THIS FILE EXISTS FOR. std.nat and v2.std.nat both declare a type spelled Nat and they +// are NOT the same concept: std.nat.Nat is CommutativeSemiring and realizes natively +// as a kernel integer, while v2.std.nat.Nat is the Peano coproduct Zero | Succ { prev: Nat }. +// v1.compiler.coercion numeric_realization_identity_note names this exact pair as the hazard a +// bare-name rule gets wrong. +// +// declared_type_inhabitance admits a kernel numeric at the FIRST by consulting +// decl_file_realizes_natively, which is keyed on the resolved DECLARING MODULE. If that +// discrimination ever decays to a spelling comparison, the RED arm below admits and goes green, +// which is the whole point of enrolling it: DESIGN 4b(4) keeps the evidence after a climb +// precisely so the higher rung stays real. + +// RED -- a kernel integer at the PEANO Nat. 5 is not Zero and not Succ, and no realization row +// covers src/v2/std/nat.dag, so this must refuse. It is the arm that fails if identity ever +// collapses to the spelling "Nat". +data peano_nat_arg_source: String = "module probe_inhabit_peano\nimport v2.std.nat { Nat }\nfn takes_peano(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_peano(n: 5) }\n" + +test fn w_kernel_numeric_at_the_peano_nat_is_refused() -> Bool { + violation_count(source: peano_nat_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// GREEN -- the same literal at the NATIVE Nat. Structurally this is a kernel value at an +// algebraic record and reads identically to the arm above; only the declaring module differs. +// It must be admitted, and admitted SILENTLY: the class is decidable, so there is no residue to +// count and nothing here asserts one. +data native_nat_arg_source: String = "module probe_inhabit_native\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: 40) }\n" + +test fn w_kernel_numeric_at_the_natively_realized_nat_is_admitted() -> Bool { + violation_count(source: native_nat_arg_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// THE ADMISSION IS A CONJUNCTION, NOT A CARVE-OUT FOR THE TYPE. The declared side realizing +// natively is only half of it; the produced value must ALSO be a kernel numeric. A String at the +// same natively-realized position stays refused. Without this arm, an implementation that +// admitted ANYTHING at a natively-realized declared type would pass the green arm above. +data string_at_native_nat_source: String = "module probe_inhabit_native_str\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: \"forty\") }\n" + +test fn w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused() -> Bool { + violation_count(source: string_at_native_nat_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// REACHABILITY, ON A DIFFERENT CLASS THAN THE WALL'S. An undefined name at the same argument +// position must be refused by SOMETHING, or the two accepting arms above cannot distinguish "the +// position is judged and the value was admitted" from "the position is never reached". An +// unresolved value name is refused through inference_error, which constructs +// InternalError { message } -- measured, not assumed. +data undefined_name_arg_source: String = "module probe_inhabit_dc_reach\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: nosuchname_zzz_dc) }\n" + +test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { + violation_count(source: undefined_name_arg_source, wanted: "InternalError") > 0 +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index ce860c4997d..e09af56ed3a 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -91,6 +91,7 @@ import v1.compiler.infer_method { builtin_kernel_seed_diagnostics, infer_builtin_call_type, resolve_builtin_call_type } import v1.compiler.infer_cycle { detect_type_cycles_kahn } +import v1.compiler.coercion { decl_file_realizes_natively, type_reference_decl_file } import v1.compiler.infer_env { TypeEnv, TypeBinding, TypeEnvCache, empty_type_env_cache, merge_type_env_cache, merge_type_env_cache_guarded, GuardedTypeEnvCacheMerge, TypeEnvCacheMergeConflict, @@ -2171,6 +2172,9 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco InhabitanceUndecidable { reason: UndecidableFormalUnresolved } } else if produced_name == "" { InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if declared_realizes_as_kernel_numeric( + declared: declared, produced: produced, source_indices: source_indices) { + Inhabits } else if kernel_value_declared_type_mismatch( formal: declared, actual: produced, type_env: scope.type_env, source_indices: source_indices) { @@ -2184,6 +2188,48 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco // The obligation carries its own position, so ONE emitter locates every refusal. A per-position // diagnostic function would be the N-representation problem moved one layer down. +// WHY A KERNEL LITERAL AT AN ALGEBRAICALLY-DECLARED NUMERIC IS ADMITTED, AND WHY THIS IS +// CONSULTING AN AUTHORITY RATHER THAN WIDENING AN ARM. std.nat declares +// `type Nat = CommutativeSemiring` and std.integer declares +// `type Int = AbelianGroup>`: the canonical form of both is an algebraic +// STRUCTURE while their values are authored as kernel integer literals. Read structurally that +// is kernel-at-structured and the relation refused it -- measured, 33 of 50 sites at the +// direct-call seam, every one correct code. +// +// The corpus does not leave this to convention. v1.compiler.coercion +// numeric_realization_declaring_modules records that exactly these declaring modules realize +// natively, and decl_file_realizes_natively answers it. So the class was never undecidable, it +// was UNCONSULTED -- which is why nothing here is counted: a residue would record a deficit +// that does not exist. +// +// THREE PROPERTIES THIS RELIES ON, none of them incidental: +// IDENTITY, NOT SPELLING. The authority is keyed on the resolved declaring module. +// numeric_realization_identity_note names the exact hazard: std.nat.Nat realizes natively +// while v2.std.nat.Nat is the Peano coproduct Zero|Succ and must NOT, so a bare-name rule +// admits the wrong one. The enrolled RED for that pair is the regression control. +// FAIL-CLOSED ON UNKNOWN IDENTITY. decl_file_realizes_natively answers false for the empty +// string, and the empty string is what an unestablished identity yields. No fallback is +// added here, so a site that cannot establish identity keeps refusing. +// A CONJUNCTION, NOT A CARVE-OUT. The produced value must ALSO be a kernel numeric, so a +// String literal at a Nat-declared position stays refused. +// +// SOURCE-LEVEL, NOT EMISSION. decl_file_realizes_natively takes only decl_file; the neighbouring +// lookup_checkpoint takes a RenderTarget and would have made an emission fact answer a +// source-level question, which is why it is deliberately not the surface used here. +fn declared_realizes_as_kernel_numeric( + declared: Node, + produced: Node, + source_indices: Map +) -> Bool { + let produced_name = authored_name_at(source_indices: source_indices, node: produced) + let produced_is_kernel_numeric = produced_name == "Int" || produced_name == "Float" + if produced_is_kernel_numeric == false { + false + } else { + decl_file_realizes_natively(decl_file: type_reference_decl_file(n: declared)) + } +} + fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: InferScope) -> List { match declared_type_inhabitance(obligation: obligation, scope: scope) { Inhabits => [] From 9cccff4b34da0d3414a4bf97b2a52f2f598afa61 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 11:03:14 +0000 Subject: [PATCH 11/27] =?UTF-8?q?Every=20arm=20in=20this=20witness=20was?= =?UTF-8?q?=20enrolled,=20reviewed,=20cited=20=E2=80=94=20and=20executed?= =?UTF-8?q?=20by=20nothing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The file declared ReadsLiveTree. A ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED by the required floor. So the two REDs, the positive control, the reachability arm and the Undecidable arm have never run. That is worse than having written no test. Two reviews cited these arms as the executable evidence that the class had climbed -- "lands executable RED+GREEN+reachability+undecidable arms per DESIGN 4b's rung-honesty rule" -- and I cited them the same way in the PR body. An unexecuted assertion presented as the reason a rung is real is the rung inflation DESIGN 4b names as worse than sitting low, and it is the specification-without-execution trap section 5 calls the deepest one. I did not find this by reading my own file. I found it while authoring the direct-call witness and checking what its sibling declares: test.claim.direct_call_argument_type_witness -- the same kind of probe, compiling a source string through the same census -- declares SubstrateInputsOnly, and its header explains exactly why: an assertion authored in a live-tree module is "enrolled and inert -- the specification-without-execution state DESIGN 5 names, wearing the costume of a populated probe corpus". Nothing here needs a live read. Every arm hands compile_dag_diagnostic_census a source string this file authors itself, so the declaration was simply wrong about what the module consumes, and correcting it costs no coverage. WHAT I AM NOT CLAIMING. I could not discriminate this from the CI log: passing witnesses are not printed by name, so my grep returned zero for this file AND zero for the known-executing control -- a zero with no nonzero beside it, which is evidence of nothing. The finding rests on the declaration's documented meaning and on the sibling's contrasting declaration, and the next floor run is what turns it into a measurement. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...ype_inhabitance_list_element_witness_test.dag | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag index 9204c53e7ae..25b0a6312d1 100644 --- a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -8,9 +8,19 @@ import gunbc.compile_diagnostic_census { census_total_count } import std.types { String, Bool, Int } -import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } - -data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// SUBSTRATE-ONLY, AND THE EARLIER ReadsLiveTree DECLARATION MADE EVERY ARM BELOW INERT. A +// ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED -- so these +// arms were enrolled, reviewed, cited as this PR's executable evidence, and executed by nothing. +// That is the specification-without-execution trap DESIGN 5 calls the deepest one, and it is +// worse here than a missing test would have been, because the arms were named as the reason the +// class had climbed. The sibling test.claim.direct_call_argument_type_witness had already made +// this exact move and said why: an assertion in a live-tree module is "enrolled and inert ... +// wearing the costume of a populated probe corpus". This file needs no live read -- every arm +// hands compile_dag_diagnostic_census a source STRING it authors itself -- so nothing is lost by +// declaring what it actually consumes. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // THE FLOOR CLAUSE THIS GUARDS: a value accepted at a declared-type position inhabits that // declared type. DESIGN names it as floor, so a breach is a below-baseline safety regression From d7f63d44988dce05f054120c57141f46e4258dcd Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 11:13:42 +0000 Subject: [PATCH 12/27] The seed mirror for the decidable admit, transported verified Exactly one file drifts (v1_compiler_infer.rs, established by comparing every candidate file against its committed pair, not by trusting the regen summary), and the decoded bytes match the candidate's sha256 e4170a14243ece044b711f62a7931e3b3cef67703d151ed0ea0587f272736f9f. Without this the .dag change is invisible: cargo builds the COMMITTED mirror, so the floor would run the old relation and report a population that says nothing about the new one. The last push of this branch made exactly that mistake and its zero was not a measurement. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v1/stage0/src/v1_compiler_infer.rs | 44 ++++++++++++++++++++------ 1 file changed, 35 insertions(+), 9 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 97151302b40..9b41fc6a3cc 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -53,6 +53,7 @@ pub use crate::std_termination::{ }; pub use crate::std_types::{container_param_name, is_kernel_type, kernel_type_set}; pub use crate::std_types::{NonEmptyStr, SourceSpan}; +pub use crate::v1_compiler_coercion::{decl_file_realizes_natively, type_reference_decl_file}; pub use crate::v1_compiler_infer_access::AccessCheckResultNode; pub use crate::v1_compiler_infer_access::{check_index_access_node, check_slice_access_node}; pub use crate::v1_compiler_infer_cycle::detect_type_cycles_kahn; @@ -3160,26 +3161,34 @@ pub fn declared_type_inhabitance( reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, }) } else { - if kernel_value_declared_type_mismatch( + if declared_realizes_as_kernel_numeric( declared.clone(), produced.clone(), - scope.type_env.clone(), source_indices.clone(), ) { - Rc::new(InhabitanceVerdict::InhabitanceRefused { - reason: InhabitanceRefusalReason::RefusedKernelAtStructured, - }) + Rc::new(InhabitanceVerdict::Inhabits) } else { - if coproduct_payload_where_parent_required( + if kernel_value_declared_type_mismatch( declared.clone(), produced.clone(), - scope.clone(), + scope.type_env.clone(), + source_indices.clone(), ) { Rc::new(InhabitanceVerdict::InhabitanceRefused { - reason: InhabitanceRefusalReason::RefusedPayloadAtParent, + reason: InhabitanceRefusalReason::RefusedKernelAtStructured, }) } else { - Rc::new(InhabitanceVerdict::Inhabits) + if coproduct_payload_where_parent_required( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedPayloadAtParent, + }) + } else { + Rc::new(InhabitanceVerdict::Inhabits) + } } } } @@ -3189,6 +3198,23 @@ pub fn declared_type_inhabitance( } } +pub fn declared_realizes_as_kernel_numeric( + declared: Rc, + produced: Rc, + source_indices: Rc>>, +) -> bool { + { + let produced_name = authored_name_at(source_indices.clone(), produced.clone()); + let produced_is_kernel_numeric = ((produced_name.clone() == "Int".to_string()) + || (produced_name.clone() == "Float".to_string())); + if (produced_is_kernel_numeric.clone() == false) { + false + } else { + decl_file_realizes_natively(type_reference_decl_file(declared.clone())) + } + } +} + pub fn declared_type_obligation_diags( obligation: Rc, scope: Rc, From d4b0e524065e99fd19987abcaa42d7c707898d2c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 11:53:56 +0000 Subject: [PATCH 13/27] The 17 repairs the wall forces, landing with the wall per the 8876 precedent A wall that correctly refuses 17 real defects refuses the WHOLE CORPUS at floor preparation, so with the wall on and the repairs absent main is red. That makes them one change, not two -- the shape 8876 used when the same ruling applied. SIXTEEN PAYLOAD-AT-PARENT SITES. A Fnv1a64Structural stored where the ContentHash union is declared -- the class 8876 repaired at five production sites and deliberately did not widen to; these are that residue. The repair is 8876's construction reached through the module's own named surface: std.content_hash `as_content_hash_structural(s)` is literally `Fnv1a64(s)`, so it is the same move, not a second idiom. It is also the local convention: the very call sites being repaired already use its sibling as_content_hash_cryptographic for the Sha256 case, one argument above. materialization_provider_witness_test.dag 14 heal_revalidation.dag 1 native_cache_fusion.dag 1 NOT A CODEMOD, AND THAT MATTERS HERE. materialization_provider carries 34 content_hash_atom calls and only 14 are at a ContentHash-declared position; the other 20 legitimately produce Fnv1a64Structural. A global rewrite would have corrupted them silently, so only the flagged lines were touched. heal_revalidation is the one whose producer is not a call: the enclosing function declares `required_roster: Fnv1a64Structural` and passes it to a ContentHash parameter. Wrapped at the call rather than narrowing the declaration -- 8876's ARM A ruling, wrap the construction, since narrowing severs the carrier from the union its peers use. ONE ACCUMULATOR DEFECT, AND IT NEEDED NO NEW HELPER. dag_acceptance's post_front_end_obligations returns List and snocs DagStageObligation, while seeding from no_rows() : List. The element types disagree; it is latent only because the list is empty, so nothing ever observes an element of the wrong type. The fix is neither a second accumulator nor a generic one. `no_obligations() -> List` ALREADY EXISTS four lines above no_rows(), and the fold now uses it. A generic `no_rows()` would have been worse than the defect: with no element type to fix it is a nickname for `[]`, and the reason these helpers exist at all is to give a fold's init an element type inference cannot supply. The other three folds over no_rows() return List and are correct and untouched -- one shared helper, four uses, one wrong. That discrimination is what the wall bought. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- dag/gunbc/heal_revalidation.dag | 4 +-- .../materialization_provider_witness_test.dag | 29 ++++++++++--------- src/v2/workflow/dag_acceptance.dag | 2 +- src/v2/workflow/native_cache_fusion.dag | 4 +-- 4 files changed, 20 insertions(+), 19 deletions(-) diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag index ae2ca155828..1edf0d9f50f 100644 --- a/dag/gunbc/heal_revalidation.dag +++ b/dag/gunbc/heal_revalidation.dag @@ -1,6 +1,6 @@ module gunbc.heal_revalidation -import std.content_hash { Fnv1a64Structural } +import std.content_hash { Fnv1a64Structural, as_content_hash_structural } import std.types { CommitSha, NonEmptyStr } import gunbc.merge_admission { CheckCoverage, @@ -151,7 +151,7 @@ fn classify_heal_revalidation_admission( if check_coverage_admits( coverage: coverage, required_head: healed_head, - required_roster: required_roster, + required_roster: as_content_hash_structural(structural: required_roster), required_gates: required_gates ) { HealRevalidationAdmittedExactCoverage { healed_head: healed_head } diff --git a/dag/test/claim/materialization_provider_witness_test.dag b/dag/test/claim/materialization_provider_witness_test.dag index feb4945dd50..000c7dbffe9 100644 --- a/dag/test/claim/materialization_provider_witness_test.dag +++ b/dag/test/claim/materialization_provider_witness_test.dag @@ -6,6 +6,7 @@ import std.content_hash { Fnv1a64, content_hash_atom, as_content_hash_cryptographic, + as_content_hash_structural, sha256_hex_digest, } import std.interface_summary { InterfaceHash, module_key, typed_module_key } @@ -258,26 +259,26 @@ test fn red_sha256_at_fnv1a64_seam_refuses_without_alias() -> Bool { Present { value: sha_b } => { let refused_a = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_a), - compiler_digest: content_hash_atom(value: "compiler-identity-1"), - stored_request_key: content_hash_atom(value: "closure-1"), + compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), + stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), stored_semantic_digest: witness_closure_digest(), - graph_digest: content_hash_atom(value: "closure-graph-1"), + graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), graph_bytes: byte_size(count: 60), - indices_digest: content_hash_atom(value: "closure-indices-1"), + indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), indices_bytes: byte_size(count: 25), - union_digest: content_hash_atom(value: "closure-diagnostics-1"), + union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), union_bytes: byte_size(count: 15) ) let refused_b = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_b), - compiler_digest: content_hash_atom(value: "compiler-identity-1"), - stored_request_key: content_hash_atom(value: "closure-1"), + compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), + stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), stored_semantic_digest: witness_closure_digest(), - graph_digest: content_hash_atom(value: "closure-graph-1"), + graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), graph_bytes: byte_size(count: 60), - indices_digest: content_hash_atom(value: "closure-indices-1"), + indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), indices_bytes: byte_size(count: 25), - union_digest: content_hash_atom(value: "closure-diagnostics-1"), + union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), union_bytes: byte_size(count: 15) ) lookup_is_refused_cross_family_content_hash(l: refused_a) @@ -411,7 +412,7 @@ test fn red_admission_wrong_content_is_refused() -> Bool { store: witness_empty_store(budget_count: 1000), req: witness_closure_request(), artifact: witness_complete_closure_artifact(), - observed_digest: content_hash_atom(value: "closure-payload-corrupt") + observed_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-payload-corrupt")) ) admission_is_refused_wrong_content_write(a: a) && (admission_is_admitted(a: a) == false) } @@ -464,9 +465,9 @@ fn witness_hash_list_contains(xs: List, wanted: ContentHash) -> Boo fn witness_carries_the_canonical_three_digests(a: MaterializedArtifact) -> Bool { let ds = artifact_carried_outputs(artifact: a) |> map(o => o.digest) (ds.count() == 3) - && witness_hash_list_contains(xs: ds, wanted: content_hash_atom(value: "closure-graph-1")) - && witness_hash_list_contains(xs: ds, wanted: content_hash_atom(value: "closure-indices-1")) - && witness_hash_list_contains(xs: ds, wanted: content_hash_atom(value: "closure-diagnostics-1")) + && witness_hash_list_contains(xs: ds, wanted: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1"))) + && witness_hash_list_contains(xs: ds, wanted: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1"))) + && witness_hash_list_contains(xs: ds, wanted: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1"))) } test fn understated_bytes_alone_hold_every_part_digest_fixed() -> Bool { diff --git a/src/v2/workflow/dag_acceptance.dag b/src/v2/workflow/dag_acceptance.dag index 7ae89c50821..78091a80bf9 100644 --- a/src/v2/workflow/dag_acceptance.dag +++ b/src/v2/workflow/dag_acceptance.dag @@ -970,7 +970,7 @@ fn is_front_end_obligation(obligation: DagStageObligation) -> Bool { } fn post_front_end_obligations(effective: List) -> List { - fold(effective, init: no_rows(), f: fn(acc, o) { + fold(effective, init: no_obligations(), f: fn(acc, o) { if is_front_end_obligation(obligation: o) { acc } else { list_snoc_item(xs: acc, item: o) } }) } diff --git a/src/v2/workflow/native_cache_fusion.dag b/src/v2/workflow/native_cache_fusion.dag index 868c3216704..fbe8dcc6cce 100644 --- a/src/v2/workflow/native_cache_fusion.dag +++ b/src/v2/workflow/native_cache_fusion.dag @@ -5,7 +5,7 @@ import std.emit_on_demand { EmitOnDemandCacheReceipt, materialization_for_lookup } import std.content_hash { ContentHash } -import std.content_hash { content_hash_atom } +import std.content_hash { content_hash_atom, as_content_hash_structural } import std.realization { Materialization, Share, Recompute } import v2.std.logic { Bool } import v2.std.text { String } @@ -32,7 +32,7 @@ fn model_lookup_for(o: HostWarmObservation, key: ContentHash) -> EmitOnDemandLoo } fn fusion_agreement_holds_for(o: HostWarmObservation) -> Bool { - let key = content_hash_atom(value: "fusion-law-synthetic-key") + let key = as_content_hash_structural(structural: content_hash_atom(value: "fusion-law-synthetic-key")) let model_share = materialization_for_lookup(lookup: model_lookup_for(o: o, key: key)) == Share host_compile_skipped(o: o) == model_share } From 3106d524450ae754d62d76d61e3f7fe1096b679a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 12:53:26 +0000 Subject: [PATCH 14/27] =?UTF-8?q?8876's=20repair=20shape=20does=20NOT=20ap?= =?UTF-8?q?ply=20to=20these=2016=20sites=20=E2=80=94=20reverting=20the=20w?= =?UTF-8?q?rap,=20keeping=20the=20one=20repair=20that=20was=20real?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ruling said to copy 8876's shape and to STOP rather than improvise if it did not apply. It does not apply, and the measurement is how I know rather than a reading: wrapping the 16 sites turned two PASSING witnesses RED. test.claim.materialization_provider_witness.understated_bytes_alone_hold_every_part_digest_fixed test.claim.heal_revalidation_witness.only_exact_healed_head_complete_coverage_admits WHY, AND IT IS THE SAME LATENT-DEFECT MECHANISM ONE LEVEL OUT. witness_hash_list_contains(xs: List, wanted: ContentHash) declares BOTH sides as the union. It is passed `ds`, a list of o.digest, and dag/std/artifact_store.dag declares those fields as raw Fnv1a64Structural. So the declaration lies on both sides and the comparison was raw-against-raw, which agrees with itself. Wrapping only `wanted` made ONE side honest and the equality stopped matching. That is exactly what DESIGN describes: a declaration that lies is inert while every consumer contradicts it in the same direction, and detonates on the first consumer that takes it at its word. My repair was that first consumer. 8876 is not this. It wrapped a CONSTRUCTION whose consumer genuinely expected the union, so one edit made producer and consumer agree. Here the consumer's own declaration is part of the lie, and the honest repair is to make the PRODUCER a ContentHash -- i.e. change artifact_store's closure_digest/content_digest fields from Fnv1a64Structural to ContentHash and follow every producer and consumer of them. That is a model change in std, in someone else's carrier, and it is not mechanical application of an established shape. KEPT, because it is a real defect and its repair is genuinely mechanical: dag_acceptance's post_front_end_obligations now seeds from no_obligations() rather than no_rows(). Element types agreed nowhere before; they agree now; the helper it should have used already existed four lines away. WHAT THIS LEAVES: the wall still refuses the 16 payload-at-parent sites, so the floor still cannot prepare, and this branch still cannot go green. That is not a reason to soften the wall -- the 16 refusals are correct. It is a reason the repair belongs to the carrier's owner. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- dag/gunbc/heal_revalidation.dag | 4 +-- .../materialization_provider_witness_test.dag | 29 +++++++++---------- src/v2/workflow/native_cache_fusion.dag | 4 +-- 3 files changed, 18 insertions(+), 19 deletions(-) diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag index 1edf0d9f50f..ae2ca155828 100644 --- a/dag/gunbc/heal_revalidation.dag +++ b/dag/gunbc/heal_revalidation.dag @@ -1,6 +1,6 @@ module gunbc.heal_revalidation -import std.content_hash { Fnv1a64Structural, as_content_hash_structural } +import std.content_hash { Fnv1a64Structural } import std.types { CommitSha, NonEmptyStr } import gunbc.merge_admission { CheckCoverage, @@ -151,7 +151,7 @@ fn classify_heal_revalidation_admission( if check_coverage_admits( coverage: coverage, required_head: healed_head, - required_roster: as_content_hash_structural(structural: required_roster), + required_roster: required_roster, required_gates: required_gates ) { HealRevalidationAdmittedExactCoverage { healed_head: healed_head } diff --git a/dag/test/claim/materialization_provider_witness_test.dag b/dag/test/claim/materialization_provider_witness_test.dag index 000c7dbffe9..feb4945dd50 100644 --- a/dag/test/claim/materialization_provider_witness_test.dag +++ b/dag/test/claim/materialization_provider_witness_test.dag @@ -6,7 +6,6 @@ import std.content_hash { Fnv1a64, content_hash_atom, as_content_hash_cryptographic, - as_content_hash_structural, sha256_hex_digest, } import std.interface_summary { InterfaceHash, module_key, typed_module_key } @@ -259,26 +258,26 @@ test fn red_sha256_at_fnv1a64_seam_refuses_without_alias() -> Bool { Present { value: sha_b } => { let refused_a = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_a), - compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), - stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), + compiler_digest: content_hash_atom(value: "compiler-identity-1"), + stored_request_key: content_hash_atom(value: "closure-1"), stored_semantic_digest: witness_closure_digest(), - graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), + graph_digest: content_hash_atom(value: "closure-graph-1"), graph_bytes: byte_size(count: 60), - indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), + indices_digest: content_hash_atom(value: "closure-indices-1"), indices_bytes: byte_size(count: 25), - union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), + union_digest: content_hash_atom(value: "closure-diagnostics-1"), union_bytes: byte_size(count: 15) ) let refused_b = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_b), - compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), - stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), + compiler_digest: content_hash_atom(value: "compiler-identity-1"), + stored_request_key: content_hash_atom(value: "closure-1"), stored_semantic_digest: witness_closure_digest(), - graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), + graph_digest: content_hash_atom(value: "closure-graph-1"), graph_bytes: byte_size(count: 60), - indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), + indices_digest: content_hash_atom(value: "closure-indices-1"), indices_bytes: byte_size(count: 25), - union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), + union_digest: content_hash_atom(value: "closure-diagnostics-1"), union_bytes: byte_size(count: 15) ) lookup_is_refused_cross_family_content_hash(l: refused_a) @@ -412,7 +411,7 @@ test fn red_admission_wrong_content_is_refused() -> Bool { store: witness_empty_store(budget_count: 1000), req: witness_closure_request(), artifact: witness_complete_closure_artifact(), - observed_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-payload-corrupt")) + observed_digest: content_hash_atom(value: "closure-payload-corrupt") ) admission_is_refused_wrong_content_write(a: a) && (admission_is_admitted(a: a) == false) } @@ -465,9 +464,9 @@ fn witness_hash_list_contains(xs: List, wanted: ContentHash) -> Boo fn witness_carries_the_canonical_three_digests(a: MaterializedArtifact) -> Bool { let ds = artifact_carried_outputs(artifact: a) |> map(o => o.digest) (ds.count() == 3) - && witness_hash_list_contains(xs: ds, wanted: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1"))) - && witness_hash_list_contains(xs: ds, wanted: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1"))) - && witness_hash_list_contains(xs: ds, wanted: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1"))) + && witness_hash_list_contains(xs: ds, wanted: content_hash_atom(value: "closure-graph-1")) + && witness_hash_list_contains(xs: ds, wanted: content_hash_atom(value: "closure-indices-1")) + && witness_hash_list_contains(xs: ds, wanted: content_hash_atom(value: "closure-diagnostics-1")) } test fn understated_bytes_alone_hold_every_part_digest_fixed() -> Bool { diff --git a/src/v2/workflow/native_cache_fusion.dag b/src/v2/workflow/native_cache_fusion.dag index fbe8dcc6cce..868c3216704 100644 --- a/src/v2/workflow/native_cache_fusion.dag +++ b/src/v2/workflow/native_cache_fusion.dag @@ -5,7 +5,7 @@ import std.emit_on_demand { EmitOnDemandCacheReceipt, materialization_for_lookup } import std.content_hash { ContentHash } -import std.content_hash { content_hash_atom, as_content_hash_structural } +import std.content_hash { content_hash_atom } import std.realization { Materialization, Share, Recompute } import v2.std.logic { Bool } import v2.std.text { String } @@ -32,7 +32,7 @@ fn model_lookup_for(o: HostWarmObservation, key: ContentHash) -> EmitOnDemandLoo } fn fusion_agreement_holds_for(o: HostWarmObservation) -> Bool { - let key = as_content_hash_structural(structural: content_hash_atom(value: "fusion-law-synthetic-key")) + let key = content_hash_atom(value: "fusion-law-synthetic-key") let model_share = materialization_for_lookup(lookup: model_lookup_for(o: o, key: key)) == Share host_compile_skipped(o: o) == model_share } From e12fc029887bcc839576a6e63da59b8bf411a1e5 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 13:32:08 +0000 Subject: [PATCH 15/27] =?UTF-8?q?One=20mismatch=20diagnostic,=20two=20defe?= =?UTF-8?q?cts,=20opposite=20repairs=20=E2=80=94=20split=20by=20the=20call?= =?UTF-8?q?ee's=20role?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The floor's preparation named 14 sites, all in one witness file, all reading `declared 'Coproduct(ContentHash)', produced 'Product(Fnv1a64Structural)'`. A blanket wrap over all 14 broke two witnesses that had been green for their whole lives, because the diagnostic names both types and cannot name which one is wrong. The discriminator is the role of the carrier on the DECLARED side, and it is visible only in the callee: ELEVEN CALLER SITES (261-268, 273-280, 414) — the callee is right and the caller is raw. `serve_resolved_graph_stored_disk_probe` takes the union so it can narrow it with a typed cross-family refusal; `provider_admit` compares union against union (`artifact_content_digest` also returns `ContentHash`). Repair: lift the argument through `as_content_hash_structural`. The corpus was already carrying the discriminating control — line 260 of the same call passes `as_content_hash_cryptographic(...)` and is NOT refused, adjacent to the raw argument that is. THREE HELPER SITES (467-469) — `witness_hash_list_contains` declared the union for a comparison over `List` and narrows nothing. Repair: narrow the signature; the arguments stay raw. The 23 further bare `content_hash_atom` calls in the same file are untouched: they flow into parameters already declared `Fnv1a64Structural` and the wall did not name them. The wall is the census. Also reframes the direct-call witness to claim only what executes. A control run built gunbc from origin/main 907f19c2cc7 and from this branch and ran identical probe sources through both: main admits a kernel 5 at the Peano `Nat`, a String at the natively-realized `Nat`, and a kernel 40 at it, exactly as this branch does. So the two red arms assert refusals that were never there — asserted, not broken — and the sentence claiming a String at a natively-realized type "stays refused" is deleted rather than softened. Both arms are enrolled in `v2.workflow.floor_expected_red` carrying the branch-and-main control table and their next-rung trigger: `kernel_value_declared_type_mismatch` repaired to fire for a kernel value at an algebraic type application. That roster self-empties, so the flip to green announces itself. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...e_inhabitance_direct_call_witness_test.dag | 21 ++++++++++----- .../materialization_provider_witness_test.dag | 26 ++++++++++--------- src/v2/workflow/floor_expected_red.dag | 23 +++++++++++++++- 3 files changed, 50 insertions(+), 20 deletions(-) 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 a7f997b6a57..294ca58857f 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 @@ -38,9 +38,12 @@ fn violation_count(source: String, wanted: String) -> Int { // which is the whole point of enrolling it: DESIGN 4b(4) keeps the evidence after a climb // precisely so the higher rung stays real. -// RED -- a kernel integer at the PEANO Nat. 5 is not Zero and not Succ, and no realization row -// covers src/v2/std/nat.dag, so this must refuse. It is the arm that fails if identity ever -// collapses to the spelling "Nat". +// RED, AND CURRENTLY FAILING -- ENROLLED IN v2.workflow.floor_expected_red rather than fixed. +// A kernel integer at the PEANO Nat. 5 is not Zero and not Succ and no realization row covers +// src/v2/std/nat.dag, so this OUGHT to refuse. It does not, and the control run on 2026-08-23 +// establishes that it never did: gunbc built from origin/main 907f19c2cc7 admits this source +// exactly as the branch does. The refusal was ASSERTED here, not broken by this change. +// The enrolment row carries the full branch-and-main control table and the next-rung trigger. data peano_nat_arg_source: String = "module probe_inhabit_peano\nimport v2.std.nat { Nat }\nfn takes_peano(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_peano(n: 5) }\n" test fn w_kernel_numeric_at_the_peano_nat_is_refused() -> Bool { @@ -57,10 +60,14 @@ test fn w_kernel_numeric_at_the_natively_realized_nat_is_admitted() -> Bool { violation_count(source: native_nat_arg_source, wanted: "DeclaredTypeNotInhabited") == 0 } -// THE ADMISSION IS A CONJUNCTION, NOT A CARVE-OUT FOR THE TYPE. The declared side realizing -// natively is only half of it; the produced value must ALSO be a kernel numeric. A String at the -// same natively-realized position stays refused. Without this arm, an implementation that -// admitted ANYTHING at a natively-realized declared type would pass the green arm above. +// THE ADMISSION IS WRITTEN AS A CONJUNCTION -- the declared side must realize natively AND the +// produced value must be a kernel numeric -- and this arm is the control for the second half. +// IT IS CURRENTLY FAILING AND ENROLLED AS A KNOWN RED. A String at the natively-realized Nat is +// admitted, by this branch and by main alike, so the second half of the conjunction is not +// enforced anywhere downstream of declared_type_inhabitance: the consumed predicate +// kernel_value_declared_type_mismatch does not fire for a kernel value at an algebraic type +// application. That is a pre-existing gap, older than this branch, and it is named as this +// class's next-rung trigger in the enrolment row. data string_at_native_nat_source: String = "module probe_inhabit_native_str\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: \"forty\") }\n" test fn w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused() -> Bool { diff --git a/dag/test/claim/materialization_provider_witness_test.dag b/dag/test/claim/materialization_provider_witness_test.dag index feb4945dd50..97d0fe672a4 100644 --- a/dag/test/claim/materialization_provider_witness_test.dag +++ b/dag/test/claim/materialization_provider_witness_test.dag @@ -6,6 +6,8 @@ import std.content_hash { Fnv1a64, content_hash_atom, as_content_hash_cryptographic, + as_content_hash_structural, + Fnv1a64Structural, sha256_hex_digest, } import std.interface_summary { InterfaceHash, module_key, typed_module_key } @@ -258,26 +260,26 @@ test fn red_sha256_at_fnv1a64_seam_refuses_without_alias() -> Bool { Present { value: sha_b } => { let refused_a = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_a), - compiler_digest: content_hash_atom(value: "compiler-identity-1"), - stored_request_key: content_hash_atom(value: "closure-1"), + compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), + stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), stored_semantic_digest: witness_closure_digest(), - graph_digest: content_hash_atom(value: "closure-graph-1"), + graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), graph_bytes: byte_size(count: 60), - indices_digest: content_hash_atom(value: "closure-indices-1"), + indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), indices_bytes: byte_size(count: 25), - union_digest: content_hash_atom(value: "closure-diagnostics-1"), + union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), union_bytes: byte_size(count: 15) ) let refused_b = serve_resolved_graph_stored_disk_probe( closure_digest: as_content_hash_cryptographic(digest: sha_b), - compiler_digest: content_hash_atom(value: "compiler-identity-1"), - stored_request_key: content_hash_atom(value: "closure-1"), + compiler_digest: as_content_hash_structural(structural: content_hash_atom(value: "compiler-identity-1")), + stored_request_key: as_content_hash_structural(structural: content_hash_atom(value: "closure-1")), stored_semantic_digest: witness_closure_digest(), - graph_digest: content_hash_atom(value: "closure-graph-1"), + graph_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-graph-1")), graph_bytes: byte_size(count: 60), - indices_digest: content_hash_atom(value: "closure-indices-1"), + indices_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-indices-1")), indices_bytes: byte_size(count: 25), - union_digest: content_hash_atom(value: "closure-diagnostics-1"), + union_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-diagnostics-1")), union_bytes: byte_size(count: 15) ) lookup_is_refused_cross_family_content_hash(l: refused_a) @@ -411,7 +413,7 @@ test fn red_admission_wrong_content_is_refused() -> Bool { store: witness_empty_store(budget_count: 1000), req: witness_closure_request(), artifact: witness_complete_closure_artifact(), - observed_digest: content_hash_atom(value: "closure-payload-corrupt") + observed_digest: as_content_hash_structural(structural: content_hash_atom(value: "closure-payload-corrupt")) ) admission_is_refused_wrong_content_write(a: a) && (admission_is_admitted(a: a) == false) } @@ -457,7 +459,7 @@ fn witness_size_understated_closure_artifact() -> MaterializedArtifact { } } -fn witness_hash_list_contains(xs: List, wanted: ContentHash) -> Bool { +fn witness_hash_list_contains(xs: List, wanted: Fnv1a64Structural) -> Bool { xs |> fold(init: false, f: (acc, x) => acc || (x == wanted)) } diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 0fb5ed8c191..4aee4ff6963 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -394,8 +394,29 @@ fn floor_expected_red_chunk_13() -> List { Cons { head: "test.claim.method_arg_declared_contract_witness_test.w_method_arg_infers_against_declared_contract_not_element_type_test", tail: Empty {} } } +// TWO ARMS OF THE DIRECT-CALL INHABITANCE WITNESS, ENROLLED BECAUSE THE WALL THEY ASSERT +// DOES NOT EXIST AND NEVER DID -- NOT BECAUSE THIS BRANCH BROKE IT. Both arms assert that a +// value at a direct-call argument is REFUSED. Both are red. The control that settles who +// caused it was run on 2026-08-23: identical probe sources, identical dispatch, gunbc built +// from origin/main 907f19c2cc7 and from the branch head, and main returns the same answer at +// every point. +// +// probe branch main verdict +// kernel 5 at the Peano Nat accepted accepted no change +// "forty" at std.nat.Nat accepted accepted no change +// 40 at std.nat.Nat accepted accepted no change +// +// So the refusals were ASSERTED, not broken. The gap is in the consumed predicate +// v1.compiler.infer kernel_value_declared_type_mismatch, which does not fire for a kernel +// value at an algebraic type application, and it is older than this branch. +// +// NEXT-RUNG TRIGGER: that predicate repaired so a non-numeric at a natively-realized declared +// type refuses. When it lands, BOTH rows here go green -- and this roster's self-emptying arm +// reds the build and names them for removal, at which point they become permanent regression +// controls under DESIGN 4b(4) rather than being deleted. The flip is EXPECTED and is not a +// regression; it is the dissolution event. fn floor_expected_red_chunk_14() -> List { - Empty {} + Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_peano_nat_is_refused", tail: Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused", tail: Empty {} } } } fn floor_expected_red_chunk_15() -> List { From b14e24c278e7864ff6d7f083a10056984467b130 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 13:49:13 +0000 Subject: [PATCH 16/27] Widen the enrolment row: it is any type application, not an algebraic one MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five probes varying only the declared type's shape, one String argument at every one, measured against a compiler built from the branch head: Int kernel primitive REFUSED NatLike = CommutativeSemiring 1-arg application admitted OneArg = List 1-arg application admitted TwoArg = Map 2-arg application admitted Closed = ZzA | ZzB { v: Int } coproduct REFUSED The two-argument `Map` kills the arity story the row's earlier wording rested on, and `List` is the specimen that makes the gap legible without any appeal to the numeric tower: a `String` reaching a `List` parameter unremarked is the ordinary compiler floor, not a numeric-tower curiosity. The refusing probes emit BOTH the pre-existing `type mismatch` and this branch's inhabitance diagnostic at the same offset; the admitting ones emit neither. So the blindness is upstream of `declared_type_inhabitance`, which inherits it faithfully — no arm of this relation could have caught it. Class: total at the level examined, blind one level down. The judgment is exhaustive over primitive / coproduct / application, and the application arm never asks what the application expands to, so there is no missing arm for exhaustiveness checking or a reviewer to see. The admitting branch has NOT been read and no line is named — this locates the class and a reproducing input, nothing more. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...e_inhabitance_direct_call_witness_test.dag | 8 +++--- src/v2/workflow/floor_expected_red.dag | 25 +++++++++++++++---- 2 files changed, 25 insertions(+), 8 deletions(-) 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 294ca58857f..1791e43aafe 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 @@ -65,9 +65,11 @@ test fn w_kernel_numeric_at_the_natively_realized_nat_is_admitted() -> Bool { // IT IS CURRENTLY FAILING AND ENROLLED AS A KNOWN RED. A String at the natively-realized Nat is // admitted, by this branch and by main alike, so the second half of the conjunction is not // enforced anywhere downstream of declared_type_inhabitance: the consumed predicate -// kernel_value_declared_type_mismatch does not fire for a kernel value at an algebraic type -// application. That is a pre-existing gap, older than this branch, and it is named as this -// class's next-rung trigger in the enrolment row. +// kernel_value_declared_type_mismatch does not fire for a kernel value at ANY type application. +// Nat is not the specimen that makes this legible -- a String reaching a List parameter is, +// and Map admits one too, so it is not about arity and not about algebra. That is a +// pre-existing gap, older than this branch, and the enrolment row in v2.workflow.floor_expected_red +// carries the five-probe table and names it as this class's next-rung trigger. data string_at_native_nat_source: String = "module probe_inhabit_native_str\nimport std.nat { Nat }\nfn takes_native(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_native(n: \"forty\") }\n" test fn w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused() -> Bool { diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 4aee4ff6963..9b77a6d924c 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -407,11 +407,26 @@ fn floor_expected_red_chunk_13() -> List { // 40 at std.nat.Nat accepted accepted no change // // So the refusals were ASSERTED, not broken. The gap is in the consumed predicate -// v1.compiler.infer kernel_value_declared_type_mismatch, which does not fire for a kernel -// value at an algebraic type application, and it is older than this branch. -// -// NEXT-RUNG TRIGGER: that predicate repaired so a non-numeric at a natively-realized declared -// type refuses. When it lands, BOTH rows here go green -- and this roster's self-emptying arm +// v1.compiler.infer kernel_value_declared_type_mismatch, and it is older than this branch and +// WIDER than these two rows. Measured 2026-08-23 by five probes varying only the declared +// type's shape, one String argument at every one: +// +// Int kernel primitive REFUSED +// NatLike = CommutativeSemiring 1-arg application admitted +// OneArg = List 1-arg application admitted +// TwoArg = Map 2-arg application admitted +// Closed = ZzA | ZzB { v: Int } coproduct REFUSED +// +// A KERNEL VALUE IS ADMITTED AT ANY TYPE APPLICATION -- not merely an algebraic one, and not +// as a function of arity: the two-argument Map is admitted exactly as List is. So the +// legible specimen is a String reaching a List parameter unremarked, which is the ordinary +// compiler floor DESIGN requires before any differentiating claim, and Nat is one instance of it. +// The class is "total at the level examined, blind one level down": the judgment is exhaustive +// over primitive / coproduct / application and the application arm never asks what the +// application EXPANDS TO, so there is no missing arm for exhaustiveness checking or review to see. +// Located, with a reproducing input; the admitting branch has NOT been read and no line is named. +// +// NEXT-RUNG TRIGGER: that predicate repaired so a kernel value at a type application refuses. When it lands, BOTH rows here go green -- and this roster's self-emptying arm // reds the build and names them for removal, at which point they become permanent regression // controls under DESIGN 4b(4) rather than being deleted. The flip is EXPECTED and is not a // regression; it is the dissolution event. From 28c1fddbd2efa73342758f4af1ad4027b9c97426 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 14:24:32 +0000 Subject: [PATCH 17/27] Round two of the wall's census: two production sites, same class, same caller-side repair MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Clearing the first 14 let preparation reach further and name two more, both outside the witness tests this time: dag/gunbc/heal_revalidation.dag:154 required_roster src/v2/workflow/native_cache_fusion.dag:36 key Both are the caller-side shape. Judged at the callee, as the class requires: `check_coverage_admits` and the whole `CheckCoverage` family declare `ContentHash` end to end (`merge_admission.dag:360,383,394,407,485,556`) and compare union against union; `EmitOnDemandCacheReceipt.key` is `ContentHash` too. Neither callee is a lying consumer, so neither declaration moves — the arguments are lifted through `as_content_hash_structural`. The census is ITERATIVE. Preparation stops at the modules it refused, so each round of repairs uncovers the next set. 14 → 2 is the wall working through the corpus, not a repair that missed. NOT repaired, and named rather than swept: `heal_revalidation.dag:155` passes `List` to `check_coverage_admits`'s `required_gates: List`. That is the same mismatch one level inside a list, and the wall did NOT name it — so it is a coverage gap in this relation at the list-element-of-a-direct-call-argument position, not a site anyone repaired. Left alone deliberately: fixing it by hand would hide the gap that its silence is evidence for. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- dag/gunbc/heal_revalidation.dag | 4 ++-- src/v2/workflow/native_cache_fusion.dag | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag index ae2ca155828..1edf0d9f50f 100644 --- a/dag/gunbc/heal_revalidation.dag +++ b/dag/gunbc/heal_revalidation.dag @@ -1,6 +1,6 @@ module gunbc.heal_revalidation -import std.content_hash { Fnv1a64Structural } +import std.content_hash { Fnv1a64Structural, as_content_hash_structural } import std.types { CommitSha, NonEmptyStr } import gunbc.merge_admission { CheckCoverage, @@ -151,7 +151,7 @@ fn classify_heal_revalidation_admission( if check_coverage_admits( coverage: coverage, required_head: healed_head, - required_roster: required_roster, + required_roster: as_content_hash_structural(structural: required_roster), required_gates: required_gates ) { HealRevalidationAdmittedExactCoverage { healed_head: healed_head } diff --git a/src/v2/workflow/native_cache_fusion.dag b/src/v2/workflow/native_cache_fusion.dag index 868c3216704..fbe8dcc6cce 100644 --- a/src/v2/workflow/native_cache_fusion.dag +++ b/src/v2/workflow/native_cache_fusion.dag @@ -5,7 +5,7 @@ import std.emit_on_demand { EmitOnDemandCacheReceipt, materialization_for_lookup } import std.content_hash { ContentHash } -import std.content_hash { content_hash_atom } +import std.content_hash { content_hash_atom, as_content_hash_structural } import std.realization { Materialization, Share, Recompute } import v2.std.logic { Bool } import v2.std.text { String } @@ -32,7 +32,7 @@ fn model_lookup_for(o: HostWarmObservation, key: ContentHash) -> EmitOnDemandLoo } fn fusion_agreement_holds_for(o: HostWarmObservation) -> Bool { - let key = content_hash_atom(value: "fusion-law-synthetic-key") + let key = as_content_hash_structural(structural: content_hash_atom(value: "fusion-law-synthetic-key")) let model_share = materialization_for_lookup(lookup: model_lookup_for(o: o, key: key)) == Share host_compile_skipped(o: o) == model_share } From 508693bf0d44a4cdaff8894dc3c1ecb09c1f29dd Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 14:27:28 +0000 Subject: [PATCH 18/27] Move the list-element evidence into a fixture, then repair the production site MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reversing my own call. `heal_revalidation.dag:155` passed `List` into `check_coverage_admits`'s `required_gates: List` — the same mismatch as the argument beside it, one level inside a list — and this relation did not name it. I left it broken because its silence was the only evidence the gap existed. That conclusion does not follow from its own premise. DESIGN §4b(4) separates exactly this: a climb deletes the redundant PRODUCTION handling and KEEPS the discriminating RED as enrolled evidence. The evidence is a probe. It is not a live wrong argument in a merge-admission path. So the evidence moved and the site is repaired: - `w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused` — a plain record at a coproduct element type inside a list at a direct-call argument. Asserts the refusal; currently fails; enrolled in `floor_expected_red_chunk_15` with its next-rung trigger. - `w_the_same_wrong_pair_directly_at_the_argument_is_refused` — the paired control, deliberately NOT enrolled. Identical two types, identical position, no list. It must stay green: if it ever reds, the probe has stopped measuring lists and the enrolment above is meaningless. This is what separates "the relation cannot judge this pair" from "the relation cannot see inside a list". - `heal_revalidation.dag:155` now lifts each element. Also: the census this wall performs is FAIL-FAST, so its output is a LOWER BOUND and never a population. Preparation stops at the modules it refused and never reaches what lies behind them — "14 sites" was the population visible from the first refusal, and clearing it surfaced two more in different files. Depth unknown; each round gets reported as it surfaces. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- dag/gunbc/heal_revalidation.dag | 2 +- ...e_inhabitance_direct_call_witness_test.dag | 29 +++++++++++++++++++ src/v2/workflow/floor_expected_red.dag | 17 ++++++++++- 3 files changed, 46 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag index 1edf0d9f50f..eded6b7f45f 100644 --- a/dag/gunbc/heal_revalidation.dag +++ b/dag/gunbc/heal_revalidation.dag @@ -152,7 +152,7 @@ fn classify_heal_revalidation_admission( coverage: coverage, required_head: healed_head, required_roster: as_content_hash_structural(structural: required_roster), - required_gates: required_gates + required_gates: required_gates |> map(g => as_content_hash_structural(structural: g)) ) { HealRevalidationAdmittedExactCoverage { healed_head: healed_head } } else { 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 1791e43aafe..eb39a7ef998 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 @@ -86,3 +86,32 @@ data undefined_name_arg_source: String = "module probe_inhabit_dc_reach\nimport test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { violation_count(source: undefined_name_arg_source, wanted: "InternalError") > 0 } + +// THE LIST-ELEMENT GAP, AUTHORED AS A FIXTURE SO THE PRODUCTION SITE CAN BE REPAIRED. +// dag/gunbc/heal_revalidation.dag passed List into check_coverage_admits's +// required_gates: List -- the same mismatch as the argument beside it, one level +// inside a list -- and this relation did NOT name it. That silence was the only evidence the +// gap existed, which made repairing the production site look like consuming the evidence. +// DESIGN 4b(4) separates those: a climb deletes the redundant PRODUCTION handling and KEEPS the +// discriminating RED as enrolled evidence. So the evidence lives here, where it is reproducible +// on demand, and the live wrong argument in an admission path is repaired. +// +// RED, AND CURRENTLY FAILING -- ENROLLED. A plain record at a coproduct element type inside a +// list at a direct-call argument. The relation judges this exact pair at the argument itself +// (the control below), and does not descend into the list, so this must refuse and does not. +data record_element_in_list_arg_source: String = "module probe_inhabit_dc_list_elem\nimport std.types { Int, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\ntype Rec { v: Int }\nfn takes_list(xs: List) -> Int { 1 }\nfn probe() -> Int { takes_list(xs: [Rec { v: 1 }]) }\n" + +test fn w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused() -> Bool { + violation_count(source: record_element_in_list_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// THE CONTROL THAT MAKES THAT RED READABLE, and it is the one that separates "the relation +// cannot judge this pair" from "the relation cannot see inside a list". SAME two types, SAME +// direct-call argument position, the record passed DIRECTLY rather than wrapped in a list. If +// this refuses and the arm above does not, the list is the whole difference. If this also +// admits, the probe proves nothing about lists and the arm above is measuring the wrong thing. +data record_directly_at_coproduct_arg_source: String = "module probe_inhabit_dc_bare_elem\nimport std.types { Int, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\ntype Rec { v: Int }\nfn takes_one(x: Cop) -> Int { 1 }\nfn probe() -> Int { takes_one(x: Rec { v: 1 }) }\n" + +test fn w_the_same_wrong_pair_directly_at_the_argument_is_refused() -> Bool { + violation_count(source: record_directly_at_coproduct_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +} diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 9b77a6d924c..11723342267 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -434,8 +434,23 @@ fn floor_expected_red_chunk_14() -> List { Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_peano_nat_is_refused", tail: Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_non_numeric_kernel_at_the_natively_realized_nat_is_still_refused", tail: Empty {} } } } +// THE LIST-ELEMENT ARM OF THE DIRECT-CALL INHABITANCE WITNESS. It asserts that a wrong element +// type inside a list at a direct-call argument is refused. It is not. Its PAIRED CONTROL -- +// w_the_same_wrong_pair_directly_at_the_argument_is_refused, deliberately NOT enrolled -- passes +// the identical two types at the identical position without the list, and must stay green: if it +// ever reds, the probe has stopped measuring lists and this enrolment is meaningless. +// +// WHY IT IS ENROLLED RATHER THAN FIXED HERE: the gap was discovered as a live wrong argument in +// dag/gunbc/heal_revalidation.dag (List into required_gates: List), +// and the relation's SILENCE was the only evidence of it. DESIGN 4b(4) puts the evidence in a +// probe and the repair in production, not the reverse, so the production site is repaired in this +// same change and the evidence moved here where anyone can reproduce it. +// +// NEXT-RUNG TRIGGER: declared_type_inhabitance descending into a list's element type at a +// direct-call argument. When it lands this row goes green and the roster's self-emptying arm +// names it for removal, at which point it becomes a permanent regression control. fn floor_expected_red_chunk_15() -> List { - Empty {} + Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused", tail: Empty {} } } fn floor_expected_red_chunk_16() -> List { From 4bf28405bbd41b0d1dcde5ec5d5ea74a6d59ffe5 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 15:23:41 +0000 Subject: [PATCH 19/27] Mark the realization-keyed admit as an interim and name the model that replaces it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `declared_realizes_as_kernel_numeric` decides that `40` inhabits `Nat` by consulting `decl_file_realizes_natively` — because `Nat`'s declaring module is kernel-backed. That is a REALIZATION fact standing in for a TYPING fact, and it amounts to peeling the applied type until a scalar appears. It is not unsound. It fails closed on unknown identity, and the admit is measured behaviour-preserving-or-narrowing against main. It is UNDER-SPECIFIC: it answers "this module's numerics are kernel-backed" where the question is "does this type admit this literal", so it grants literal syntax module-wide permission to inhabit anything whose implementation eventually mentions a numeric carrier. The two answers coincide today for `Nat` and `Int`, and stop coinciding the moment a module declares a numeric type that should not take bare literals. The durable model is an expected-type-directed literal introduction judgment: `40` inhabits `Nat` because `Nat` SUPPLIES a numeral introduction. Lean is the worked precedent — numerals elaborate against the expected type through an `OfNat` obligation, and literal introduction stays separate from coercion insertion. Recorded at the predicate and in `floor_expected_red_chunk_14`'s next-rung trigger so the interim is never cited as the design. Two constraints on whoever builds the replacement, both live here rather than hypothetical: a judgment that peels a declared type to its representation defeats walls that already hold (`TransparentAlias` may be exposed; `OpaqueType`, `SoleConstructorCarrier`, `Refinement`, `Brand` may not — `sole_constructor` is a real executing construction wall), and exposure must derive a canonical view once per type identity and cache it, with cycle detection and a measured expansion budget. No behaviour changes. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v1/04_infer.dag | 8 +++++++ src/v2/workflow/floor_expected_red.dag | 31 +++++++++++++++++++++++++- 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index e09af56ed3a..0003136bdad 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2216,6 +2216,14 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco // SOURCE-LEVEL, NOT EMISSION. decl_file_realizes_natively takes only decl_file; the neighbouring // lookup_checkpoint takes a RenderTarget and would have made an emission fact answer a // source-level question, which is why it is deliberately not the surface used here. +// INTERIM, AND THE ROW THAT DISSOLVES IT IS v2.workflow.floor_expected_red chunk_14. +// This decides that a kernel numeral inhabits Nat by asking whether Nat's DECLARING MODULE is +// kernel-backed -- a REALIZATION fact answering a TYPING question. It fails closed on unknown +// identity and is measured behaviour-preserving against main, so it is not unsound; it is +// UNDER-SPECIFIC, and it grants literal syntax module-wide permission to inhabit anything whose +// implementation eventually mentions a numeric carrier. The durable model is an +// expected-type-directed literal introduction judgment -- a type admits a numeral because it +// SUPPLIES one, not because its module realizes natively. Do not build on this predicate. fn declared_realizes_as_kernel_numeric( declared: Node, produced: Node, diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 11723342267..7e75db7aebd 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -426,7 +426,36 @@ fn floor_expected_red_chunk_13() -> List { // application EXPANDS TO, so there is no missing arm for exhaustiveness checking or review to see. // Located, with a reproducing input; the admitting branch has NOT been read and no line is named. // -// NEXT-RUNG TRIGGER: that predicate repaired so a kernel value at a type application refuses. When it lands, BOTH rows here go green -- and this roster's self-emptying arm +// NEXT-RUNG TRIGGER, TWO PARTS. The mechanical one: that predicate repaired so a kernel value at +// a type application refuses. The MODEL one, which is what the durable repair looks like and is +// recorded here so the interim is never cited as the design: +// +// declared_realizes_as_kernel_numeric decides that 40 inhabits Nat by consulting +// v1.compiler.coercion decl_file_realizes_natively -- i.e. because Nat's DECLARING MODULE is +// kernel-backed. That is a REALIZATION fact standing in for a TYPING fact, and it amounts to +// peeling the applied type until a scalar appears. It is not unsound: it fails closed on unknown +// identity, and the admit is measured behaviour-preserving-or-narrowing against main. It is +// UNDER-SPECIFIC. It answers "this module's numerics are kernel-backed" where the question is +// "does this type admit this literal", and it therefore grants literal syntax module-wide +// permission to inhabit anything whose implementation eventually mentions a numeric carrier. +// The two answers coincide today for Nat and Int and stop coinciding the moment a module +// declares a numeric type that should NOT take bare literals. +// +// THE DURABLE MODEL IS AN EXPECTED-TYPE-DIRECTED LITERAL INTRODUCTION JUDGMENT: 40 inhabits Nat +// because Nat SUPPLIES A NUMERAL INTRODUCTION, not because its module realizes natively. Lean is +// the worked precedent -- numerals elaborate against the expected type through an OfNat +// obligation, and literal introduction is kept separate from coercion insertion. When that lands, +// declared_realizes_as_kernel_numeric and its consumption of decl_file_realizes_natively dissolve; +// they are the interim, and this row is their dissolution trigger. +// +// TWO CONSTRAINTS ON WHOEVER BUILDS IT, both live in this repository rather than hypothetical. +// A judgment that peels a declared type to its representation defeats abstraction walls that +// already hold: TransparentAlias may be exposed; OpaqueType, SoleConstructorCarrier, Refinement +// and Brand MAY NOT -- sole_constructor is a real, executing construction wall and a peeling +// judgment walks through it silently. And exposure must derive a canonical view ONCE per type +// identity and cache it, with cycle detection and a measured expansion budget: recursive aliases +// can loop, renormalizing at every use site is expensive, and this corpus is already living on a +// per-witness cost line. When it lands, BOTH rows here go green -- and this roster's self-emptying arm // reds the build and names them for removal, at which point they become permanent regression // controls under DESIGN 4b(4) rather than being deleted. The flip is EXPECTED and is not a // regression; it is the dissolution event. From 5e850d30c22801092d790015beb955d523edc43e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 21:26:32 +0000 Subject: [PATCH 20/27] =?UTF-8?q?The=20control=20arm=20went=20red=20and=20?= =?UTF-8?q?caught=20a=20mis-designed=20probe=20=E2=80=94=20plus=20a=20doub?= =?UTF-8?q?le-wrap=20I=20introduced?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First execution of these arms. Two failures, both mine, both found by controls rather than by review. 1. THE PAIRED CONTROL FAILED, WHICH IS WHY IT EXISTS. `w_the_same_wrong_pair_directly_at_the_argument_is_refused` asserted that a plain record at a coproduct is refused at a direct-call argument. It is not — `kernel_value_declared_type_mismatch` gates its entire body on `is_kernel_type(actual_name)`, so a RECORD literal is never judged at any position, list or not. The pair was therefore measuring "records are never judged", and its enrolled twin would have been filed as evidence about lists. Both arms rebuilt on a kernel `String`, which is judged at this position by execution (a String at a closed coproduct refuses — measured). The list is now the only difference between the two arms, which is what the pair claimed all along. 2. MY OWN heal_revalidation REPAIR WAS A DOUBLE WRAP. Lifting `required_roster`/`required_gates` through `as_content_hash_structural` wrapped values that were ALREADY the union: the witness passes `Fnv1a64(content_hash_atom(...))` and `check_coverage_admits` takes `ContentHash`. So the comparison became `Fnv1a64(Fnv1a64(x))` against `Fnv1a64(x)` and reddened `only_exact_healed_head_complete_coverage_admits`, green until I touched it. `heal_revalidation`'s own two parameters were the only things in the chain declaring `Fnv1a64Structural`, sandwiched between a caller and a callee that both speak `ContentHash`. The chain is now `ContentHash` end to end and the lifts are gone. Reading the callee is half the discriminator. The caller is the other half, and a declaration sitting between two that agree with each other is the one that is wrong. I read the callee, lifted, and never read the caller. Ledger for the record (run 32664496347): planned=executed=terminal=10705, known_red_held 36→39 — the three enrolled arms held exactly as predicted — interrupted_before_verdict=0, known_red_now_passing=0, failed=2. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- dag/gunbc/heal_revalidation.dag | 14 ++++----- ...e_inhabitance_direct_call_witness_test.dag | 29 ++++++++++++------- src/v2/workflow/floor_expected_red.dag | 14 +++++++-- 3 files changed, 38 insertions(+), 19 deletions(-) diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag index eded6b7f45f..737903c0af4 100644 --- a/dag/gunbc/heal_revalidation.dag +++ b/dag/gunbc/heal_revalidation.dag @@ -1,6 +1,6 @@ module gunbc.heal_revalidation -import std.content_hash { Fnv1a64Structural, as_content_hash_structural } +import std.content_hash { ContentHash } import std.types { CommitSha, NonEmptyStr } import gunbc.merge_admission { CheckCoverage, @@ -135,8 +135,8 @@ fn classify_workflow_dispatch_preflight( fn classify_heal_revalidation_admission( state: HealRevalidationState, - required_roster: Fnv1a64Structural, - required_gates: List, + required_roster: ContentHash, + required_gates: List, ) -> HealRevalidationAdmissionVerdict { match state { HealRevalidationNotRequired { head } => @@ -151,8 +151,8 @@ fn classify_heal_revalidation_admission( if check_coverage_admits( coverage: coverage, required_head: healed_head, - required_roster: as_content_hash_structural(structural: required_roster), - required_gates: required_gates |> map(g => as_content_hash_structural(structural: g)) + required_roster: required_roster, + required_gates: required_gates ) { HealRevalidationAdmittedExactCoverage { healed_head: healed_head } } else { @@ -166,8 +166,8 @@ fn classify_heal_revalidation_admission( fn heal_revalidation_admits( state: HealRevalidationState, - required_roster: Fnv1a64Structural, - required_gates: List, + required_roster: ContentHash, + required_gates: List, ) -> Bool { match classify_heal_revalidation_admission( state: state, 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 eb39a7ef998..b25aa54bccd 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 @@ -96,21 +96,30 @@ test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { // discriminating RED as enrolled evidence. So the evidence lives here, where it is reproducible // on demand, and the live wrong argument in an admission path is repaired. // -// RED, AND CURRENTLY FAILING -- ENROLLED. A plain record at a coproduct element type inside a -// list at a direct-call argument. The relation judges this exact pair at the argument itself -// (the control below), and does not descend into the list, so this must refuse and does not. -data record_element_in_list_arg_source: String = "module probe_inhabit_dc_list_elem\nimport std.types { Int, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\ntype Rec { v: Int }\nfn takes_list(xs: List) -> Int { 1 }\nfn probe() -> Int { takes_list(xs: [Rec { v: 1 }]) }\n" +// RED, AND CURRENTLY FAILING -- ENROLLED. A kernel String at a coproduct element type inside a +// list at a direct-call argument. +// +// THE PRODUCED VALUE IS A KERNEL STRING BECAUSE THE FIRST VERSION OF THIS PAIR USED A RECORD +// LITERAL AND ITS CONTROL WENT RED, which is the only reason the mis-design was caught rather +// than enrolled. kernel_value_declared_type_mismatch judges only a KERNEL produced value -- +// is_kernel_type(actual_name) gates its whole body -- so a record literal at a coproduct is not +// judged AT ANY POSITION, list or not. The old pair therefore measured "records are never +// judged" and would have been enrolled as evidence about lists. A String is judged at this +// position by execution (measured: a String at a closed coproduct REFUSES), so the list is now +// the only difference between the two arms. +data record_element_in_list_arg_source: String = "module probe_inhabit_dc_list_elem\nimport std.types { Int, String, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\nfn takes_list(xs: List) -> Int { 1 }\nfn probe() -> Int { takes_list(xs: [\"forty\"]) }\n" test fn w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused() -> Bool { violation_count(source: record_element_in_list_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 } -// THE CONTROL THAT MAKES THAT RED READABLE, and it is the one that separates "the relation -// cannot judge this pair" from "the relation cannot see inside a list". SAME two types, SAME -// direct-call argument position, the record passed DIRECTLY rather than wrapped in a list. If -// this refuses and the arm above does not, the list is the whole difference. If this also -// admits, the probe proves nothing about lists and the arm above is measuring the wrong thing. -data record_directly_at_coproduct_arg_source: String = "module probe_inhabit_dc_bare_elem\nimport std.types { Int, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\ntype Rec { v: Int }\nfn takes_one(x: Cop) -> Int { 1 }\nfn probe() -> Int { takes_one(x: Rec { v: 1 }) }\n" +// THE CONTROL THAT MAKES THAT RED READABLE, and it separates "the relation cannot judge this +// pair" from "the relation cannot see inside a list". SAME two types, SAME direct-call argument +// position, the String passed DIRECTLY rather than wrapped in a list. If this refuses and the +// arm above does not, the list is the whole difference. If this also admits, the probe proves +// nothing about lists and the arm above is measuring the wrong thing -- which is exactly what +// happened to this pair's first version, so this arm is not a formality. +data record_directly_at_coproduct_arg_source: String = "module probe_inhabit_dc_bare_elem\nimport std.types { Int, String, List }\ntype Cop = | CopA { v: Int } | CopB { w: Int }\nfn takes_one(x: Cop) -> Int { 1 }\nfn probe() -> Int { takes_one(x: \"forty\") }\n" test fn w_the_same_wrong_pair_directly_at_the_argument_is_refused() -> Bool { violation_count(source: record_directly_at_coproduct_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index ee1e26e7047..91fa39b373a 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -493,8 +493,18 @@ fn floor_expected_red_chunk_14() -> List { // WHY IT IS ENROLLED RATHER THAN FIXED HERE: the gap was discovered as a live wrong argument in // dag/gunbc/heal_revalidation.dag (List into required_gates: List), // and the relation's SILENCE was the only evidence of it. DESIGN 4b(4) puts the evidence in a -// probe and the repair in production, not the reverse, so the production site is repaired in this -// same change and the evidence moved here where anyone can reproduce it. +// probe and the repair in production, not the reverse, so the evidence lives here where anyone +// can reproduce it. +// +// THE PRODUCTION SITE WAS REPAIRED TWICE AND ONLY THE SECOND WAY WAS RIGHT. Lifting the argument +// through as_content_hash_structural DOUBLE-WRAPPED a value that was already the union -- the +// witness passes Fnv1a64(content_hash_atom(...)) and check_coverage_admits takes ContentHash, so +// heal_revalidation's own two parameters were the ONLY things in the chain declaring the family +// member. Lifting made the comparison Fnv1a64(Fnv1a64(x)) against Fnv1a64(x) and reddened +// heal_revalidation_witness only_exact_healed_head_complete_coverage_admits, a witness that had +// been green. The chain is now ContentHash end to end and the lifts are gone. Reading the CALLEE +// is half the discriminator; the CALLER is the other half, and a declaration sandwiched between +// two that agree with each other is the one that is wrong. // // NEXT-RUNG TRIGGER: declared_type_inhabitance descending into a list's element type at a // direct-call argument. When it lands this row goes green and the roster's self-emptying arm From 76645a502cb16b81777a55533ecb155a0538d2da Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 21:28:18 +0000 Subject: [PATCH 21/27] =?UTF-8?q?Unenrol=20the=20list-element=20arm=20unti?= =?UTF-8?q?l=20its=20control=20is=20green=20=E2=80=94=20believed=20is=20no?= =?UTF-8?q?t=20measured?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The row was enrolled while its paired control was RED, and the control's red proved the pair measured the wrong thing entirely: a record literal is never judged at any position, so the list was doing no work. Both arms are rebuilt on a kernel String, and the rebuilt pair HAS NOT EXECUTED. An enrolment asserts a known, real gap. A control that reds and an arm that reds are indistinguishable as evidence, so enrolling now would re-file a claim that is currently believed rather than measured — the exact state that put two unverified reds on this roster earlier today. Until a run shows the control GREEN and the arm RED, the arm fails loudly as an ordinary failure. That is the honest reading of an unproven claim, and a red I have to look at is better than a held row asserting something I cannot support. Re-enrolment is one line once the measurement exists. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v2/workflow/floor_expected_red.dag | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 91fa39b373a..2b62f483a03 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -509,8 +509,19 @@ fn floor_expected_red_chunk_14() -> List { // NEXT-RUNG TRIGGER: declared_type_inhabitance descending into a list's element type at a // direct-call argument. When it lands this row goes green and the roster's self-emptying arm // names it for removal, at which point it becomes a permanent regression control. +// DELIBERATELY EMPTY. THE ROW THAT BELONGS HERE IS NOT ENROLLED YET, ON PURPOSE. +// w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused was enrolled here while its +// paired control was RED, and the control's red proved the pair was measuring the wrong thing +// entirely -- a record literal is never judged at any position, so the list was doing no work. +// Both arms were rebuilt on a kernel String. THE REBUILT PAIR HAS NOT EXECUTED. +// +// An enrolment asserts a KNOWN, REAL gap. A CONTROL THAT REDS AND AN ARM THAT REDS ARE +// INDISTINGUISHABLE AS EVIDENCE, so enrolling before the control is green would re-file a claim +// that is currently believed rather than measured -- the exact state that put two unverified reds +// on this roster earlier. Until the run shows the control GREEN and the arm RED, the arm fails +// loudly as an ordinary failure, which is the honest reading of an unproven claim. fn floor_expected_red_chunk_15() -> List { - Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused", tail: Empty {} } + Empty {} } fn floor_expected_red_chunk_16() -> List { From 8d75f3688fb7cf8af50b471519117f0315390560 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 22:25:30 +0000 Subject: [PATCH 22/27] =?UTF-8?q?Withdraw=20the=20list-element=20gap=20?= =?UTF-8?q?=E2=80=94=20measured=20green,=20the=20wall=20was=20there=20all?= =?UTF-8?q?=20along?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Run 32667623528, whole required CI green: planned=executed=terminal=10705, passed=10423, failed=0, phases_run=3 failed=0, known_red_held=38. The list-element arm was left UNENROLLED precisely so a red would show loudly. It PASSES. So a kernel String at a coproduct element type inside a list at a direct-call argument IS refused, the relation descends into a list literal's elements at this position, and the gap this pair was authored to document does not exist. WHY I BELIEVED IT DID, and the distinction is the correction: the site that started this was `heal_revalidation` passing a `List` VARIABLE into a `List` parameter. That is list-typed-value compatibility, and the relation answers `Undecidable` for a generic carrier BY DESIGN — its silence there was specified behaviour, not blindness. My probe passes a list LITERAL with a wrong element, which is a different judgment and one the relation makes. I inferred the second from the silence on the first, and the two were never the same question. The list-typed-value case remains UNMEASURED and nothing now claims otherwise. The arms stay as a permanent regression control over a wall shown real (§4b(4): evidence stays enrolled as evidence once the wall is established). `floor_expected_red_chunk_15` stays empty — there is nothing red to enrol. Also green in this run: `heal_revalidation only_exact_healed_head_complete_ coverage_admits`, the witness my double-wrap had reddened, and `w_the_same_wrong_pair_directly_at_the_argument_is_refused`, the control whose red caught the mis-designed probe. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...e_inhabitance_direct_call_witness_test.dag | 17 ++++++++++++++-- src/v2/workflow/floor_expected_red.dag | 20 +++++++++---------- 2 files changed, 24 insertions(+), 13 deletions(-) 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 b25aa54bccd..fc7d87256d6 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 @@ -96,8 +96,21 @@ test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { // discriminating RED as enrolled evidence. So the evidence lives here, where it is reproducible // on demand, and the live wrong argument in an admission path is repaired. // -// RED, AND CURRENTLY FAILING -- ENROLLED. A kernel String at a coproduct element type inside a -// list at a direct-call argument. +// GREEN, AND THE CLAIM IT WAS BUILT TO DOCUMENT IS WITHDRAWN. A kernel String at a coproduct +// element type inside a list at a direct-call argument IS REFUSED. Measured, run 32667623528. +// +// THIS PAIR WAS AUTHORED TO DOCUMENT A GAP THAT DOES NOT EXIST. The relation descends into a +// list literal's elements at this position and always did; it is kept as a permanent regression +// control over that fact rather than deleted, per DESIGN 4b(4) -- evidence stays enrolled as +// evidence once a wall is shown real. +// +// WHY IT LOOKED LIKE A GAP, and the distinction is the whole correction: the site that started +// this was dag/gunbc/heal_revalidation.dag passing a List VARIABLE into a +// List parameter. That is list-typed-value compatibility, and the relation answers +// Undecidable for a generic carrier BY DESIGN. This probe instead passes a list LITERAL with a +// wrong element, which is a different judgment and one the relation makes. I inferred the second +// from the silence on the first. THE LIST-TYPED-VALUE CASE REMAINS UNMEASURED and no arm here +// claims anything about it. // // THE PRODUCED VALUE IS A KERNEL STRING BECAUSE THE FIRST VERSION OF THIS PAIR USED A RECORD // LITERAL AND ITS CONTROL WENT RED, which is the only reason the mis-design was caught rather diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 2b62f483a03..e7245aafc7a 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -509,17 +509,15 @@ fn floor_expected_red_chunk_14() -> List { // NEXT-RUNG TRIGGER: declared_type_inhabitance descending into a list's element type at a // direct-call argument. When it lands this row goes green and the roster's self-emptying arm // names it for removal, at which point it becomes a permanent regression control. -// DELIBERATELY EMPTY. THE ROW THAT BELONGS HERE IS NOT ENROLLED YET, ON PURPOSE. -// w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused was enrolled here while its -// paired control was RED, and the control's red proved the pair was measuring the wrong thing -// entirely -- a record literal is never judged at any position, so the list was doing no work. -// Both arms were rebuilt on a kernel String. THE REBUILT PAIR HAS NOT EXECUTED. -// -// An enrolment asserts a KNOWN, REAL gap. A CONTROL THAT REDS AND AN ARM THAT REDS ARE -// INDISTINGUISHABLE AS EVIDENCE, so enrolling before the control is green would re-file a claim -// that is currently believed rather than measured -- the exact state that put two unverified reds -// on this roster earlier. Until the run shows the control GREEN and the arm RED, the arm fails -// loudly as an ordinary failure, which is the honest reading of an unproven claim. +// DELIBERATELY EMPTY, AND PERMANENTLY SO -- THE ROW THAT WAS HERE ASSERTED A GAP THAT DOES NOT +// EXIST. w_wrong_element_type_in_a_list_at_a_direct_call_argument_is_refused was enrolled while +// its paired control was RED; the control's red proved the pair measured "records are never +// judged" rather than anything about lists. Rebuilt on a kernel String and left UNENROLLED so a +// red would show loudly, it PASSES (run 32667623528, failed=0). The relation descends into a +// list literal's elements at a direct-call argument and always did. +// +// The arm stays in the witness file as a permanent regression control over that fact. Nothing is +// enrolled here because there is nothing red to enrol. fn floor_expected_red_chunk_15() -> List { Empty {} } From 6b9808500a1bdefef06f97953a5a3e32a3846cc8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 25 Aug 2026 15:04:18 +0000 Subject: [PATCH 23/27] =?UTF-8?q?WIP:=20Compiler=20floor=20=E2=80=94=20dec?= =?UTF-8?q?lared-type=20inhabitance=20across=20every=20grammar=20type=20po?= =?UTF-8?q?s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .probe_fx/ish/control.dag | 8 ++++++++ .probe_fx/ish/probe.dag | 8 ++++++++ .probe_fx/ish/variant.dag | 11 +++++++++++ .probe_fx/probe/collide.dag | 8 ++++++++ .probe_fx/probe/control.dag | 8 ++++++++ .probe_fx/probe/globcollide.dag | 8 ++++++++ .probe_fx/probe/lib.dag | 7 +++++++ .probe_fx/probe/qualified.dag | 7 +++++++ .probe_fx/probe/reexport.dag | 8 ++++++++ .probe_fx/probe/viareexport.dag | 8 ++++++++ 10 files changed, 81 insertions(+) create mode 100644 .probe_fx/ish/control.dag create mode 100644 .probe_fx/ish/probe.dag create mode 100644 .probe_fx/ish/variant.dag create mode 100644 .probe_fx/probe/collide.dag create mode 100644 .probe_fx/probe/control.dag create mode 100644 .probe_fx/probe/globcollide.dag create mode 100644 .probe_fx/probe/lib.dag create mode 100644 .probe_fx/probe/qualified.dag create mode 100644 .probe_fx/probe/reexport.dag create mode 100644 .probe_fx/probe/viareexport.dag diff --git a/.probe_fx/ish/control.dag b/.probe_fx/ish/control.dag new file mode 100644 index 00000000000..28f3c6cd6c8 --- /dev/null +++ b/.probe_fx/ish/control.dag @@ -0,0 +1,8 @@ +module ish.control + +import std.types { String } +import std.algebra { trim } + +fn trim_wrapper(value: String) -> String { + trim(value) +} diff --git a/.probe_fx/ish/probe.dag b/.probe_fx/ish/probe.dag new file mode 100644 index 00000000000..4ff72f69fa9 --- /dev/null +++ b/.probe_fx/ish/probe.dag @@ -0,0 +1,8 @@ +module ish.probe + +import std.types { String } +import std.algebra { trim } + +fn trim(value: String) -> String { + trim(value) +} diff --git a/.probe_fx/ish/variant.dag b/.probe_fx/ish/variant.dag new file mode 100644 index 00000000000..92d12382041 --- /dev/null +++ b/.probe_fx/ish/variant.dag @@ -0,0 +1,11 @@ +module ish.variant + +import std.types { String, Bool } + +type IshVariantHolder + = Bool { value: String } + | IshOther { value: String } + +fn ish_variant_use(value: String) -> IshVariantHolder { + IshOther { value: value } +} diff --git a/.probe_fx/probe/collide.dag b/.probe_fx/probe/collide.dag new file mode 100644 index 00000000000..5ad56fb9797 --- /dev/null +++ b/.probe_fx/probe/collide.dag @@ -0,0 +1,8 @@ +module probe.collide + +import std.types { Bool } +import probe.lib { target_symbol } + +fn target_symbol() -> Bool { + target_symbol() +} diff --git a/.probe_fx/probe/control.dag b/.probe_fx/probe/control.dag new file mode 100644 index 00000000000..60b0bf4eafc --- /dev/null +++ b/.probe_fx/probe/control.dag @@ -0,0 +1,8 @@ +module probe.control + +import std.types { Bool } +import probe.lib { target_symbol } + +fn wrapper_distinct_name() -> Bool { + target_symbol() +} diff --git a/.probe_fx/probe/globcollide.dag b/.probe_fx/probe/globcollide.dag new file mode 100644 index 00000000000..7e2771f7315 --- /dev/null +++ b/.probe_fx/probe/globcollide.dag @@ -0,0 +1,8 @@ +module probe.globcollide + +import std.types { Bool } +import probe.lib + +fn target_symbol() -> Bool { + target_symbol() +} diff --git a/.probe_fx/probe/lib.dag b/.probe_fx/probe/lib.dag new file mode 100644 index 00000000000..a0fe62a986f --- /dev/null +++ b/.probe_fx/probe/lib.dag @@ -0,0 +1,7 @@ +module probe.lib + +import std.types { Bool } + +fn target_symbol() -> Bool { + true +} diff --git a/.probe_fx/probe/qualified.dag b/.probe_fx/probe/qualified.dag new file mode 100644 index 00000000000..563b0e43f7e --- /dev/null +++ b/.probe_fx/probe/qualified.dag @@ -0,0 +1,7 @@ +module probe.qualified + +import std.types { Bool } + +fn target_symbol() -> Bool { + probe.lib.target_symbol() +} diff --git a/.probe_fx/probe/reexport.dag b/.probe_fx/probe/reexport.dag new file mode 100644 index 00000000000..4ff171527d0 --- /dev/null +++ b/.probe_fx/probe/reexport.dag @@ -0,0 +1,8 @@ +module probe.reexport + +import std.types { Bool } +import probe.lib { target_symbol } + +fn passthrough() -> Bool { + target_symbol() +} diff --git a/.probe_fx/probe/viareexport.dag b/.probe_fx/probe/viareexport.dag new file mode 100644 index 00000000000..e7cfc54e0c5 --- /dev/null +++ b/.probe_fx/probe/viareexport.dag @@ -0,0 +1,8 @@ +module probe.viareexport + +import std.types { Bool } +import probe.reexport { target_symbol } + +fn target_symbol() -> Bool { + target_symbol() +} From 2b8ed295f680b148e9c260d4ab60db4bcfbf9137 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 25 Aug 2026 15:51:23 +0000 Subject: [PATCH 24/27] WIP: counted non-blocking residue for the four undecidable inhabitance reasons (seed mirrors not yet regenerated) --- src/v1/00_core.dag | 6 ++++++ src/v1/04_infer.dag | 36 +++++++++++++++++++++++++++++++++++- 2 files changed, 41 insertions(+), 1 deletion(-) diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index b2c3a901aff..0fcb5c02332 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -197,6 +197,7 @@ type CompilerDiagnostic } | AdmitCallersEntryNotDeclRef { constructor_decl_name: String, span: SourceSpan } | DeclaredTypeNotInhabited { position: String, expected: String, got: String, span: SourceSpan } + | DeclaredTypeInhabitanceUndecided { position: String, reason: String, span: SourceSpan } | UnlistedImportUse { name: String, span: SourceSpan } | AmbiguousReference { name: String, candidates: List, span: SourceSpan } | AmbiguousAnonymousRecordLiteral { candidates: List, span: SourceSpan } @@ -345,6 +346,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan { } => s AdmitCallersEntryNotDeclRef { constructor_decl_name: _, span: s } => s DeclaredTypeNotInhabited { position: _, expected: _, got: _, span: s } => s + DeclaredTypeInhabitanceUndecided { position: _, reason: _, span: s } => s UnlistedImportUse { name: _, span: s } => s AmbiguousReference { name: _, candidates: _, span: s } => s AmbiguousAnonymousRecordLiteral { candidates: _, span: s } => s @@ -423,6 +425,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String { concat("admit_callers entry on '", cn, "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored") DeclaredTypeNotInhabited { position: pos, expected: e, got: g, span: _ } => concat("value does not inhabit its declared type at the ", pos, ": declared '", e, "', produced '", g, "'") + DeclaredTypeInhabitanceUndecided { position: pos, reason: r, span: _ } => + concat("declared-type inhabitance is undecidable at the ", pos, " (", r, "): the modeled facts do not settle whether the produced value inhabits its declared type, so no verdict is asserted in either direction") UnlistedImportUse { name: n, span: _ } => concat("unlisted import use '", n, "' (referenced but not in any import's name list)") AmbiguousReference { name: n, candidates: cs, span: _ } => concat("ambiguous reference '", n, "': ", to_string(value: cs |> count), " candidates: ", join(cs, separator: ", "), " — qualify by containment path, alias, or rename") AmbiguousAnonymousRecordLiteral { candidates: cs, span: _ } => concat("ambiguous anonymous record literal shape matches ", to_string(value: cs |> count), " structs: ", join(cs, separator: ", "), " — add a nominal type") @@ -497,6 +501,7 @@ fn is_interpreter_blocking_diagnostic(d: CompilerDiagnostic) -> Bool { MethodExistenceFrontierAdmitted { method: _, receiver_type: _, trigger: _, span: _ } => false ReceiverTypeUnestablished { method: _, span: _ } => false ServiceConfigReferenceJudgmentDeferred { field: _, referenced_name: _, trigger: _, span: _ } => false + DeclaredTypeInhabitanceUndecided { position: _, reason: _, span: _ } => false _ => true } } @@ -507,6 +512,7 @@ fn is_discovery_corpus_advisory_typecheck_diagnostic(d: CompilerDiagnostic) -> B MethodExistenceFrontierAdmitted { method: _, receiver_type: _, trigger: _, span: _ } => true ReceiverTypeUnestablished { method: _, span: _ } => true ServiceConfigReferenceJudgmentDeferred { field: _, referenced_name: _, trigger: _, span: _ } => true + DeclaredTypeInhabitanceUndecided { position: _, reason: _, span: _ } => true WhereRefinementUnenforced { predicate: _, formal_type: _, reason: r, span: _ } => is_where_refinement_unenforced_advisory_reason(reason: r) _ => false diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 9cda01b2a71..8e0da8ff5e0 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2441,10 +2441,44 @@ fn declared_realizes_as_kernel_numeric( } } +// THE UNDECIDABLE ARM IS COUNTED, NOT SILENT, AND NOT A REFUSAL. It used to read +// `InhabitanceUndecidable { reason: _ } => []`, which is total over the verdict and blind one +// level down: the four reasons are declared precisely because they are different facts, and the +// wildcard gave all four the SAME rendering as Inhabits -- an undecidable seam and a decided-good +// seam left the relation as the identical empty list, so nothing downstream could tell a value +// that was judged from one that was never judgeable. That is the fail-open fabrication DESIGN +// section 5 forbids, and its cost is the one section 5 names: the deficit's frequency was zero by +// construction, so no reason could ever rank for the modeling that would settle it. +// +// WHY ADVISORY AND NOT A REFUSAL. Refusing here would fabricate a verdict in the other direction: +// the facts do not settle inhabitance, so asserting non-inhabitance is exactly as invented as +// asserting inhabitance. Undecidable is a property of the facts, never of the wiring, and the +// honest report is that no verdict was reached -- located, per-reason, and countable, so the four +// populations are observable and prioritizable. DeclaredTypeInhabitanceUndecided is registered +// 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_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" + UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape" + UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against" + UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam" + } +} + fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: InferScope) -> List { match declared_type_inhabitance(obligation: obligation, scope: scope) { Inhabits => [] - InhabitanceUndecidable { reason: _ } => [] + InhabitanceUndecidable { reason: r } => + [make_error_node( + diagnostic: DeclaredTypeInhabitanceUndecided { + position: declared_type_position_label(position: obligation.position), + reason: inhabitance_undecidable_reason_label(reason: r), + span: obligation.span + }, + module_name: scope.module_name + )] InhabitanceRefused { reason: _ } => [make_error_node( diagnostic: DeclaredTypeNotInhabited { From 6a07875e3692c9954b0145209981b3c6062c6c49 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 25 Aug 2026 17:00:51 +0000 Subject: [PATCH 25/27] Declare the ten unwired type positions and their next-rung trigger --- src/v1/04_infer.dag | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 8e0da8ff5e0..9fada5a6ab6 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2297,6 +2297,35 @@ fn coproduct_variant_payload_admits_type_name( // was produced; declared_type_inhabitance is the single relation that decides; the position // travels with the obligation so the diagnostic can locate the refusal without the decision // procedure forking per position. +// TWO OF THE TWELVE ARE WIRED. THE OTHER TEN ARE DECLARED HERE AND PRODUCE NOTHING YET, AND +// THAT IS STATED AS A COUNT RATHER THAN LEFT TO BE DISCOVERED FROM THE ABSENCE OF CALLERS. +// Measured by construction site, not by reading: PositionDirectCallArgument and +// PositionListElement are the only two members CONSTRUCTED anywhere -- every other member +// occurs solely in declared_type_position_label's match, which renders a name and judges +// nothing. So this coproduct is today an OBLIGATION VOCABULARY, of which two positions have a +// producer. +// +// WHY THAT IS NOT AN UNDECIDABLE ARM AND MUST NEVER BE FILED AS ONE: an unwired position is a +// MISSING OBLIGATION PRODUCER, not a fact the model cannot settle. It is absent from the census +// rather than present with a verdict -- so it produces no diagnostic, blocking or advisory, and +// nothing in the corpus is red on its account. Recording these as expected-red rows would be +// exactly the rung inflation 4b names, since there is no red to expect; and recording them as +// InhabitanceUndecidable would report "we did not look" as "it cannot be decided", which is the +// same inflation aimed at this relation's own self-description. +// +// NEXT-RUNG TRIGGER, one per position and all the same shape: a producer at that grammar seam +// that builds a DeclaredTypeObligation and hands it to declared_type_obligation_diags. The +// decision procedure is already shared and position-agnostic, so wiring one is authoring a +// construction site, never extending this relation -- which is the whole point of the carrier +// and is why the residual ten cost a call each rather than a rule each. +// +// THE TEN AWAITING A PRODUCER: PositionRecordLiteralField, PositionMapValue, +// PositionDataInitializer, PositionDeclaredReturn, PositionLetAnnotation, PositionVariantPayload, +// PositionGenericTypeArgument, PositionCastTarget, PositionParameterDefault, +// PositionCallableReturn. Wiring any of them is a separate change with its own evidence: a +// discriminating RED at that seam plus an accepted positive control, per 4b(1). Until then this +// carrier's honest claim is TWO POSITIONS JUDGED, ten declared -- and any statement that it +// judges "every grammar type position" is false. type DeclaredTypePosition = PositionRecordLiteralField | PositionListElement From 943a42151d4b4a8a08195bc329195c7f3b47eee2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 25 Aug 2026 17:44:43 +0000 Subject: [PATCH 26/27] Regenerate the seed mirrors and add the compile-forced cli_run arms for the new variant --- src/v1/stage0/src/cli_run.rs | 4 ++++ src/v1/stage0/src/v1_compiler_infer.rs | 20 +++++++++++++++++++- src/v1/stage0/src/v1_std_core.rs | 9 +++++++++ 3 files changed, 32 insertions(+), 1 deletion(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index dd722c12465..79e49d5eb1c 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -5090,6 +5090,9 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str } CompilerDiagnostic::AdmitCallersEntryNotDeclRef { .. } => "AdmitCallersEntryNotDeclRef", CompilerDiagnostic::DeclaredTypeNotInhabited { .. } => "DeclaredTypeNotInhabited", + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { .. } => { + "DeclaredTypeInhabitanceUndecided" + } CompilerDiagnostic::UnlistedImportUse { .. } => "UnlistedImportUse", CompilerDiagnostic::AmbiguousReference { .. } => "AmbiguousReference", CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { .. } => { @@ -5147,6 +5150,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str .. } => constructor_decl_name.clone(), CompilerDiagnostic::DeclaredTypeNotInhabited { position, .. } => position.clone(), + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { position, .. } => position.clone(), CompilerDiagnostic::UnlistedImportUse { name, .. } => name.clone(), CompilerDiagnostic::AmbiguousReference { name, .. } => name.clone(), CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { candidates, .. } => { diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index d3d7016c629..2712b794df5 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -3505,13 +3505,31 @@ pub fn declared_realizes_as_kernel_numeric( } } +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(), + InhabitanceUndecidableReason::UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape".to_string(), + InhabitanceUndecidableReason::UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against".to_string(), + InhabitanceUndecidableReason::UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam".to_string(), +} +} + pub fn declared_type_obligation_diags( obligation: Rc, scope: Rc, ) -> Rc>> { match (*declared_type_inhabitance(obligation.clone(), scope.clone())).clone() { InhabitanceVerdict::Inhabits => Rc::new(vec![]), - InhabitanceVerdict::InhabitanceUndecidable { reason: _, .. } => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceUndecidable { reason: r, .. } => { + Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { + position: declared_type_position_label(obligation.position.clone()), + reason: inhabitance_undecidable_reason_label(r.clone()), + span: obligation.span.clone(), + }), + scope.module_name.clone(), + )]) + } InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => Rc::new(vec![make_error_node( Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { position: declared_type_position_label(obligation.position.clone()), diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index 47d0da65843..9a02a12a3c5 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -540,6 +540,11 @@ pub enum CompilerDiagnostic { got: String, span: Rc, }, + DeclaredTypeInhabitanceUndecided { + position: String, + reason: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -703,6 +708,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { span: s, .. } => s.clone(), CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { span: s, .. } => s.clone(), @@ -756,6 +762,7 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, .. } => v1_rt::concat(v1_rt::concat("admit_callers entry on '".to_string(), cn.clone()), "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored".to_string()), CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { position: pos, reason: r, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("declared-type inhabitance is undecidable at the ".to_string(), pos.clone()), " (".to_string()), r.clone()), "): the modeled facts do not settle whether the produced value inhabits its declared type, so no verdict is asserted in either direction".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::AmbiguousAnonymousRecordLiteral { candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous anonymous record literal shape matches ".to_string(), ((cs.clone().len() as i64)).to_string()), " structs: ".to_string()), cs.clone().join(&", ".to_string())), " — add a nominal type".to_string()), @@ -857,6 +864,7 @@ pub fn is_interpreter_blocking_diagnostic(d: Rc) -> bool { CompilerDiagnostic::MethodExistenceFrontierAdmitted { .. } => false, CompilerDiagnostic::ReceiverTypeUnestablished { .. } => false, CompilerDiagnostic::ServiceConfigReferenceJudgmentDeferred { .. } => false, + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { .. } => false, _ => true, } } @@ -867,6 +875,7 @@ pub fn is_discovery_corpus_advisory_typecheck_diagnostic(d: Rc true, CompilerDiagnostic::ReceiverTypeUnestablished { .. } => true, CompilerDiagnostic::ServiceConfigReferenceJudgmentDeferred { .. } => true, + CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { .. } => true, CompilerDiagnostic::WhereRefinementUnenforced { reason: r, .. } => { is_where_refinement_unenforced_advisory_reason(r.clone()) } From f57bc0ec105d3940950a8273838a1788b6851d6f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 25 Aug 2026 19:43:20 +0000 Subject: [PATCH 27/27] Regenerate the infer mirror the merge dropped: the .dag had #9192's fix, the .rs did not The merge commit 4c9c55c6a4b resolved the generated-mirror conflict by taking one side whole. That is a SILENT deletion -- no conflict markers, clean tree, and the committed mirror became an OLDER COMPILER than the .dag it claims to mirror. Measured, with the control that makes it a result rather than a name-mangling artifact: fn .dag .rs(before) select_formal_for_call_argument 1 0 call_argument_formal_at_position 1 0 call_formal_claimed_by_a_label 1 0 declared_type_inhabitance 1 1 <- pre-existing, same grep, present in both declared_type_obligation_diags 1 1 <- same and `select_formal_for_call_argument` IS spelled that way in origin/main's mirror, so the grep works and the absence is real. #9192 landed to stop inference binding named arguments by POSITION -- refusing valid programs -- and this branch would have re-shipped the seed without that fix while the .dag said it had it. REGENERATED, NOT RE-RESOLVED AND NOT SPLICED. No hand edit to the .rs. The emitted file was taken from target/stage0-regen-candidate/src/ and installed whole. Receipts, from runs that did not share a candidate directory: round 1 (broken head): first_generation_equal=false FAIL generated surface drift: v1_compiler_infer.rs round 2 (installed): first_generation_equal=true planned=135 executed=135 declared_divergent=1 [main.rs] The fixed point is demonstrated at byte grain, not just by the flag: the installed file's sha256 210e64fb2ad08be2 was recorded BEFORE the confirming run, and that run re-emitted the identical hash. diff -rq over the candidate tree reports no other differing file. CI independently reached the same verdict on the broken head (run 32884947431), with a byte-identical message -- so the mirror-to-source comparison on a PR is intact and this red was the gate working, not a flake. --- src/v1/stage0/src/v1_compiler_infer.rs | 511 +++++++++++++++++++------ 1 file changed, 387 insertions(+), 124 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 2712b794df5..6f4a70b80c9 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -1,6 +1,7 @@ // Generated by v1 compiler -- do not edit. // Source module: v1.compiler.infer +use self::CallArgumentFormalSelection::*; use self::DeclaredTypePosition::*; use self::DescentSizeExpr::*; use self::InhabitanceRefusalReason::*; @@ -3843,6 +3844,292 @@ pub fn direct_call_structured_record_literal_resolved_type_mismatch( } } +pub fn call_argument_formal_selection_note() -> String { + thread_local! { + static CACHED: String = { + "SINGLE AUTHORITY (DESIGN §3) for one question: which declared formal does a call argument bind to. The question was answered in TWO places with DIFFERENT rules, and the divergence produced wrong emitted types with no diagnostic anywhere. build_call_application_plan matched an argument to a formal by AUTHORED LABEL, falling back to position -- the same rule the interpreter's call_function_inner uses. The ExprCall inference fold, which chooses the EXPECTED type each argument is inferred under, selected purely by SOURCE POSITION and read the argument's label only to tag the result node. So a call passing named arguments in a different order than declared handed each argument its NEIGHBOUR's formal, while the type check -- running the other rule -- correctly paired them and reported nothing. Measured live: src/v1/05_emit.dag:2993 calls emit_typed_match_unified with all seven arguments named and source_indices ahead of recurse, so the recurse lambda was inferred against render_pattern's fn(MatchPattern) -> String; it emitted |node: Rc, d| and the stage0 build failed E0308 + E0282, from a call the compiler had declared clean. THE FIX IS NOT A SECOND COPY OF THE NAME-FIRST SEARCH. Pasting the rule into the fold would leave two implementations that agree today and drift later, which is the same §3 failure one layer down. This selector is the rule, held once; the fold consumes it directly, and the plan builder consumes it INVERTED -- a formal's argument is the argument that selects that formal's index -- so neither side can encode a rule the other does not. It returns the formal's INDEX as well as its node precisely so that inversion needs no second search. It is deliberately PRE-TYPE: it reads authored labels only, needs no substitution and no inferred types, so it is available before recursive argument inference begins and call_subst still accumulates in authored source order, leaving generic unification order untouched. Unknown and duplicate labels stay owned by direct_call_shape_wall_note's walls; this selector decides correspondence, never admission. THE LABEL TEST IS call_param_caller_labels, NOT EXACT EQUALITY, and the distinction is the underscore idiom: a parameter declared _ctx is addressable by callers as ctx, so exact equality missed it and fell through to the positional arm -- measured, ignore_ctx(n: 1, ctx: []) against fn ignore_ctx(_ctx: List, n: Int) kept the fabricated empty-list refusal until this was corrected. call_param_caller_labels is used rather than call_arg_label_matches_param because the two answer different questions: that predicate governs ADMISSION and returns true for a bare _ against ANY label, which is correct for asking whether a label names a declared parameter and catastrophic for asking WHICH parameter a label selects -- an anonymous parameter would claim the first label it saw. call_param_caller_labels answers the selection question directly, yielding [] for a bare _ so it can never be selected by name, so the hazard is closed by the authority chosen rather than by a guard beside it. INJECTIVITY, AND WHY IT DOES NOT SUBSUME THE RUNTIME-KEY WALL. The relation this selector defines must be a partial bijection: functional -- one argument selects one formal -- falls out of the selector's shape, but INJECTIVE -- one formal receives at most one argument -- does not, and its absence was silent wrongness below the floor. Measured on both compilers before the fix: f(a: 1, _a: 2, b: 3) against fn f(_a: Int, b: Int) compiled CLEAN and emitted f(2, 3), dropping the argument a: 1 with no diagnostic anywhere, because a and _a are two caller spellings of ONE formal and nothing asked whether two arguments had chosen the same one. formal_identity_duplicate_diags closes that: an argument whose selected formal index was already claimed by an EARLIER argument is refused. THE TWO WALLS PARTITION BY CAUSE AND MUST NOT BE MERGED. duplicate_label_diags asks whether two arguments produce the same RUNTIME BINDING KEY, via call_arg_bound_param_at's running counter over positionally-eligible names, and it also catches collisions this selector cannot see; it stays separate by operator ruling. This wall asks whether two arguments select the same SEMANTIC FORMAL. The questions coincide on exactly one input shape -- two arguments carrying the SAME authored label -- and there the key wall already owns the refusal, so this wall is guarded to fire only when the two labels DIFFER. Without that guard both fired and f(a: 1, a: 2, b: 3) produced TWO byte-identical diagnostics, measured; suppressing on identical labels is not a courtesy to the reader but the statement of which wall owns which cause.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum CallArgumentFormalSelection { + CallArgumentFormalSelected { formal_index: i64, formal: Rc }, + CallArgumentFormalUnavailable, +} +impl CallArgumentFormalSelection { + pub fn formal_index(&self) -> i64 { + match self { + CallArgumentFormalSelection::CallArgumentFormalSelected { + formal_index: __val, + .. + } => __val.clone(), + CallArgumentFormalSelection::CallArgumentFormalUnavailable => { + panic!("no formal_index on unit variant") + } + } + } + pub fn formal(&self) -> Rc { + match self { + CallArgumentFormalSelection::CallArgumentFormalSelected { formal: __val, .. } => { + __val.clone() + } + CallArgumentFormalSelection::CallArgumentFormalUnavailable => { + panic!("no formal on unit variant") + } + } + } +} + +pub fn call_argument_label_selects_formal_index( + label: String, + formal_index: i64, + value_params: Rc>>, + source_indices: Rc>>, +) -> bool { + match Rc::new({ + let mut __result = Vec::new(); + for candidate in Rc::new( + value_params + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + if { + let mut __found = false; + for caller_label in call_param_caller_labels(authored_name_at( + source_indices.clone(), + candidate.1.clone(), + )) + .iter() + .cloned() + { + if (caller_label.clone() == label.clone()) { + __found = true; + break; + } + } + __found + } { + __result.push(candidate); + } + } + __result + }) + .first() + .cloned() + { + Some(named) => (named.0.clone() == formal_index.clone()), + None => false, + } +} + +pub fn call_formal_claimed_by_a_label( + formal_index: i64, + arguments: Rc>>, + value_params: Rc>>, + source_indices: Rc>>, +) -> bool { + { + let mut __found = false; + for other in arguments.iter().cloned() { + if match arg_name_at(other.clone(), source_indices.clone()) { + Some(label) => call_argument_label_selects_formal_index( + label.clone(), + formal_index.clone(), + value_params.clone(), + source_indices.clone(), + ), + None => false, + } { + __found = true; + break; + } + } + __found + } +} + +pub fn call_argument_positional_rank( + arguments: Rc>>, + argument_index: i64, + source_indices: Rc>>, +) -> i64 { + (Rc::new({ + let mut __result = Vec::new(); + for other in Rc::new( + arguments + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + if ((other.0.clone() < argument_index.clone()) + && match arg_name_at(other.1.clone(), source_indices.clone()) { + Some(_) => false, + None => true, + }) + { + __result.push(other); + } + } + __result + }) + .len() as i64) +} + +pub fn call_argument_formal_at_position( + arguments: Rc>>, + value_params: Rc>>, + argument_index: i64, + source_indices: Rc>>, +) -> Rc { + match Rc::new({ + let mut __result = Vec::new(); + for candidate in Rc::new( + value_params + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + if !call_formal_claimed_by_a_label( + candidate.0.clone(), + arguments.clone(), + value_params.clone(), + source_indices.clone(), + ) { + __result.push(candidate); + } + } + __result + }) + .iter() + .cloned() + .skip(call_argument_positional_rank( + arguments.clone(), + argument_index.clone(), + source_indices.clone(), + ) as usize) + .next() + { + Some(positional) => Rc::new(CallArgumentFormalSelection::CallArgumentFormalSelected { + formal_index: positional.0.clone(), + formal: positional.1.clone(), + }), + None => Rc::new(CallArgumentFormalSelection::CallArgumentFormalUnavailable), + } +} + +pub fn select_formal_for_call_argument( + argument: Rc, + argument_index: i64, + arguments: Rc>>, + value_params: Rc>>, + source_indices: Rc>>, +) -> Rc { + match arg_name_at(argument.clone(), source_indices.clone()) { + Some(label) => match Rc::new({ + let mut __result = Vec::new(); + for candidate in Rc::new( + value_params + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + if { + let mut __found = false; + for caller_label in call_param_caller_labels(authored_name_at( + source_indices.clone(), + candidate.1.clone(), + )) + .iter() + .cloned() + { + if (caller_label.clone() == label.clone()) { + __found = true; + break; + } + } + __found + } { + __result.push(candidate); + } + } + __result + }) + .first() + .cloned() + { + Some(named) => Rc::new(CallArgumentFormalSelection::CallArgumentFormalSelected { + formal_index: named.0.clone(), + formal: named.1.clone(), + }), + None => call_argument_formal_at_position( + arguments.clone(), + value_params.clone(), + argument_index.clone(), + source_indices.clone(), + ), + }, + None => call_argument_formal_at_position( + arguments.clone(), + value_params.clone(), + argument_index.clone(), + source_indices.clone(), + ), + } +} + +pub fn call_argument_selects_formal_index( + argument: Rc, + argument_index: i64, + formal_index: i64, + arguments: Rc>>, + value_params: Rc>>, + source_indices: Rc>>, +) -> bool { + match (*select_formal_for_call_argument( + argument.clone(), + argument_index.clone(), + arguments.clone(), + value_params.clone(), + source_indices.clone(), + )) + .clone() + { + CallArgumentFormalSelection::CallArgumentFormalSelected { + formal_index: selected, + .. + } => (selected.clone() == formal_index.clone()), + CallArgumentFormalSelection::CallArgumentFormalUnavailable => false, + } +} + #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] pub struct CallFormalApplication { pub index: i64, @@ -3903,13 +4190,27 @@ pub fn build_call_application_plan( ), matched_arg: match Rc::new({ let mut __result = Vec::new(); - for ta in typed_args.iter().cloned() { - if arg_has_name( - ta.clone(), - param_name.clone(), + for candidate in Rc::new( + typed_args + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + if call_argument_selects_formal_index( + candidate.1.clone(), + candidate.0.clone(), + pair.0.clone(), + typed_args.clone(), + value_params.clone(), source_indices.clone(), ) { - __result.push(ta); + __result.push(candidate); } } __result @@ -3917,13 +4218,8 @@ pub fn build_call_application_plan( .first() .cloned() { - Some(named_ta) => Some(named_ta.clone()), - None => typed_args - .clone() - .iter() - .cloned() - .skip(pair.0.clone() as usize) - .next(), + Some(bound) => Some(bound.1.clone()), + None => None, }, }) }); @@ -4577,6 +4873,42 @@ pub fn direct_call_shape_diags( } __result }); + let formal_identity_duplicate_diags = Rc::new({ + let mut __result = Vec::new(); + for pair in Rc::new( + typed_args + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + __result.extend((*match (*select_formal_for_call_argument(pair.1.clone(), pair.0.clone(), typed_args.clone(), sig_params.clone(), source_indices.clone())).clone() { + CallArgumentFormalSelection::CallArgumentFormalSelected { formal_index: mine, formal: chosen, .. } => { + let my_label = arg_name_at(pair.1.clone(), source_indices.clone()); +let earlier_same_formal = { let mut __found = false; for other in Rc::new(typed_args.clone().iter().cloned().enumerate().map(|(i, v)| (i as i64, v)).collect::>()).iter().cloned() { if (((other.0.clone() < pair.0.clone()) && !(arg_name_at(other.1.clone(), source_indices.clone()).as_deref() == my_label.clone().as_deref())) && match (*select_formal_for_call_argument(other.1.clone(), other.0.clone(), typed_args.clone(), sig_params.clone(), source_indices.clone())).clone() { + CallArgumentFormalSelection::CallArgumentFormalSelected { formal_index: theirs, .. } => (theirs.clone() == mine.clone()), + CallArgumentFormalSelection::CallArgumentFormalUnavailable => false, +}) { __found = true; break; } } __found }; +if earlier_same_formal.clone() { + Rc::new(vec![make_error_node(Rc::new(CompilerDiagnostic::CallArgumentDuplicate { + callee: func_name.clone(), + argument: authored_name_at(source_indices.clone(), chosen.clone()), + span: pair.1.clone().span.clone(), +}), module_name.clone())]) + } else { + Rc::new(vec![]) + } +}, + CallArgumentFormalSelection::CallArgumentFormalUnavailable => Rc::new(vec![]), +}).iter().cloned()); + } + __result + }); let arity_scan = scan_call_shape_arity( sig_params.clone(), typed_args.clone(), @@ -4597,8 +4929,11 @@ pub fn direct_call_shape_diags( None => Rc::new(vec![]), }; v1_rt::concat( - v1_rt::concat(unknown_label_diags.clone(), surplus_diags.clone()), - v1_rt::concat(duplicate_label_diags.clone(), deficit_diags.clone()), + v1_rt::concat( + v1_rt::concat(unknown_label_diags.clone(), surplus_diags.clone()), + v1_rt::concat(duplicate_label_diags.clone(), deficit_diags.clone()), + ), + formal_identity_duplicate_diags.clone(), ) } } @@ -7092,116 +7427,44 @@ pub fn infer_expr_body( { let value_params = call_sig_split.value_params.clone(); let generic_names = call_sig_split.generic_names.clone(); - let final_state = Rc::new( - call_args - .clone() - .iter() - .cloned() - .enumerate() - .map(|(i, v)| (i as i64, v)) - .collect::>(), - ) - .iter() - .cloned() - .fold( - Rc::new(ArgGenericFoldState { - results: Rc::new(vec![]), - subst: v1_rt::rc_empty_map::>(), - }), - |st: Rc, pair: (i64, Rc)| { - let a = pair.1.clone(); - let formal_lookup = value_params - .clone() - .iter() - .cloned() - .skip(pair.0.clone() as usize) - .next(); - let formal_raw = match formal_lookup.clone() { - Some(p) => param_node_type_expr(p.clone()), - None => { - type_variable_node("callable_param".to_string()) - } - }; - let has_formal = match formal_lookup.clone() { - Some(_) => true, - None => false, - }; - let formal_param_type = substitute_generics( - formal_raw.clone(), - st.subst.clone(), - scope.type_env.clone().source_indices.clone(), - ); - let expected = if has_formal.clone() { - Some(formal_param_type.clone()) - } else { - None - }; - let ar = infer_expr( - arg_value(a.clone()), - scope.clone(), - expected.clone(), - ); - let next_subst = - if (is_lambda_expr(arg_value(a.clone())) - || !has_formal.clone()) - { - st.subst.clone() - } else { - if should_unify_record_lit_generics( - formal_raw.clone(), - arg_value(a.clone()), - generic_names.clone(), - scope - .type_env - .clone() - .source_indices - .clone(), - ) { - unify_record_lit_generics( - formal_raw.clone(), - ar.typed.clone(), - generic_names.clone(), - scope.clone(), - st.subst.clone(), - ) - } else { - unify_generics( - formal_raw.clone(), - resolved_type(ar.typed.clone()), - generic_names.clone(), - scope - .type_env - .clone() - .source_indices - .clone(), - st.subst.clone(), - ) - } - }; - Rc::new(ArgGenericFoldState { - results: v1_rt::concat( - st.results.clone(), - Rc::new(vec![Rc::new(ArgInferResult { - typed_arg: make_arg_node( - arg_name_at( - a.clone(), - scope - .type_env - .clone() - .source_indices - .clone(), - ), - ar.typed.clone(), - a.span.clone(), - a.span.clone(), - ), - diagnostics: ar.diagnostics.clone(), - })]), - ), - subst: next_subst.clone(), - }) - }, - ); + let final_state = Rc::new(call_args.clone().iter().cloned().enumerate().map(|(i, v)| (i as i64, v)).collect::>()).iter().cloned().fold(Rc::new(ArgGenericFoldState { + results: Rc::new(vec![]), + subst: v1_rt::rc_empty_map::>(), +}), |st: Rc, pair: (i64, Rc)| { + let a = pair.1.clone(); +let formal_selection = select_formal_for_call_argument(a.clone(), pair.0.clone(), call_args.clone(), value_params.clone(), scope.type_env.clone().source_indices.clone()); +let formal_raw = match (*formal_selection.clone()).clone() { + CallArgumentFormalSelection::CallArgumentFormalSelected { formal: p, .. } => param_node_type_expr(p.clone()), + CallArgumentFormalSelection::CallArgumentFormalUnavailable => type_variable_node("callable_param".to_string()), +}; +let has_formal = match (*formal_selection.clone()).clone() { + CallArgumentFormalSelection::CallArgumentFormalSelected { .. } => true, + CallArgumentFormalSelection::CallArgumentFormalUnavailable => false, +}; +let formal_param_type = substitute_generics(formal_raw.clone(), st.subst.clone(), scope.type_env.clone().source_indices.clone()); +let expected = if has_formal.clone() { + Some(formal_param_type.clone()) + } else { + None + }; +let ar = infer_expr(arg_value(a.clone()), scope.clone(), expected.clone()); +let next_subst = if (is_lambda_expr(arg_value(a.clone())) || !has_formal.clone()) { + st.subst.clone() + } else { + if should_unify_record_lit_generics(formal_raw.clone(), arg_value(a.clone()), generic_names.clone(), scope.type_env.clone().source_indices.clone()) { + unify_record_lit_generics(formal_raw.clone(), ar.typed.clone(), generic_names.clone(), scope.clone(), st.subst.clone()) + } else { + unify_generics(formal_raw.clone(), resolved_type(ar.typed.clone()), generic_names.clone(), scope.type_env.clone().source_indices.clone(), st.subst.clone()) + } + }; +Rc::new(ArgGenericFoldState { + results: v1_rt::concat(st.results.clone(), Rc::new(vec![Rc::new(ArgInferResult { + typed_arg: make_arg_node(arg_name_at(a.clone(), scope.type_env.clone().source_indices.clone()), ar.typed.clone(), a.span.clone(), a.span.clone()), + diagnostics: ar.diagnostics.clone(), +})])), + subst: next_subst.clone(), +}) +}); final_state.clone() } };