Origin: Surfaced during PR #631 review pass while addressing CodeRabbit Findings 1 + 5 — implementing parameterised-alias substitution in the _canonical_named_type walker (vera/wasm/inference.py) closes the canonicaliser half but leaves a parallel gap in _type_expr_to_wasm_type (vera/codegen/core.py).

The pattern

_type_expr_to_wasm_type(te) recurses through type aliases via:

if name in self._type_aliases:
    return self._type_expr_to_wasm_type(self._type_aliases[name])

It looks up the alias body and recurses, but does not consult _type_alias_params to substitute the alias's own type parameters. For non-parameterised aliases this is fine; for parameterised aliases it loses the binding.

Empirical reachability

type Id<T> = T;

private fn make_list(@Unit -> @Id<Array<Int>>)
  requires(true) ensures(true) effects(pure)
{ [10, 20, 30] }

_type_expr_to_wasm_type(NamedType("Id", [Array<Int>])):

1. name = "Id". Look up _type_aliases["Id"] → NamedType("T").
2. Recurse on NamedType("T").
3. name = "T". Not a primitive. Not in _type_aliases. Returns "unsupported".
4. → [E605] Function 'make_list' has unsupported return type — skipped.

The function is dropped from the output, even though Id<Array<Int>> is semantically Array<Int> (and _canonical_named_type post-PR-#631 correctly resolves it).

The case type Box<T> = Array<T> happens to work because the alias body's outer name (Array) hits the bare-name branch in _type_expr_to_wasm_type before the type variable is encountered — coincidental, not load-bearing.

Recommended fix

Mirror the substitution mechanism added in PR #631 to _canonical_named_type:

if name in self._type_aliases:
    alias = self._type_aliases[name]
    alias_params = self._type_alias_params.get(name)
    if (alias_params and te.type_args
            and len(alias_params) == len(te.type_args)):
        local_subst = dict(zip(alias_params, te.type_args))
        alias = self._substitute_type_vars(alias, local_subst)
    return self._type_expr_to_wasm_type(alias)

Requires _substitute_type_vars (currently on InferenceMixin in vera/wasm/inference.py) to be available from CodeGenerator in vera/codegen/core.py — either move to a shared module or duplicate the small helper.

Acceptance test

type Id<T> = T;
private fn make_list(@Unit -> @Id<Array<Int>>) ...  // currently E605

should compile cleanly and run end-to-end.

Relationship to PR #631

PR #631 closed the canonicaliser half of the parameterised-alias gap (_canonical_named_type). This issue tracks the parallel gap in the compilability check (_type_expr_to_wasm_type), which is reached via a different code path (function-decl registration, not interpolation/apply_fn return inference). Together they would close the broader "parameterised aliases work end-to-end on the WASM target" question.

The Box<T> = Array<T> shape works today because of the coincidental Array-bare-name match; the Id<T> = T shape is the canonical reproducer for what's actually broken.