Summary

vera check accepts a program that interpolates a String-returning function call into a string literal, but vera compile / vera run emits invalid WASM:

Error: Unhandled WASM trap: failed to compile: wasm[0]::function[N]::main
Caused by:
    0: WebAssembly translation error
    1: Invalid input WebAssembly code at offset NNN: type mismatch: expected i64, found i32

Type-check is silent; the failure surfaces only at the wasmtime validation step, and the error points at the WASM offset rather than the offending source line.

Minimum reproducer

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

private fn make(@Unit -> @String)
  requires(true) ensures(true) effects(pure)
{
  "hello"
}

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

vera check: OK.
vera run: type mismatch: expected i64, found i32 at WASM offset 911.

What works (i.e. narrowing)

-- WORKS: string_concat instead of interpolation
IO.print(string_concat(make(()), "\n"))

-- WORKS: interpolating a slot ref of String type
let @String = "hello";
IO.print("\(@String.0)\n")

-- WORKS: interpolating an Int-returning call
private fn make_int(@Unit -> @Int) ... { 42 }
IO.print("\(make_int(()))\n")

So the trigger is specifically:

1. Expression is a function call (not a slot ref or literal)
2. Return type is String (i32_pair)
3. Used as an interpolation segment inside a string literal

The most likely root cause: the interpolated-string lowering treats the expression as i64 (the to_string path for numerics) without first checking whether it's already a String — for slot refs the type info propagates but for function calls it doesn't, so an i32_pair gets fed into an i64-expecting to_string site.

Discovery context

Surfaced by an agent writing a browser variant of Conway's Life. The agent had the workaround in mind (use string_concat) within minutes, but the path from "vera check passes" to "the WASM offset 4179 is the i64-vs-i32 bug" was opaque — they had to bisect the program by removing constructs until the trap stopped firing.

For an LLM agent the friction is real:

• The error is at run-time, not compile-time, so the standard "fix the diagnostic" loop doesn't engage
• The error message points at WASM bytes, not Vera source
• The diagnostic shape (i64/i32 mismatch) suggests a numeric-conversion bug, which is misleading because the offending expression returns String

Suggested investigation site

vera/wasm/operators.py::_translate_interpolated_string (per calls.py grep — string_concat is the lowering target). Specifically the segment-handling for the Expr parts: probably needs a type dispatch on _infer_expr_wasm_type(part) to choose between "already String, just concat" vs "convert to String via to_string/bool_to_string/etc."

For the diagnostic side: ideally vera check would catch this at type-check time as a codegen-precondition violation, OR the WASM compile error would map back to the source expression via _resolve_trap_frames.

Workaround

Replace "\(call())" with string_concat(call(), ...):

-- before (traps)
IO.print("\(make_state())\n")

-- after (works)
IO.print(string_concat(make_state(), "\n"))

Acceptance

• The minimum reproducer above type-checks AND runs cleanly, OR
• vera check reports a clear diagnostic at the offending interpolation site if the codegen genuinely cannot handle this shape