Summary

In a block expression, the pattern helper(...); next_expr where helper is a user-defined function returning @Unit in non-tail position produces invalid WASM. Type-checks cleanly, then vera run fails at WASM instantiation with a stack-balance error.

Surfaces in any IO-effecting program of non-trivial size, because the natural render(grid); IO.sleep(120); recurse(...) shape lands on it the moment render is a user helper rather than a single inline IO.print. Discovered by a sandboxed Claude.ai instance writing Conway's Game of Life — the same session as #583.

Reproducer

effect IO {
  op print(String -> Unit);
}

private fn helper(@Unit -> @Unit)
  requires(true) ensures(true) effects(<IO>)
{
  IO.print("middle ")
}

public fn main(@Unit -> @Unit)
  requires(true) ensures(true) effects(<IO>)
{
  IO.print("start ");
  helper(());
  IO.print("end\n")
}

vera check → OK
vera run:

Error: Unhandled WASM trap: failed to compile: wasm[0]::function[2]::main

Caused by:
    0: WebAssembly translation error
    1: Invalid input WebAssembly code at offset 86: type mismatch:
       expected a type but nothing on stack

Narrowing matrix

So the trigger is specifically: user-defined function returning @Unit, called in a non-tail statement position within a block. Built-in IO.* operations returning Unit work. Returning anything else with a value rep works. Putting the same Unit fn in the tail position works.

Root cause

vera/wasm/context.py::_is_void_expr (line 456) determines whether an expression produces a WASM stack value. For ExprStmts in non-tail position, the surrounding translate_block (line 422-434) emits a drop instruction iff _is_void_expr returns False.

_is_void_expr correctly handles:

• QualifiedCall (e.g. IO.print) — explicitly checked per-qualifier
• UnitLit — explicitly checked
• FnCall to effect ops in self._effect_ops — explicitly checked
• AssertExpr / AssumeExpr — explicitly checked
• Compound expressions (MatchExpr, IfExpr, Block, HandleExpr) — recursive

It does NOT handle:

• FnCall to a user-defined function whose declared return type is Unit

Falls through to return False, caller emits a drop, but the user fn left nothing on the stack → "expected a type but nothing on stack".

Fix sketch

Add a clause to _is_void_expr for ast.FnCall to user-defined functions declared with @Unit return type. The function-return-type registry (self._fn_ret_types, populated in vera/codegen/functions.py:76-80) currently excludes Unit-returning functions (the if ret_wt and ret_wt != "unsupported" filter), so the registry needs to either:

• expand to include Unit-returning functions explicitly (with None as a sentinel and a key-presence check at the lookup site), or
• be supplemented with a separate _unit_returning_fns: set[str] populated alongside.

Either approach is ~5-10 lines. Recursive cases (Unit user fn inside an if / match arm in non-tail position) are already handled by the existing recursive structure of _is_void_expr — once the FnCall base case is right, the compound cases are right by recursion.

Acceptance

• The reproducer above runs cleanly post-fix and prints start middle end.
• New conformance tests in tests/conformance/ covering: user Unit fn in non-tail position; user Unit fn nested inside if/match non-tail; the three-IO.print baseline (which works today and should keep working).
• All existing tests remain green.

Workaround

Until fixed: restructure so user-defined Unit-returning calls are always the final expression of their enclosing block. Two patterns:

1. Fold trailing actions into the helper. Instead of print_rows(grid); IO.print("Generation: ..."), change print_rows to accept the generation number and print the trailing line as its own terminal expression. The recursive helper now ends the surrounding block.
2. Reshape the loop. Replace render(grid); IO.sleep(120); if ... { recurse() } else { () } with a structure where the recursive call is the tail expression of the active branch and the terminal frame's render is the tail of the other branch.

Both are mechanical but distort the natural shape of the code.

Why no test caught this

Every Vera example uses IO.* for IO and _is_void_expr covers QualifiedCall correctly. The shape that breaks — a user-defined helper that wraps an IO.print (or other Unit-returning effect op) and is called mid-block — is a pattern that appears the moment programs grow past trivial size, but the test suite favors flat structures or terminal-position calls. Conway's render-then-sleep-then-recurse loop is the first test of this shape in the codebase.

Adjacent improvement

The error message at WASM instantiation is non-actionable — Invalid input WebAssembly code at offset 86: type mismatch: expected a type but nothing on stack gives the user no hint that the cause is "you called a user Unit fn in non-tail position". Even pre-fix, surfacing a Vera-native diagnostic at compile time when this pattern is detected would close the same verifier-vs-runtime gap that the v0.0.119–v0.0.134 bug-killing campaign worked on.

Out of scope for the primary fix, but worth queueing as a defensive follow-up.