Summary

Type aliases over Array<T> (and likely other pair-typed values like String) compile cleanly through vera check but break at WASM codegen. Two distinct failure modes depending on where the alias is used.

Discovered while a sandboxed Claude.ai instance was writing Conway's Game of Life and used type Row = Array<Bool>; as a natural domain abstraction. The agent isolated the root cause through stepwise narrowing.

Reproducer 1 — alias as parameter type → invalid WAT

type Row = Array<Bool>;

private fn row_len(@Row -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  array_length(@Row.0)
}

public fn main(@Unit -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  let @Array<Bool> = [true, false, true];
  row_len(@Array<Bool>.0)
}

vera check → OK
vera run → fails at WASM instantiation:

WebAssembly translation error
Invalid input WebAssembly code at offset 879:
  type mismatch: expected a type but nothing on stack

Reproducer 2 — alias in let binding → silent E602 skip

type Row = Array<Bool>;

public fn main(@Unit -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  let @Row = [true, false, true];
  array_length(@Row.0)
}

vera check → OK
vera run → "No exported functions to call" because main was silently skipped with E602 ("body contains unsupported expressions"). The user-facing error is misleading because it precedes the Compilation notes section that contains the actual diagnostic, and that section is also dominated by the harmless prelude-generic skips that fire on every Vera program.

Root cause (sketch)

Type aliases are resolved by the type-checker but the alias-to-target mapping doesn't fully propagate to the WASM codegen layer. When codegen encounters @Row (slot ref) or @Row (parameter binding), the type lookup either:

• fails to resolve Row to its underlying Array<Bool> representation → translator returns None → function gets E602'd (let-binding case), or
• partially resolves but loses the pair-type-ness needed for Array<Bool> → emits a slot-load WAT sequence that produces type-stack imbalance (parameter case).

Likely sites: vera/wasm/helpers.py::_type_name_to_wasm_type (or similar) doesn't handle alias resolution; vera/wasm/inference.py slot-type lookup doesn't follow aliases; the parameter-binding emit in vera/codegen/functions.py lowers each param via type-name-to-WASM-type without checking the alias table.

Workarounds

Until this is fixed, agents writing Vera should avoid type aliases over pair-typed values:

• Array<T> directly instead of type Row = Array<Bool>.
• Array<Array<Bool>> directly instead of type Grid = Array<Row>.
• Other pair types (String) likely affected too; not yet tested.

Type aliases over single-pointer ADTs (Option<Int>, Result<T, E>, user data types) are believed to work but should be tested as part of the fix.

Acceptance

• Both reproducers above run cleanly post-fix.
• New conformance tests in tests/conformance/ covering type-alias-over-Array<T> in parameter, let-binding, and return-type positions.
• Optional: also cover String aliases and nested cases (type Grid = Array<Row>).

Adjacent improvement (worth scoping but optional)

When codegen E602-skips a monomorphic user function (as opposed to a generic prelude declaration), the failure mode is currently silent — vera run later reports "no exported functions" or "unknown func" with no link back to the compile-time warning. Consider:

• Promoting E602/E604 from warning to error when the function is monomorphic (i.e. has no forall<T> parameters) — these are actionable bugs, not the harmless prelude-generic skip pattern.
• Tracking the specific expression that failed translation, not just the function-level summary.

These are separable from the alias fix and could land independently.