Hold the argument-to-formal rule in one place: inference bound named arguments by position, refusing valid programs

[briansrls]

What this repairs

Which declared formal a call argument binds to was answered in two places with different rules:

authority	rule	drives
build_call_application_plan	name-first, positional fallback	the type check
ExprCall argument fold	position only	expected-type propagation

So a call passing named arguments in a different order than declared inferred each argument against its neighbour's formal, while the type check ran a different rule and reported nothing. The green type check was never evidence against the defect — it was produced by the other authority.

A third path, call_arg_bound_param_at, is not a third authority for this fact and is deliberately left alone. It answers a different question — under which runtime binding key an actual would be stored, for detecting duplicate writes — where a named actual keys on its literal caller label and only unlabeled actuals advance its positional counter. Routing it through the selector would replace a runtime-key question with a formal-identity answer and reintroduce the underscore-shadow false refusal its current form was written to remove.

Two independent symptoms, both measured

Wrong emitted type. src/v1/05_emit.dag calls emit_typed_match_unified with seven named arguments, source_indices ahead of recurse. The recurse lambda was inferred against render_pattern's fn(MatchPattern) -> String.

Fabricated refusal — correct code rejected. take_list(label: "a", xs: []) is valid and main refuses it:

empty list literal: expected type is not a collection

because the [] sits at source position 1 and was handed label: String's formal. DESIGN §5 forbids this as firmly as fabricated success. This is what makes the repair provable without the typed-lambda emission route, and it shows the blast radius reaches any expression whose accepted type consumes the expected input — not only lambdas.

The construction

select_formal_for_call_argument is the rule, held once. The fold consumes it directly; build_call_application_plan consumes it inverted — a formal's argument is the argument that selects that formal's index — so neither side can encode a rule the other does not. It returns the formal's index alongside its node precisely so the inversion needs no second search.

Deliberately pre-type: it reads authored labels only, so it runs before recursive argument inference, call_subst still accumulates in authored source order, and generic unification order is untouched.

The label test is call_param_caller_labels, not exact equality — a parameter declared _ctx is addressable by callers as ctx. It is not call_arg_label_matches_param either: that predicate governs admission and returns true for a bare _ against any label, which is correct for "does this label name a declared parameter" and catastrophic for "which parameter does this label select" — an anonymous parameter would claim the first label it saw.

Both directions of the bijection

The selector alone makes the relation functional (one argument selects one formal). It does not make it injective, and that gap was silent wrongness below the floor:

fn f(_a: Int, b: Int) -> Int { b }
f(a: 1, _a: 2, b: 3)

compiles clean on both compilers and emits f(2, 3) — the argument a: 1 is dropped with no diagnostic anywhere, because a and _a are two caller spellings of one formal and nothing asked whether two arguments had chosen the same one.

formal_identity_duplicate_diags closes it: an argument whose selected formal index was already claimed by an earlier argument is refused.

The two duplicate walls partition by cause. duplicate_label_diags asks whether two arguments produce the same runtime binding key, and catches collisions this selector cannot see. This wall asks whether two arguments select the same semantic formal. They coincide on exactly one input shape — two arguments carrying the same authored label — and there the key wall already owns the refusal, so this wall fires only when the labels differ. Without that guard both fired and f(a: 1, a: 2, b: 3) produced two byte-identical diagnostics (measured). The guard states which wall owns which cause rather than deduplicating output after the fact.

Controls, executed

Both compilers built from committed mirrors; no hand-edited mirror in either binary.

control	main	this PR
out-of-order named args, empty list	refuses (fabricated)	clean
out-of-order underscore alias (f(n: 1, ctx: []) vs fn f(_ctx: List<Int>, n: Int))	refuses (fabricated)	clean
two caller spellings, one formal (f(a: 1, _a: 2, b: 3))	clean — emits f(2, 3), drops an argument	refuses
two anonymous positional slots (keep_first(7, 8, 9))	clean	clean
same label twice (f(a: 1, a: 2, b: 3))	1 diagnostic	1 diagnostic
declaration order	clean	clean, emitted identical
mixed positional+named	clean	clean, emitted identical
named then positional (f(b: 2, 1)) — review 55769	clean	clean (was: fabricated refusal)
unknown label	2 hard	identical, spans included

