Type-argument arity is unchecked in BOTH directions in alias_chain_type_arg_subst — a floor-band bijection failure where correct and incorrect compile identically

dag/test/claim/type_argument_arity_witness_test.dag

@@ -0,0 +1,92 @@
+module test.claim.type_argument_arity_witness
+
+import std.types { String, Bool, Int, List }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import tools.multi_module_compile_fixture {
+  MultiModuleCompileFixture,
+  MultiModuleCompileFixtureOutcome,
+  FixtureInstrumentRefused,
+  FixtureCompileRefused,
+  FixtureCompileCompleted,
+  FixtureSource,
+  fixture_source,
+  compile_fixture,
+  fixture_blocking_rows,
+  fixture_has_class
+}
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+// THE SUBJECT. v1.compiler.infer alias_chain_type_arg_subst folded a generic declaration's
+// PARAMETERS against a use site's supplied TYPE ARGUMENTS positionally and absorbed a
+// disagreement in BOTH directions: a surplus argument was never read, and a missing argument
+// left its parameter unsubstituted so the expanded record kept a type-variable field. Neither
+// state produced a diagnostic anywhere, so a correct application and an arity-wrong one
+// compiled identically -- the floor band's exact-bijection rule failing silently, which
+// DESIGN section 4b calls a below-baseline safety regression rather than a missing feature.
+//
+// The one call site that noticed widened a `lossy` flag that stood the field-presence wall
+// DOWN instead of refusing -- the absorbing fallback of DESIGN section 5, whose deficit
+// frequency is zero by construction. That flag is deleted with this wall (section 4b(4)
+// dissolution on climb: the proof replaces the degradation rather than accumulating beside it),
+// and the evidence that the higher rung is real is exactly the two REDs and the control below.
+//
+// WHY THE ISOLATED FIXTURE. The RED is an invalid program, so it is authorable only where a
+// fixture hands source to the compiler -- never in the accepted corpus. A single module
+// expresses the whole subject, but tools.multi_module_compile_fixture is used rather than the
+// live-tree census because it compiles a caller-authored manifest in isolation, which is what
+// lets this witness declare SubstrateInputsOnly truthfully and therefore actually execute on
+// the required floor.
+
+
+data surplus_source: String = "module ta.entry\ntype TaBoxed<T> { item: T }\ntype TaPair<A, B> { left: A, right: B }\nfn ta_surplus(b: TaBoxed<Int, String>) -> Int { b.item }\n"
+data deficit_source: String = "module ta.entry\ntype TaBoxed<T> { item: T }\ntype TaPair<A, B> { left: A, right: B }\nfn ta_deficit(p: TaPair<Int>) -> Int { p.left }\n"
+data green_source: String = "module ta.entry\ntype TaBoxed<T> { item: T }\ntype TaPair<A, B> { left: A, right: B }\nfn ta_one(b: TaBoxed<Int>) -> Int { b.item }\nfn ta_two(p: TaPair<Int, String>) -> Int { p.left }\n"
+
+fn arity_run(source: String) -> MultiModuleCompileFixtureOutcome {
+  compile_fixture(MultiModuleCompileFixture {
+    sources: [fixture_source("ta/entry.dag", source)],
+    entry: "ta/entry.dag"
+  })
+}
+
+fn refused_with_class(o: MultiModuleCompileFixtureOutcome, wanted: String) -> Bool {
+  match o {
+    FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
+      fixture_has_class(rows, wanted) && count(fixture_blocking_rows(rows)) > 0,
+    FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false,
+    FixtureInstrumentRefused { cause: c } => false
+  }
+}
+
+fn completed_with_no_diagnostics(o: MultiModuleCompileFixtureOutcome) -> Bool {
+  match o {
+    FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
+      count(rows) == 0 && count(files) > 0 && n > 0,
+    FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false,
+    FixtureInstrumentRefused { cause: c } => false
+  }
+}
+
+// DISCRIMINATING RED, DIRECTION ONE: more type arguments than the declaration has parameters.
+// The class name is asserted, not merely "something refused" -- a typo in the fixture source
+// would satisfy the weaker reading.
+test fn surplus_type_argument_refuses() -> Bool {
+  refused_with_class(arity_run(surplus_source), "TypeArgumentArityMismatch")
+}
+
+// DISCRIMINATING RED, DIRECTION TWO: fewer type arguments than parameters. Authored separately
+// from the surplus arm because the two absorbed through DIFFERENT mechanisms -- the surplus
+// argument was never read, the missing one left a parameter unsubstituted -- so one arm is not
+// evidence about the other.
+test fn deficit_type_argument_refuses() -> Bool {
+  refused_with_class(arity_run(deficit_source), "TypeArgumentArityMismatch")
+}
+
+// THE POSITIVE CONTROL. The same declarations applied at their declared arity compile clean --
+// zero diagnostics of ANY severity. Without this the REDs above are satisfied by a wall that
+// refuses every generic application.
+test fn matched_type_argument_arity_compiles_clean() -> Bool {
+  completed_with_no_diagnostics(arity_run(green_source))
+    && !refused_with_class(arity_run(green_source), "TypeArgumentArityMismatch")
+}

