Summary

Defining a nested type alias chain (e.g. type Row = Array<Int>; type Grid = Array<Row>;) and then performing a 2D index through the alias inside a user function silently skips that function from WASM codegen. vera check accepts the program; vera run fails with a misleading WAT compilation failed: unknown func: $caller pointing at callers of the skipped function rather than the function that was actually skipped.

Replacing the alias chain with the fully-expanded type (Array<Array<Int>>) at every use site makes the same code compile and run correctly.

Minimal repro (10 lines)

type Row = Array<Int>;
type Grid = Array<Row>;

public fn main(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  let @Grid = [[10]];
  array_length(@Grid.0[0])
}

$ vera check repro.vera
OK: repro.vera

$ vera run repro.vera --fn main
Error: No exported functions to call.
...
Compilation notes:
  - Function 'main' body contains unsupported expressions — skipped.

(vera run does at least surface the skip in the "Compilation notes" footer when main itself is the skipped function. When the skip is on a private helper that main calls, the error is much harder to read — see "Misleading error" below.)

What works (control)

Removing the alias layer and writing the same expression with the expanded type:

public fn main(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  let @Array<Array<Int>> = [[10]];
  array_length(@Array<Array<Int>>.0[0])
}

This compiles and prints 1.

A single-level alias (one layer of aliasing) appears to work in some shapes — the failures I have observed all involve alias-of-alias where the outer alias wraps an inner alias's type via Array<...>.

Misleading error when the skip is on a helper

In the original 200-line program (a Conway's Game of Life implementation), the skip happened on a private helper cell_alive(@Grid, @Int, @Int -> @Int) whose body did @Grid.0[@Int.1][@Int.0] and array_length(@Grid.0[@Int.1]). The diagnostic was:

Error at file.vera, line 0, column 0:

  WAT compilation failed: unknown func: failed to find name `$cell_alive`
       --> <anon>:24:10
        |
     24 |     call $cell_alive
        |          ^

This points at the calling function live_neighbors (line 24 of the WAT, not the source) and names the missing symbol $cell_alive, but says nothing about why $cell_alive is missing. The reader has to know the implicit rule "missing $X symbol = X was silently skipped from codegen" to even know where to look. There were no Compilation notes printed in this case (multi-function program, error during WAT-stage compilation).

A user encountering this for the first time will look for cell_alive, see it defined in the source, and have no path forward. Two suggestions:

1. Always print the skip footer, including when vera run fails at the WAT stage. Move the "Compilation notes" footer earlier in the output — or repeat it — so it's visible whenever any function was skipped.
2. Make unknown func: $X errors look up X in the skipped-functions list and surface a single-line hint: ($X was silently skipped during codegen — see "Compilation notes" above for why).

Hypothesis (offered for triage; please disregard if wrong)

Either:

• The codegen pass that translates @T.n references where T is a nested-alias does not unfold the alias chain before checking whether the resulting access pattern is supported, so it falls into the "unsupported expression" bucket and silently drops the function; OR
• The expression-supportedness check examines the display name of the type (Grid) rather than the resolved structural type (Array<Array<Int>>), and lookup of supported operations is keyed by the unresolved display.

A targeted fix would be to fully resolve all type aliases in a pre-codegen pass and have downstream codegen see only the expanded form.

Why it matters

The natural way to write any 2D-grid algorithm — Game of Life, image processing, board games, matrix ops — is to introduce type Row = Array<T>; type Grid = Array<Row>; for readability. The Best Practices section of SKILL.md does not warn against this; the array-literals example in SKILL.md (let @Array<Array<Int>> = [[1, 2], [3, 4]];) implicitly suggests aliasing would be fine. As written, every such program will compile-check, look correct, and then fail at WASM emission with an error that does not name the actual cause.

(Encountered while writing a Conway's Game of Life implementation. Workaround: I expanded Grid/Row to Array<Array<Int>>/Array<Int> everywhere — adds visual noise but works and is the only thing that did.)

Environment

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