Refine empty collection constraints through generic callback results

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"
+}

dag/test/claim/empty_collection_constraint_witness_test.dag

@@ -0,0 +1,69 @@
+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, 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 }
+
+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
+  }
+}
+
+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<String> }\nfn asks(xs: List<Module>) -> 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_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<String> }\ntype Source { modules: List<Module> }\nfn modules_for_source(source: Source) -> List<Module> { source.modules }\nfn asks(sources: List<Source>) -> 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_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>) -> 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_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>) -> 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<T>(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>) -> 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
+}
+
+
+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<T>(xs: List<T>) -> List<T> {\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)
+}