Distinct nominal product types silently inhabit a direct-call argument

[gunbai-bot]

DESIGN section 4b floor: "values inhabit declared types". Measured on a
compiler built from this tree, each fixture its own entry compile, every
one of these reported ZERO blocking diagnostics:

Alpha at a Beta parameter distinct constructors
Wrapper at a Wrapper parameter one constructor, distinct
type arguments, K phantom
Alpha at a Beta parameter neither applied, actual a call

THE BRIEF FRAMED THIS AS GENERICS DEFEATING THE CHECK. IT IS NOT. The
third case has no type parameters anywhere and is admitted for the same
reason as the first two, and the case that DID refuse -- Alpha{...} at a
Beta parameter -- refused because its actual is a record LITERAL, not
because it is non-generic. Read off the producers rather than inferred
from the silence: structured_application_site_type_mismatch is the only
judgment that ever compared product heads here and it fires solely for an
ExprRecordLit actual; kernel_value_declared_type_mismatch returns false
at its first gate for a non-kernel actual; coproduct_payload_where_parent
_required leaves its body unless the formal's declaration is a coproduct.
A call actual at a product formal was judged by nothing. Root-cause count:
ONE, and one arm closes all three.

THE ARM lives in declared_type_inhabitance, the single decision procedure,
and consumes v1.compiler.type_head_exposure rather than deriving a second
head view. Two new refusal reasons. Every guard fails open: containers,
callables, optionals, anonymous records, unresolvable names, arity
mismatch and type-variable arguments are all admitted.

node_type_shape now renders an application's arguments. Without it the
type-argument refusal printed declared 'Node(Wrapper)', produced
'Node(Wrapper)' -- typed and located and carrying nothing actionable.

FALSE-POSITIVE CENSUS, because this relation runs on EVERY module: the
direct-call TYPE judgment's v2.* exemption (module_skips_direct_call_arg
_check) does not cover this path. src/v2/compiler/00_compile.dag, the
widest required entry, is 0 blocking / 2167 advisory with the arm on --
byte-identical to the same binary with the arm disabled by env var, a
one-variable A/B rather than two builds. dag/std/abi.dag, src/v1/04_infer
.dag and src/v1/compile.dag are 0 blocking.

TWO CUTS OF THIS ARM PRODUCED 15 FALSE POSITIVES ON THAT ENTRY and both
refutations are recorded in the annotation rather than quietly fixed:
asking whether an argument's NAME resolves in the type environment is not
a type-variable test, because type PARAMETERS are bound there and S and R
answer exactly as KindA does; and the exposure's constructor_identity is
keyed on the REFERENCING file, so one Measure read from two modules
yields two identities and can never establish agreement across modules.
The test that works is that a type variable resolves to nothing.

Five witness arms: three discriminating REDs against the prior compiler
and two anti-refuse-everything controls, all verified by execution. The
enrolled expected-red roster needs no edit -- the peano arm is untouched
by construction (declared_realizes_as_kernel_numeric runs ahead of this
predicate) and measured unchanged.

Co-Authored-By: Claude Opus 5 noreply@anthropic.com

Files

• src/v1/04_infer.dag — the arm in declared_type_inhabitance, two new InhabitanceRefusalReason members, and the guards
• src/v1/04_types.dag — node_type_shape renders an application's arguments
• dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag — three discriminating REDs, two controls
• src/v1/stage0/src/v1_compiler_infer{,_types}.rs — regenerated mirrors (claim_executor --required-regen, not hand-written)

Measurement table

Every refusal is DeclaredTypeNotInhabited at the exact direct-call argument, caret on the actual.

fixture	before	after
Alpha<String> at Beta<String>	0	1 — declared Node(Beta<Primitive(String)>), produced Node(Alpha<Primitive(String)>)
Wrapper<KindB> at Wrapper<KindA> (no brands)	0	1 — declared Node(Wrapper<Product(KindA)>), produced Node(Wrapper<Product(KindB)>)
same, actual a variable not a call	0	1
Alpha at Beta, non-generic, actual a call	0	1
Alpha{...} record literal at Beta	1	2 (pre-existing type mismatch + this arm)
bare "plain" at Beta<String>	1	1 (unchanged)
matching applied type	0	0 (unchanged)
type-variable type argument	0	0 (guard control)

What this does NOT close

• A record LITERAL of a distinct constructor at an APPLIED formal (Alpha { a: "z" } at Beta<String>) is still admitted. That is structured_application_site_type_mismatch's territory — it peels the formal but the literal carries no type arguments — and it is a separate seam with its own evidence, not silently folded in here.
• The arm judges ONE level of type argument. A nested application argument is left unjudged and says so.
• Ten of the twelve DeclaredTypePosition members still have no obligation producer; this changes the relation, not the wiring.