Summary

Codegen's Eq auto-derivation is scalar-rep-based, not structural. _adt_satisfies_eq accepts a field only if its WASM rep is scalar (i64/i32/f64), and _translate_adt_eq compares each field with a scalar .eq. Measured against the documented guideline (Eq is satisfied by primitives — including String — and ADTs whose fields are themselves Eq), this is wrong in both directions:

• False-reject: a String field is i32_pair, so a String-field ADT (e.g. Box<String>) is rejected with E613 even though String satisfies Eq.
• False-accept: a concrete ADT field is an i32 pointer, so it passes the scalar check and is compared with i32.eq — pointer identity, not value. Structurally-equal values with distinct heap pointers compare unequal (and aliased pointers compare equal regardless of value).

Repro (false-reject)

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)
{ let @Box<String> = MkBox("a"); eq2(@Box<String>.0, @Box<String>.0) }

vera compile rejects this with E613 though String is Eq. The false-accept is the dual: an ADT with a concrete nested-ADT field compiles and compares that field by pointer.

Root cause

The Eq check (vera/codegen/monomorphize.py _adt_satisfies_eq) and the eq codegen (vera/wasm/operators.py _translate_adt_eq) both work from WASM reps, not Vera field types. _translate_adt_eq expands the comparison inline and has no String-field path and no nested-ADT recursion.

Proper fix (a feature)

Structural Eq derivation:

• Thread Vera field types into the constructor layout (it stores only (offset, wasm_type) today).
• Generate per-ADT recursive $eq_<ADT> WASM functions (inline expansion can't handle recursive types like List<T>), dispatching per field type: scalar .eq, String byte comparison, nested-ADT recursion, Array/handle → not derivable.
• Update _adt_satisfies_eq to match (recurse into ADT fields, accept String, reject Array/handles).

Current state

#767 added type-argument validation for the type-parameter-field path on the parameterized-name (slot-ref) form, so Box<Int> is accepted and Box<String> rejected consistently with the scalar-only basis. The scalar-only basis itself is unchanged; this issue tracks lifting it to structural.

Related

• Per-monomorphization static verification for generic functions #732 / Per-monomorphization static verification for generic functions (#732) #767 — where both facets were found.
• Eq auto-derivation is type-arg-blind on the constructor-inferred path (false-accepts Box<String>) #772 — the constructor-inferred path's type-arg blindness (a sibling Eq-derivation gap).