v2 infer: a parameter containing a type variable inside a constructor is matched and judged, not admitted

[gunbai-bot]

Why

In v2 infer, a call argument at a parameter that contains a type variable inside a constructor (a: List<T>) was accepted whatever the argument's type:

• fn g<T>(a: List<T>, b: List<T>) called as g(1, 2) was accepted.
• g(xs_of_int, xs_of_pair) was accepted too.
• The same callee declared non-generically (fn g(a: List<Int>, b: List<Int>)) refuses g(1, 2).

DESIGN §4b puts "values inhabit declared types" on the compiler floor, so this was a below-floor wall that applied to every generic in v2.

Found while building XL-2 step 1's collection concat route (session/stern-swift-290). That route's refusal controls could not discriminate, because the roster row's signature is generic. calm-boar-904 ruled that this lands first, with concat stacked behind it.

§6b: where it broke

v2.compiler.infer infer_judge_application_argument_instantiating already instantiates a parameter that is a type variable (x: T, the DeclaredTypeVariable arm).

A parameter that only contains one took the DeclaredType arm and went to the declared-position judge as written. v2.std.inhabitance inhabitance_node_undecidable_reason then answered UndecidableGenericFormal, which infer admits with a counted advisory.

The argument's type was derived, so nothing about the call was undecidable. The undecidability came from never instantiating the parameter.

The repair: one matcher, the existing judge

• infer_match_generic_formal matches the parameter type first-order against the argument's derived type:
  • an Instantiation parameter needs an Instantiation argument with the same constructor and arity, and recurses on each pair of arguments;
  • a bare type variable binds its first instance, through the existing TypeVariableInstance list.
