Monomorphization: key specializations on instantiation identity, not a resolved type

[dpmills]

specialize_use's memo compared two values produced by two different procedures: a candidate's key was resolve_var_type(&use_expr.ty) taken before its pin, while an entry's was clone.ty — the clone's type after the pin and a full re-entrant coalesce. Neither is a faithful identity for what a clone gets specialized to, and the mismatch broke the memo in both directions.

False hits, i.e. a miscompile

A resolved type is a polarity-correct rendering: a domain resolves from upper bounds — what the definition body demands — so a position the body never touches is narrowed away, and an argument's refinement, which arrives as a lower bound of that domain, is invisible unless compact_type's opposite-polarity fallback happens to fire at that exact position. The clone's interior reads its parameter at a positive position and sees precisely those refinements. So two uses differing only in a key-invisible position shared a clone whose interior was resolved against the first use's argument:

h = \a, b -> a + b
h(1, 2) + h(1, 5)

Both uses keyed on ((1, Int) ⇒ Int) — element 0's refinement reached the key, element 1's did not — and the shared clone typed .1 as 2. The post-inline consistency wall then panicked with Type mismatch for Apply: expected 5, found 2. A difference in the first argument keyed apart and compiled fine, so the failure was confined to differences the rendering could not see.

A write-only table

For any definition whose clone type gains a refinement across the pin, no candidate key could ever equal a stored one, so every call site minted its own clone — including character-identical ones — and the table accumulated several entries under one key. The comment justifying the stored key claimed a later same-typed use would resolve through the first pin's extended chains; it cannot, because every use instantiates its own fresh variables, which the first clone's pin never touches.

SpecKey

SpecKey replaces the resolved type. It is the pair of directed reads of the use's instantiation, kept apart: the positive read is the stamping view (a domain from the definition's demands), the negative read is the clone's view (a domain from the argument that flowed in, a codomain from the consumer's demand). The negative read is the load-bearing half — it is the polarity the clone's interior reads its parameter at — and the pair is exhaustive, because use-specific information enters an instantiation through exactly two channels: an arg <: domain edge and a codomain <: demand edge.

Both reads stay directed, which matters: following both bound lists at every variable instead walks out of one use's cone and into every other (two calls' arguments meet at the shared variable of an operator's scheme), so every use keys on the whole program's literals and they all compare equal. Keeping the two views separate matters too — a merged view forgets which direction a contribution came from, and the pin the key stands in for is direction-sensitive. Within a read, merging is always union: a key that narrows can only under-split, and under-splitting is a miscompile while over-splitting is a wasted clone. An under-determined position is one canonical empty view rather than a fresh Infer placeholder, so two unexercised uses can now share.

Both sides of the comparison are now taken by one procedure at one point in the pin's lifecycle, and an entry stores the key of the use that minted it, with a debug_assert that no two entries share a key.

poly_used_directly_and_through_wrapper_shares_specializations drops from five specializations to four: the direct f(1) and the f(y) reached inside g's Int clone instantiate f identically, so they now group onto one specialization — which is what the test's name and its "the memo is per frame, not per demanding region" comment always asked for.

