Problem

examples/list_ops.vera passes vera check and vera verify but fails at runtime with a WASM compilation error:

Error: Runtime contract violation: failed to compile: wasm[0]::function[2]::length

Caused by:
    WebAssembly translation error
    Invalid input WebAssembly code at offset 189: type mismatch: expected i64 but nothing on stack

Root cause

The length function over a recursive List<T> ADT triggers a WASM type mismatch during wasmtime validation. The error is in the generated WASM — a code path leaves the stack empty where an i64 is expected.

This appears to be a codegen edge case with recursive generic ADTs. The monomorphized length function (operating on List<Int>) likely has a code path in the match expression where the recursive case doesn't properly return a value on the WASM stack.

Reproduction

vera check examples/list_ops.vera    # OK
vera verify examples/list_ops.vera   # OK (with Tier 3 runtime checks)
vera run examples/list_ops.vera --fn test_list  # FAILS

Notes

• The type checker and verifier are correct — the function is well-typed and the contracts are consistent
• This is purely a codegen limitation in the WASM translation layer
• Likely related to how match expressions over recursive ADTs generate WASM block/br_table instructions
• The sum function in the same file would likely have the same issue

Design goal alignment

This is a Goal 2 (correctness) issue — the compiler pipeline should produce valid WASM for all programs that pass type checking. A program that type-checks but crashes at compile time represents a soundness gap in the codegen layer.