• infer_type_instantiated substitutes the bindings into the parameter type. The result goes to the same infer_judge_declared_position every parameter uses, so a variable bound twice to different instances refuses there. No second inhabitance relation is added.
• A constructor or arity mismatch refuses with the judge's own application_argument_does_not_inhabit, located at the application.
• One alias rule, shared by every judgment (review 75435; calm-boar-904 approved option 1). infer_declared_type_obligation is the one producer of a DeclaredTypeObligation in infer. It presents the declared type, the produced type and the produced type's refinement carrier with every transparent alias unfolded (infer_type_alias_normalized). So the plain route and the generic route, and every declared position (argument, return, record field, let annotation, binder default, fold member and carrier), see one type per alias family. v2.std.inhabitance holds no index, so the reading is supplied by the producer, exactly as produced_declared_carrier already was. The generic route's earlier shortcut and its match-time alias arms are deleted: it normalizes both sides once and ends at the same judge.
• What the plain path now admits (stated). An argument whose type is a transparent alias of the declared type, or the reverse, now inhabits it: fn p(a: FreeMonoid<Pair>) accepts a List<Pair>, which it refused before on spelling alone.
• Only transparent aliases unfold (calm-boar-904's constraint). A refinement (where), and a nominal brand (spelled where brand(..), std.types WherePredicateMarker), never unfold (infer_alias_is_refined). So a raw carrier is never admitted where a refined or branded type is declared. Its carrier is reached only by the judge's one-step widening.
• A refined argument matches through its declared carrier (review 75350). The generic match asks the judge's own subsumption fact, refinement_declared_carrier, on a shape mismatch.
• An argument whose type isn't derived binds nothing and stays the counted frontier.
• DFS first (calm-boar-904's condition 1): no existing structural matcher or unifier over TypeVariableInstance exists in infer. infer_match_coproduct_of_type zips declared parameters against a scrutinee's arguments for match, but doesn't match a pattern type against a produced one. This PR reuses its decomposer, infer_type_head_and_args.

Controls (v2.test.claim.compiler.generic_formal_instantiation)

claim_batch ran on this head, then again with src/v2/compiler/04_infer.dag checked out from main, in one remote dispatch:

control	head	main
Int at a List<T> parameter refuses	PASS	FAIL
one T at two instances (List<Int>, List<Pair>) refuses	PASS	FAIL
nested (List<List<T>> binds T=Int, then a Pair at T) refuses	PASS	FAIL
one consistent instance is accepted	PASS	PASS
nested consistent instance is accepted	PASS	PASS
alias: FreeMonoid<T> parameter, List<Pair> arguments, accepted	PASS	PASS
alias: FreeMonoid<T> parameter, List<Pair> and List<Int>, refuses	PASS	FAIL
a where refinement of List<Int> at List<T> matches through its carrier	PASS	PASS
a record wrapping a list refuses at List<T> and at List<Int>	PASS	FAIL
plain FreeMonoid<Pair> parameter takes List<Pair> and refuses List<Int>	PASS	FAIL
a refined Pos still refuses a raw Int, plain and generic	PASS	FAIL
an alias of a refined type keeps the refinement (refuses Int, admits Pos)	PASS	FAIL

claim_batch, remote. The "main" column is the same binary with src/v2/compiler, src/v2/std and src/v2/extdeps checked out from main.

The refusal controls assert the reason application_argument_does_not_inhabit, not merely "not accepted".

Residue, stated

A type variable inside a shape this match doesn't open stays UndecidableGenericFormal, as before:

• an Arrow, e.g. f: fn(T) -> T;
• an optional, e.g. T?;
• a type variable in the head position of a constructor.

The next-rung trigger is in the new failure-mode row, gunbc.recurring_failure_mode generic_formal_containing_a_type_variable_unjudged.

Census of newly admitted sites (calm-boar-904's condition)

Instrument. gunbc test //v2/test/parse/expression_bodied_fn_decl_parse:all (the N7 native route), run before and after:

• before: main 3f5d1154a2, after the v2: kinded type params; type applications checked in exact bijection; de-fork MachineWidth onto std.machine_constraints #13038 revert Revert #13038: main red on 62 lambda/fold claims #13293;
• after: v2: bare concat over lists binds the std.algebra collection roster row and is typed by it (XL-2 step 1) #13207's head eddcb4c5e7, which contains this PR.

The [native-verdict] chains were diffed link by link. Each occurrence was mapped to its file and an offset through [native-context-split] ranges, because occurrence numbers shift between builds.

Result: no infer verdict on any chain flips from refused to accepted. The alias rule newly admits nothing in this population.

The only differences are resolve links:

• main's bare concat refusals in v2.std.node and v2.std.node_query (resolve_reason_unbound_symbol) are gone on the head. v2: bare concat over lists binds the std.algebra collection roster row and is typed by it (XL-2 step 1) #13207's roster route clears them, not this PR.
• The chain then stops at the next wall, a bare count in both files (resolve_unbound_name_is_declared_in_several_modules).

The required floor is also PASS on this head.

Limit, stated. This instrument reports only the chain each test stops on (neat-raven-383), not a verdict for every call site. A full per-site census needs v2 resolve/infer diagnostics over the whole closure, which no existing instrument prints. Within what is observable, the set of newly admitted sites is empty.

Freeze note (sharp-raven-357 amendment)

This PR adds floor_cross_claim_pure_producers_warm rows (#13043 has not landed). Claim identities:

• v2.test.claim.compiler.generic_formal_instantiation.gfi_not_a_list_reason
• v2.test.claim.compiler.generic_formal_instantiation.gfi_two_instances_reason
• v2.test.claim.compiler.generic_formal_instantiation.gfi_nested_mismatch_reason
• v2.test.claim.compiler.generic_formal_instantiation.gfi_one_instance_reason
• v2.test.claim.compiler.generic_formal_instantiation.gfi_nested_agrees_reason
• v2.test.claim.compiler.generic_formal_instantiation.gfi_alias_agrees_reason
• v2.test.claim.compiler.generic_formal_instantiation.gfi_alias_disagrees_reason
• gfi_refined_carrier_reason, gfi_record_wrapper_generic_reason, gfi_record_wrapper_plain_reason
• gfi_plain_alias_agrees_reason, gfi_plain_alias_disagrees_reason, gfi_refined_refuses_raw_plain_reason, gfi_refined_refuses_raw_generic_reason, gfi_alias_of_refined_refuses_raw_reason, gfi_alias_of_refined_admits_refined_reason (same module)

🤖 Generated with Claude Code

[gunbai-bot]

Re review 75350: fixed the refinement-carrier case, but not by routing the mismatch to the judge, because that would reopen the hole this PR closes.

Why not route to the judge. At a shape mismatch, T is still unbound, so the instantiated parameter still mentions a type variable. infer_judge_declared_position then answers UndecidableGenericFormal, which infer admits, so g(1) at List<T> would be accepted again.

What changed. infer_match_generic_formal_or_carrier asks the judge's own subsumption fact on a mismatch: refinement_declared_carrier, one step and never walked. It then retries the match against the declared carrier, and refuses only when neither the argument nor its carrier matches. After a successful carrier match, the instantiated parameter (now concrete) goes to the one judge, which widens the refinement by the same rule.

On the cited case. NonEmptyList<T> = Refined<List<T>>. std.refinement Refined<B> is a record { base: B }, not a where refinement, so refinement_declared_carrier answers Absent for it in the existing judge too. A non-generic fn p(a: List<Int>) already refuses that wrapper, so refusing it at List<T> is the consistent verdict. The new controls pin both halves.

Controls, claim_batch on head / with 04_infer.dag from main:

• gfi_refined_argument_matches_through_its_carrier (type Ns = List<Int> where nonempty at List<T>): PASS on head, PASS on main (main accepted it as undecidable).
• gfi_record_wrapper_refuses_as_the_plain_formal_does (a record wrapping a list, at List<T> and at List<Int>, both refuse): PASS on head, FAIL on main (main admitted the generic one).
• The other 7 controls: unchanged. All PASS on head, and the refusal controls FAIL on main.

[gunbai-bot]

Re review 75435: fixed by option 1, approved by calm-boar-904.

• One alias rule. infer_declared_type_obligation is now the single producer of every DeclaredTypeObligation in infer. It normalizes the declared type, the produced type and the refinement carrier through infer_type_alias_normalized. The plain route and the generic route therefore share one rule.
• Removed. The generic shortcut in infer_judge_generic_formal and the match-time alias arms are deleted.
• Only transparent aliases unfold. Refinements and brands do not (infer_alias_is_refined), per calm-boar-904's constraint.
• Added controls:
  • gfi_plain_formal_takes_its_alias: the plain route accepts the alias and refuses a disagreement;
  • gfi_refined_type_still_refuses_its_raw_carrier: refuses on both routes;
  • gfi_alias_of_a_refined_type_keeps_the_refinement.

All 12 controls PASS on head. On main, every control exercising new behaviour FAILS (table in the PR body). The newly admitted sites from the floor census will be listed in the PR body once CI reports them.