The type checker currently supports only call-site generic instantiation — when a generic function is called, the type arguments are inferred from the concrete argument types at the call site. There is no Hindley-Milner style global type inference.

This means:

• Generic functions must have their type parameters inferable from call-site arguments
• No let-polymorphism or principal type inference
• Type annotations are always explicit in function signatures

This is by design (explicitness is a core Vera principle), but incremental improvements may be warranted as the language evolves.

Spec reference: This is a known limitation noted in vera/README.md § Current Limitations.