Summary

A generic constrained forall<T where Eq<T>> is accepted when called with a value whose type is inferred from a constructor — e.g. eq2(MkBox("a"), …) — even when the concrete type isn't Eq-derivable (here Box<String>, because String is an i32_pair field, not scalar-Eq). The generated equality then compares the wrong representation (the string pointer, not the value) at run time. This is a false-accept (a soundness gap), not a spurious rejection.

Current state (post-#767)

#767 made _adt_satisfies_eq validate type arguments — but only on the parameterized-name path:

• A slot reference carries the full type: let @Box<String> = MkBox("a"); eq2(@Box<String>.0, …) passes Box<String> to the Eq check, which splits base + args and correctly rejects it (E613). Box<Int> is accepted.
• A constructor inference resolves to the bare ADT name: eq2(MkBox("a"), …) infers the constrained type var as Box (no args), because the monomorphizer's _infer_vera_type_name returns ctor_to_adt.get(name) for a ConstructorCall. That bare name is correct for clone naming (the ADT is a uniform pointer, so one g$Box clone serves all Box<T>), but it leaves _adt_satisfies_eq("Box") with no type args to validate → it false-accepts Box<String>.

Repro

public data Box<T> { MkBox(T) }

private forall<T where Eq<T>> fn eq2(@T, @T -> @Bool)
  requires(true) ensures(true) effects(pure) { @T.1 == @T.0 }

public fn main(@Unit -> @Bool)
  requires(true) ensures(true) effects(pure)
{ eq2(MkBox("a"), MkBox("a")) }   -- compiles; should be E613 (String is not Eq-derivable as a field)

The slot-ref form of the same program (let @Box<String> = MkBox("a"); eq2(@Box<String>.0, @Box<String>.0)) is correctly rejected after #767.

Root cause

The ability check (_check_constraints → _adt_satisfies_eq in vera/codegen/monomorphize.py) receives the constrained type var's name from the monomorphizer's type-arg inference, which drops type args for a ConstructorCall (returns the bare ADT name). That's correct for cloning; lossy for the Eq check.

Why this is deferred (the fix is broad)

Closing it means giving the Eq check the concrete type args on the constructor path. Both routes are meaningfully larger than the slot-ref fix:

1. Make the constraint-var inference carry the parameterized name (Box<String>) — but _infer_vera_type_name is the shared monomorphizer inference; changing it would alter discovery, clone mangling, and emitted WAT for every constructor-inferred generic instantiation, not just Eq-constrained ones.
2. Thread the original call's argument types to the constraint-check site separately — a new data path into _check_constraints.

Either risks the byte-identical-WAT surface and the discovery / differential invariants, so it was out of scope for #767's slot-ref fix.

Pre-existing

The bare-name constructor inference and the type-arg-blind Eq check both predate #732. #767 fixed the parameterized-name half; this is the residue.

Related

• Per-monomorphization static verification for generic functions #732 / Per-monomorphization static verification for generic functions (#732) #767 — the per-monomorphization verification PR, where the slot-ref half was fixed and this was found.
• Monomorphizer type-inference / reindex completeness gaps (nested unify, builtin-return table, scope-aware De Bruijn) #769 — monomorphizer type-inference completeness gaps (same family: inference dropping precision a downstream consumer needs).