The anonymous-slot control confirms the historical "every _ is the same key" false refusal is not revived. The same-label control confirms the two walls no longer double-report.

The underscore-alias control is load-bearing for a reason worth recording: an earlier version of the selector used exact name equality, so ctx never matched _ctx and the fabricated refusal survived. An earlier in-order underscore test had passed by luck — the mis-selected argument was an Int literal, which ignores its expected type.

Mixed calls — corrected after review

An earlier revision of this body claimed the divergence between the selector's raw index and call_arg_bound_param_at's running counter was unwritable, on the evidence that a labelled argument preceding an unlabelled one is already refused upstream:

three(1, b: "x", [])  ->  refused by both: "argument 'b' supplied more than once"

That is positional-then-named, and generalising from it to "a labelled argument preceding an unlabelled one" was wrong. The reverse order is accepted, and review 55769 caught that the selector refused it:

fn f(a: Int, b: Int) -> Int { a }
f(b: 2, 1)

Argument 0 claims formal b by name; argument 1 took formal index 1 by raw index — the same formal — and the injectivity wall refused a program main accepts. A fabricated refusal introduced by the change that exists to remove one.

The repair: the positional fallback now selects the k-th formal not claimed by any label in the call, where k counts unlabelled arguments before this one. Computed inside the selector, not by routing through call_arg_bound_param_at — which answers a different question and whose underscore handling must not be disturbed.

The case is enrolled as a regression witness.

Out of scope, and measured so it is not read as closed

Emission ordering for mixed calls is wrong on main and remains wrong here. src/v1/05_emit.dag order_typed_call_args opens with

let has_unnamed = args |> any(arg => arg_name_at(...) == none)
if has_unnamed { args } else { ...reorder by name... }

so if any argument is unlabelled the emitter does no reordering at all and emits source order. Measured on both compilers:

fn f(a: Int, b: Int) -> Int { a }
f(b: 2, 1)
  interpreter -> a == 1    (label-correct)
  emitter     -> f(2, 1)   i.e. a == 2

The emitted program computes a different answer than the interpreted one — below-floor silent wrongness, pre-existing, and a fourth consumer of the argument-to-formal question running its own third rule.

It is not fixed here: its blast radius is corpus-wide call ordering, and this PR's subject is expected-type propagation and the type-check plan. The enrolled witness states in its own note that it covers the source-language half only, so a census cannot read its green as covering mixed calls.

Corpus comparison

Both compilers over src/v1 + dag + src/v2: identical diagnostics (0 blocking, 201 advisory).

One dag-target artifact byte-differs, in item_registry_keys ordering at identical file length. A determinism control — the same compiler run twice — reproduces it (differ: byte 100478390), so it is pre-existing nondeterminism, not attributable to this change, and it is filed separately against the producer rather than normalised away here.

Consequently dag-artifact.json byte equality is an excluded oracle for this PR. Rust mirror file-set and byte equality remain valid on the measured subject, as does diagnostic-set equality.

Bootstrap receipt

main compiler regenerating main      first_generation_equal=true
self-applied compiler built          exit 0
this PR regenerating itself          first_generation_equal=true, 135/135, EXIT=0

The gate is discriminating rather than passing by default: the run immediately before this one reported FAIL generated surface drift: v1_compiler_infer.rs against a stale mirror.

Relationship to #9182

#9182 (B1, Rust lambda annotation) is hard-dependent on this and stays draft. B1 cannot emit a correct type from a malformed typed graph.

[gunbai-bot]

Side-chat ruling log (routed here so it is findable on the PR, not only in chat)

Scope ruling. This stays a standalone prerequisite; #9182 (B1) does not absorb it. P1 is an inference law, not a Rust-emission law; it must survive even if B1 is reverted; and a combined bootstrap would obscure whether a changed mirror came from corrected inference or newly emitted annotations.

Instrument objection, accepted. An earlier measurement used a compiler containing three hand-corrected Rust annotations. Those were not part of the subject, but they were part of the instrument — in a self-hosted experiment that distinction matters. Every measurement now in the PR body was re-taken with compilers built from committed mirrors, no hand edits in either binary.

