Summary

Calling any user-defined function whose return type is @Unit in statement position (followed by ;, with a separate final expression) traps vera run with WebAssembly translation error: type mismatch: expected a type but nothing on stack. vera check and vera verify both pass cleanly — the error only surfaces at WASM compile time.

The same call works when written as the block's final expression. Built-in IO.print (which also returns @Unit) is not affected, even in statement position.

Minimal repro (13 lines, no IO, no ADTs, no String)

private fn pure_helper(@Nat -> @Unit)
  requires(true) ensures(true) effects(pure)
{
  ()
}

public fn main(@Unit -> @Unit)
  requires(true) ensures(true) effects(<IO>)
{
  pure_helper(1);
  ()
}

$ vera check repro.vera
OK: repro.vera

$ vera run repro.vera --fn main
Error: Unhandled WASM trap: failed to compile: wasm[0]::function[1]::main

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

What works (control)

Replace pure_helper(1); with the call as the final expression and it compiles & runs:

public fn main(@Unit -> @Unit)
  requires(true) ensures(true) effects(<IO>)
{
  pure_helper(1)        -- no `;`, no trailing `()`
}

A built-in Unit-returning call as a statement also works:

public fn main(@Unit -> @Unit)
  requires(true) ensures(true) effects(<IO>)
{
  IO.print("hi");       -- statement form is fine for builtins
  ()
}

Hypothesis (offered for triage; please disregard if wrong)

The codegen path for user-defined function calls in statement position seems to leave the Unit return value on the WASM stack (no drop), while the path for built-in IO.* operations either returns nothing or drops correctly. The next expression () then pushes a value the verifier didn't expect to find a slot for, surfacing as "expected a type but nothing on stack" once the function epilogue runs. A targeted check would be: emit drop after every statement-position call whose return type is Unit (or non-Never), regardless of whether the callee is built-in or user-defined.

Why it matters

The natural pattern for breaking a main function into helpers is:

helper_a();
helper_b();
helper_c();
()

Right now this requires every helper to be inlined into main or chained as (((helper_a(); helper_b()); helper_c()))-style nesting, which defeats the point. SKILL.md's own "Best Practices" section recommends extracting helpers to control De Bruijn slot complexity, so this bug bites exactly the workflow Vera asks agents to follow. (Encountered while writing a 250-line λ-calculus interpreter; tried to factor a report(@String, @Term, @Nat -> @Unit) helper out of main; everything check'd and verify'd cleanly but main then refused to compile to WASM.)

Environment

• Vera v0.0.127 (editable install from aallan/vera@main)
• Python 3.14.3, macOS 25.4 (arm64)
• wasmtime-44.0.0