Monomorphized WAT name mangling is non-injective (_mangle_fn_name collides distinct instantiations)

[aallan]

Summary

Monomorphizer._mangle_fn_name (vera/monomorphize.py) builds WAT symbol names by lossy replacement — ct.replace("<", "_").replace(">", "").replace(", ", "_"), joined with _ — so the mapping from instantiation to symbol is not injective. A generic instantiated at a parameterized built-in and at a user type whose name coincides with the mangled form collide to the same $-suffixed symbol:

• g<Map<String, Int>> → g$Map_String_Int
• g<Map_String_Int> (a user ADT literally named Map_String_Int) → g$Map_String_Int

Multi-parameter joins can also collide across the _ boundary: g<A_B, C> vs g<A, B_C> both → g$A_B_C.

Impact

Codegen only. The verifier keeps the original decl.name for its clones (#732) and never mangles, so this is not a verification-soundness issue — vera verify is unaffected. On the codegen side a collision either (a) trips a loud duplicate-symbol error, or (b) routes both instantiations to the first-registered clone (silently wrong). Which one occurs depends on whether Pass 1.5 clone emission has collision detection on the mangled name; needs confirming.

Pre-existing

_mangle_fn_name was relocated verbatim from vera/codegen/monomorphize.py by #732; the non-injectivity predates it. Surfaced by the PR #767 review (CodeRabbit). It is out of scope for #732: a robust fix (escaped, length-prefixed component encoding) changes every monomorphized WAT symbol, churning the byte-identical-WAT baseline that PR is gated on.

Fix

Make the encoding injective — escape _ / < / > / , distinctly, or use length-prefixed components (g$3Map6String3Int-style), so distinct instantiations never share a symbol.

Related

• Per-monomorphization static verification for generic functions #732 / Per-monomorphization static verification for generic functions (#732) #767 — where surfaced.
• Monomorphizer type-inference / reindex completeness gaps (nested unify, builtin-return table, scope-aware De Bruijn) #769 — sibling monomorphizer-precision gaps.