Subject renamed. The 173-file comparison is the v2 compiler closure, not "whole-corpus emission". The whole-bundle path is a separate subject gated elsewhere; keeping the names apart prevents a trajectory splice.

Census framing. Carry as exact 13 sites at exact head, with mixed named/positional calls excluded and a regex instrument — not a timeless corpus fact. The known-positive control is load-bearing: two earlier census implementations returned plausible populations while being structurally unable to see lambda-bearing calls.

Correction I owe on my own claim. I said the other twelve sites could not change shape because their callees take no callable parameter. That was reasoning past the evidence — a wrong expected formal reaches empty collection literals, record literals, optionals, generics and aliases, none of which need a lambda. The empty-list probe in the PR body is that class executing. Emitted-output delta over those twelve is zero; their typed-graph effects are measured only to that depth.

Open, and deliberately not done here. A third authority (call_arg_bound_param_at) also answers argument-to-parameter binding. It is not routed through the shared selector, because it tracks runtime binding keys rather than formal identity, and consolidating it would change which diagnostic fires on already-refused shapes. That ruling is in flight.

[gunbai-bot]

Confirmed and fixed in 214f919861. The finding is correct and I verified it by execution before changing anything.

fn f(a: Int, b: Int) -> Int { a }
f(b: 2, 1)

main   -> 0 diagnostics
#9192  -> call shape mismatch calling 'f': argument 'b' supplied more than once

A fabricated refusal introduced by the change that exists to remove one. The cause is exactly as diagnosed: the positional fallback used the argument's raw source index, so argument 1 selected formal index 1 — which argument 0 had already claimed by name — and the injectivity wall refused it.

Why it escaped my controls, since that matters more than the fix: I had measured three(1, b: "x", []) — positional-then-named, which is already refused upstream — and generalised to "a labelled argument preceding an unlabelled one is already refused." That generalisation was false, and I never tested the reverse order. The PR body has been corrected rather than quietly patched.

The repair. The positional fallback now selects the k-th formal not claimed by any label in the call, where k counts unlabelled arguments before this one. That running rank is computed inside the selector rather than by routing through call_arg_bound_param_at, per the standing ruling that the two answer different questions — formal identity versus runtime binding key — and that disturbing the latter risks reviving the underscore-shadow false refusal it was written to remove.

Controls, both compilers built from committed mirrors:

control	main	this PR
out-of-order named args	1 (fabricated)	0
out-of-order underscore alias	1 (fabricated)	0
two spellings, one formal	0 (silent, drops an argument)	1 (refuses)
two anonymous positional slots	0	0
same label twice	1	1
named then positional — this review	0	0

The case is enrolled as a regression witness in guarantee_probe_corpus_witness_test.dag.

---

One correction to the review's premise, which makes the finding larger rather than smaller.

The review states the interpreter "correctly binds 1 to a at runtime, while this selector assigns both arguments to b" — implying main is correct and only the selector is wrong. Measured, main is also wrong, in a different consumer:

f(b: 2, 1)
  interpreter -> a == 1     (label-correct)
  emitter     -> f(2, 1)    i.e. a == 2

The emitted program computes a different answer than the interpreted one. src/v1/05_emit.dag order_typed_call_args opens with

let has_unnamed = args |> any(arg => arg_name_at(...) == none)
if has_unnamed { args } else { ...reorder by name... }

so whenever any argument is unlabelled the emitter does no reordering at all and emits source order. That is a fourth consumer of the argument-to-formal question, running its own third rule — below-floor silent wrongness, pre-existing on main, unrelated to the namespace work.

It is not fixed in this PR, deliberately. Its blast radius is corpus-wide call ordering, while this PR's subject is expected-type propagation and the type-check plan. It is recorded in the PR body with the measurement, and the enrolled witness states in its own note that it covers the source-language half only — so neither the PR nor a witness census can be read as having closed it. It has been handed to the lane cataloguing this class as its own row.

Fixed point re-established after the change: regen in flight at time of writing; the prior run refused with FAIL generated surface drift against the stale mirror, so the gate is discriminating rather than passing by default.

— sent from deep-ant-102