Summary
A generic function imported from another module and instantiated only by the importer is monomorphized nowhere, so the call crashes at run time. The importer's monomorphization discovery builds from its local program.declarations (the imported generic isn't in generic_decls), and the defining module only monomorphizes its own instantiations. The emitted WAT then references the un-monomorphized bare name (call $gid), which has no implementation.
Repro (two modules)
genmod.vera:
public forall<T> fn gid(@T -> @T)
requires(true) ensures(@T.result == @T.0) effects(pure) { @T.0 }
main.vera:
import genmod;
public fn main(@Unit -> @Int)
requires(true) ensures(true) effects(pure) { gid(42) }
vera check main.vera → OK; vera run main.vera → fails at call $gid (the gid$Int clone was never emitted). The qualified form (genmod::gid(42)) crashes identically.
Root cause
Cross-module generic monomorphization isn't implemented. To fix, the importer must discover instantiations of imported generics and emit their clones — monomorphizing a body defined in another module with that module's registration context (helpers, ADTs, prelude). The #732 differential test (test_imported_generic_symmetric_between_codegen_and_verifier) pins the current symmetric "neither side monomorphizes imported generics" behavior as a forward-compatibility tripwire: closing this gap must move codegen discovery and the verifier's discovery in lockstep, or it reintroduces a false Tier-1.
Note on a related review comment
A #767 CodeRabbit review flagged this as "generic-instantiation discovery only matches ast.FnCall, not ModuleCall / QualifiedCall." That's a mis-diagnosis: the unqualified call crashes too, and the imported generic isn't in the importer's generic_decls, so adding qualified-call handling alone wouldn't create the instance. The real gap is cross-module monomorphization.
Pre-existing
The importer has never monomorphized imported generics; #732 added the differential test that documents the symmetric behavior.
Related
Summary
A generic function imported from another module and instantiated only by the importer is monomorphized nowhere, so the call crashes at run time. The importer's monomorphization discovery builds from its local
program.declarations(the imported generic isn't ingeneric_decls), and the defining module only monomorphizes its own instantiations. The emitted WAT then references the un-monomorphized bare name (call $gid), which has no implementation.Repro (two modules)
genmod.vera:main.vera:vera check main.vera→ OK;vera run main.vera→ fails atcall $gid(thegid$Intclone was never emitted). The qualified form (genmod::gid(42)) crashes identically.Root cause
Cross-module generic monomorphization isn't implemented. To fix, the importer must discover instantiations of imported generics and emit their clones — monomorphizing a body defined in another module with that module's registration context (helpers, ADTs, prelude). The #732 differential test (
test_imported_generic_symmetric_between_codegen_and_verifier) pins the current symmetric "neither side monomorphizes imported generics" behavior as a forward-compatibility tripwire: closing this gap must move codegen discovery and the verifier's discovery in lockstep, or it reintroduces a false Tier-1.Note on a related review comment
A #767 CodeRabbit review flagged this as "generic-instantiation discovery only matches
ast.FnCall, notModuleCall/QualifiedCall." That's a mis-diagnosis: the unqualified call crashes too, and the imported generic isn't in the importer'sgeneric_decls, so adding qualified-call handling alone wouldn't create the instance. The real gap is cross-module monomorphization.Pre-existing
The importer has never monomorphized imported generics; #732 added the differential test that documents the symmetric behavior.
Related