Summary

Type checker accepts a SlotRef of a parameterised FnType alias with fewer type-args than the alias requires, silently passing through to codegen where the bug surfaces as a runtime trap.

Reproducer

type Pair<A, B> = fn(A -> B) effects(pure);

private fn use_map(@Option<Int>, @Pair<Int> -> @Option<Int>)
  requires(true) ensures(true) effects(pure)
{
  option_map(@Option<Int>.0, @Pair<Int>.0)
}

Pair<A, B> is declared with 2 type-args (A, B), but @Pair<Int>.0 supplies only 1. vera check returns OK; vera compile produces option_map$Int_B (literal alias-local name B in suffix); vera run fails with:

Caused by:
    0: WebAssembly translation error
    1: Invalid input WebAssembly code at offset 1058: unknown table 0: table index out of bounds

Root cause

vera/checker/ accepts a SlotRef whose type_name references a parameterised alias without verifying that the supplied type_args count matches the alias's parameter count. The mismatch then flows through:

1. The monomorphizer's _resolve_arg_fn_shape in vera/codegen/monomorphize.py sees len(alias_params) != len(arg.type_args) and falls through to the unsubstituted alias body.
2. _infer_fn_alias_type_args matches the alias body against the param type with the unsubstituted T / B etc. names.
3. The generic's type-vars stay unbound and fall to the "Bool" phantom-var default at _infer_type_args_from_call:300.
4. The mono mangler emits a literal alias-local name in the suffix (option_map$Int_B) and the call site references a non-existent function-table entry.

Why this is a type-checker bug, not a codegen bug

Codegen catches the wrong shape but can't emit a useful diagnostic — there's no source-located information about WHY the alias is being matched incorrectly. The type checker has full visibility:

• The SlotRef's type_args length is known at type-check time.
• The alias's type_alias_params length is known.
• A simple len(a) == len(b) check at SlotRef validation rejects the malformed input with a clear [E1xx] diagnostic.

Investigation context

Surfaced as F3 in the multi-agent review of PR #659 (which fixed the closely-related #604 mono-suffix bug for the correct-arity case). Original reproducer + verification in PR #659 review summary comment.

A defensive comment was added to _resolve_arg_fn_shape in PR #659 documenting the gap. No codegen-side behaviour change was made — the fix belongs upstream.

Acceptance criteria

• vera check rejects @Pair<Int>.0 (where Pair<A, B> is declared with 2 type-args) with a source-located diagnostic
• New error code (e.g. E1xx "alias arity mismatch") added to vera/errors.py
• Unit test in tests/test_checker.py pinning the diagnostic
• The reproducer above fails at vera check rather than at vera run
• Once the type checker rejects, the defensive comment in vera/codegen/monomorphize.py::_resolve_arg_fn_shape and the matching one in vera/wasm/calls.py::_resolve_arg_fn_shape_wasm can be removed (they document a now-impossible path)

References

• PR Fix mono-suffix bug for FnType-alias SlotRef args + release v0.0.145 #659 — fixed the correct-arity SlotRef-FnType-alias bug (Five prelude combinators silently skipped from every WASM compile (option_map / option_and_then / result_map + two _unwrap_or variants) #604)
• This issue tracks the wrong-arity gap PR Fix mono-suffix bug for FnType-alias SlotRef args + release v0.0.145 #659 surfaced but didn't fix.