Monomorphization by specialization (doc/eidos.md §4.1, §5, §8): a worklist specializer driven by the type arguments the bridge keeps on application spines. There is no inference and no unification: a monomorphic definition's body mentions a polymorphic definition only as a spine head saturated with closed type arguments (the linter's poly-mode guarantee), so each such spine is a specialization request; the clone is pure type substitution through the audited clone primitive (instantiateDefn), memoized on the normalized argument list. Clones carry their provenance (SpecOrigin) and are named origin$tag, where the tag renders the type arguments (originTag) — so an unrelated instantiation elsewhere never renames a clone.

Polymorphic definitions are templates: they are dropped from the output (their instantiations replace them), so the result is monomorphic (ReWire.Eidos.Lint mono mode) — except the builtin-named definitions (rwPrim*), whose polymorphic signatures carry the builtins' type assumptions to the Eidos-to-Hyle fold (their bodies are error stubs, and they are never referenced as variables — references become Prim occurrences at the bridge); they ride through unchanged. The worklist runs in generations; an instantiation chain deeper than the budget (the historical typechecker bound, raised by --depth) is rejected with the retired specializer's diagnostic.