Summary

A non-void cross-module call (ModuleCall / QualifiedCall, e.g. vera.math::magnitude(x)) used directly as a constructor argument (a Tuple/ADT field) passes vera check but crashes at codegen:

WAT compilation failed: unknown func: failed to find name `$mkt`

_translate_constructor_call can't infer the WASM type of the argument (_infer_vera_type and _infer_expr_wasm_type both return None for ModuleCall/QualifiedCall), so it raises CodegenSkip; the enclosing function is silently dropped from the module, and any call to it dangles at run time.

This is the non-void sibling of #902. #902 fixed the case where the field argument is Unit-valued (via _is_void_expr); the non-void module-call case is still open.

Minimal repro

vera/math.vera = the standard conformance math module (exports magnitude(@Int -> @Int), non-void). main.vera:

import vera.math(magnitude);

private fn mkt(@Int -> @Tuple<Int, Int>)
  requires(true) ensures(true) effects(pure)
{ Tuple(vera.math::magnitude(@Int.0), 9) }

public fn main(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  let @Tuple<Int, Int> = mkt(-5);
  match @Tuple<Int, Int>.0 { Tuple(@Int, @Int) -> @Int.1 }
}

$ vera check main.vera     # OK
$ vera run main.vera       # WAT compilation failed: unknown func: failed to find name `$mkt`

Isolation (what is and isn't affected)

Expected

vera run prints 9 (the tuple's second field). Either the constructor-argument WASM-type inference resolves the callee's declared return type for ModuleCall/QualifiedCall (as it already does for same-file calls), or — parity with #902 — the field is laid out from the resolved return type rather than skipped.

Root-cause pointer

vera/wasm/data.py _translate_constructor_call: the per-argument WASM-type resolution has no case for ModuleCall/QualifiedCall, so it falls through to CodegenSkip. The #902 fix added _is_void_expr handling for the Unit case; the general non-void case needs the callee's declared return type resolved (via the resolver / imported-fn signature) and mapped to its WASM representation, mirroring how a same-file FnCall field argument is already handled.

Scope

Confirmed on release/v0.1.0 (post-#903 merge 505e113). The affected code path predates the v0.1.0 burndown, so this is pre-existing on main as well. Distinct from #904 (where-in-generic). Fix is a separate PR into release/v0.1.0 per the burndown plan; must land before v0.1.0's "No known bugs." claim.