Consequences carried along: ReadPurpose::SpecializationKey becomes Instantiation (that resolution no longer keys anything — it seeds the clone's channel-domain pairings and blames a resolution failure, so its refinement exclusion is now justified by those consumers being refinement-insensitive rather than by the false claim that a refinement the read could not see can only cause a miss); HistoryKind derives Ord so a kind can key a BTreeMap; and a specialize_use doc block that had detached from its function is reattached.

The remaining imprecision is documented on SpecializeFrame::specs and in the new "Keying a specialization" design section: the key summarizes the pin's input, so two uses differing only in a position the clone never reads still key apart. Closing that means keying on the pin's output — the finished clone, deduped structurally — which cannot be a lookup, only a build-then-dedupe. The two compose, so nothing here has to be undone to get there.

Retiring "witness"

The second commit is a vocabulary sweep with no behaviour change. design/type-inference.md defined a witness as "the term for a refinement in its role as a black box to the subtyping lattice", and the word had spread through the solver, the design docs, and four identifiers.

The distinction does not earn a word. We already have base and refinement; "the refinement as the lattice sees it" is a fact about the lattice, not a second kind of object. Worse, the word names precisely a limitation — that the lattice accumulates refinements and matches them by identity instead of reasoning about what they imply — so having a term for it quietly asserts that the limitation is permanent.

So witness → refinement throughout (185 occurrences, 26 files), including join_witnesses → join_refinements and type_carries_witness → type_carries_refinement (channelize), input_witnesses → input_refinements (coalesce), the flag on types_agree_modulo_unread, and the #### Refinements as witness sets section, which becomes #### Refinements on the lattice with an opening sentence that states the opacity as a property of the lattice rather than as the definition of a term.

Testing

Four end-to-end regression cases for the miscompile plus its controls (a difference in a key-visible position, and identical calls that must still share), two unit tests for the memo's two halves, and unit tests for SpecKey itself. Full ./ci.sh passes.

A function's kind is part of its identity

KeyView.fun is keyed by KindMerge, the way KeyView.history is keyed by HistoryKind and for the same reason: 𝐷 ⇒ 𝑉 and 𝐷 ⤇ 𝑉 are one shape that compiles to different code, so a clone pinned at ⤇ — whose body iterates the domain — must not serve a ⇒ use that never supplies one. A union at one position keeps the two apart rather than letting one shadow the other.

The kind is read through KindMerge::of, the same resolved-from-bounds view compaction takes, rather than off the FunKind itself. That distinction is the whole of it: an inferred kind is a variable, freshly minted per instantiation, so keying on its identity would give every use its own key and retire sharing altogether. Its bounds are the answer, and reading them mid-solve is the bargain every other field in the key already makes — the guarantee is agreement with the pin, not omniscience about the graph.

[dpmills]

This change is part of the following stack:

• Monomorphization: key specializations on instantiation identity, not a resolved type #50 ◀
  • Type functions: state a relationship between type variables other than subtyping #51
    • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
      • Annotations stop standing in for binder structure, and stop outliving inference #60
        • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
          • A mutable variable read is an explicit operation, not a subtyping rule #64
            • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62

_{Change managed by git-spice.}

[groundlar]

Reviewed against the design docs, and verified the fix differentially rather than by inspection: built dacbbc2 in an isolated clone and ran the same 12-program probe set against both commits. One real miscompile fixed (h = \a, b -> a + b at h(1,2) + h(1,2) + h(1,5)), zero regressions in the differential, full ./ci.sh green locally.

The design is right, and the two-directed-reads-kept-apart argument — plus the "why not saturate" paragraph, which is the part most people would get wrong — is worth more than the code. Comments below are one structural concern, one follow-up bug that is not yours, and three small documentation asks.

[groundlar]

Context from comparing this against other monomorphizers

Not a blocker — this is the right fix. Two things I turned up that seem worth recording in the design doc, plus one concrete suggestion.

1. The resolved-type key was a fossil of the pre-dce4285 architecture. That commit removed a separate post-coalesce monomorphize pass, whose own doc comment read:

"This is classic monomorphization, deferred until after types are known so it can key specialization on the resolved type — which is what lets one definition be shared across same-typed uses."

Post-coalesce, a resolved type is all you can see: expr.ty has been overwritten and the arena is gone. dce4285 moved specialization into the walk and made var-laden instantiation types available at the point of keying — but the key stayed a resolved type. This PR retires it. Worth a sentence in Keying a specialization, because it makes SpecKey an argument for in-walk specialization rather than a cost of it — the key is only expressible because monomorphization runs where the graph is still live.

2. The key is already a function of the post-emission graph. I ran emit_node alone on let h = λp → p.0 + p.1 in (h(1,2), h(1,N)) — no coalescing, no pin — and computed spec_key on both uses:

	h(1,2) vs h(1,5)	h(1,2) vs h(1,2)
resolve_var_type	((1, Int) ⇒ Int) — equal	equal
spec_key	differ	equal

So the discriminating information is in the graph the instant emission finishes, and the resolved type collides exactly as the commit message describes. The pin transports it across polarity; it doesn't discover it.

That suggests a cheap test, and it closes the verification gap I raised on SpecializeFrame::specs: assert that spec_key taken right after emission equals spec_key taken at specialization time. That turns "both sides computed by one procedure at one point in the pin's lifecycle" from a discipline into a checked property, and it would fail loudly if a future change made the key sensitive to intervening pins.

3. Where Cambra sits relative to everyone else — the framing I'd suggest for that design-doc paragraph. rustc keys on Instance { def, args }, frozen by typeck; C++ on the template-argument list; Swift on a substitution map; MLton on the type-argument list in a single post-inference pass. All of them key on a finished value, because their generic bodies are already typed and instantiation is substitution.

Cambra has no Type::ForAll and never types a generic body at all ("The definition's own subtree is never coalesced in place"), so monomorphization here is the act of typing the body, not duplication of already-typed code. That puts us in C++'s category — the one mainstream compiler where instantiation genuinely re-runs semantic analysis rather than substituting — and it is the real reason the key must be read off a live graph. A reader arriving from rustc will otherwise assume that's an implementation choice.

For completeness on what is not the reason: poly-calls-poly doesn't block a phase split. Discovering the set of instantiations is a reachability fixpoint in every monomorphizer (rustc's collector, Swift's pass-manager worklist), and the pre-dce4285 pass handled it by recursing into each new specialization. The cost of deferral is only that coalesce destructively overwrites expr.ty — which is why that pass also needed rederive_dependent_types.

Prior art worth a look: Lutze, Schuster & Brachthäuser, The Simple Essence of Monomorphization (OOPSLA 2025) — monomorphization via a flow analysis explicitly inspired by algebraic subtyping (Dolan & Mycroft), i.e. this type system. Closest prior art I found, including on where monomorphization stops being possible (polymorphic recursion, which they detect as cyclic flow).

[dpmills]

Context from comparing this against other monomorphizers

Not a blocker — this is the right fix. Two things I turned up that seem worth recording in the design doc, plus one concrete suggestion.

1. The resolved-type key was a fossil of the pre-dce4285 architecture. That commit removed a separate post-coalesce monomorphize pass, whose own doc comment read:

"This is classic monomorphization, deferred until after types are known so it can key specialization on the resolved type — which is what lets one definition be shared across same-typed uses."

Post-coalesce, a resolved type is all you can see: expr.ty has been overwritten and the arena is gone. dce4285 moved specialization into the walk and made var-laden instantiation types available at the point of keying — but the key stayed a resolved type. This PR retires it. Worth a sentence in Keying a specialization, because it makes SpecKey an argument for in-walk specialization rather than a cost of it — the key is only expressible because monomorphization runs where the graph is still live.

Added

2. The key is already a function of the post-emission graph. I ran emit_node alone on let h = λp → p.0 + p.1 in (h(1,2), h(1,N)) — no coalescing, no pin — and computed spec_key on both uses:

h(1,2) vs h(1,5) h(1,2) vs h(1,2)
resolve_var_type ((1, Int) ⇒ Int) — equal equal
spec_key differ equal
So the discriminating information is in the graph the instant emission finishes, and the resolved type collides exactly as the commit message describes. The pin transports it across polarity; it doesn't discover it.

That suggests a cheap test, and it closes the verification gap I raised on SpecializeFrame::specs: assert that spec_key taken right after emission equals spec_key taken at specialization time. That turns "both sides computed by one procedure at one point in the pin's lifecycle" from a discipline into a checked property, and it would fail loudly if a future change made the key sensitive to intervening pins.

Once we have #51, this isn't entirely true. I added a section discussing

3. Where Cambra sits relative to everyone else — the framing I'd suggest for that design-doc paragraph. rustc keys on Instance { def, args }, frozen by typeck; C++ on the template-argument list; Swift on a substitution map; MLton on the type-argument list in a single post-inference pass. All of them key on a finished value, because their generic bodies are already typed and instantiation is substitution.

Cambra has no Type::ForAll and never types a generic body at all ("The definition's own subtree is never coalesced in place"), so monomorphization here is the act of typing the body, not duplication of already-typed code. That puts us in C++'s category — the one mainstream compiler where instantiation genuinely re-runs semantic analysis rather than substituting — and it is the real reason the key must be read off a live graph. A reader arriving from rustc will otherwise assume that's an implementation choice.

For completeness on what is not the reason: poly-calls-poly doesn't block a phase split. Discovering the set of instantiations is a reachability fixpoint in every monomorphizer (rustc's collector, Swift's pass-manager worklist), and the pre-dce4285 pass handled it by recursing into each new specialization. The cost of deferral is only that coalesce destructively overwrites expr.ty — which is why that pass also needed rederive_dependent_types.

Prior art worth a look: Lutze, Schuster & Brachthäuser, The Simple Essence of Monomorphization (OOPSLA 2025) — monomorphization via a flow analysis explicitly inspired by algebraic subtyping (Dolan & Mycroft), i.e. this type system. Closest prior art I found, including on where monomorphization stops being possible (polymorphic recursion, which they detect as cyclic flow).

Added this discussion to the design