…, #873)

An imported generic instantiated only by the importer was monomorphized
nowhere — check passed but run failed WASM validation at `call $gid`, for
both the bare and module-qualified call forms (#774). The importer now
harvests imported public generics, merges the unshadowed ones into its
`generic_decls` (so discovery + emission + the call-site rewrite cover
them), and the shared discovery walks `ModuleCall` targets. The clone is
owned by the importer and carries the usual Tier-3 runtime postcondition
guard. The #814 asymmetric variant — a generic shadowed by a local
non-generic and module-qualified-called — previously false-Tier-1'd; it is
now monomorphized under a distinct `mod$<path>$gen$…` name reached only by
the qualified call, bringing codegen into agreement with the verifier.

A generic whose only call site is inside a closure body failed run with
`unknown func` (#873): the lifted closure body was compiled without
`generic_fn_info`. `_compile_lifted_closure` now threads `generic_fn_info`
+ `known_fns`.

Two completeness gaps one level deeper in the shadowed path (PR #888
review): (1) a shadowed generic whose body calls another generic now gets
that transitive clone emitted — an unshadowed sibling (a normal clone) or a
same-module shadowed sibling (its own `mod$…` clone reached by rewriting the
intra-module bare call) — on both codegen and the verifier, so the #732
differential stays a true equality (a codegen-only transitive fix would be a
new false Tier-1); (2) the statement-position result-shape predicates
(`_is_void_expr` / `_is_pair_result_expr`) now share one ModuleCall target
resolver with the desugar, so a shadowed generic returning `@String`/`@Unit`
drops the correct stack shape.

Codegen and verifier discovery move in lockstep — proved by the #732
differential (flipped to pin the new "both monomorphize" symmetry,
parametrized over both call forms, plus shadowed and transitive-shadowed
variants). Mutation-validated eight ways.

Intake (pre-existing, orthogonal, filed): transitive module import
main->mid->base `unknown func` (#890); generic over a parameterized ADT
`expected i64 found i32` in the clone (#891).

Run-level conformance programs `ch08_cross_module_generic` and
`ch09_generic_in_closure`; spec §11.16 documents importer-owned
cross-module monomorphization.

Co-Authored-By: Claude <[email protected]>

…, #873)

An imported generic instantiated only by the importer was monomorphized
nowhere — check passed but run failed WASM validation at `call $gid`, for
both the bare and module-qualified call forms (#774). The importer now
harvests imported public generics, merges the unshadowed ones into its
`generic_decls` (so discovery + emission + the call-site rewrite cover
them), and the shared discovery walks `ModuleCall` targets. The clone is
owned by the importer and carries the usual Tier-3 runtime postcondition
guard. The #814 asymmetric variant — a generic shadowed by a local
non-generic and module-qualified-called — previously false-Tier-1'd; it is
now monomorphized under a distinct `mod$<path>$gen$…` name reached only by
the qualified call, bringing codegen into agreement with the verifier.

A generic whose only call site is inside a closure body failed run with
`unknown func` (#873): the lifted closure body was compiled without
`generic_fn_info`. `_compile_lifted_closure` now threads `generic_fn_info`
+ `known_fns`.

Two completeness gaps one level deeper in the shadowed path (PR #888
review): (1) a shadowed generic whose body calls another generic now gets
that transitive clone emitted — an unshadowed sibling (a normal clone) or a
same-module shadowed sibling (its own `mod$…` clone reached by rewriting the
intra-module bare call) — on both codegen and the verifier, so the #732
differential stays a true equality (a codegen-only transitive fix would be a
new false Tier-1); (2) the statement-position result-shape predicates
(`_is_void_expr` / `_is_pair_result_expr`) now share one ModuleCall target
resolver with the desugar, so a shadowed generic returning `@String`/`@Unit`
drops the correct stack shape.

Codegen and verifier discovery move in lockstep — proved by the #732
differential (flipped to pin the new "both monomorphize" symmetry,
parametrized over both call forms, plus shadowed and transitive-shadowed
variants). Mutation-validated eight ways.

Intake (pre-existing, orthogonal, filed): transitive module import
main->mid->base `unknown func` (#890); generic over a parameterized ADT
`expected i64 found i32` in the clone (#891).

Run-level conformance programs `ch08_cross_module_generic` and
`ch09_generic_in_closure`; spec §11.16 documents importer-owned
cross-module monomorphization.

Co-Authored-By: Claude <[email protected]>

…, #873)

An imported generic instantiated only by the importer was monomorphized
nowhere — check passed but run failed WASM validation at `call $gid`, for
both the bare and module-qualified call forms (#774). The importer now
harvests imported public generics, merges the unshadowed ones into its
`generic_decls`, and the shared discovery walks `ModuleCall` targets. The
#814 asymmetric variant — a generic shadowed by a local non-generic and
module-qualified-called — is now monomorphized under a distinct
`mod$<path>$gen$…` name reached only by the qualified call.

A generic whose only call site is inside a closure body failed run with
`unknown func` (#873): `_compile_lifted_closure` now threads
`generic_fn_info` + `known_fns`.

Completeness gaps closed one level deeper (PR #888 review): a shadowed
generic calling another generic emits the transitive clone (both sides);
the statement-position result-shape predicates share one ModuleCall target
resolver with the desugar; an unshadowed generic calling a shadowed sibling
has its shadowed clone discovered by scanning the emitted normal clones.

Soundness keystone (CR 3519156263): an imported generic's clone RUNS in the
importer but its body lives in another module, so a LYING module contract
ran unverified — a false Tier-1 (verify clean, run traps the clone's
postcondition). Worse, a same-named LOCAL generic absorbed the module call's
instantiation into its bare key, proving the local's contract in the module
clone's place. The importer now records every shadowed module clone under
its `mod$…` base (never the bare name a local generic owns), and verifies
each imported generic's clone (shadowed and unshadowed) at its own
instantiations, turning a lying module contract into an honest E500. The
warm incremental session runs the same verification so warm == cold.

Codegen and verifier discovery move in lockstep — proved by the #732
differential (namespaced keys distinguish module clone from same-named
local generic). Mutation-validated: disable the imported-generic verify
pass → lying-contract tests stop catching E500; desync either side's mod$…
key → differential flips; disable either side's normal-clone scan → the
unshadowed-caller case flips.

Run-level conformance programs `ch08_cross_module_generic` and
`ch09_generic_in_closure`; spec §11.16.

Co-Authored-By: Claude <[email protected]>

#873)

Closes #774
Closes #773
Closes #873

… mono clone (#891)

A generic instantiated over a parameterized ADT — `gid(MkBox(7))` for
`gid : forall<T> fn(@t -> @t)` and `data Box<T> { MkBox(T) }` — passed
`vera check`/`vera verify` but trapped at `vera run` with
`type mismatch: expected i64, found i32` while compiling the `gid$Box`
clone.

Root cause: `_infer_expr_wasm_type`'s `ResultRef` arm
(`vera/wasm/inference.py`) inferred only the scalar primitives and
returned `None` for everything else. Once `T = Box`, the clone's
postcondition `@T.result == @T.0` compares two i32 heap pointers, but the
`ResultRef` (`@Box.result`) defaulted to the scalar i64, so the equality
fell through to the `i64.eq` default while the operands were i32 — an
ill-typed clone body wasmtime rejects at instantiation. The `SlotRef`
operand (`@Box.0`) and the clone's `param`/`result` signature were
already i32; only the postcondition op disagreed.

Fix: the `ResultRef` and `SlotRef` arms now share one
`_ref_type_name_wasm_type` helper, so an ADT-bound (and pair-/handle-bound)
type variable lowers to i32 consistently across the signature and every
slot/result read.

New conformance program `ch02_generic_over_param_adt` (run level; suite
now 112) plus a regression test in `tests/test_codegen_monomorphize.py`
pin `gid(MkBox(42))` unwrapping to 42. Mutation-validated: reverting the
`ResultRef` arm to the pre-fix scalar-only logic restores the trap,
flipping the test RED.

Pre-existing on main; found by the PR #888 soundness review.

Co-Authored-By: Claude <[email protected]>

… mono clone (#891)

A generic instantiated over a parameterized ADT — `gid(MkBox(7))` for
`gid : forall<T> fn(@t -> @t)` and `data Box<T> { MkBox(T) }` — passed
`vera check`/`vera verify` but trapped at `vera run` with
`type mismatch: expected i64, found i32` while compiling the `gid$Box`
clone.

Root cause: `_infer_expr_wasm_type`'s `ResultRef` arm
(`vera/wasm/inference.py`) inferred only the scalar primitives and
returned `None` for everything else. Once `T = Box`, the clone's
postcondition `@T.result == @T.0` compares two i32 heap pointers, but the
`ResultRef` (`@Box.result`) defaulted to the scalar i64, so the equality
fell through to the `i64.eq` default while the operands were i32 — an
ill-typed clone body wasmtime rejects at instantiation. The `SlotRef`
operand (`@Box.0`) and the clone's `param`/`result` signature were
already i32; only the postcondition op disagreed.

Fix: the `ResultRef` and `SlotRef` arms now share one
`_ref_type_name_wasm_type` helper, so an ADT-bound (and pair-/handle-bound)
type variable lowers to i32 consistently across the signature and every
slot/result read.

New conformance program `ch02_generic_over_param_adt` (run level; suite
now 112) plus a regression test in `tests/test_codegen_monomorphize.py`
pin `gid(MkBox(42))` unwrapping to 42. Mutation-validated: reverting the
`ResultRef` arm to the pre-fix scalar-only logic restores the trap,
flipping the test RED.

Pre-existing on main; found by the PR #888 soundness review.

Co-Authored-By: Claude <[email protected]>

… mono clone (#891)

A generic instantiated over a parameterized ADT — `gid(MkBox(7))` for
`gid : forall<T> fn(@t -> @t)` and `data Box<T> { MkBox(T) }` — passed
`vera check`/`vera verify` but trapped at `vera run` with
`type mismatch: expected i64, found i32` while compiling the `gid$Box`
clone.

Root cause: `_infer_expr_wasm_type`'s `ResultRef` arm
(`vera/wasm/inference.py`) inferred only the scalar primitives and
returned `None` for everything else. Once `T = Box`, the clone's
postcondition `@T.result == @T.0` compares two i32 heap pointers, but the
`ResultRef` (`@Box.result`) defaulted to the scalar i64, so the equality
fell through to the `i64.eq` default while the operands were i32 — an
ill-typed clone body wasmtime rejects at instantiation. The `SlotRef`
operand (`@Box.0`) and the clone's `param`/`result` signature were
already i32; only the postcondition op disagreed.

Fix: the `ResultRef` and `SlotRef` arms now share one
`_ref_type_name_wasm_type` helper, so an ADT-bound (and pair-/handle-bound)
type variable lowers to i32 consistently across the signature and every
slot/result read.

New conformance program `ch02_generic_over_param_adt` (run level; suite
now 112) plus a regression test in `tests/test_codegen_monomorphize.py`
pin `gid(MkBox(42))` unwrapping to 42. Mutation-validated: reverting the
`ResultRef` arm to the pre-fix scalar-only logic restores the trap,
flipping the test RED.

Pre-existing on main; found by the PR #888 soundness review.

Co-Authored-By: Claude <[email protected]>

…rence (#878)

A generic whose type argument must be inferred from a user-fn call's return
type in argument position monomorphized to the Bool phantom-var default: on a
check-green program `vera run` emitted a call to a `$Bool` clone Pass 1.5 never
produced, so the caller (often `main`) was skipped and dropped from the exports
("No exported functions to call"), or a private helper left a dangling `call`
that failed WAT validation.

Root cause is the lossy WAT collapse `i32 -> "Bool"` (a Decimal handle, an ADT,
and an Option/Result pointer are all i32 — the same value as the phantom
default) applied to user-fn returns on both the discovery and the body-emission
sides:

- Discovery (vera/codegen/monomorphize.py): `_build_mono_context` seeded the
  shared `fn_ret_types` from WAT signatures, so a generic bound solely by a
  user-fn return was discovered as `$Bool` while the #732 verifier discovered
  the precise type — a differential desync masked only by identity clone
  bodies. Now seeds from each fn's declared return TypeExpr, exactly as the
  verifier does, with the WAT collapse kept only as a fallback.
- Body-emission (vera/wasm/inference.py): `_get_arg_type_info_wasm` had no
  FnCall branch, so a parameterized return in `Option<VeraT>` position bound
  nothing; and a user-fn call in bare `@VeraT` position collapsed i32 to Bool.
  It now mirrors discovery's FnCall branch (shared _BUILTIN_PARAMETERIZED_RETURNS
  plus a non-generic-user-fn parameterized case) and consults the declared
  return TypeExpr for the ambiguous i32 case. GENERIC calls are excluded from
  the user-fn branch (their declared return is over the callee's own type vars,
  not concrete types) so they fall through to generic-return resolution exactly
  as discovery does — keeping the two consultors in lockstep.

Test values are deliberately Decimal returns (`0.3333...`) that cannot coincide
with the Bool default (1/0), the exact Bool-coincidence trap CLAUDE.md warns
about. New run-level conformance program ch09_generic_infer_user_fn_return (suite
123) plus three regression tests (crash-via-IO, WAT-mangle discriminator,
discovery-vs-verifier differential); each change is independently mutation-
validated. Does not weaken #888's cross-module/closure discovery.

Co-Authored-By: Claude <[email protected]>

…rence (#878)

A generic whose type argument must be inferred from a user-fn call's return
type in argument position monomorphized to the Bool phantom-var default: on a
check-green program `vera run` emitted a call to a `$Bool` clone Pass 1.5 never
produced, so the caller (often `main`) was skipped and dropped from the exports
("No exported functions to call"), or a private helper left a dangling `call`
that failed WAT validation.

Root cause is the lossy WAT collapse `i32 -> "Bool"` (a Decimal handle, an ADT,
and an Option/Result pointer are all i32 — the same value as the phantom
default) applied to user-fn returns on both the discovery and the body-emission
sides:

- Discovery (vera/codegen/monomorphize.py): `_build_mono_context` seeded the
  shared `fn_ret_types` from WAT signatures, so a generic bound solely by a
  user-fn return was discovered as `$Bool` while the #732 verifier discovered
  the precise type — a differential desync masked only by identity clone
  bodies. Now seeds from each fn's declared return TypeExpr, exactly as the
  verifier does, with the WAT collapse kept only as a fallback.
- Body-emission (vera/wasm/inference.py): `_get_arg_type_info_wasm` had no
  FnCall branch, so a parameterized return in `Option<VeraT>` position bound
  nothing; and a user-fn call in bare `@VeraT` position collapsed i32 to Bool.
  It now mirrors discovery's FnCall branch (shared _BUILTIN_PARAMETERIZED_RETURNS
  plus a non-generic-user-fn parameterized case) and consults the declared
  return TypeExpr for the ambiguous i32 case. GENERIC calls are excluded from
  the user-fn branch (their declared return is over the callee's own type vars,
  not concrete types) so they fall through to generic-return resolution exactly
  as discovery does — keeping the two consultors in lockstep.

Test values are deliberately Decimal returns (`0.3333...`) that cannot coincide
with the Bool default (1/0), the exact Bool-coincidence trap CLAUDE.md warns
about. New run-level conformance program ch09_generic_infer_user_fn_return (suite
123) plus three regression tests (crash-via-IO, WAT-mangle discriminator,
discovery-vs-verifier differential); each change is independently mutation-
validated. Does not weaken #888's cross-module/closure discovery.

Co-Authored-By: Claude <[email protected]>

…rence (#878)

A generic whose type argument must be inferred from a user-fn call's return
type in argument position monomorphized to the Bool phantom-var default: on a
check-green program `vera run` emitted a call to a `$Bool` clone Pass 1.5 never
produced, so the caller (often `main`) was skipped and dropped from the exports
("No exported functions to call"), or a private helper left a dangling `call`
that failed WAT validation.

Root cause is the lossy WAT collapse `i32 -> "Bool"` (a Decimal handle, an ADT,
and an Option/Result pointer are all i32 — the same value as the phantom
default) applied to user-fn returns on both the discovery and the body-emission
sides:

- Discovery (vera/codegen/monomorphize.py): `_build_mono_context` seeded the
  shared `fn_ret_types` from WAT signatures, so a generic bound solely by a
  user-fn return was discovered as `$Bool` while the #732 verifier discovered
  the precise type — a differential desync masked only by identity clone
  bodies. Now seeds from each fn's declared return TypeExpr, exactly as the
  verifier does, with the WAT collapse kept only as a fallback.
- Body-emission (vera/wasm/inference.py): `_get_arg_type_info_wasm` had no
  FnCall branch, so a parameterized return in `Option<VeraT>` position bound
  nothing; and a user-fn call in bare `@VeraT` position collapsed i32 to Bool.
  It now mirrors discovery's FnCall branch (shared _BUILTIN_PARAMETERIZED_RETURNS
  plus a non-generic-user-fn parameterized case) and consults the declared
  return TypeExpr for the ambiguous i32 case. GENERIC calls are excluded from
  the user-fn branch (their declared return is over the callee's own type vars,
  not concrete types) so they fall through to generic-return resolution exactly
  as discovery does — keeping the two consultors in lockstep.

Test values are deliberately Decimal returns (`0.3333...`) that cannot coincide
with the Bool default (1/0), the exact Bool-coincidence trap CLAUDE.md warns
about. New run-level conformance program ch09_generic_infer_user_fn_return (suite
123) plus three regression tests (crash-via-IO, WAT-mangle discriminator,
discovery-vs-verifier differential); each change is independently mutation-
validated. Does not weaken #888's cross-module/closure discovery.

Co-Authored-By: Claude <[email protected]>