src/v1/04_infer.dag

@@ -39,6 +39,7 @@ import v1.std.core {
   FrontierOccurrenceKey, diagnostic_frontier_occurrence_key,
   InternalError, TypeMismatch, VariantCollision, SoleConstructorViolation, OptionalCastNotEliminated, BareNoneNotAdmittedByFieldType, ConstructorCallAdmissionRefused, UnresolvedType, FieldNotFound, MethodNotFound, MethodExistenceUndecided, MethodExistenceFrontierAdmitted, ReceiverTypeUnestablished, FrontierOccurrenceBudgetExceeded, MissingField, AmbiguousReference, ServiceConfigReferenceJudgmentDeferred, UnlistedVariantValueUse,
   CallArgumentNameUnknown, CallPositionalSurplus, CallPositionalDeficit, CallNamedArgOnFunctionValue, CallArgumentDuplicate,
+  TypeArgumentArityMismatch,
   resource_use_name_at, resource_use_resource,
   is_child_accessor_in_model, is_tree_size_reducing, is_property_contraction,
   expr_has_self_call, expr_has_non_tail_self_call,
@@ -6009,31 +6010,68 @@ fn alias_chain_generic_decl(env: TypeEnv, carrier: Node, target: Node) -> Node {
   else { resolve_generic_use_decl(env: env, n: carrier) }
 }
 
-fn alias_chain_type_arg_subst(env: TypeEnv, carrier: Node, target: Node, type_args: List<Node>) -> Map<String, Node> {
+data alias_chain_type_arg_arity_note: String = "WHY THIS SEAM REFUSES INSTEAD OF SUBSTITUTING WHAT FITS (DESIGN sec 5, the absorbing fallback; sec 4b floor band 'applications bind in exact bijection'). alias_chain_type_arg_subst folded the DECLARED parameters against the SUPPLIED type arguments positionally and absorbed every disagreement in both directions at once: with fewer arguments than parameters the fold's Absent arm left the surplus parameters unsubstituted, so the expanded record kept type-variable fields and field access on it was judged against a hole; with more arguments than parameters the surplus arguments were simply never read. Neither state produced a diagnostic, so `Alias<Int>` and `Alias<Int, String>` against a one-parameter Alias compiled identically -- correct and incorrect indistinguishable at the floor band. One of the three call sites did notice: expand_alias_chain_for_field_access computed `dropped_args` at its recursion seam and widened `lossy`, which is the absorbing fallback in its purest form -- the failure arm stood the field-presence wall DOWN rather than refusing, so the deficit's frequency was zero by construction and nothing ranked it for repair. The other two call sites (alias_chain_target_after_args, and the record branch's re-substitution over an unresolved-parameter field) did not check at all. The repair is construction before validation: the subst is now Optional and has NO spelling for a partial map, so a mismatch cannot be handed downstream by any caller; and alias_chain_arity_diagnostics states the refusal ONCE, typed and located, at the seam that owns both the declaration and the application. SCOPE, stated rather than implied: the refused population is exactly the state `dropped_args` already computed -- both counts nonzero and unequal -- so this wall adds no refusal to a shape the code was not already treating as wrong, and a zero-parameter declaration or a zero-argument use is untouched. Container spellings are excluded because their arity has its own authority (container_expected_arity) and its own diagnostic. AND THE CARRIER MUST BE A USE-SITE LEAF, which is the qualification the first cut of this wall omitted and CI refused it for -- correctly, and the refusal is recorded here rather than quietly patched out. alias_chain_carrier answers the authored node only when it is NoConnective and named; otherwise it answers structural_from_expanded_type, whose children are the record's FIELDS or the coproduct's VARIANTS, not type arguments at all. Reading those as arguments made the check compare a declaration's field count against its parameter count, so `type Medium<R> { carried: R  fidelity: DecodeFidelity }` reported 'two type arguments supplied, one type parameter declared' at its own declaration -- 2460 diagnostics over 154 sites and 65 type names across dag/ and src/v2/, none of them a use site and none of them wrong source. The predicate therefore requires connective == NoConnective, which is exactly the branch where children ARE the applied arguments, and is the same position the deleted dropped_args occupied. WHY THIS WAS NOT CAUGHT BEFORE PUSHING: the corpus control was run with a compiler built BEFORE the change, so it exercised nothing and its zero was a fact about the old binary. A control that cannot flip is not a control."
+
+fn alias_chain_type_arg_arity_mismatch(carrier: Node, decl: Node, type_args: List<Node>) -> Bool {
+  let declared = decl.params |> count
+  let supplied = type_args |> count
+  carrier.connective == NoConnective && declared > 0 && supplied > 0 && declared != supplied
+}
+
+fn alias_chain_type_arg_subst(env: TypeEnv, carrier: Node, target: Node, type_args: List<Node>) -> Map<String, Node>? {
   let decl = alias_chain_generic_decl(env: env, carrier: carrier, target: target)
-  fold(decl.params |> enumerate, init: empty_map(), f: (acc, pair) =>
-    let slot = generic_param_name_at(n: pair.second, source_indices: env.source_indices)
-    match type_args |> skip(pair.first) |> first {
-      Present { value: arg } => map_insert(acc, slot, resolve_scrutinee_type_node(env: env, n: arg))
-      Absent => acc
+  if alias_chain_type_arg_arity_mismatch(carrier: carrier, decl: decl, type_args: type_args) { none }
+  else {
+    Present { value: fold(decl.params |> enumerate, init: empty_map(), f: (acc, pair) =>
+      let slot = generic_param_name_at(n: pair.second, source_indices: env.source_indices)
+      match type_args |> skip(pair.first) |> first {
+        Present { value: arg } => map_insert(acc, slot, resolve_scrutinee_type_node(env: env, n: arg))
+        Absent => acc
+      }
+    ) }
+  }
+}
+
+fn alias_chain_arity_diagnostics(carrier: Node, carrier_name: String, env: TypeEnv, module_name: String) -> List<ErrorNode> {
+  let type_args = carrier.children
+  if carrier_name == "" || (type_args |> count) == 0 || is_container_type(name: carrier_name) { [] }
+  else {
+    match lookup_type_by_name(env: env, name: carrier_name) {
+      Present { value: target } =>
+        let decl = alias_chain_generic_decl(env: env, carrier: carrier, target: target)
+        if alias_chain_type_arg_arity_mismatch(carrier: carrier, decl: decl, type_args: type_args) {
+          [make_error_node(
+            diagnostic: TypeArgumentArityMismatch {
+              type_name: carrier_name,
+              supplied: type_args |> count,
+              declared: decl.params |> count,
+              span: carrier.span
+            },
+            module_name: module_name
+          )]
+        } else { [] }
+      Absent => []
     }
-  )
+  }
 }
 
 fn alias_chain_target_after_args(target: Node, carrier: Node, env: TypeEnv) -> Node {
   let type_args = carrier.children
   if type_args |> count == 0 { target }
   else {
     let decl = alias_chain_generic_decl(env: env, carrier: carrier, target: target)
-    let subst = alias_chain_type_arg_subst(env: env, carrier: carrier, target: target, type_args: type_args)
-    let is_parameterized_alias = decl.inferred != none && decl.children |> count == 0 && decl.connective == NoConnective
-    if is_parameterized_alias {
-      match decl.inferred {
-        Present { value: Resolved { node: alias_body } } => substitute_generics(n: alias_body, subst: subst, source_indices: env.source_indices)
-        _ => target
-      }
-    } else {
-      substitute_generics(n: decl, subst: subst, source_indices: env.source_indices)
+    match alias_chain_type_arg_subst(env: env, carrier: carrier, target: target, type_args: type_args) {
+      Absent => target
+      Present { value: subst } =>
+        let is_parameterized_alias = decl.inferred != none && decl.children |> count == 0 && decl.connective == NoConnective
+        if is_parameterized_alias {
+          match decl.inferred {
+            Present { value: Resolved { node: alias_body } } => substitute_generics(n: alias_body, subst: subst, source_indices: env.source_indices)
+            _ => target
+          }
+        } else {
+          substitute_generics(n: decl, subst: subst, source_indices: env.source_indices)
+        }
     }
   }
 }
@@ -6043,7 +6081,7 @@ fn alias_chain_carrier(n: Node) -> Node {
   else { structural_from_expanded_type(normed: n) }
 }
 
-fn expand_alias_chain_for_field_access(n: Node, env: TypeEnv, module_name: String, origin_name: String, seen: Map<String, Bool>, lossy: Bool) -> NodeResolveResult {
+fn expand_alias_chain_for_field_access(n: Node, env: TypeEnv, module_name: String, seen: Map<String, Bool>) -> NodeResolveResult {
   let peel_result = if needs_alias_field_expansion(n: n, env: env) {
     peel_alias_once_for_field_access(n: n, env: env, module_name: module_name)
   } else {
@@ -6052,53 +6090,49 @@ fn expand_alias_chain_for_field_access(n: Node, env: TypeEnv, module_name: Strin
   let peeled = peel_result.resolved
   let carrier = alias_chain_carrier(n: peeled)
   let carrier_name = if carrier.name != "" { carrier.name } else { authored_name_at(source_indices: env.source_indices, node: carrier) }
+  let own_diags = concat(peel_result.diagnostics, alias_chain_arity_diagnostics(carrier: carrier, carrier_name: carrier_name, env: env, module_name: module_name))
   let structural = structural_from_expanded_type(normed: resolve_scrutinee_type_node(env: env, n: peeled))
   let is_record = structural.connective == Conj || structural.connective == Disj
   if is_record {
     let resolved_record = if record_has_unresolved_param_field(record: structural, env: env) && (carrier.children |> count) > 0 && carrier_name != "" {
       match lookup_type_by_name(env: env, name: carrier_name) {
         Present { value: target } =>
-          let subst = alias_chain_type_arg_subst(env: env, carrier: carrier, target: target, type_args: carrier.children)
-          substitute_generics(n: structural, subst: subst, source_indices: env.source_indices)
+          match alias_chain_type_arg_subst(env: env, carrier: carrier, target: target, type_args: carrier.children) {
+            Present { value: subst } => substitute_generics(n: structural, subst: subst, source_indices: env.source_indices)
+            Absent => structural
+          }
         Absent => structural
       }
     } else { structural }
-    let fail_closed = lossy && record_has_unresolved_param_field(record: resolved_record, env: env)
-    if fail_closed {
-      NodeResolveResult { resolved: nominal_type_ref(name: origin_name), diagnostics: peel_result.diagnostics }
-    } else { NodeResolveResult { resolved: resolved_record, diagnostics: peel_result.diagnostics } }
+    NodeResolveResult { resolved: resolved_record, diagnostics: own_diags }
   } else {
     let next_name = carrier_name
 
     let is_optional = structural.return_cardinality == CardOptional
     if is_optional {
-      let expanded_inner = expand_alias_chain_for_field_access(n: with_required_cardinality(n: structural), env: env, module_name: module_name, origin_name: origin_name, seen: seen, lossy: lossy)
+      let expanded_inner = expand_alias_chain_for_field_access(n: with_required_cardinality(n: structural), env: env, module_name: module_name, seen: seen)
       NodeResolveResult {
         resolved: with_optional_cardinality(n: expanded_inner.resolved),
-        diagnostics: concat(peel_result.diagnostics, expanded_inner.diagnostics)
+        diagnostics: concat(own_diags, expanded_inner.diagnostics)
       }
     } else {
     let stop = next_name == "" || emit_map_has(m: seen, key: next_name)
     if stop {
-      NodeResolveResult { resolved: structural, diagnostics: peel_result.diagnostics }
+      NodeResolveResult { resolved: structural, diagnostics: own_diags }
     } else {
       match lookup_type_by_name(env: env, name: next_name) {
         Present { value: target } =>
           let next_seen = map_insert(seen, next_name, true)
           let type_arg_count = carrier.children |> count
-          let decl = alias_chain_generic_decl(env: env, carrier: carrier, target: target)
-          let param_count = decl.params |> count
-          let dropped_args = type_arg_count > 0 && param_count > 0 && param_count != type_arg_count
-          let next_lossy = lossy || dropped_args
-          let next_n = if type_arg_count > 0 && !dropped_args {
+          let next_n = if type_arg_count > 0 {
             alias_chain_target_after_args(target: target, carrier: carrier, env: env)
           } else { target }
-          let expanded_next = expand_alias_chain_for_field_access(n: next_n, env: env, module_name: module_name, origin_name: origin_name, seen: next_seen, lossy: next_lossy)
+          let expanded_next = expand_alias_chain_for_field_access(n: next_n, env: env, module_name: module_name, seen: next_seen)
           NodeResolveResult {
             resolved: expanded_next.resolved,
-            diagnostics: concat(peel_result.diagnostics, expanded_next.diagnostics)
+            diagnostics: concat(own_diags, expanded_next.diagnostics)
           }
-        Absent => NodeResolveResult { resolved: structural, diagnostics: peel_result.diagnostics }
+        Absent => NodeResolveResult { resolved: structural, diagnostics: own_diags }
       }
     }
     }
@@ -6109,8 +6143,7 @@ fn expand_type_for_field_access_with_seen(n: Node, env: TypeEnv, module_name: St
   if is_deferred_field_access_base(n: n, env: env) {
     NodeResolveResult { resolved: n, diagnostics: [] }
   } else {
-    let origin_name = authored_name_at(source_indices: env.source_indices, node: n)
-    expand_alias_chain_for_field_access(n: n, env: env, module_name: module_name, origin_name: origin_name, seen: seen, lossy: false)
+    expand_alias_chain_for_field_access(n: n, env: env, module_name: module_name, seen: seen)
   }
 }
 

src/v1/stage0/src/cli_run.rs

@@ -5599,6 +5599,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc<ErrorNode>) -> (String, Str
         CompilerDiagnostic::CallPositionalDeficit { .. } => "CallPositionalDeficit",
         CompilerDiagnostic::CallArgumentDuplicate { .. } => "CallArgumentDuplicate",
         CompilerDiagnostic::CallNamedArgOnFunctionValue { .. } => "CallNamedArgOnFunctionValue",
+        CompilerDiagnostic::TypeArgumentArityMismatch { .. } => "TypeArgumentArityMismatch",
         CompilerDiagnostic::OccurrenceTransportViolation { .. } => "OccurrenceTransportViolation",
         CompilerDiagnostic::SourceAnnotationRefused { .. } => "SourceAnnotationRefused",
         CompilerDiagnostic::ContainerSpellingUnrecognized { .. } => "ContainerSpellingUnrecognized",
@@ -5663,6 +5664,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc<ErrorNode>) -> (String, Str
         CompilerDiagnostic::CallPositionalDeficit { parameter, .. } => parameter.clone(),
         CompilerDiagnostic::CallArgumentDuplicate { argument, .. } => argument.clone(),
         CompilerDiagnostic::CallNamedArgOnFunctionValue { argument, .. } => argument.clone(),
+        CompilerDiagnostic::TypeArgumentArityMismatch { type_name, .. } => type_name.clone(),
         CompilerDiagnostic::OccurrenceTransportViolation { .. } => {
             "(occurrence-transport-refusal)".to_string()
         }