Wire generic type argument inhabitance

dag/gunbc/spark/serving_realization.dag

@@ -344,6 +344,20 @@ fn list_tail_of(xs: List<ServingRequirementRefusal>) -> List<ServingRequirementR
   }
 }
 
+fn realization_list_head_of(xs: List<SparkServingRealization>) -> SparkServingRealization? {
+  match list_head(xs: xs) {
+    HeadFound { value: v } => Present { value: v }
+    HeadAbsent => none
+  }
+}
+
+fn realization_list_tail_of(xs: List<SparkServingRealization>) -> List<SparkServingRealization> {
+  match list_tail(xs: xs) {
+    TailFound { tail: t } => t
+    TailAbsent => xs
+  }
+}
+
 // ── Normative policy and selection ────────────────────────────────────────────────────────────
 
 // Capabilities and contracts say what is POSSIBLE. They cannot rank two equally capable
@@ -866,15 +880,15 @@ fn select_spark_serving_realization(
       match policy.privilege {
         LeastRequiredEffects => RealizationSelected { realization: best }
         PreferSystemIntegration =>
-          match list_head_of(xs: admitted) {
+          match realization_list_head_of(xs: admitted) {
             Absent => RealizationSelected { realization: best }
             Present { value: head } =>
-              match list_head_of(xs: list_tail_of(xs: admitted)) {
+              match realization_list_head_of(xs: realization_list_tail_of(xs: admitted)) {
                 Absent => RealizationSelected { realization: head }
                 Present { value: second } => RealizationChoiceRequired {
                   first: head,
                   second: second,
-                  more: list_tail_of(xs: list_tail_of(xs: admitted)),
+                  more: realization_list_tail_of(xs: realization_list_tail_of(xs: admitted)),
                   cause: "PreferSystemIntegration does not order equally capable realizations by a modeled fact; the tie is a genuine choice rather than a derivation" as NonEmptyStr,
                 }
               }

dag/test/claim/record_literal_call_arg_handoff_witness_test.dag

@@ -1,6 +1,14 @@
 module test.claim.record_literal_call_arg_handoff_witness
 
+import gunbc.compile_diagnostic_census {
+  CensusObserved,
+  CensusNotRunnable,
+  census_blocking_rows,
+  census_rows_of_class,
+  census_total_count,
+}
 import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import v2.std.algebra { filter }
 
 data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
 
@@ -10,7 +18,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
 // path refused for that shape. Pair 1 (nominal-at-literal): Box at Node param — diagnostics_witness
 // record_literal_field_walls carries it on the production compile path. Pair 2 (resolved-type
 // legacy): warm-fox Cons/FreeMonoid<Node> at inline sole_constructor NormalizedTree in
-// compile_dag_rust_emit_check — the shape main's legacy path refused before the skip. On the
+// compile_dag_diagnostic_census — the shape main's legacy path refused before the skip. On the
 // current base v2.compiler.normalized_tree is still type NormalizedTree = Node, so the same call on
 // the production compile path stays green because it is Node-at-Node, not because the check is
 // complete; when gunbc#8256 lands the sealed carrier (type NormalizedTree sole_constructor { root:
@@ -26,13 +34,17 @@ fn w_nominal_record_at_call_arg_red() -> Bool {
   )
 }
 
-fn w_container_element_record_at_call_arg_red() -> Bool {
-  compile_dag_rust_emit_check(
-    "module warmfox_bl1_prediction\nimport std.algebra { Cons, Empty, FreeMonoid }\nimport v2.std.node { Node, TypeNode, Atom }\nimport std.occurrence_identity { OccurrenceSynthetic }\n\ntype NormalizedTree sole_constructor {\n  root: Node,\n}\n\nfn fc_module_root() -> Node {\n  Node {\n    kind: TypeNode { connective: Atom { identity: ^fc_seg } },\n    children: [],\n    occurrence_id: OccurrenceSynthetic,\n  }\n}\n\nfn fc_single_found_root() -> FreeMonoid<Node> {\n  Cons { head: fc_module_root(), tail: Empty }\n}\n\nfn validate_module_roots(roots: FreeMonoid<NormalizedTree>) -> Bool {\n  true\n}\n\nfn bad_call() -> Bool {\n  validate_module_roots(roots: fc_single_found_root())\n}\n",
-    "src/warmfox_bl1_prediction.rs",
-    [],
-    []
-  )
+data container_element_record_at_call_arg_red_source: String = "module warmfox_bl1_prediction\nimport std.algebra { Cons, Empty, FreeMonoid }\nimport v2.std.node { Node, TypeNode, Atom }\nimport std.occurrence_identity { OccurrenceSynthetic }\n\ntype NormalizedTree sole_constructor {\n  root: Node,\n}\n\nfn fc_module_root() -> Node {\n  Node {\n    kind: TypeNode { connective: Atom { identity: ^fc_seg } },\n    children: [],\n    occurrence_id: OccurrenceSynthetic,\n  }\n}\n\nfn fc_single_found_root() -> FreeMonoid<Node> {\n  Cons { head: fc_module_root(), tail: Empty }\n}\n\nfn validate_module_roots(roots: FreeMonoid<NormalizedTree>) -> Bool {\n  true\n}\n\nfn bad_call() -> Bool {\n  validate_module_roots(roots: fc_single_found_root())\n}\n"
+
+fn generic_type_argument_violation_count(source: String) -> Int {
+  match compile_dag_diagnostic_census(source) {
+    CensusObserved { rows: rows } =>
+      census_total_count(
+        rows: census_rows_of_class(rows: census_blocking_rows(rows: rows), wanted: "DeclaredTypeNotInhabited")
+          |> filter(row => row.subject_name == "generic type argument")
+      )
+    CensusNotRunnable { cause: _ } => 0 - 1
+  }
 }
 
 fn w_nominal_record_at_call_arg_green() -> Bool {
@@ -48,8 +60,11 @@ test fn record_literal_nominal_mismatch_at_call_arg_still_refuses() -> Bool {
   !w_nominal_record_at_call_arg_red()
 }
 
+// Assert the diagnostic's modeled identity and its declared position, not merely refusal. The
+// census projects DeclaredTypeNotInhabited's rendered position into subject_name, so an
+// UnresolvedType, parse error, lookup miss, or any other blocking diagnostic cannot satisfy it.
 test fn record_literal_container_element_mismatch_at_call_arg_still_refuses() -> Bool {
-  !w_container_element_record_at_call_arg_red()
+  generic_type_argument_violation_count(source: container_element_record_at_call_arg_red_source) == 1
 }
 
 test fn record_literal_matching_nominal_at_call_arg_accepts() -> Bool {

src/v1/04_infer.dag

@@ -3029,13 +3029,13 @@ fn foreign_concrete_coproduct_where_parent_required(
 // 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
+// THREE OF THE TWELVE ARE WIRED. THE OTHER NINE 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.
+// Measured by construction site, not by reading: PositionDirectCallArgument,
+// PositionListElement, and PositionGenericTypeArgument are the only three 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 three 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
@@ -3049,14 +3049,13 @@ fn foreign_concrete_coproduct_where_parent_required(
 // 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.
+// and is why the residual nine cost a call each rather than a rule each.
 //
-// THE TEN AWAITING A PRODUCER: PositionRecordLiteralField, PositionMapValue,
+// THE NINE 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
+// PositionCastTarget, PositionParameterDefault, PositionCallableReturn. Wiring any of them is 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
+// carrier's honest claim is THREE POSITIONS JUDGED, nine declared -- and any statement that it
 // judges "every grammar type position" is false.
 type DeclaredTypePosition
   = PositionRecordLiteralField
@@ -3892,6 +3891,7 @@ fn call_argument_selects_formal_index(argument: Node, argument_index: Int, forma
 type CallFormalApplication {
   index: Int
   param_name: String
+  formal_raw: Node
   formal_subst: Node
   formal: Node
   matched_arg: Optional<Node>
@@ -3931,6 +3931,7 @@ fn build_call_application_plan(
       CallFormalApplication {
         index: pair.first,
         param_name: param_name,
+        formal_raw: formal_raw,
         formal_subst: formal_subst,
         formal: peel_nominal_alias_identity(n: formal_subst, env: type_env, module_name: module_name),
         matched_arg: match typed_args |> enumerate |> filter(candidate => call_argument_selects_formal_index(argument: candidate.second, argument_index: candidate.first, formal_index: pair.first, arguments: typed_args, value_params: value_params, source_indices: source_indices)) |> first {
@@ -4009,6 +4010,71 @@ fn direct_call_argument_inhabitance_diags(
   )
 }
 
+// A direct-call obligation over an applied element container reaches the shared relation as the
+// OUTER generic node, where UndecidableGenericFormal is the honest verdict for that outer fact.
+// Its concrete element pair is a separate declared position and used to have no producer at all:
+// List<RightCensoredCost> could therefore inhabit List<ExactCompletionCost> even though both
+// element identities were established. Construct that inner obligation here, at the same matched
+// formal/actual seam, and leave the position-agnostic relation unchanged. Both sides must expose
+// the same applied constructor and arity; a bare, malformed, or different carrier is not this
+// position and produces no fabricated comparison. Every aligned argument gets its own obligation,
+// so this is the generic-argument position rather than a List-specific second relation. A raw
+// generic formal (K/V/T) and an inference placeholder (`element`) do not yet name an identity that
+// this nominal obligation can judge; keep those with the existing outer obligation instead of
+// manufacturing false mismatches from an unresolved substitution.
+fn direct_call_generic_type_argument_inhabitance_diags(
+  plan: List<CallFormalApplication>,
+  scope: InferScope
+) -> List<ErrorNode> {
+  let source_indices = scope.type_env.source_indices
+  flat_map(
+    plan,
+    app =>
+      match app.matched_arg {
+        Present { value: ta } =>
+          let actual_expr = arg_value(n: ta)
+          let actual = resolved_type(n: actual_expr)
+          if exposure_is_application(exposure: exposure_view_for_node(n: app.formal_subst, source_indices: source_indices))
+            && exposure_is_application(exposure: exposure_view_for_node(n: actual, source_indices: source_indices))
+            && (app.formal_subst.children |> count) > 0
+            && (app.formal_subst.children |> count) == (actual.children |> count)
+            && authored_name_at(source_indices: source_indices, node: app.formal_subst)
+              == authored_name_at(source_indices: source_indices, node: actual) {
+            flat_map(
+              app.formal_subst.children |> enumerate,
+              declared_pair =>
+                match app.formal_raw.children |> skip(declared_pair.first) |> first {
+                  Present { value: raw_declared_child } =>
+                    match actual.children |> skip(declared_pair.first) |> first {
+                      Present { value: produced_child } =>
+                        if applied_type_argument_identity_known(
+                            name: authored_name_at(source_indices: source_indices, node: child_type_node(ch: raw_declared_child)), scope: scope)
+                          && applied_type_argument_identity_known(
+                            name: authored_name_at(source_indices: source_indices, node: child_type_node(ch: produced_child)), scope: scope) {
+                          declared_type_obligation_diags(
+                            obligation: DeclaredTypeObligation {
+                              position: PositionGenericTypeArgument,
+                              subject: app.param_name,
+                              declared: peel_nominal_alias_identity(
+                                n: child_type_node(ch: declared_pair.second), env: scope.type_env, module_name: scope.module_name),
+                              produced: peel_nominal_alias_identity(
+                                n: child_type_node(ch: produced_child), env: scope.type_env, module_name: scope.module_name),
+                              span: actual_expr.span
+                            },
+                            scope: scope
+                          )
+                        } else { [] }
+                      Absent => []
+                    }
+                  Absent => []
+                }
+            )
+          } else { [] }
+        Absent => []
+      }
+  )
+}
+
 fn container_element_nominal_brand_mismatch(
   formal: Node,
   actual: Node,
@@ -5891,6 +5957,10 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu
           plan: call_application_plan,
           scope: scope
         )
+        let generic_type_argument_inhabitance_diags = direct_call_generic_type_argument_inhabitance_diags(
+          plan: call_application_plan,
+          scope: scope
+        )
         InferResult {
           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(func_name: func_name, sig_lookup: call_sig_lookup) } }, descent_evidence: none },
@@ -5899,7 +5969,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, concat(structured_arg_diags, inhabitance_arg_diags))))
+          diagnostics: concat(arg_diags, concat(arg_shape_diags, concat(arg_compat_diags, concat(structured_arg_diags, concat(inhabitance_arg_diags, generic_type_argument_inhabitance_diags)))))
         }
       } else {
         let first_arg_type = match typed_args |> first {