From 65122c2e94cfa8743c3bcaaea6c583dd2a0cab38 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 20:57:37 +0000 Subject: [PATCH 1/8] Model empty collection constraint refinement and author controls --- ...pty_collection_constraint_witness_test.dag | 56 +++++++++++++++++++ src/v1/04_infer.dag | 11 ++++ 2 files changed, 67 insertions(+) create mode 100644 dag/test/claim/empty_collection_constraint_witness_test.dag diff --git a/dag/test/claim/empty_collection_constraint_witness_test.dag b/dag/test/claim/empty_collection_constraint_witness_test.dag new file mode 100644 index 00000000000..cd60ac840bd --- /dev/null +++ b/dag/test/claim/empty_collection_constraint_witness_test.dag @@ -0,0 +1,56 @@ +module test.claim.empty_collection_constraint_witness + +import std.types { String, Bool, Int } +import v2.std.optional { Present, Absent } +import gunbc.compile_diagnostic_census { CompileDiagnosticCensus } +import gunbc.guarantee_probe_corpus { census_blocking_count_for_class } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// Permanent source-level controls for v1.compiler.infer.infer_call_arguments_generic_pass. +// The census compiles each authored program against the live tree; a failed observation +// refuses the claim. std.occurrence_identity.occurrence_allocation_fold is the later consumer of this shape. +fn callback_inference_error_count(source: String) -> Int { + match census_blocking_count_for_class(census: compile_dag_diagnostic_census(source), wanted: "InternalError") { + Present { value: n } => n + Absent => 0 - 1 + } +} + +data empty_fold_source: String = "module probe_generic_empty_fold\nimport std.types { Int, List, String }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Module { module: String, declarations: List }\nfn asks(xs: List) -> Int {\n let modules = fold_list(xs: xs, empty: [], cons: fn(acc, m) { list_snoc_item(xs: acc, item: m) })\n fold_list(xs: modules, empty: 0, cons: fn(acc, m) { acc + count(m.declarations) })\n}\n" + +test fn empty_fold_element_binds() -> Bool { + callback_inference_error_count(source: empty_fold_source) == 0 +} + +data nested_empty_fold_source: String = "module probe_nested_empty_fold\nimport std.types { Int, List, String }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Module { module: String, declarations: List }\ntype Source { modules: List }\nfn modules_for_source(source: Source) -> List { source.modules }\nfn asks(sources: List) -> Int {\n let modules = fold_list(\n xs: sources,\n empty: [],\n cons: fn(acc, source) {\n fold_list(\n xs: modules_for_source(source: source),\n empty: acc,\n cons: fn(inner, m) { list_snoc_item(xs: inner, item: m) }\n )\n }\n )\n fold_list(xs: modules, empty: 0, cons: fn(acc, m) { acc + count(m.declarations) })\n}\n" + +test fn nested_empty_fold_element_binds() -> Bool { + callback_inference_error_count(source: nested_empty_fold_source) == 0 +} + +data callback_result_element_binds_source: String = "module probe_callback_result\nimport std.types { Int, List }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Element { value: Int }\nfn asks(xs: List) -> Int {\n let elements = fold_list(xs: xs, empty: [], cons: fn(acc, n) { list_snoc_item(xs: acc, item: Element { value: n }) })\n fold_list(xs: elements, empty: 0, cons: fn(acc, e) { acc + e.value })\n}\n" + +test fn callback_result_element_binds() -> Bool { + callback_inference_error_count(source: callback_result_element_binds_source) == 0 +} + +data determined_element_missing_field_refuses_source: String = "module probe_callback_result\nimport std.types { Int, List }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Element { value: Int }\nfn asks(xs: List) -> Int {\n let elements = fold_list(xs: xs, empty: [], cons: fn(acc, n) { list_snoc_item(xs: acc, item: Element { value: n }) })\n fold_list(xs: elements, empty: 0, cons: fn(acc, e) { acc + e.missing })\n}\n" + +test fn determined_element_missing_field_refuses() -> Bool { + callback_inference_error_count(source: determined_element_missing_field_refuses_source) >= 1 +} + +data conflicting_established_constraints_refuse_source: String = "module probe_conflicting_constraints\nimport std.types { Int, String }\nfn same(left: T, right: T) -> T { left }\nfn asks() -> Int { same(left: 1, right: \"conflict\") }\n" + +test fn conflicting_established_constraints_refuse() -> Bool { + callback_inference_error_count(source: conflicting_established_constraints_refuse_source) >= 1 +} + +data callback_result_conflict_refuses_source: String = "module probe_callback_conflict\nimport std.types { Int, List, String }\nimport v2.std.algebra { fold_list }\nfn asks(xs: List) -> Int { fold_list(xs: xs, empty: 0, cons: fn(acc, n) { \"conflict\" }) }\n" + +test fn callback_result_conflict_refuses() -> Bool { + callback_inference_error_count(source: callback_result_conflict_refuses_source) >= 1 +} + diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 6bd0bcbc811..701730cd427 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -1,5 +1,16 @@ module v1.compiler.infer +// Empty collection constraints serve the self-host seed route consumed by +// v2.compiler.compile.native_lane_universe_after_ownership. An empty literal +// contributes an unresolved element variable, never Unit from an unresolved +// non-collection formal. Generic substitution refines unresolved slots using +// concrete arguments and callback results; rebinding applies that substitution. +// Established structure and cardinality remain constraints, and conflicting +// established constraints refuse. This rule does not widen compatibility or +// permit a field read on a never-constrained enclosing generic. The v2-side +// replacement is the application-argument substitution producer owned by +// adhoc-8760f34f-ec2; this is bounded maintenance of its executable seed route. + import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceSynthetic } import std.types { SourceSpan, NonEmptyStr, container_param_name, container_template_algebra, kernel_type_set, is_kernel_type } import std.content_hash { From 0eb833e87211a403a814e342186a9c00f0b27cc8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:01:50 +0000 Subject: [PATCH 2/8] Carry generic refinement conflicts through every unification caller --- src/v1/04_infer.dag | 175 ++++++++++++++++++++++++++++++-------------- 1 file changed, 120 insertions(+), 55 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 701730cd427..9d75b1d186d 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -4769,15 +4769,15 @@ fn direct_call_arg_type_mismatch( } } -fn borrowed_callable_call_type(gnode: Node, typed_args: List, scope: InferScope) -> Node { +fn borrowed_callable_call_type(gnode: Node, typed_args: List, scope: InferScope) -> GenericConstraintRefinement { let source_indices = scope.type_env.source_indices let base = callable_inferred(n: gnode) let tp_names = fn_type_param_names(item: gnode, source_indices: source_indices) if tp_names |> count == 0 { - base + GenericConstraintRefinement { refined: base, diagnostics: [] } } else { let value_params = gnode.params |> filter(p => !param_is_generic_decl(p: p, source_indices: source_indices)) - let subst = fold(value_params |> enumerate, init: empty_map(), f: (acc, pair) => + let subst = fold(value_params |> enumerate, init: GenericUnification { subst: empty_map(), diagnostics: [] }, f: (acc, pair) => let formal_raw = param_node_type_expr(n: pair.second) let param_name = authored_name_at(source_indices: source_indices, node: pair.second) let matched_arg = match typed_args |> filter(ta => arg_has_name(arg: ta, name: param_name, source_indices: source_indices)) |> first { @@ -4785,11 +4785,11 @@ fn borrowed_callable_call_type(gnode: Node, typed_args: List, scope: Infer Absent => typed_args |> skip(pair.first) |> first } match matched_arg { - Present { value: ta } => unify_generics(formal: formal_raw, actual: resolved_type(n: arg_value(n: ta)), generic_names: tp_names, source_indices: source_indices, acc: acc) + Present { value: ta } => unify_generics(formal: formal_raw, actual: resolved_type(n: arg_value(n: ta)), generic_names: tp_names, source_indices: source_indices, acc: acc, span: ta.span, scope: scope) Absent => acc } ) - substitute_generics(n: base, subst: subst, source_indices: source_indices) + GenericConstraintRefinement { refined: substitute_generics(n: base, subst: subst.subst, source_indices: source_indices), diagnostics: subst.diagnostics } } } @@ -5920,26 +5920,6 @@ fn is_lambda_expr(e: Node) -> Bool { } } -// A lambda argument contributes NOTHING to the call's generic substitution -- the -// argument fold skips it -- yet its own parameter types are read OUT of that -// substitution. So the substitution a lambda is inferred under is whatever the -// arguments to its LEFT happened to bind, and a type variable bound by an argument to -// its RIGHT, or by a sibling field of the record literal that CONTAINS it, is not there -// yet: the parameter falls to type_variable_node("callable_param") and every method -// call on it then fails to resolve. Measured before this pass existed, both blocking: -// a lambda field beside the field that binds R refused `map` and `count` on its own -// parameter with receiver type 'Primitive()', and a lambda argument declared ahead of -// the argument that binds R refused a field access with "no field 'px' on type 'R'". -// The repair is one extra ROUND of the same fold, not a second rule: the fold is run -// again from the substitution the first round ended with, so every argument sees every -// binding derivable in one forward pass regardless of authored order. Re-running is -// sound rather than merely convenient because the substitution is a fixed point of the -// second round: lambda arguments are skipped for unification, so deferring what they -// would have contributed cannot change the result, and a formal whose generic slot is -// already bound is substituted to a concrete node that unify_generics no longer binds. -// It is bounded at two rounds and says so: a binding that is only derivable FROM a -// substituted expected type -- a lambda return feeding a later formal -- is still out -// of reach, and that is a narrowing stated rather than implied. fn expr_contains_lambda(n: Node) -> Bool { is_lambda_expr(e: n) || (n.children |> any(c => expr_contains_lambda(n: c))) } @@ -5994,16 +5974,23 @@ fn infer_call_arguments_generic_pass(call_args: List, value_params: List + unify_generics(formal: result_formal, actual: resolved_type(n: ar.typed), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: initial_unification, span: a.span, scope: scope) + _ => initial_unification + } } else if should_unify_record_lit_generics(formal: formal_raw, arg_expr: arg_value(n: a), generic_names: generic_names, source_indices: scope.type_env.source_indices) { - unify_record_lit_generics(formal: formal_raw, record: ar.typed, generic_names: generic_names, scope: scope, acc: st.subst) + unify_record_lit_generics(formal: formal_raw, record: ar.typed, generic_names: generic_names, scope: scope, acc: initial_unification) } else { - unify_generics(formal: formal_raw, actual: resolved_type(n: ar.typed), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: st.subst) + unify_generics(formal: formal_raw, actual: resolved_type(n: ar.typed), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: initial_unification, span: a.span, scope: scope) } ArgGenericFoldState { - results: concat(st.results, [ArgInferResult { typed_arg: make_arg_node(occurrence_identity: a.occurrence_identity, name: arg_name_at(n: a, source_indices: scope.type_env.source_indices), value: ar.typed, span: a.span, name_span: a.span), diagnostics: ar.diagnostics }]), - subst: next_subst + results: concat(st.results, [ArgInferResult { typed_arg: make_arg_node(occurrence_identity: a.occurrence_identity, name: arg_name_at(n: a, source_indices: scope.type_env.source_indices), value: ar.typed, span: a.span, name_span: a.span), diagnostics: concat(ar.diagnostics, next_unification.diagnostics) }]), + subst: next_unification.subst } ) } @@ -7140,13 +7127,13 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu _ => global_bare_callable_node(type_env: scope.type_env, name: func_name) } } - let resolved_type = match type_match { - Present { value: tn } => tn + let resolved_call = match type_match { + Present { value: tn } => GenericConstraintRefinement { refined: tn, diagnostics: [] } Absent => match global_bare_callable { Present { value: gnode } => if (gnode.params |> count) > 0 { borrowed_callable_call_type(gnode: gnode, typed_args: typed_arg_nodes, scope: scope) } - else { callable_return_type(n: gnode) } - Absent => error_type + else { GenericConstraintRefinement { refined: callable_return_type(n: gnode), diagnostics: [] } } + Absent => GenericConstraintRefinement { refined: error_type, diagnostics: [] } } } let call_diags = match type_match { @@ -7175,11 +7162,11 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu typed: make_named_expr_node(occurrence_identity: texpr.occurrence_identity, name: func_name, expr_data: ExprCall { call_semantics: Present { value: PlainCallSemantics { target: resolved_plain_call_target_for_outcome(outcome: call_target) } }, descent_evidence: none }, children: typed_arg_nodes, - inferred: Present { value: Resolved { node: resolved_type } }, + inferred: Present { value: Resolved { node: resolved_call.refined } }, span: span, name_span: node_name_span(n: texpr) ), - diagnostics: concat(arg_diags, call_diags) + diagnostics: concat(concat(arg_diags, call_diags), resolved_call.diagnostics) } } } @@ -7587,7 +7574,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu Present { value: elem } => child_type_node(ch: elem) Absent => unit_type } - } else { unit_type } + } else { type_variable_node(id: "empty_list_element") } Absent => type_variable_node(id: "empty_list_element") } } @@ -7599,7 +7586,12 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu Present { value: _ } => [] Absent => [inference_error(message: "empty list literal: expected type has no element type", span: span, module_name: scope.module_name)] } - } else { [inference_error(message: "empty list literal: expected type is not a collection", span: span, module_name: scope.module_name)] } + } else { + match exp.inferred { + Present { value: TypeVariable { id: _ } } => [] + _ => [inference_error(message: "empty list literal: expected type is not a collection", span: span, module_name: scope.module_name)] + } + } Absent => [] } } else { [] } @@ -11466,23 +11458,96 @@ fn param_is_generic_decl(p: Node, source_indices: Map) -> && (pname == tname || (type_expr_is_var && pname == pt.name)) } -fn unify_generics(formal: Node, actual: Node, generic_names: List, source_indices: Map, acc: Map) -> Map { +type GenericUnification { subst: Map, diagnostics: List } +type GenericConstraintRefinement { refined: Node, diagnostics: List } + +fn generic_constraint_refusal(established: Node, span: SourceSpan, scope: InferScope) -> GenericConstraintRefinement { + GenericConstraintRefinement { + refined: established, + diagnostics: [inference_error(message: "conflicting established generic constraints", span: span, module_name: scope.module_name)] + } +} + +fn refine_generic_constraint(established: Node, incoming: Node, span: SourceSpan, scope: InferScope) -> GenericConstraintRefinement { + let established_variable = match established.inferred { Present { value: TypeVariable { id: _ } } => true _ => false } + let incoming_variable = match incoming.inferred { Present { value: TypeVariable { id: _ } } => true _ => false } + if established.return_cardinality != incoming.return_cardinality { + generic_constraint_refusal(established: established, span: span, scope: scope) + } else if established_variable { + GenericConstraintRefinement { refined: incoming, diagnostics: [] } + } else if incoming_variable { + GenericConstraintRefinement { refined: established, diagnostics: [] } + } else if is_fully_resolved(n: established, source_indices: scope.type_env.source_indices) && is_fully_resolved(n: incoming, source_indices: scope.type_env.source_indices) { + if node_type_equals(left: established, right: incoming, source_indices: scope.type_env.source_indices) { + GenericConstraintRefinement { refined: established, diagnostics: [] } + } else { generic_constraint_refusal(established: established, span: span, scope: scope) } + } else if type_node_label(n: established, source_indices: scope.type_env.source_indices) != type_node_label(n: incoming, source_indices: scope.type_env.source_indices) + || established.connective != incoming.connective + || count(established.children) != count(incoming.children) + || count(established.params) != count(incoming.params) { + generic_constraint_refusal(established: established, span: span, scope: scope) + } else { + let child_results = established.children |> enumerate |> map(pair => + match incoming.children |> skip(pair.first) |> first { + Present { value: other } => refine_generic_constraint(established: pair.second, incoming: other, span: span, scope: scope) + Absent => generic_constraint_refusal(established: pair.second, span: span, scope: scope) + } + ) + let param_results = established.params |> enumerate |> map(pair => + match incoming.params |> skip(pair.first) |> first { + Present { value: other } => refine_generic_constraint(established: pair.second, incoming: other, span: span, scope: scope) + Absent => generic_constraint_refusal(established: pair.second, span: span, scope: scope) + } + ) + let payload_result = match established.inferred { + Present { value: Resolved { node: left } } => match incoming.inferred { + Present { value: Resolved { node: right } } => Present { value: refine_generic_constraint(established: left, incoming: right, span: span, scope: scope) } + _ => none + } + _ => none + } + let payload_diags = match payload_result { Present { value: r } => r.diagnostics Absent => [] } + let diagnostics = concat(concat(flat_map(child_results, r => r.diagnostics), flat_map(param_results, r => r.diagnostics)), payload_diags) + if count(diagnostics) > 0 { + GenericConstraintRefinement { refined: established, diagnostics: diagnostics } + } else { + GenericConstraintRefinement { + refined: Node { + occurrence_identity: established.occurrence_identity, name: established.name, span: established.span, ident_span: established.ident_span, + children: map(child_results, r => r.refined), connective: established.connective, + params: map(param_results, r => r.refined), + inferred: match payload_result { Present { value: r } => Present { value: Resolved { node: r.refined } } Absent => established.inferred }, + return_cardinality: established.return_cardinality, uses: established.uses, body: established.body, transport: established.transport, + properties: established.properties, type_annotation: established.type_annotation, + is_self_recursive: established.is_self_recursive, has_non_tail_self_call: established.has_non_tail_self_call, + match_pattern: established.match_pattern, module_item_kind: established.module_item_kind, expr_data: established.expr_data + }, + diagnostics: [] + } + } + } +} + +fn unify_generics(formal: Node, actual: Node, generic_names: List, source_indices: Map, acc: GenericUnification, span: SourceSpan, scope: InferScope) -> GenericUnification { let bind_name = type_node_label(n: formal, source_indices: source_indices) let f_bare = formal.children |> count == 0 && formal.connective == NoConnective if (f_bare || match formal.inferred { Present { value: TypeVariable { id: _ } } => true _ => false }) && (generic_names |> any(g => g == bind_name)) { - - match map_get(acc, bind_name) { - Absent => map_insert(acc, bind_name, actual) - Present { value: _ } => acc + match map_get(acc.subst, bind_name) { + Absent => GenericUnification { subst: map_insert(acc.subst, bind_name, actual), diagnostics: acc.diagnostics } + Present { value: established } => + let refinement = refine_generic_constraint(established: established, incoming: actual, span: span, scope: scope) + GenericUnification { + subst: map_insert(acc.subst, bind_name, refinement.refined), + diagnostics: concat(acc.diagnostics, refinement.diagnostics) + } } } else if formal.children |> count == 1 && actual.children |> count == 1 { match formal.children |> first { - Present { value: fc } => - match actual.children |> first { - Present { value: ac } => unify_generics(formal: fc, actual: ac, generic_names: generic_names, source_indices: source_indices, acc: acc) - Absent => acc - } + Present { value: fc } => match actual.children |> first { + Present { value: ac } => unify_generics(formal: fc, actual: ac, generic_names: generic_names, source_indices: source_indices, acc: acc, span: span, scope: scope) + Absent => acc + } Absent => acc } } else { acc } @@ -11504,7 +11569,7 @@ fn should_unify_record_lit_generics(formal: Node, arg_expr: Node, generic_names: } } -fn unify_record_lit_field_walk(struct_fields: List, record: Node, generic_names: List, scope: InferScope, acc: Map) -> Map { +fn unify_record_lit_field_walk(struct_fields: List, record: Node, generic_names: List, scope: InferScope, acc: GenericUnification) -> GenericUnification { fold(struct_fields, init: acc, f: (st, sf) => let field_name = authored_name_at(source_indices: scope.type_env.source_indices, node: sf) match record.children |> filter(fi => field_init_node_name_at(n: fi, source_indices: scope.type_env.source_indices) == field_name) |> first { @@ -11518,19 +11583,19 @@ fn unify_record_lit_field_walk(struct_fields: List, record: Node, generic_ Present { value: nested_record } => unify_record_lit_generics(formal: field_formal, record: nested_record, generic_names: generic_names, scope: scope, acc: st) Absent => - unify_generics(formal: field_formal, actual: resolved_type(n: actual_value), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: st) + unify_generics(formal: field_formal, actual: resolved_type(n: actual_value), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: st, span: actual_value.span, scope: scope) } Absent => st } ) } -fn unify_record_lit_generics(formal: Node, record: Node, generic_names: List, scope: InferScope, acc: Map) -> Map { +fn unify_record_lit_generics(formal: Node, record: Node, generic_names: List, scope: InferScope, acc: GenericUnification) -> GenericUnification { if formal.children |> count == 0 { let formal_name = type_node_label(n: formal, source_indices: scope.type_env.source_indices) let is_generic_slot = generic_names |> any(g => g == formal_name) if is_generic_slot { - unify_generics(formal: formal, actual: resolved_type(n: record), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: acc) + unify_generics(formal: formal, actual: resolved_type(n: record), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: acc, span: record.span, scope: scope) } else { match record_lit_expr_optional(expr: record) { Present { value: record_lit } => @@ -11544,10 +11609,10 @@ fn unify_record_lit_generics(formal: Node, record: Node, generic_names: List - unify_generics(formal: formal, actual: resolved_type(n: record), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: acc) + unify_generics(formal: formal, actual: resolved_type(n: record), generic_names: generic_names, source_indices: scope.type_env.source_indices, acc: acc, span: record.span, scope: scope) } } } else { From 34c313568685fec20f9b6b4d0683a646838ec6ed Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:04:01 +0000 Subject: [PATCH 3/8] Record generated-only seed growth and require clean positive controls --- .../empty_collection_constraint_seed_growth.dag | 16 ++++++++++++++++ .../empty_collection_constraint_witness_test.dag | 15 +++++++++++---- src/v1/04_infer.dag | 2 +- 3 files changed, 28 insertions(+), 5 deletions(-) create mode 100644 dag/gunbc/empty_collection_constraint_seed_growth.dag diff --git a/dag/gunbc/empty_collection_constraint_seed_growth.dag b/dag/gunbc/empty_collection_constraint_seed_growth.dag new file mode 100644 index 00000000000..ca4bffb4b78 --- /dev/null +++ b/dag/gunbc/empty_collection_constraint_seed_growth.dag @@ -0,0 +1,16 @@ +module gunbc.empty_collection_constraint_seed_growth + +import gunbc.seed_growth { SeedGrowthJustification } +import gunbc.roadmap_model { RoadmapNodeId } + +// Consumed by review of the PURPOSE-admitted executable seed prerequisite for +// native_lane_universe_after_ownership. The new declarations are authored in +// .dag and their Rust mirrors are generated; the hand-authored Rust roster is +// empty. This receipt does not add an admission exception or a handwritten mirror. +data empty_collection_constraint_seed_growth: SeedGrowthJustification = SeedGrowthJustification { + hand_authored_declarations: [], + reason: "Bounded executable seed maintenance for the self-host program: v1.compiler.infer.GenericUnification carries substitution and diagnostics through every existing caller; GenericConstraintRefinement, generic_constraint_refusal and refine_generic_constraint preserve established constraints while refining unresolved element slots. These declarations are authored in src/v1/04_infer.dag; generated Rust is installed only through regeneration, with no hand-authored Rust declarations added. The native_lane_universe_after_ownership corpus receipt exposes the constraint loss after canonical generic-argument substitution. This row records the source growth, not permission for a new seed admission exception.", + owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, + trigger: "The self-host route derives empty-literal and application-argument substitutions in v2.std.inhabitance, refining concrete argument and callback-result constraints and refusing conflicts before admission; fierce-swift work item adhoc-8760f34f-ec2 owns that v2-side capability. The executable v1 seed rule then leaves with its superseded route. A v2 declaration without execution does not discharge the obligation.", + current_boundary: "v1.compiler.infer GenericUnification, GenericConstraintRefinement, generic_constraint_refusal, refine_generic_constraint; generic pass and every unification consumer, with no compatibility widening or field-deferral change" +} diff --git a/dag/test/claim/empty_collection_constraint_witness_test.dag b/dag/test/claim/empty_collection_constraint_witness_test.dag index cd60ac840bd..71635d00537 100644 --- a/dag/test/claim/empty_collection_constraint_witness_test.dag +++ b/dag/test/claim/empty_collection_constraint_witness_test.dag @@ -2,7 +2,7 @@ module test.claim.empty_collection_constraint_witness import std.types { String, Bool, Int } import v2.std.optional { Present, Absent } -import gunbc.compile_diagnostic_census { CompileDiagnosticCensus } +import gunbc.compile_diagnostic_census { CompileDiagnosticCensus, CensusObserved, CensusNotRunnable, census_blocking_rows, census_total_count } import gunbc.guarantee_probe_corpus { census_blocking_count_for_class } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } @@ -18,22 +18,29 @@ fn callback_inference_error_count(source: String) -> Int { } } +fn callback_compiles_clean(source: String) -> Bool { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count(rows: census_blocking_rows(rows: rows)) == 0 + CensusNotRunnable { cause: _ } => false + } +} + data empty_fold_source: String = "module probe_generic_empty_fold\nimport std.types { Int, List, String }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Module { module: String, declarations: List }\nfn asks(xs: List) -> Int {\n let modules = fold_list(xs: xs, empty: [], cons: fn(acc, m) { list_snoc_item(xs: acc, item: m) })\n fold_list(xs: modules, empty: 0, cons: fn(acc, m) { acc + count(m.declarations) })\n}\n" test fn empty_fold_element_binds() -> Bool { - callback_inference_error_count(source: empty_fold_source) == 0 + callback_compiles_clean(source: empty_fold_source) } data nested_empty_fold_source: String = "module probe_nested_empty_fold\nimport std.types { Int, List, String }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Module { module: String, declarations: List }\ntype Source { modules: List }\nfn modules_for_source(source: Source) -> List { source.modules }\nfn asks(sources: List) -> Int {\n let modules = fold_list(\n xs: sources,\n empty: [],\n cons: fn(acc, source) {\n fold_list(\n xs: modules_for_source(source: source),\n empty: acc,\n cons: fn(inner, m) { list_snoc_item(xs: inner, item: m) }\n )\n }\n )\n fold_list(xs: modules, empty: 0, cons: fn(acc, m) { acc + count(m.declarations) })\n}\n" test fn nested_empty_fold_element_binds() -> Bool { - callback_inference_error_count(source: nested_empty_fold_source) == 0 + callback_compiles_clean(source: nested_empty_fold_source) } data callback_result_element_binds_source: String = "module probe_callback_result\nimport std.types { Int, List }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Element { value: Int }\nfn asks(xs: List) -> Int {\n let elements = fold_list(xs: xs, empty: [], cons: fn(acc, n) { list_snoc_item(xs: acc, item: Element { value: n }) })\n fold_list(xs: elements, empty: 0, cons: fn(acc, e) { acc + e.value })\n}\n" test fn callback_result_element_binds() -> Bool { - callback_inference_error_count(source: callback_result_element_binds_source) == 0 + callback_compiles_clean(source: callback_result_element_binds_source) } data determined_element_missing_field_refuses_source: String = "module probe_callback_result\nimport std.types { Int, List }\nimport v2.std.algebra { fold_list, list_snoc_item }\ntype Element { value: Int }\nfn asks(xs: List) -> Int {\n let elements = fold_list(xs: xs, empty: [], cons: fn(acc, n) { list_snoc_item(xs: acc, item: Element { value: n }) })\n fold_list(xs: elements, empty: 0, cons: fn(acc, e) { acc + e.missing })\n}\n" diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 9d75b1d186d..470ad53516a 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -11474,7 +11474,7 @@ fn refine_generic_constraint(established: Node, incoming: Node, span: SourceSpan if established.return_cardinality != incoming.return_cardinality { generic_constraint_refusal(established: established, span: span, scope: scope) } else if established_variable { - GenericConstraintRefinement { refined: incoming, diagnostics: [] } + GenericConstraintRefinement { refined: if incoming_variable { established } else { incoming }, diagnostics: [] } } else if incoming_variable { GenericConstraintRefinement { refined: established, diagnostics: [] } } else if is_fully_resolved(n: established, source_indices: scope.type_env.source_indices) && is_fully_resolved(n: incoming, source_indices: scope.type_env.source_indices) { From f511bb067201a881c093a10b92cae796ac685196 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:09:29 +0000 Subject: [PATCH 4/8] Refine resolved payloads before accepting matching constraint shapes --- src/v1/04_infer.dag | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 470ad53516a..c862018891d 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -11477,15 +11477,15 @@ fn refine_generic_constraint(established: Node, incoming: Node, span: SourceSpan GenericConstraintRefinement { refined: if incoming_variable { established } else { incoming }, diagnostics: [] } } else if incoming_variable { GenericConstraintRefinement { refined: established, diagnostics: [] } - } else if is_fully_resolved(n: established, source_indices: scope.type_env.source_indices) && is_fully_resolved(n: incoming, source_indices: scope.type_env.source_indices) { - if node_type_equals(left: established, right: incoming, source_indices: scope.type_env.source_indices) { - GenericConstraintRefinement { refined: established, diagnostics: [] } - } else { generic_constraint_refusal(established: established, span: span, scope: scope) } } else if type_node_label(n: established, source_indices: scope.type_env.source_indices) != type_node_label(n: incoming, source_indices: scope.type_env.source_indices) || established.connective != incoming.connective || count(established.children) != count(incoming.children) || count(established.params) != count(incoming.params) { - generic_constraint_refusal(established: established, span: span, scope: scope) + if is_fully_resolved(n: established, source_indices: scope.type_env.source_indices) + && is_fully_resolved(n: incoming, source_indices: scope.type_env.source_indices) + && node_type_equals(left: established, right: incoming, source_indices: scope.type_env.source_indices) { + GenericConstraintRefinement { refined: established, diagnostics: [] } + } else { generic_constraint_refusal(established: established, span: span, scope: scope) } } else { let child_results = established.children |> enumerate |> map(pair => match incoming.children |> skip(pair.first) |> first { From dbbcbde4730287eb112dc7e2fa6a33eb2d51ea23 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:28:54 +0000 Subject: [PATCH 5/8] Regenerate inference mirror for empty collection constraint refinement Source f511bb067201a881c093a10b92cae796ac685196. required-regen --regen-affected-scope selected WholePopulationScope; planned/executed/adjudicated 155, first_generation_equal=false, sole generated-surface drift v1_compiler_infer.rs. Entire candidate src comparison confirms precisely that mirror differs. Candidate-only Cargo.toml is crate-layout output and was not installed. RLIMIT_AS 23622320128 bytes; sampled peak RSS 11275136 KiB. No generated mirror hand edits. --- src/v1/stage0/src/v1_compiler_infer.rs | 482 ++++++++++++++++++++++--- 1 file changed, 427 insertions(+), 55 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 1080dd6fde2..7ad9cc5b5e8 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -6591,7 +6591,7 @@ pub fn borrowed_callable_call_type( gnode: Rc, typed_args: Rc>>, scope: Rc, -) -> Rc { +) -> Rc { { let source_indices = scope.type_env.clone().source_indices.clone(); let base = crate::v1_compiler_infer_types::callable_inferred(gnode.clone()); @@ -6600,7 +6600,10 @@ pub fn borrowed_callable_call_type( source_indices.clone(), ); if ((tp_names.clone().len() as i64) == 0) { - base + Rc::new(GenericConstraintRefinement { + refined: base.clone(), + diagnostics: Rc::new(vec![]), + }) } else { { let value_params = Rc::new({ @@ -6624,8 +6627,11 @@ pub fn borrowed_callable_call_type( .iter() .cloned() .fold( - v1_rt::rc_empty_map::>(), - |acc: Rc>>, pair: (i64, Rc)| { + Rc::new(GenericUnification { + subst: v1_rt::rc_empty_map::>(), + diagnostics: Rc::new(vec![]), + }), + |acc: Rc, pair: (i64, Rc)| { let formal_raw = crate::v1_std_core::param_node_type_expr(pair.1.clone()); let param_name = crate::v1_std_core::authored_name_at( source_indices.clone(), @@ -6664,12 +6670,21 @@ pub fn borrowed_callable_call_type( tp_names.clone(), source_indices.clone(), acc.clone(), + ta.span.clone(), + scope.clone(), ), std::option::Option::None => acc.clone(), } }, ); - substitute_generics(base, subst.clone(), source_indices.clone()) + Rc::new(GenericConstraintRefinement { + refined: substitute_generics( + base.clone(), + subst.subst.clone(), + source_indices.clone(), + ), + diagnostics: subst.diagnostics.clone(), + }) } } } @@ -9190,32 +9205,54 @@ pub fn infer_call_arguments_generic_pass( scope.clone(), expected.clone(), ); - let next_subst = if (is_lambda_expr(crate::v1_std_core::arg_value(a.clone())) - || !has_formal.clone()) - { - st.subst.clone() + let initial_unification = Rc::new(GenericUnification { + subst: st.subst.clone(), + diagnostics: Rc::new(vec![]), + }); + let next_unification = if !has_formal.clone() { + initial_unification.clone() } else { - if should_unify_record_lit_generics( - formal_raw.clone(), - crate::v1_std_core::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(), - ) + if is_lambda_expr(crate::v1_std_core::arg_value(a.clone())) { + match formal_raw.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { + node: result_formal, + .. + }) => unify_generics( + result_formal.clone(), + crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + generic_names.clone(), + scope.type_env.clone().source_indices.clone(), + initial_unification.clone(), + a.span.clone(), + scope.clone(), + ), + _ => initial_unification.clone(), + } } else { - unify_generics( + if should_unify_record_lit_generics( formal_raw.clone(), - crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + crate::v1_std_core::arg_value(a.clone()), generic_names.clone(), scope.type_env.clone().source_indices.clone(), - st.subst.clone(), - ) + ) { + unify_record_lit_generics( + formal_raw.clone(), + ar.typed.clone(), + generic_names.clone(), + scope.clone(), + initial_unification.clone(), + ) + } else { + unify_generics( + formal_raw.clone(), + crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + generic_names.clone(), + scope.type_env.clone().source_indices.clone(), + initial_unification.clone(), + a.span.clone(), + scope.clone(), + ) + } } }; Rc::new(ArgGenericFoldState { @@ -9232,10 +9269,13 @@ pub fn infer_call_arguments_generic_pass( a.span.clone(), a.span.clone(), ), - diagnostics: ar.diagnostics.clone(), + diagnostics: v1_rt::concat( + ar.diagnostics.clone(), + next_unification.diagnostics.clone(), + ), })]), ), - subst: next_subst.clone(), + subst: next_unification.subst.clone(), }) }, ) @@ -11055,15 +11095,24 @@ let global_bare_callable = match type_match.clone() { _ => crate::v1_compiler_infer_lookup::global_bare_callable_node(scope.type_env.clone(), func_name.clone()), }, }; -let resolved_type = match type_match.clone() { - Some(tn) => tn.clone(), +let resolved_call = match type_match.clone() { + Some(tn) => Rc::new(GenericConstraintRefinement { + refined: tn.clone(), + diagnostics: Rc::new(vec![]), +}), std::option::Option::None => match global_bare_callable.clone() { Some(gnode) => if ((gnode.params.clone().len() as i64) > 0) { borrowed_callable_call_type(gnode.clone(), typed_arg_nodes.clone(), scope.clone()) } else { - crate::v1_compiler_infer_types::callable_return_type(gnode.clone()) + Rc::new(GenericConstraintRefinement { + refined: crate::v1_compiler_infer_types::callable_return_type(gnode.clone()), + diagnostics: Rc::new(vec![]), +}) }, - std::option::Option::None => error_type(), + std::option::Option::None => Rc::new(GenericConstraintRefinement { + refined: error_type(), + diagnostics: Rc::new(vec![]), +}), }, }; let call_diags = match type_match.clone() { @@ -11098,9 +11147,9 @@ Rc::new(InferResult { })), descent_evidence: std::option::Option::None, }), typed_arg_nodes.clone(), Some(Rc::new(InferredNode::Resolved { - node: resolved_type.clone(), + node: resolved_call.refined.clone(), })), span.clone(), crate::v1_std_core::node_name_span(texpr.clone())), - diagnostics: v1_rt::concat(arg_diags.clone(), call_diags.clone()), + diagnostics: v1_rt::concat(v1_rt::concat(arg_diags.clone(), call_diags.clone()), resolved_call.diagnostics.clone()), }) }, } @@ -12046,7 +12095,7 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), std::option::Option::None => unit_type(), } } else { - unit_type() + type_variable_node("empty_list_element".to_string()) } } std::option::Option::None => { @@ -12071,11 +12120,15 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), )]), } } else { - Rc::new(vec![inference_error( - "empty list literal: expected type is not a collection".to_string(), - span.clone(), - scope.module_name.clone(), - )]) + match exp.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: _, .. }) => Rc::new(vec![]), + _ => Rc::new(vec![inference_error( + "empty list literal: expected type is not a collection" + .to_string(), + span.clone(), + scope.module_name.clone(), + )]), + } } } std::option::Option::None => Rc::new(vec![]), @@ -20112,13 +20165,301 @@ pub fn param_is_generic_decl( } } +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct GenericUnification { + pub subst: Rc>>, + pub diagnostics: Rc>>, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct GenericConstraintRefinement { + pub refined: Rc, + pub diagnostics: Rc>>, +} + +pub fn generic_constraint_refusal( + established: Rc, + span: Rc, + scope: Rc, +) -> Rc { + Rc::new(GenericConstraintRefinement { + refined: established.clone(), + diagnostics: Rc::new(vec![inference_error( + "conflicting established generic constraints".to_string(), + span.clone(), + scope.module_name.clone(), + )]), + }) +} + +pub fn refine_generic_constraint( + established: Rc, + incoming: Rc, + span: Rc, + scope: Rc, +) -> Rc { + stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || { + let established_variable = match established.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: _, .. }) => true, + _ => false, + }; + let incoming_variable = match incoming.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: _, .. }) => true, + _ => false, + }; + if (established.return_cardinality.clone() != incoming.return_cardinality.clone()) { + generic_constraint_refusal(established.clone(), span.clone(), scope.clone()) + } else { + if established_variable.clone() { + Rc::new(GenericConstraintRefinement { + refined: if incoming_variable.clone() { + established.clone() + } else { + incoming.clone() + }, + diagnostics: Rc::new(vec![]), + }) + } else { + if incoming_variable.clone() { + Rc::new(GenericConstraintRefinement { + refined: established.clone(), + diagnostics: Rc::new(vec![]), + }) + } else { + if ((((type_node_label( + established.clone(), + scope.type_env.clone().source_indices.clone(), + ) != type_node_label( + incoming.clone(), + scope.type_env.clone().source_indices.clone(), + )) || (established.connective.clone() != incoming.connective.clone())) + || ((established.children.clone().len() as i64) + != (incoming.children.clone().len() as i64))) + || ((established.params.clone().len() as i64) + != (incoming.params.clone().len() as i64))) + { + if ((crate::v1_compiler_infer_types::is_fully_resolved( + established.clone(), + scope.type_env.clone().source_indices.clone(), + ) && crate::v1_compiler_infer_types::is_fully_resolved( + incoming.clone(), + scope.type_env.clone().source_indices.clone(), + )) && crate::v1_compiler_infer_types::node_type_equals( + established.clone(), + incoming.clone(), + scope.type_env.clone().source_indices.clone(), + )) { + Rc::new(GenericConstraintRefinement { + refined: established.clone(), + diagnostics: Rc::new(vec![]), + }) + } else { + generic_constraint_refusal( + established.clone(), + span.clone(), + scope.clone(), + ) + } + } else { + { + let child_results = Rc::new({ + let mut __result = Vec::new(); + for pair in Rc::new( + established + .children + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + __result.push( + match incoming + .children + .clone() + .iter() + .cloned() + .skip(pair.0.clone() as usize) + .next() + { + Some(other) => refine_generic_constraint( + pair.1.clone(), + other.clone(), + span.clone(), + scope.clone(), + ), + std::option::Option::None => { + generic_constraint_refusal( + pair.1.clone(), + span.clone(), + scope.clone(), + ) + } + }, + ); + } + __result + }); + let param_results = Rc::new({ + let mut __result = Vec::new(); + for pair in Rc::new( + established + .params + .clone() + .iter() + .cloned() + .enumerate() + .map(|(i, v)| (i as i64, v)) + .collect::>(), + ) + .iter() + .cloned() + { + __result.push( + match incoming + .params + .clone() + .iter() + .cloned() + .skip(pair.0.clone() as usize) + .next() + { + Some(other) => refine_generic_constraint( + pair.1.clone(), + other.clone(), + span.clone(), + scope.clone(), + ), + std::option::Option::None => { + generic_constraint_refusal( + pair.1.clone(), + span.clone(), + scope.clone(), + ) + } + }, + ); + } + __result + }); + let payload_result = + match established.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { node: left, .. }) => { + match incoming.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { + node: right, .. + }) => Some(refine_generic_constraint( + left.clone(), + right.clone(), + span.clone(), + scope.clone(), + )), + _ => std::option::Option::None, + } + } + _ => std::option::Option::None, + }; + let payload_diags = match payload_result.clone() { + Some(r) => r.diagnostics.clone(), + std::option::Option::None => Rc::new(vec![]), + }; + let diagnostics = v1_rt::concat( + v1_rt::concat( + Rc::new({ + let mut __result = Vec::new(); + for r in child_results.iter().cloned() { + __result + .extend((*r.diagnostics.clone()).iter().cloned()); + } + __result + }), + Rc::new({ + let mut __result = Vec::new(); + for r in param_results.iter().cloned() { + __result + .extend((*r.diagnostics.clone()).iter().cloned()); + } + __result + }), + ), + payload_diags.clone(), + ); + if ((diagnostics.clone().len() as i64) > 0) { + Rc::new(GenericConstraintRefinement { + refined: established.clone(), + diagnostics: diagnostics.clone(), + }) + } else { + Rc::new(GenericConstraintRefinement { + refined: Rc::new(Node { + occurrence_identity: established + .occurrence_identity + .clone(), + name: established.name.clone(), + span: established.span.clone(), + ident_span: established.ident_span.clone(), + children: Rc::new({ + let mut __result = Vec::new(); + for r in child_results.iter().cloned() { + __result.push(r.refined.clone()); + } + __result + }), + connective: established.connective.clone(), + params: Rc::new({ + let mut __result = Vec::new(); + for r in param_results.iter().cloned() { + __result.push(r.refined.clone()); + } + __result + }), + inferred: match payload_result.clone() { + Some(r) => Some(Rc::new(InferredNode::Resolved { + node: r.refined.clone(), + })), + std::option::Option::None => { + established.inferred.clone() + } + }, + return_cardinality: established.return_cardinality.clone(), + uses: established.uses.clone(), + body: established.body.clone(), + transport: established.transport.clone(), + properties: established.properties.clone(), + type_annotation: established.type_annotation.clone(), + is_self_recursive: established.is_self_recursive.clone(), + has_non_tail_self_call: established + .has_non_tail_self_call + .clone(), + match_pattern: established.match_pattern.clone(), + module_item_kind: established.module_item_kind.clone(), + expr_data: established.expr_data.clone(), + ident: None, + }), + diagnostics: Rc::new(vec![]), + }) + } + } + } + } + } + } + }) +} + pub fn unify_generics( mut formal: Rc, mut actual: Rc, mut generic_names: Rc>, mut source_indices: Rc>>, - mut acc: Rc>>, -) -> Rc>> { + mut acc: Rc, + mut span: Rc, + mut scope: Rc, +) -> Rc { loop { let bind_name = type_node_label(formal.clone(), source_indices.clone()); let f_bare = (((formal.children.clone().len() as i64) == 0) @@ -20139,12 +20480,35 @@ pub fn unify_generics( __found }) { - match v1_rt::map_get(&acc, bind_name.clone()) { + match v1_rt::map_get(&acc.subst.clone(), bind_name.clone()) { std::option::Option::None => { - break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); + break Rc::new(GenericUnification { + subst: v1_rt::rc_map_insert( + acc.subst.clone(), + bind_name.clone(), + actual.clone(), + ), + diagnostics: acc.diagnostics.clone(), + }); } - Some(_) => { - break acc.clone(); + Some(established) => { + let refinement = refine_generic_constraint( + established.clone(), + actual.clone(), + span.clone(), + scope.clone(), + ); + break Rc::new(GenericUnification { + subst: v1_rt::rc_map_insert( + acc.subst.clone(), + bind_name.clone(), + refinement.refined.clone(), + ), + diagnostics: v1_rt::concat( + acc.diagnostics.clone(), + refinement.diagnostics.clone(), + ), + }); } } } else { @@ -20209,11 +20573,12 @@ pub fn unify_record_lit_field_walk( record: Rc, generic_names: Rc>, scope: Rc, - acc: Rc>>, -) -> Rc>> { - struct_fields.iter().cloned().fold( - acc.clone(), - |st: Rc>>, sf: Rc| { + acc: Rc, +) -> Rc { + struct_fields + .iter() + .cloned() + .fold(acc.clone(), |st: Rc, sf: Rc| { let field_name = crate::v1_std_core::authored_name_at( scope.type_env.clone().source_indices.clone(), sf.clone(), @@ -20254,13 +20619,14 @@ pub fn unify_record_lit_field_walk( generic_names.clone(), scope.type_env.clone().source_indices.clone(), st.clone(), + actual_value.span.clone(), + scope.clone(), ), } } std::option::Option::None => st.clone(), } - }, - ) + }) } pub fn unify_record_lit_generics( @@ -20268,8 +20634,8 @@ pub fn unify_record_lit_generics( record: Rc, generic_names: Rc>, scope: Rc, - acc: Rc>>, -) -> Rc>> { + acc: Rc, +) -> Rc { if ((formal.children.clone().len() as i64) == 0) { { let formal_name = type_node_label( @@ -20293,6 +20659,8 @@ pub fn unify_record_lit_generics( generic_names.clone(), scope.type_env.clone().source_indices.clone(), acc.clone(), + record.span.clone(), + scope.clone(), ) } else { match crate::v1_std_core::record_lit_expr_optional(record.clone()) { @@ -20321,6 +20689,8 @@ pub fn unify_record_lit_generics( generic_names.clone(), scope.type_env.clone().source_indices.clone(), acc.clone(), + record.span.clone(), + scope.clone(), ) } } @@ -20330,6 +20700,8 @@ pub fn unify_record_lit_generics( generic_names.clone(), scope.type_env.clone().source_indices.clone(), acc.clone(), + record.span.clone(), + scope.clone(), ), } } From 3f48550059806faba265d406f95e7d3b30eee9da Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:43:55 +0000 Subject: [PATCH 6/8] Compare refinement constructors through the existing algebra alias projection --- dag/test/claim/empty_collection_constraint_witness_test.dag | 6 ++++++ src/v1/04_infer.dag | 6 ++++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/dag/test/claim/empty_collection_constraint_witness_test.dag b/dag/test/claim/empty_collection_constraint_witness_test.dag index 71635d00537..4cc45d887ce 100644 --- a/dag/test/claim/empty_collection_constraint_witness_test.dag +++ b/dag/test/claim/empty_collection_constraint_witness_test.dag @@ -61,3 +61,9 @@ test fn callback_result_conflict_refuses() -> Bool { callback_inference_error_count(source: callback_result_conflict_refuses_source) >= 1 } + +data collection_alias_callback_source: String = "module probe_collection_alias_callback\nimport std.types { List }\nimport std.algebra { freemonoid_empty }\nimport v2.std.algebra { fold_list, list_snoc_item }\nfn asks(xs: List) -> List {\n fold_list(xs: xs, empty: freemonoid_empty(), cons: fn(acc, item) { list_snoc_item(xs: acc, item: item) })\n}\n" + +test fn collection_alias_callback_result_binds() -> Bool { + callback_compiles_clean(source: collection_alias_callback_source) +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index c862018891d..4b6c394e8ce 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -5,6 +5,8 @@ module v1.compiler.infer // contributes an unresolved element variable, never Unit from an unresolved // non-collection formal. Generic substitution refines unresolved slots using // concrete arguments and callback results; rebinding applies that substitution. +// Constructor comparison consumes infer_types.canonical_template_name, the +// existing declared container-algebra head projection; aliases are not new heads. // Established structure and cardinality remain constraints, and conflicting // established constraints refuse. This rule does not widen compatibility or // permit a field read on a never-constrained enclosing generic. The v2-side @@ -111,7 +113,7 @@ import v1.compiler.infer_types { bare_map_node, bare_set_node, callable_inferred, normalize_access_type_node, - node_type_shape, node_type_compatible, node_type_equals, prefer_specific_type, + node_type_shape, node_type_compatible, node_type_equals, prefer_specific_type, canonical_template_name, is_declared_container_alias_spelling, structural_carrier_template_name, node_type_deps, method_receiver_element_node, @@ -11477,7 +11479,7 @@ fn refine_generic_constraint(established: Node, incoming: Node, span: SourceSpan GenericConstraintRefinement { refined: if incoming_variable { established } else { incoming }, diagnostics: [] } } else if incoming_variable { GenericConstraintRefinement { refined: established, diagnostics: [] } - } else if type_node_label(n: established, source_indices: scope.type_env.source_indices) != type_node_label(n: incoming, source_indices: scope.type_env.source_indices) + } else if canonical_template_name(n: established, source_indices: scope.type_env.source_indices) != canonical_template_name(n: incoming, source_indices: scope.type_env.source_indices) || established.connective != incoming.connective || count(established.children) != count(incoming.children) || count(established.params) != count(incoming.params) { From a5df024f55f8dfff71bc0b52c83460d66f15b824 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:44:52 +0000 Subject: [PATCH 7/8] Bind alias control to the declared freemonoid producer --- dag/test/claim/empty_collection_constraint_witness_test.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/test/claim/empty_collection_constraint_witness_test.dag b/dag/test/claim/empty_collection_constraint_witness_test.dag index 4cc45d887ce..97e44080639 100644 --- a/dag/test/claim/empty_collection_constraint_witness_test.dag +++ b/dag/test/claim/empty_collection_constraint_witness_test.dag @@ -62,7 +62,7 @@ test fn callback_result_conflict_refuses() -> Bool { } -data collection_alias_callback_source: String = "module probe_collection_alias_callback\nimport std.types { List }\nimport std.algebra { freemonoid_empty }\nimport v2.std.algebra { fold_list, list_snoc_item }\nfn asks(xs: List) -> List {\n fold_list(xs: xs, empty: freemonoid_empty(), cons: fn(acc, item) { list_snoc_item(xs: acc, item: item) })\n}\n" +data collection_alias_callback_source: String = "module probe_collection_alias_callback\nimport std.types { List }\nimport v2.std.algebra { fold_list, list_snoc_item, freemonoid_empty }\nfn asks(xs: List) -> List {\n fold_list(xs: xs, empty: freemonoid_empty(), cons: fn(acc, item) { list_snoc_item(xs: acc, item: item) })\n}\n" test fn collection_alias_callback_result_binds() -> Bool { callback_compiles_clean(source: collection_alias_callback_source) From d946695311abe749e34defc556b13ad1daf74cb5 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:58:58 +0000 Subject: [PATCH 8/8] Regenerate refinement mirror with canonical constructor comparison Source a5df024f55f. required-regen --regen-affected-scope: WholePopulationScope; planned/executed/adjudicated 155; sole generated drift v1_compiler_infer.rs. Whole candidate src comparison confirms only this mirror differs; candidate-only Cargo.toml not installed. Elapsed 742.539 seconds, sampled peak RSS 11272528 KiB, RLIMIT_AS 23622320128 bytes. Pre-installation drift receipt, not fixed-point pass; no generated hand edits. --- src/v1/stage0/src/v1_compiler_infer.rs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 7ad9cc5b5e8..211d2535b46 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -204,15 +204,15 @@ pub use crate::v1_compiler_infer_sigs::{ }; pub use crate::v1_compiler_infer_types::KernelTypeBuild; pub use crate::v1_compiler_infer_types::{ - bare_map_node, bare_set_node, callable_inferred, callable_return_type, child_type_node, - emit_map_has, extract_optional_inner_node, for_each_element_type_node, infer_binop_type_node, - infer_literal_node, is_declared_container_alias_spelling, is_fully_resolved, - is_type_expr_annotation, kernel_profile_lookup, make_callable_type, make_container_type, - method_receiver_element_node, node_is_collection, node_is_element_collection, - node_is_keyed_collection, node_is_set_collection, node_type_compatible, node_type_deps, - node_type_equals, node_type_shape, nominal_type_ref, normalize_access_type_node, - prefer_specific_type, resolve_type_variables_from_template, resolved_type, - structural_carrier_template_name, template_return_has_variables, + bare_map_node, bare_set_node, callable_inferred, callable_return_type, canonical_template_name, + child_type_node, emit_map_has, extract_optional_inner_node, for_each_element_type_node, + infer_binop_type_node, infer_literal_node, is_declared_container_alias_spelling, + is_fully_resolved, is_type_expr_annotation, kernel_profile_lookup, make_callable_type, + make_container_type, method_receiver_element_node, node_is_collection, + node_is_element_collection, node_is_keyed_collection, node_is_set_collection, + node_type_compatible, node_type_deps, node_type_equals, node_type_shape, nominal_type_ref, + normalize_access_type_node, prefer_specific_type, resolve_type_variables_from_template, + resolved_type, structural_carrier_template_name, template_return_has_variables, template_return_is_receiver_self, }; pub use crate::v1_compiler_ownership::fold_terminal_expr; @@ -20226,10 +20226,10 @@ pub fn refine_generic_constraint( diagnostics: Rc::new(vec![]), }) } else { - if ((((type_node_label( + if ((((crate::v1_compiler_infer_types::canonical_template_name( established.clone(), scope.type_env.clone().source_indices.clone(), - ) != type_node_label( + ) != crate::v1_compiler_infer_types::canonical_template_name( incoming.clone(), scope.type_env.clone().source_indices.clone(), )) || (established.connective.clone() != incoming.connective.clone()))