v0.1.5

aallan released this 17 Jul 14:20

1a38bcd

Added

Release documentation-consistency sweep. The spec's §9.3/§9.4 Map-key and Set-element lists no longer offer Unit (contradicting §2.2.2's E135 zero-size rejection), and SKILL's Map/Set sections state the E135 constraint; SKILL's conformance count is re-anchored to check_doc_counts.py (the gate's regex had silently stopped matching a reworded sentence, letting the count drift 18 stale — the re-anchored pattern is mutation-validated); FAQ leads with the PyPI install route and carries live test/example counts plus the <Diverge> effect; TOOLCHAIN drops stale release-relative claims; CONTRIBUTING's release checklist names every check_version_sync.py surface including README and the unconditional uv.lock regen.
The veralang distribution ships to production PyPI (#737), through the approval-gated Trusted Publishing workflow, and the installation documentation carries both routes with an accurate account of what each installs: python -m pip install veralang (LSP extra: "veralang[lsp]") delivers the compiler and the vera command only, while the GitHub source checkout additionally provides the bundled examples, the conformance suite, and the specification — so the source route is the recommended default in the agent-facing docs (SKILL.md, the FAQ) whose teaching material lives in the checkout, and the PyPI route leads on the toolchain-oriented surfaces (PYPI_README, the site's install section). The distribution is named veralang; the installed command remains vera and Python code imports vera — pip install vera is an unrelated PyPI project and is never the right command.
check_doc_counts.py gates the README project-status test count (PR #1088 review). The README's "N tests" figure in the Project status section matched none of the oracle's README patterns, so it had silently drifted hundreds of tests stale; a new anchored pattern locks it to the live collection count, mutation-validated (a stale figure fails the gate).
Approval-gated, tokenless release automation (#481) turns a strictly increasing version on main into one tested wheel/sdist artifact, publishes that exact artifact through PyPI Trusted Publishing, verifies registry filenames and SHA-256 hashes, then creates the immutable tag and GitHub Release. A separate manual TestPyPI path stages the current version; a guarded recovery path cannot overwrite a published version or bypass package changes. Build, OIDC publication, registry verification, and GitHub release privileges remain separate jobs, and release policy now forbids tag-moving/fold-in releases after publication.
PyPI publication readiness (#737) renames the Python distribution to veralang while preserving the vera command and import package, adds a dedicated registry README, and gates the built sdist/wheel contents plus an installed-wheel CLI smoke test in CI. The existing GitHub-source installation path remains supported; the first live production package remains the completion gate for #737.
Inference + JSON composition example (#379) demonstrates an effectful model call flowing through pure JSON parsing, typed integer extraction, and a statically proved 0–100 normalization contract. Raw JSON and tagged or untagged fenced responses are accepted, with the original completion retained in malformed-response diagnostics.

Fixed

A mismatch diagnostic renders a leaked type variable as ?, not a bare letter (#1069). A refinement alias over a generic container — type M = { @Map<String, Int> | ... } — read through an element derivation inference cannot thread (map_values(@M.0)[0]) leaves the built-in's value-type variable unsubstituted; the mismatch message then stripped its internal #b namespacing marker (#970/#982) down to a bare V that reads as a real type (body has type V, expected Int). Such a leaked internal placeholder — a namespaced built-in var or a fresh inference hole — now renders as the unknown marker ? (body has type ?, expected Int) at the actual-type slot of every reachable type-mismatch message — the subsumption sites (function body [E121], let value [E170], anonymous-function body [E171], constructor field [E213], effect- and ability-operation argument [E204]/[E241], apply_fn argument [E202], Ord-operation operand [E242], handler state initial value / with update [E331]/[E335]), the operator/index/interpolation family (arithmetic operands [E140], equality and ordering comparison [E142]/[E143], logical operands [E144]/[E145], unary ! and - [E146]/[E147], string-interpolation part [E148], array index [E160], non-indexable collection [E161]), assert/assume arguments [E172]/[E173], if condition and branch types [E300]/[E301] (description and fix text), and the contract and refinement predicates (requires [E123], ensures [E124], refinement [E126]) — recursing into type arguments (Array<?>) and into a function type's effect row (effects(<State<?>>); pretty_effect renders each effect instance's type arguments, so an unscrubbed row would surface the same bare letter). The handful of actual-type renders a leaked placeholder provably cannot reach keep plain pretty_type: the numeric-join [E141] and ordering-compatibility [E142] arms (operands proven numeric/orderable first), match-arm unification [E302] (is_subtype accepts a TypeVar arm), the Eq-ability operand message (contains_typevar early-return), apply_fn's arity message (the value is proven a function type), and the data-invariant message (invariant in data is grammar-rejected, #686). The change is message text only: what the checker accepts or rejects is unchanged, a genuine user forall var (plain T) keeps its own spelling, and a built-in's unsubstituted expected signature (Array<T>) is deliberately left untouched.
A fn-typed slot works as the closure argument to array_map / array_mapi (#1056). array_map([1, 2, 3], @Mapper.0) — where type Mapper = fn(Int -> Int); and @Mapper.0 is a let-bound or parameter slot — was check-green but dropped the enclosing function via [E602] ("could not infer array_map closure return type"), while an inline fn(...) { ... } at the same position compiled and apply_fn over the identical slot already resolved fine. The map emission inferred the output element type only from an inline AnonFn; it now routes through the same _closure_arg_return_type resolver apply_fn uses, recovering the return type from the slot's FnType alias signature (including a type-changing Int -> String mapper, whose output element type must come from the slot rather than the input array) and emitting the call_indirect exactly as for an inline closure. The shared inference also covers array_mapi and the array_fold accumulator.
A self-referential type alias through a type argument is rejected at check time (E132) (#1059). type F = Future<F>;, the mutual type A = Future<B>; type B = Future<A>;, and type L = Array<L>; were all admitted by vera check — the #648 cyclic-alias walk followed only bare type A = B references and never descended into a generic's type arguments — and then either crashed code generation with an unguarded RecursionError in _type_expr_to_wasm_type (the Future spellings, whose type argument the WAT-type mapper recurses through) or compiled to a degenerate type inhabited only by [] (Array<L>). The cycle detector now walks the full alias-reference graph, descending into every type_arg and RefinementType base while excluding a generic alias's own type parameters, so every such previously-admitted self-referential alias is now the same [E132] Cyclic type alias diagnostic the direct type A = B; type B = A cycle already produced. The rule is structural — a self-reference inside a type argument the generic alias discards (type Wrap<T> = Int; type C = Wrap<C>;) is rejected on the same rule, and the edge set covers arbitrarily nested type arguments (type A = Future<Array<B>>; type B = A;). Function-type parameter/return positions are exempt (type FA = fn(FA -> Int) effects(pure); registers — a function value is a table-index indirection, the same exemption data ADTs get; spec §2.6.3 now says so). The cycle walk runs on an explicit stack, so a thousand-alias legal chain checks clean instead of crashing the checker with a RecursionError (PR #1066 review). A legal acyclic nesting (type A = Future<Int>; type B = Future<A>;) still checks.
Container builtins over alias-spelled or user-fn arguments emit with the right host tag (#1063). The Map/Set builtins' emission inference (map_keys / map_values / map_get / set_to_array) fell through to the "b" (i32) host-import tag — the empty-collection escape hatch — for the same aliased and user-fn argument spellings, and returned silently WRONG values on a check-green, verify-green program (i64 values truncated to their low 32 bits, String keys garbled; pre-existing on main, reproduced there before fixing; #1055's aliased index pins passed over it only by fresh-heap luck). All three container inference helpers now consult the shared rebuilder first, with values above 2^32 pinning the tags; the genuinely-unknown empty-collection shape keeps its permissive fall-through, also pinned.
An alias to a Future (type FA = Future<Option<Int>>;) compiles at the match-scrutinee and constructor-argument sites (#1054). The alias spelling was check- and verify-green but E602-skipped where the direct spelling compiled: the SlotRef/ResultRef WAT-type mapper resolved the slot name through the name-only base-name hop (dropping the alias's type arguments) and its Future-transparency arm guarded on AST type arguments an alias-spelled ref does not carry. The mapper now canonicalizes an alias to its target's full compound spelling first (the #1037 walk) and adds the string-form Future arm its sibling scalar mapper carries — the alias analog of #1046, closing the last mapper in the family without the canonicalizer. Found by this PR's adversarial review.
Indexing directly on a builtin call result compiles (#1048). array_concat([1, 2], [3, 4])[2] — a subscript applied straight to a builtin call, for any element type — was check-green but dropped the enclosing function via [E602], while the let-bound form (let @Array<Int> = array_concat(...); @Array<Int>.0[2]) compiled. _infer_index_element_type_expr's FnCall arm resolved only user-function returns (the _fn_ret_type_exprs registry holds no builtins), so element-type inference returned None and the function was skipped. The arm now recovers a builtin call's return NamedType through the same _get_arg_type_info_wasm consultor the sibling Vera-type inference and instantiation discovery use — arg-forwarding for array_concat/array_append/array_slice/array_filter and the _BUILTIN_PARAMETERIZED_RETURNS table for the concrete-Array builtins (array_range, string_split, json_keys, …) — then extracts the element type exactly as the user-function path does; chained indexing through a nested Array<Array<T>> result resolves too. Builtins whose element is a type variable (array_map/array_mapi/array_flatten) stay absent from that consultor and still route through the let-bound form.
Alias-spelled container arguments to the element-type derivations canonicalize (#1055). map_values(@M.0)[0] via type M = Map<String, Int>; (and set_to_array via a Set alias) E602-dropped where the direct spelling compiled: the argument reached the #1051 derivations as its bare alias name with no type arguments, so the class arms never saw the container shape. The shared argument-type rebuilder now canonicalizes a bare alias name to its target's full compound spelling (the #1037 walk) before parsing. The array builtins with aliased arguments (array_flatten(@Grid.0)) additionally drop earlier, in the builtin's call emission — that alias extension rides #1053.
Indexing directly on a type-variable-element builtin call result compiles (#1051, the type-variable follow-up to #1048). The eight Array-returning builtins whose element type depends on the call's arguments — array_reverse, array_sort_by, array_flatten, map_keys, map_values, set_to_array, array_map, array_mapi — were check-green but dropped the enclosing function via [E602] when indexed directly (array_reverse([10, 20, 30])[0]), while the let-bound form (let @Array<Int> = array_reverse(...); @Array<Int>.0[0]) compiled. They are deliberately absent from the shared _get_arg_type_info_wasm consultor #1048 reuses — _BUILTIN_PARAMETERIZED_RETURNS is registry-locked to type-variable-free returns (a TypeVar-carrying entry would bind a phantom var in clone-name discovery, rejected by test_parameterized_table_matches_registry) — so _builtin_call_ret_named_type now derives their return NamedType from the call's arguments, per mechanism class: argument-forwarding (array_reverse/array_sort_by return arg0's type verbatim, array_flatten unwraps one Array<> layer), container-arg-derived (map_keys/map_values/set_to_array read K/V/T off the Map/Set argument), and closure-return-derived (array_map/array_mapi take the element from the closure argument's declared return type). The derivation stays off the shared consultor, so clone-name discovery is untouched; a genuinely unresolvable argument shape (e.g. a nested type-variable-element builtin, whose call already fails to emit) keeps the loud [E602] skip.
array_flatten of an inline nested array literal compiles (#1052). array_flatten([[10, 20], [30, 40]]) — a nested array literal passed straight as a call argument — was check-green but dropped the enclosing function via [E602] ("could not recover inner element type for array_flatten"), while the let-bound-argument form (let @Array<Array<Int>> = [[..], [..]]; array_flatten(@Array<Array<Int>>.0)) compiled. _translate_array_flatten recovered the inner element type T only from a SlotRef @Array<Array<T>> argument; an inline literal fell through to the loud skip. T is now taken from the inner literal's element type through the same _infer_array_element_type recovery a nested literal in a let position already uses; the Array<String> inner variant resolves too. An empty inline literal (array_flatten([])) carries no element type and still keeps the loud skip.
A type-variable-element builtin nested as another builtin's call argument compiles (#1053, the call-emission sibling of #1051). array_reverse(array_flatten(x)) — a type-variable-element Array builtin passed straight as another combinator's argument — was check-green but dropped the enclosing function via [E602] ("could not infer array_reverse element type"), even fully let-bound. The outer combinator's element-type probe (_infer_concat_elem_type) dropped the inner <T> layer of a SlotRef @Array<Array<T>> (it returned the bare Array), so the inner array_flatten could not be unwrapped; inference now falls back to the shared #1051 _builtin_call_ret_named_type derivation and reads back the element name, so array_reverse/array_sort_by of an inner array_flatten resolve. The converse nesting — a builtin call as array_flatten's own argument (array_flatten(array_map(xs, |x| [..]))) — recovers T the same way in _translate_array_flatten. Consultor-resolvable inner calls (array_reverse(array_concat(a, b))) and typevar-in-typevar (array_reverse(array_reverse(x))) already worked; a genuinely unresolvable inner call keeps the loud [E602] skip. Three more call-argument spellings ride the same fix: an alias-spelled array argument (type Grid = Array<Array<Int>>; array_flatten(@Grid.0), type Row = Array<Int>; array_reverse(@Row.0)) reached the combinators' emission probes as its bare alias name and dropped — they now canonicalize through the same shared rebuilder #1055 taught the index-side derivations (the call-emission dual of that fix). A user-fn call argument with a flat Array<T> return (array_reverse(mk()), array_sort_by(mk(), cmp)) already resolved through this fix's fallback and is pinned; a NESTED return (array_flatten(mkn()) with mkn(-> @Array<Array<Int>>)) stayed unresolvable because the shared consultor deliberately blanks nested type-arg positions (clone-name-discovery lockstep) — the rebuilder now reads the registered fn's declared return type directly, off the consultor, so discovery is untouched.
Directly indexing a nested type-variable-element builtin result compiles (#1094, completing the #1048/#1051/#1053 family). array_reverse(array_reverse([10, 20, 30]))[0], array_sort_by(map_values(m), cmp)[0], array_reverse(map_values(m))[0], and array_flatten(array_reverse(x))[0] — a subscript applied straight to a type-variable-element Array builtin whose own argument is another type-variable-element builtin — were check- and verify-green but dropped the enclosing function via [E602], while every let-bound spelling (let @Array<Int> = array_reverse(array_reverse(x)); @Array<Int>.0[0]) ran. The #1051 per-class element-type derivation resolved its argument through the shared _get_arg_type_info_wasm consultor only, which deliberately cannot report a type-variable-element inner call (its element type depends on the call's arguments), so the derivation returned None and the index dropped. The class-1 argument-forwarding arm (array_reverse/array_sort_by), the array_flatten unwrap arm, and the class-2 container arm now resolve a FnCall argument through _builtin_call_ret_named_type — the shared consultor first, then the same per-class derivation, recursing — so the inner call's element type is recovered; every other argument shape (SlotRef, array/nested literal) still routes through the consultor, and a genuinely unresolvable argument keeps the loud [E602] skip. A Block-wrapped argument (array_reverse({ array_reverse(x) })[0]) resolves via its tail expression on both the element inference and the deep resolution, matching the container emissions' Block handling. The new examples/scoreboard.vera reads a top score with the natural direct-index spelling array_sort_by(map_values(@Board.0), cmp)[0] over a type Board = Map<String, Int>; alias.
Alias-spelled inner element names classify as their target's representation at the array emissions (#1067). With type Row = Array<Int>; type Grid = Array<Row>;, array_reverse(@Grid.0)[0][0] returned 4626322722586886145 and array_length(array_reverse(@Grid.0)[0]) returned 81948 — check-green, verify-green, garbage: the emission probes recovered the element as the bare alias name Row, and the size/pair classification fell to the 4-byte opaque-pointer default for what is really an 8-byte (ptr, len) pair, so every combinator copied half of each element; array_concat and the depth-2 array_flatten (@Array<Array<Row>>) read past their allocations (unreachable traps), and the @Row-comparator array_sort_by trapped mid-sort. Element names now canonicalize to the target's compound spelling at the element-probe exit, in array_flatten's input gate and T-recovery (whose alias-layer unwrap also sees through an alias-spelled middle layer, so array_flatten(@Grid.0) and array_flatten(@Array<Row>.0) compile instead of dropping), and all five shapes plus the sort compute correct values. The direct spellings (@Array<Row>, @Array<Array<Row>>) mis-classified identically through the pre-existing direct arm — latent on main, where those shapes still E602-dropped for unrelated reasons — and are fixed and pinned alongside the alias spellings.
A generic alias of a container as a declared return derives through its target, never its own type args (#1068). type MyMap<V> = Map<String, V>; fn mk(-> @MyMap<Int>) then map_keys(mk())[0] handed the runner a VALIDATION-FAILING module while vera compile exited 0: the container derivation consumed ("MyMap", ("Int",))'s type args positionally with no container-name check, deriving key element Int where the target says String, and the emission contradicted the derivation in the same function. The shared rebuilder now substitutes a generic alias's args through its target (substitute_type_vars) and canonicalizes — so MyMap<Int> resolves to Map<String, Int> and both map_keys and map_values over it compute correct values — and the container derivation additionally verifies the resolved argument IS Map/Set before reading K/V/T off it, so an unresolvable alias shape stays a loud [E602] skip rather than an invalid module. Caught before merge — the consuming derivation is this PR's own (#1051) machinery, so no released version is affected.
Bare-alias user-fn returns and Block-wrapped arguments resolve through the container emissions (#1071, completing the #1063 family). A user fn whose DECLARED return is a bare alias of a container (fn mkm(-> @M) with type M = Map<String, Int>;) silently truncated through map_keys / map_values / map_get / set_to_array — the shared consultor's user-fn arm only reports parameterized returns, so the bare alias exited unresolved before any alias handling and the emission fell to the "b" mis-tag (values returned as their low 32 bits, String keys garbled; pre-existing on main, reproduced there before fixing). The rebuilder now recovers a registered non-generic user fn's declared return directly when the consultor reports nothing, off the consultor, and a Block-wrapped container argument (map_values({ @M.0 })) resolves via its tail expression instead of riding the same mis-tag. The _map_wasm_tag fall-through comments now state exactly which argument shapes resolve and which still reach the permissive tag.
A Map or Set with a zero-size key, value, or element type is a checker error (E135) (#1075). Map<String, Unit> — direct or alias spelling — checked clean and compiled exit-0 to INVALID WASM ("expected i32 but nothing on stack": the zero-size value pushes no operand where the container's host import expects one); pre-existing on main, surfaced by the PR #1061 adversarial delta review. The determination follows spec §2.2's declared-vs-materialized line: Map keys/values and Set elements are raw, unboxed host-serialized values — representationally the Array<Unit> element case its E135 gate (#945) already rejects with this exact rationale — not the boxed-ADT-field case (Box<Unit> / Option<Unit> fields live inside a heap layout and stay legal, as does Map<String, Option<Unit>>, pinned). Rejection also keeps one canonical form (DESIGN.md principle 3): Map<K, Unit> is informationally a Set<K>, which the fix text names. The type-resolution gate now covers Map (both positions, reported per position) and Set, keyed on erasure (Future<Unit> rejects identically); the annotation-free spellings, whose types exist only through inference, are backstopped at codegen — _map_wasm_tag refuses the tag through the same RECURSIVE erasure oracle the checker keys on (_slot_name_erases_to_unit: alias chains canonicalized, Future<...> payloads recursed), and container entry types resolve rebuilder-first so a parameterized user-fn return reaches the tag as its full spelling rather than a bare Future head — a literal name comparison here was defeated by any indirection (async(async(())), a fn returning @Future<Unit> directly or behind type FU = Future<Unit> / type Task = Future<Unit>, all previously exit-0 invalid modules; PR #1083 adversarial review) — so the emission takes the loud [E602] skip instead of emitting an invalid module, while the genuinely element-type-free empty-collection shape (map_keys(map_new())) keeps its permissive fall-through. The same entry resolver routes an alias-of-Array user-fn return (type Names = Array<String>) into the existing Array-typed loud skip instead of a mis-tagged scalar slot. Spec §2.2 names the container rule alongside the Array one, and ch02_map_unit_value_rejected joins the conformance suite's negative fixtures (161 programs).
A nested constructor pattern after a zero-size component selects the right match arm (#1042). match Tuple((), MkBox(4242)) { Tuple(@Unit, MkBox(@Int)) -> ..., Tuple(@Unit, MkNot(@Int)) -> ... } silently ran the MkNot arm — check-green, verify-green, wrong value. Construction stores nothing for a zero-size component, but the nested-pattern tag walk gave it four bytes (the registered layout's generic type or an i32 default), so every nested constructor tag after it was checked at the wrong offset, failed against garbage, and match fall-through picked a later arm — whose extraction (computed correctly) then returned the real value through the wrong arm. The walk now gives erased components zero width, mirroring construction and the extraction walks; the same shape through a transparent Future<Unit> and through a user-ADT parent is pinned. Pre-existing for bare Unit since zero-size components landed (#902); surfaced by the #1035 review. The registered-layout side of the divergence (wildcard sub-patterns, structural Eq) is #1043.
A Future<Unit> component in a let-destructure or match binding erases like bare Unit (#1031). A zero-size Future<Unit> tuple/ADT component was check-green but CodegenSkipped the whole enclosing function (E602): the three codegen declaration-position guards — and the constructor-argument WASM-type inference that gates reachability (constructing a Future<Unit> field needs async(())) — compared the bare string Unit, so the transparent Future<Unit> wrapper (representation-identical to its Unit payload, #841) missed the zero-size branch and fell through to the skip. All four sites now key on erasure (mirroring erases_to_unit / codegen's _type_expr_to_wasm_type), so a declaration binding a Future<Unit> component compiles and binds nothing, exactly like bare Unit, with the non-zero-size sibling component landing at the correct offset. An alias to the compound (type FU = Future<Unit>;, including alias-of-alias chains) erases the same way: the keying canonicalizes an alias to its target's full compound spelling rather than resolving the base name only, which dropped the type arguments (FU resolved to Future, not Future<Unit>) and skipped the function — an alias inside Future<...> already worked. Reads of the erased component stay checker-rejected (E182, #1005), unchanged.
An alias to a representable compound (type FI = Future<Int>;) maps to its WAT type (#1037). A FI destructure/match component or standalone let @FI = async(41); binding was check+verify green but E602-skipped the whole enclosing function, while the direct Future<Int> spelling compiled: _slot_name_to_wasm_type resolved aliases through the same name-only recursion the zero-size keying had (FI resolved to bare Future, matched no branch, returned no representation). The mapper now canonicalizes an alias to its target's full compound spelling through the walk shared with the zero-size keying, so an alias binds exactly like its target written directly — the component binds a real local (await recovers the payload) and siblings land at the correct offsets. Zero-size erasure is unaffected, and a genuinely unrepresentable name still skips loudly.
await of a Future<T> compiles in match-scrutinee position (#1038). match await(@Future<T>.0) { ... } was check/verify-green but skipped the enclosing function (E602, "could not infer match scrutinee WASM type") for every non-Unit payload — an Option<Int>, a user ADT, and a scalar Int alike — because the SlotRef/ResultRef WASM-type mapper did not treat Future<T> as transparent the way the let-binding path already does. It now unwraps Future<T> to T's representation, so awaiting a future directly in scrutinee position matches the await-into-a-let-then-match form that already worked. (Future<String> in that position remains blocked upstream by its own let-binding limitation, a separate gap.)
Reading a zero-size slot is a checker error (E182) (#1005). A @Unit.n read — a normal function's @Unit param or a get clause's @Unit op parameter alike — passed check and died at codegen with the E699 dangling-slot internal error, since a Unit value compiles to no WASM local. The checker now rejects the read everywhere with a fix pointing at the unit literal (), keyed on representation (erases_to_unit) so a Future<Unit> slot is rejected the same way; declaring the parameter stays legal, mirroring the declare-vs-read line the E206 generic-at-Unit guard draws.
Effect ops in array-literal elements compile; a let of a zero-size type is a checker error (E183) (#1006). [get(()), 1] was check/verify-green but skipped the enclosing function (E602) because codegen's element-type inference did not know effect ops — both op-injection sites now record get's Vera result type (State<T>'s T) alongside the WAT type they already recorded, and the element dispatches through the clause-aware lowering (a transforming get clause applies to the element). let @Unit = put(5);, whose binding could never be read, is now rejected at check with a fix pointing at the statement form put(5); — uniformly for any zero-size binding, effect-op or plain RHS.
A let of a pair-represented Future<T> payload binds two locals (#1039). let @Future<String> = async("hello"); — and any Future<T> whose payload is pair-represented (String, Array<T>) — was check/verify-green but skipped the enclosing function (E602, "has no WASM representation"). Future<T> is representation-transparent (#841), so Future<String> is an i32_pair, but the let translator's pair detection keyed on the literal String/Array names rather than the transparent payload, so the wrapper fell to the scalar branch — where the scalar mapper recursed through it to a pair inner and returned no WASM type. The pair predicate is now Future-transparent, mirroring the existing Future arm in the scalar mapper, so a pair-payload Future binds and reads two locals exactly like a bare String/Array let; a scalar (Future<Int>) or pointer (Future<Box>) payload stays a single local, and a zero-size payload (Future<Unit>) still skips loudly.
A closure that captures a Future<T> free variable serialises it at the payload's width (#1044). Capturing a Future<String> returned 0 and capturing a Future<Int> trapped at WASM validation (expected i32, found i64): the capture-width decision in the closure free-variable walker matched only the literal String/Array names and routed everything else — including a representation-transparent Future<T> wrapper (#841) — through the scalar mapper that maps unknowns to i32, so a pair payload stored ptr-only (its length read back as adjacent zero) and an i64 payload pushed an i64 into an i32.store. The decision now runs through the same Future-transparent _is_pair_type_name / _slot_name_to_wasm_type deciders the let-binding and slot-read paths use; both the capture-store and capture-load sides read the corrected width from the one capture record, so they stay in agreement.
Array<Future<T>> elements are sized, loaded, and stored at the payload's representation (#1045). Array<Future<Int>> trapped at WASM validation (expected i32, found i64) and Array<Future<String>> trapped (values remaining on stack): the five module-level array-element helpers matched String / Array / the scalar dict with no Future strip, so an i64 payload was sized as a 4-byte i32 and a pair payload as a single word. Since Future<T> is representation-transparent (#841), the helpers now strip Future<…> (nesting included) to the payload before deciding. The parallel index-read path needed the same fix: element-type inference dropped the wrapper's type argument, collapsing Future<Int> to a bare Future that fell to the i32 default — it now preserves the Future<…> payload so the read stride and load op match the store.
An alias to a pair-payload Future (type FS = Future<String>;) binds like its target (#1046). let @FS = async("hello"); was check/verify-green but E602-skipped the enclosing function even with the #1039 and #1037 fixes in place: the pair predicate resolved the alias through the name-only base-name hop, which drops type arguments — FS resolved to bare Future, missed the Future-transparency arm, and fell to the scalar mapper, whose canonical String spelling has no scalar representation. The predicate now canonicalizes an alias to its target's full compound spelling first (the #1037 _canonicalize_alias_slot_name walk, cycle-cut threaded through the Future recursion), so an alias — including alias-of-alias chains — behaves exactly like its target written directly; the scalar-alias sibling (type FI = Future<Int>;, #1037) is unchanged.
vera run displays a bare Future<String> return as its string (#1047). A function returning Future<String> printed a raw heap pointer instead of the string, because the return-is-String predicate that populates fn_string_returns (so execute() decodes the (ptr, len) pair for display) lacked the Future strip. Future<T> is representation-transparent (#841), so a Future<String> return has the same pair shape as a String; the predicate now recurses through the wrapper. The emitted WASM was already sound — a caller that awaits the future gets the right value; only the top-level display was affected.
Array combinators over Array<Future<T>> copy elements at the payload's representation (#1057). Once #1045 made Array<Future<T>> literals and index reads sound, the array combinators became reachable on those arrays and returned garbage on check/verify-green programs: array_concat / array_slice / array_reverse / array_filter over Array<Future<Int>> returned wrong values (a 4-byte stride copied over the 8-byte i64 payloads), Array<Future<String>> concat half-read the two-word pair, array_append trapped at WASM validation (expected i32, found i64), and array_flatten flattened garbage. Each combinator recovered its element type through a site that returned the bare head Future with the type argument dropped — _infer_concat_elem_type for concat/slice/reverse/filter, a separate element-local decision for array_append, and a separate inner-type AST walk for array_flatten — so the element helpers could not strip Future<…> (#841) and collapsed to the 4-byte i32 default. Every site now preserves the full Future<…> spelling (and array_append strips the wrapper before typing its element local), mirroring the #1045 index-read fix.
An aliased Future<T> array element is stored at the payload's representation (#1058). type FI = Future<Int>; let @Array<FI> = [async(1)]; was check-green then trapped at WASM validation (expected i32, found i64): the array-literal store resolved the element type through the name-only base-name hop, which drops type arguments, so FI resolved to bare Future and the i64 payload was stored with i32.store. The literal store now canonicalizes an alias to its target's full compound spelling (Future<Int>) before resolving, mirroring the #1046 _canonicalize_alias_slot_name order, so an aliased Future element — scalar or pair payload — stores exactly like its target spelled directly.
Array combinators over alias-spelled element types copy at the target's representation (#1062). The alias-spelled sibling of #1057, one layer down: once the #1058 fix made Array<FI> (type FI = Future<Int>) arrays constructible, the combinators became reachable on them and received the bare alias name as the element type — from the shared element-type probe (concat/slice/reverse/filter), the array_append element inference, and the array_flatten inner-type walk. The module-level element helpers have no alias table, so the raw name fell to the 4-byte i32 default on check/verify-green programs: silent wrong values for Future aliases (concat returned 9448928052300 for an expected 1122), an expected i32, found i64 validation trap for array_append, and — reachable even before #1058 — a wrong element for a scalar alias like type Flag = Bool, whose 1-byte elements were copied at the 4-byte stride. Each site now canonicalizes a bare alias name to its target's full compound spelling before resolving, mirroring the #1058 literal-store fix; the index-read path was already alias-clean via its canonical element resolution (#559).
Array combinators over alias-named collections resolve the real element type (#1064). Pre-existing on main (no #1057/#1058/#1062 enabler involved): with type Flags = Array<Bool>;, array_concat(@Flags.1, @Flags.0) was check/verify-green but wrong — the collection slot's own name misses the Array match in the element-type probe, so the probe returned None and concat fell back to an 8-byte default stride. The fallback is coincidentally correct for Int, String, and array elements (why the shape survived unnoticed) and silently wrong for 1-byte Bool/Byte elements; array_slice and the map-family combinators loudly skipped the enclosing function instead. A literal whose elements are alias-typed slots (array_concat([@Flags.1], [@Flags.0])) hit the sibling hole in the probe's literal branch — the bare alias name sized the two-word pair elements at 4 bytes and indexing the result trapped unreachable. The probe now canonicalizes an alias-named collection to its target's full spelling and takes the element from it, canonicalizing a bare element name in turn (so type Grid = Array<Row> — whose target spelling keeps Row opaque — resolves to the row's real pair shape rather than regressing to the 4-byte default), and the literal branch canonicalizes bare inferred names the same way. Aliased collections of Int and of aliased rows keep their previous values, now by construction rather than by the 8-byte coincidence.
An array element spelled Future<Alias> is sized at the payload's representation (#1074). The alias-inside-Future<…> sibling of #1062, one layer deeper: an element written Array<Future<FlagA>> (type FlagA = Bool) — or hidden behind another alias, type X = Future<FlagA>; Array<X> — was check+verify+compile-green but mis-sized. The alias canonicalization resolved only a top-level alias name (or peeled the Future<…> wrapper), never an alias sitting inside the wrapper's type argument, so the element deciders _strip_future'd Future<FlagA> to a bare FlagA the name-keyed size dict fell to the 4-byte i32 default: a Bool/Byte payload's 1-byte-packed data was read at a 4-byte stride (silent wrong values — every element misread), while an Int/Nat/Float64/String payload trapped at WASM validation (expected i32, found i64 / values remaining on stack) at instantiation, behind an exit-0 compile. Pre-existing, not a regression: before this branch's combinator commits the same sites returned the bare head Future, whose element size is the identical 4-byte i32 default — the same wrong stride; #1057/#1058/#1062 fixed the non-alias and alias-of-Future payloads but the alias-inside-Future variant was never within the canonicalizer's reach and had no fixture. _canonicalize_alias_slot_name now recurses into the transparent Future<…> payload (Future<FlagA> → Future<Bool>) and the four element-type deciders (_infer_concat_elem_type for concat/slice/reverse/filter, the array-literal store, the array_flatten inner walk, and the index-read element inference) route through it uniformly; array_append's element inference already consulted the shared canonicalizer. Found by the adversarial delta review of this PR's combinator commits; the fix ships on the same branch.
Registered constructor layouts erase zero-size fields (#1043). A declared Unit field — or a transparent Future<Unit>, or an alias/alias-chain to either — was given a spurious 4-byte i32 slot in the registered ConstructorLayout (the _resolve_field_wasm_type wt is None fallback returned "i32"), while construction lays such a field out erasure-aware: zero-size, storing nothing. Every consumer trusting the registered offsets then read a shifted address on a check-green program: a wildcard over the erased field plus a nested constructor pattern matched the wrong arm off zeroed fresh-alloc memory, and structural Eq/show/hash compared, rendered, and folded the wrong bytes — all silently wrong. Registration now returns the "unit" sentinel for any erases-to-Unit field (mirroring construction), _wasm_type_size/_wasm_type_align learn it as size 0 / align 1, the erased field's Vera type name canonicalises to Unit (so a Future<Unit> field is Eq-derivable and rendered like the zero-size value it is), and the pattern-match and structural-eq/show/hash consumers treat a zero-size field as the equal-by-definition value it represents.
A wildcard over a type-parameter field instantiated to Unit reads the right offset (#1060). A generic constructor's type-parameter field (Box<T> field T) registers as the generic 4-byte i32 placeholder, but construction lays each instantiation out concretely — Box<Unit> erases the field to zero bytes (it is not boxed). A WILDCARD sub-pattern over that field advanced the match offset walk by the generic i32 width regardless, so on a Box<Unit> every field after the erased one was read four bytes too high — silently, on a check-green program with no diagnostics: match b { MkB(@Int, _, @Int) -> @Int.0 } returned 0 instead of the real trailing Int, N(_, @String) on Named<Unit> read the String header at the wrong offset, and En(_, MkBox(@Int)) on Entry<Unit> read the nested constructor tag at a shifted address and matched the wrong arm. This is the type-parameter sibling of #1043's declared-Unit field: only the two wildcard walks (_extract_constructor_fields and _sub_pattern_wasm_type) were wrong — @Unit bindings, let-destructures, and structural Eq/show/hash already recompute each field from the concrete instantiation and were correct for the same shapes spelled with the literal Unit argument (a non-literal erases-to-Unit argument — an alias, Future<Unit> — hit the same class of hole in Eq and in the width recomputation itself; that is #1070, fixed below). The wildcard walks now recompute a bare type-parameter field's width from the scrutinee's concrete type arguments, mirroring the eq/show recomputation. Where the instantiation is unrecoverable (a direct-call scrutinee whose inferred type dropped its arguments) and a later field is read, the function now LOUD-skips (E602) rather than reading a wrong offset; a trailing unrecoverable wildcard — whose width is never consumed — still compiles.
Erases-to-Unit type arguments work spelled non-literally: Box<U>, Box<Future<Unit>>, aliases, chains (#1070). The #1060 wildcard width recomputation resolved a type-parameter field's concrete type from the scrutinee's type arguments — but the width function's zero-size test was the literal name Unit. Registration canonicalises a declared erased field to Unit (#1043); a type argument keeps its use-site spelling, so Box<U> (type U = Unit;), Box<Future<Unit>>, Box<FU> (type FU = Future<Unit>;), and alias chains got 4 bytes and every later field was again read at a shifted offset — silently, check-green: the trailing Int read 0 instead of 22, and the nested-constructor variant matched off garbage. The same literal-test disease broke structural Eq over the same spellings — pre-existing, not introduced by #1060 (the #1060 claim that eq/show/hash "were already correct" held only for the literal spelling): the == dispatch's concreteness gate and free-type-variable heuristic both classified U as an unresolved type variable, so the comparison silently fell back to the scalar pointer compare and two structurally equal values compared unequal; show/hash over the same shapes loud-skipped (E602). Every site now keys on erasure rather than the literal name — the width function (_eq_field_wasm_type), the resolved-field-type canonicalisation (_resolve_field_type_for_eq, mirroring registration), the dispatch gates (_eq_type_name_fully_concrete, _type_arg_is_free_var), and the Eq-derivability gate (_type_eq_derivable, kept in lockstep with the $eq generator per the #732 differential) — so all these spellings behave exactly like the literal Unit: wildcards read the constructed offsets, Eq compares structurally, and show/hash render and fold the real fields. Rider: a zero-size binding (@Unit) after an unrecoverable type-parameter wildcard no longer counts as a "later read" (it binds nothing and loads nothing), so that trailing shape compiles instead of over-conservatively loud-skipping; a genuine read beyond the erased binding still loud-skips.
Structural == over non-Unit alias type arguments compares values, not pointers (#1076). Box<MyInt> (type MyInt = Int;), Box<MyStr>, Box<MyBool>, Box<Future<Int>>, and alias chains: the == dispatch's free-type-variable heuristic and concreteness gate classified the alias spelling as an unresolved type variable, so the comparison silently fell back to the scalar pointer compare — two structurally equal values compared unequal (0) on a check-green program, while the literal spellings compared correctly. This is the non-Unit half of the heuristic #1070 patched for erases-to-Unit spellings; pre-existing alongside it. The fix grounds a spelling — alias chains resolved, transparent Future<...> wrappers peeled to their payload — at every site the #1070 pass keyed on erasure: the classifier and concreteness gate (so the dispatch routes structurally), the E613 derivability gate (kept in lockstep with the $eq generator per the #732 differential — a wrong loud E613 was the alternative failure), the field-type resolution (so a MyStr field dispatches to the String content comparison and a Future<Int> field compares its payload), and the width function (so the #1060 wildcard walks size a MyInt/Future<Int> field as i64, not the 4-byte pointer default — a following Bool read the right offset). Distinct values keep comparing unequal, including payloads that collide in their low 32 bits (2^32 + 7 vs 7), and a genuine free type variable still classifies free (the dead base-generic clone keeps its harmless scalar lowering, #912). Grounding the shared field resolution also lets show/hash render and fold such fields instead of loud-skipping.
show/hash accept aliased-Unit spellings at the two sites the #1070 pass missed (#1077). show/hash of a Tuple<U, Int> (type U = Unit;) loud-skipped the enclosing function: the Tuple-variadic plan branch passed raw type arguments to the per-field dispatch — unlike the registered-ADT branch #1070 fixed — so the unknown name U abandoned the whole render; the arguments are now grounded exactly like ADT field resolutions, and the erased component takes zero width so the following Int is read at its constructed offset. A bare value of an erases-to-Unit alias type (a function returning @U) missed the top-level show/hash Unit arms, which compared the literal name; both arms now key on erasure. All four shapes were loud drops (E602), never wrong values; the literal spellings were already correct and stay pinned.
Element-wise == on arrays of parameterized ADTs compares structurally (#1078). Array<Box<Int>> — literal spelling included — silently pointer-compared its elements: an IndexExpr operand's element type reaches the dispatch as the bare head (Box; the element-type inference drops the recovered NamedType's type arguments), so a parameterized element was classified as a lost-type-argument clone (#772/#912 residue class) and == took the scalar fallback — equal elements compared unequal on a check-green program, while the same values compared directly (no array) and arrays of non-generic ADTs were correct. The == recovery chain now re-derives the full element spelling from the indexed collection, which carries its complete type arguments; aliased instantiations (Array<Box<U>>, Array<Box<MyInt>>) ride the #1070/#1076 grounding from there. Distinct elements keep comparing unequal, i64-wide.
Structural == over an alias of a WHOLE ADT compares values, not pointers (#1085). type MyBox = Box<Int>; then @MyBox.0 == @MyBox.1: the operand reached the == dispatch as the bare alias name MyBox, absent from _adt_type_names, so the structural branch was skipped and == fell to the scalar pointer compare — two structurally equal, distinct-pointer values compared unequal (0) on a check-green program, while the array-element form and the direct Box<Int> spelling compared correctly. This is the whole-OPERAND sibling of #1076, which grounded type ARGUMENTS (Box<MyInt>) but not an operand whose own type is an alias of the ADT. The operand's spelling is now grounded through the shared _canonical_field_type canonicalizer at the dispatch site (alias chains resolved, transparent Future<...> peeled), so MyBox → Box<Int> and the base Box routes to the structural $eq helper; an alias to a non-generic ADT and an alias chain ground the same way. Distinct values keep comparing unequal, i64-wide (2^32 + 7 vs 7), and a registered ADT or a genuine free T is returned unchanged, so the lost-type-arg and dead base-generic-clone controls still take the harmless scalar fallback (#912). The same grounding also fixes == through a refinement of a whole ADT (type NB = { @Box<Int> | true }; then @NB.0 == @NB.1) — the refinement alias resolves to its base spelling in the same walk, where it previously fell to the same silent pointer compare (equal values → 0 on a check-green program; pinned equal-and-distinct). Pre-existing alongside #1076; found by the adversarial review of PR #1084.
A forall<T where Eq<T>> instantiated at an Eq alias is accepted, not wrong-loud E613'd (#1086). same(mk(), mk()) where the argument is @Box<MyInt> (type MyInt = Int;) was rejected with a wrong-loud [E613] "Type 'MyInt' does not satisfy ability 'Eq'": the monomorphizer's top-level constraint gate (_check_constraints) tested concrete in type_set (a primitive) then _adt_satisfies_eq (a registered ADT layout) — an alias name is neither, so a legal program the alias-resolving checker accepted was refused before codegen. The gate now grounds the spelling through the shared _type_eq_derivable oracle — the SAME derivability check the $eq generator's field resolution mirrors, so the #732 checker↔codegen differential holds at this entry point too — accepting MyInt (→ Int), an alias of a whole ADT, and a transparent-Future alias (FI / Future<Int> → Int) alike. A genuinely non-Eq alias (type BadArr = Array<Int>;) grounds to a non-Eq type and still raises the correct [E613] with no codegen [E699] invariant hit (the two sides stay in lockstep). The emitted clone name and message keep the un-ground spelling (the #772/#932 hard constraint). Pre-existing; found by the adversarial review of PR #1084.
show / hash of a bare or aliased Future value renders the payload, not E602 (#1087). show(@FI.0) (type FI = Future<Int>;) and show(@Future<Int>.0) loud-skipped the enclosing function ([E602]): the argument's inferred type reached the top-level show/hash dispatch as FI / Future<Int>, matched no primitive / Unit / composite arm, and abandoned the render — while show of the literal Int payload rendered fine. #1077 keyed the top-level Unit arm on erasure (covering aliased-Unit spellings); this is the non-Unit bare-Future sibling at the same dispatch. _translate_show / _translate_hash now ground the inferred type through the shared _canonical_field_type canonicalizer (alias chains resolved, transparent Future<...> peeled to its payload — FI → Int), so the render / fold dispatches exactly as the literal payload would; a non-alias, non-Future name is returned unchanged, leaving every other arm untouched. Distinct payloads still hash distinctly at i64 width (2^32 + 7 vs 7). The grounding also covers a bare aliased-primitive (type MyInt = Int;, show(@MyInt.0)) and refinement (type Pos = { @Int | ... };) value, which loud-skipped the same way. That top-level grounding alone still missed two spellings (PR #1090 review): a composite Future payload — show(@FOI.0) with type FOI = Future<Option<Int>>;, bare spelling included — and an alias of a whole ADT (type MyBox = Box;, #1091, found during this PR), because the composite path then recovers the argument's PARAMETERIZED type from its declared spelling (_parameterized_arg_type), undoing the grounding before _show_value / _hash_value resolves constructor plans. The recovered spelling is now grounded at both dispatch sites, and the composite render's Array arms ground their element type the same way (a @Array<FI> slot's element reached the size table, the element load, and the recursive render as the raw alias — [mkf(), mkf()] array literals included). A Tuple component and a generic-ADT constructor argument of an aliased-Future type already rendered correctly — the recovery's raw component spellings are grounded at consumption by the #1076/#1077 plan resolutions — and stay pinned. All these shapes were loud drops ([E602]), never wrong values. Pre-existing; found by the adversarial review of PR #1084 and CodeRabbit's review of PR #1090.
An int literal coerced into a @Byte-instantiated generic constructor field is stored at the field's width (#1092). let @Box<Byte> = MkB(0); — the one literal-at-Byte-field spelling the checker admits (an in-range 0..255 literal coerces to @Byte through the generic instantiation; a declared Byte field rejects the literal with [E213], and out-of-range, negative, or non-literal @Int arguments are loud [E170] rejections) — was constructed at the literal's own i64 width: construction sized the field from the ARGUMENT's inferred WASM type and stored at the 8-byte-aligned i64 slot, while every READER — field extraction, the structural-$eq helper, show/hash — sizes the field from the instantiated type (Byte → i32 at the i32 offset). Extraction read 0 for a stored 255, and MkB(0) == MkB(255) compared the same wrong bytes on both sides and returned equal — silently, on a check-green program; the @Byte-slot passthrough (MkB(@Byte.0)) always stored i32 and was correct. Construction now stores the coerced literal at the field's i32 Byte width, keyed on the checker-recorded target type (the #820 side-table; the target's argument name is grounded, so Box<MB> via type MB = Byte; — the spelling the #1086 fix newly admits under forall<T where Eq<T>> — coerces like the literal Byte, and an Int-instantiated literal field keeps its i64 store, 2^32 staying distinct from 0). Pre-existing on the base (direct spelling included); found by the independent adversarial review of PR #1090. #1060 made the type-parameter wildcard walks instantiation-aware for a slot scrutinee, but a direct-call scrutinee — match mk() { MkB(@Int, _, @Int) -> @Int.0 } where mk() -> @Box<Unit> — still LOUD-skipped (E602) whenever a later field was read: codegen's _infer_vera_type(FnCall) returns the bare base head ("Box") for a parameterized i32-pointer return, dropping the <Unit> the walk needs, so it refused to guess a shifted offset — the sound interim behavior. The match lowering now recovers the scrutinee's full concrete type (Box<Unit>) from the callee's declared return type (_fn_ret_type_exprs, which a non-generic signature declares fully — no type variables to resolve), matching the slot form, so those shapes compile and read the real value (a trailing Int, a nested constructor tag, a Named<Unit> String read-back).
A generic-call match scrutinee resolves its instantiation from the call site (#1072). The generic sibling of #1065: match wrap(5) { … } where forall<T> fn wrap(@T -> @P2<T, Unit>) — the declared return carries type variables, so the #1065 non-generic recovery did not apply and the wildcard walk could not learn the erased field's width. On main this family read shifted offsets silently (the pre-#1060 walk; the repro returns 0 instead of 22 on a check-green program); the #1049 stack turned it into a sound E602 LOUD-skip. The match lowering now binds the callee's type variables from the call site — the same _unify_param_arg_wasm unification the generic call-rewrite performs — substitutes them into the declared return, and renders the full instantiation (P2<Int, Unit>), covering the concrete-Unit-type-arg return, a var-typed field at String (i32_pair width), a fully concrete parameterized return on a generic fn, and the nested-constructor and String-read-back variants. An unresolved variable still falls back to the LOUD-skip (sound); instantiating the variable itself at Unit stays E206-rejected at check, and a phantom-var callee stays E121-rejected.
A module-call match scrutinee recovers its instantiation through the shared resolver (#1073). The module door of the same family: match boxlib::mk() { … } never entered the #1065/#1072 recovery (it dispatches on the bare-name call form) and fell to the same bare-base-head collapse — a silent wrong value on main, a sound E602 LOUD-skip on the #1049 stack. The match lowering now resolves the qualified target through the single shared module-call resolver (the #774-reviewed source of truth) and recurses into the same declared-return recovery, covering imported non-generic and imported generic (#1072 x #1073 compound) scrutinees.
array_map / array_mapi / array_fold over Array<Future<T>> size the output element (and fold accumulator) at the payload's representation (#1079). The bare-head family (#1057's mechanism) at the closure-return / fold-accumulator inference site, found during the #1074 work: _infer_closure_return_vera_type (and _infer_fold_init_vera_type's SlotRef-init fallback) returned the canonical NamedType's bare .name — "Future", the type argument dropped — before the element deciders run, so the #1045/#1057 element fixes and the #1074 payload canonicalizer never reached this path, and the DIRECT Future<Int> spelling mis-sized too, not only aliases. array_map rejects an async closure, so the trigger is a pure closure forwarding an existing Future value — the identity/reshuffle pattern. Failure modes behind a check+verify-green, exit-0 compile split by payload: Int/Nat/Float64/String payloads trapped — indirect call type mismatch at run for map/mapi (the registered call_indirect signature said the closure returns i32 while the closure compiled returning i64/f64/i32_pair), expected i32, found i64 at WASM validation for a fold accumulator (the acc local was typed i32 while the init pushes i64) — while Bool payloads were silently wrong (both signatures agree at i32, so the 4-byte-stride stores simply misread through the 1-byte-packed index reads). Both sites now render the FULL compound spelling — _format_named_type plus the #1074-extended _canonicalize_alias_slot_name payload walk — covering the direct, aliased-element (type FI = Future<Int>), and aliased-payload (Future<Big>, type Big = Int) spellings, the array_mapi and array_fold twins, a block-wrapped closure literal reaching the SlotRef-init fallback, and a chained array_concat(array_map(...), …). Twelve regression tests, each mutation-validated against its exact pre-fix failure.
array_map over Array<Future<Bool>> reads back the values it wrote (#1081). A silent regression the #1041 merge introduced and the #1079 write-side fix closes: #1041's element-READ stripping sizes Future<Bool> index reads at the payload's 1-byte stride, but array_map's element WRITE path still inferred the bare head "Future" (#1079's mechanism) and stored at the 4-byte default — the previously-consistent 4/4 round-trip became 1/4, and an identity map over [false, true, false, true] read back all-false (2222 for the base-correct 2121) with every downstream element misread. Pinned with the base-correct 2121-pattern regression test plus a no-map control from the adversarial review of the merge.
Collection-alias Array<Future<Alias>> elements canonicalize through the array combinators (#1082). The #1074 residual arm, found by the #1041-merge adversarial review: _infer_concat_elem_type's collection-alias arm (#1064) resolves type Rows = Array<Future<FlagA>> to the target spelling and extracts the element — but returned a COMPOUND element (Future<FlagA>) verbatim, skipping the payload canonicalization the sibling bare-element branch performs (type FF = Future<FlagA>; type Rows = Array<FF> already worked). _strip_future then handed the size dict the unresolved alias FlagA, which fell to the 4-byte default: silent wrong values through array_concat / array_reverse for Bool AND i64 payloads (concat of two distinct >2^32 futures returned 0; reverse returned byte-scrambled garbage) and coincidence-dependent reads through array_slice / array_filter, all check+verify-green. On this branch the arm's verbatim return is neutralized by the #1067 single-exit canonicalization (_infer_concat_elem_type canonicalizes every raw result, and the #1074-extended payload walk resolves Future<FlagA> → Future<Bool>); six regression tests — including the previously-coincidence-green slice shape — pin the behavior, four of them flipping RED if the exit canonicalization is removed.
Nested generic where-helpers are parent-qualified mono bases (#1014). Two same-named forall helpers under different parents were keyed flat, first-seen-wins, so the second parent's call silently ran the first parent's body (check-green, wrong value). A shared transform now qualifies every nested generic base (a$where$g) and rewrites its lexically-visible calls, on both the codegen and verifier sides — the same collision also merged the two helpers' instance sets in the verifier, which now keys them distinctly.
Imported module where-helpers get the parent-qualified hoist (#1015). Two imported functions each carrying a same-named non-generic where-helper silently resolved to the first one's body; each resolved module's AST now receives the same #991 hoist the main program gets before registration.
A grandchild helper calling an aunt inside a generic clone's where-tree compiles (#1012). The generic clone hoister rewrote calls with this-level names only; it now threads the full ancestor scope, mirroring the non-generic hoister, so the call resolves to the hoisted aunt instead of dangling at WAT assembly.
A forall helper under a generic ancestor is instantiated per clone (#1002). Clone hoisting substituted only the ancestor's type variables, leaving an own-forall helper as a still-generic template whose call dangled on a check-green, verify-green program; a per-clone instantiation worklist now clones it at its concrete call sites, and the verifier discovers and verifies the same instances (a lying nested contract is a loud E500).
Imported function bodies seed generic-instantiation discovery (#999). An imported non-generic function calling its own nested forall helper compiled to a dangling name because discovery only scanned the importer's declarations; resolved-module bodies are now qualified (module-namespaced, so two modules' same-named nested helpers stay distinct bases), harvested, and seeded on both the codegen and verifier sides, with #998 origin threading so clones compile against their module's span tables; nested-helper instances key on one canonical concrete-free module-qualified chain across emission, discovery, and per-instance verification.
Private module generics reached transitively through a public generic are harvested — module-qualified (#1000, supersedes draft PR #1026). The public generic's clone body call now routes to the module's own private helper under mod$<path>$<name> — never a bare name, so a same-named local function keeps its body in BOTH directions (pre-fix the transitive call was silently captured by the local). Every imported declaration's private-generic calls are routed — non-generic callers and private-to-private chains included — and the verifier discovers and verifies the same qualified instances on every path (including through a locally-shadowed public generic), so a lying private contract is a loud E500 even when another module has a truthful same-named one.
A module function constructing its own ADT compiles regardless of the importer's type imports (#1008). Constructor layouts were registered per the importer's filter, so make's body dropped to unknown constructor unless the importer also named the type — module-own layouts (public, private, or out-of-filter) now register unconditionally, while importer visibility and the checker's E210/E320 rails are unchanged.
vera compile prints the E602 "function skipped" warning on the text error path (#1004). When a CodegenSkip drops a called function, the caller's dangling call $f fails WAT assembly with an opaque unknown func; the warning explaining why the function was dropped was suppressed on the text error path (the --json envelope already carried it) and is now printed alongside the error. The type-error and --target wasi-p2 family-gate text paths are corrected the same way, so a warning alongside those errors is no longer dropped.
The @Int -> @Nat narrowing into an apply_fn closure formal is now obligated and runtime-guarded (#1017). A provably-negative @Int argument narrowing into a @Nat closure formal via apply_fn verified clean (a false Tier 1) and, for a runtime value, entered the formal reinterpreted with no trap. The verifier's apply_fn branch now emits the @Nat narrowing obligation (mirroring the generic call-argument path — E503 for a provable negative, a guarded Tier 3 otherwise) and code generation guards the call_indirect argument — the narrowing dual of the #820 argument-widening handler at this site.
The refinement-predicate narrowing into an apply_fn closure formal is now obligated and runtime-guarded (#1024). apply_fn(f, 0) where f's formal is { @Nat | @Nat.0 > 0 } verified clean (a false Tier 1) and ran silently: a refinement over @Nat is a @Nat type, so the #1017 handler claimed the site and discharged only the base's >= 0 — which 0 satisfies — leaving the strict predicate unchecked with no runtime backstop. The verifier's apply_fn branch now discharges the full predicate refined-first (ahead of the #1017 @Nat arm, mirroring the generic call-argument path — E505 for a provable violation, a guarded Tier 3 otherwise), and code generation guards each refined closure formal at the lifted body's prologue — the closure-side dual of the refined-parameter guard named functions already carry.
A refined closure RETURN is now obligated and runtime-guarded (#1032, the return-side dual of #1024, found while fixing it). fn(@Int -> @Pos) { @Int.0 } (with Pos = { @Nat | @Nat.0 > 0 }) applied to -5 — or to 0, which clears the @Nat base's >= 0 — returned the violating value through the refined slot on a verify-clean program: the verifier's closure-return handling covered the widening (#820) and bare-@Nat narrowing (#984) directions but no refinement, and the lifted closure emitted no return guard while the #984 gate excluded refinements assuming a boundary guard that did not exist. The verifier now records a refined closure return as a guarded Tier 3 (the closure body is opaque to the SMT layer — never a false Tier 1), and code generation checks the lifted body's return value against the full predicate, mirroring the named path's refined-return guard, so a violating value traps with the refinement message instead of leaking. The refinement obligation stream is also now honest about the boundaries codegen cannot guard: a refined base with a non-plain type argument (Array<{ @Int | ... }>-style) records tier3_unguarded (E506 disclosure) at every parameter/return boundary — named or closure — instead of claiming a runtime guard that never fires (#1036 tracks emitting the guard itself).
Map / Set entries and array_concat over map_values handle representation-transparent Future<T> values (#1097). A Map<String, Future<Int>> value round-trip (map_insert / map_get / map_values) was check- and verify-green but compiled exit-0 to an INVALID module. Future<T> is representation-transparent (#841) — a Future<Int> IS an i64, a Future<String> an i32_pair — but the Map/Set host-tag classifier (_map_wasm_tag, shared by keys, values, and Set elements) did not strip the transparent wrapper, so a Future<Int> value fell through to the "b" (single-i32) tag while the value expression pushed an i64: the registered host import disagreed with the stack ("type mismatch: expected i32, found i64", or "values remaining on stack" for the pair payload). The classifier now canonicalizes an alias name (type FI = Future<Int>;) and strips Future<…> wrappers to the payload before tagging — so a Future<Unit> value still takes the zero-size loud [E602] skip and a Future<Array<Int>> value the existing Array-reject skip, never an invalid module — and the same fix covers Set<Future<T>> elements and Future-typed map keys. A second, latent site rode behind it: array_concat(map_values(m), map_values(m)) over such a map ran a wrong-stride copy (silent garbage) — the two rebuilt arms of the array combinators' element-type inference (_infer_concat_elem_type) returned the bare head "Future" with the type argument dropped, so the copy loop strided the 8-byte i64 payloads at the 4-byte i32 default, while the let-bound @Array<Future<Int>> SlotRef form was already correct (#1057). Both arms now mirror the direct SlotRef arm through a shared helper, preserving the full Future<…> spelling.

Documentation

Spec §11.8 now matches code generation: every non-trivial contract is compiled as a runtime check regardless of the verifier's tier (#958). The section previously claimed Tier-1-proved contracts are omitted from the compiled output; code generation is tier-agnostic (vera/codegen/contracts.py has no notion of tiers), so a Tier-1 proof means the emitted check provably never fires, not that it is absent — the runtime guard is the deliberate backstop that keeps a false Tier 1 a loud trap rather than a silent wrong answer.
scripts/check_pypi_readme_examples.py gates the PyPI project page's Vera blocks at parse + check + verify (pre-commit hook pypi-readme-examples + a CI lint step): the Try-it program on PyPI is now held to the same standard as the other doc surfaces, and a broken contract in it fails the gate.
Spec §0.5.1 and SKILL.md now state that ? inside a type printed by a diagnostic marks a component the checker could not infer (Array<?>) — a rendering marker distinct from the typed-hole expression ? (§4.17) written in source.
The concurrent-await alias-Future limitation (spec §9.5.4) is now anchored to a tracking issue (#1095), with a matching KNOWN_ISSUES.md limitation row: confirming it still reproduces requires a genuinely concurrent repro, since an eager-path probe never reaches the handle-check.

Assets 5