Lesson 7.7 — Type classes and traits: instance resolution, coherence, dictionaries vs monomorphization¶

Techniques: instance resolution — solving class constraints $C\ \tau$ by matching instance heads and recursing on their contexts, with superclasses and defaulting (Wadler & Blott 1989 [WB89]; Jones's qualified types [Jon94]; GHC's matchGlobalInst; rustc's trait selection); coherence — every constraint has at most one solution, enforced by non-overlapping instances and Rust's orphan rules (RFC 1023/2451 [RFC1023, RFC2451]); dictionary passing vs monomorphization — compiling constrained polymorphism by passing evidence at run time (GHC, [HHPW96]) or by specializing every instance (rustc, GHC's SPECIALIZE) · Pebble implements: none (Pebble has no generics); the lab's ★ milestone L5 implements Eq by dictionary passing for MiniML (labs/ch07-hm §6) · Drills: — (see §9) · Prerequisites: Lessons 7.2, 7.4; Lesson 6.9 (monomorphization, erasure, dictionaries) · Time: 5 hours

Lesson 6.9 compared how generics are compiled. This lesson is about how the type checker decides which code a constrained call needs. member x xs = x == y || … is polymorphic in the element type but uses ==, so its type is Eq a => a -> [a] -> Bool: HM(X) with X = type classes (Lesson 7.4). Inference produces the constraint; instance resolution proves it for concrete types and produces evidence (a dictionary); coherence guarantees that the evidence is unique, so the program's meaning does not depend on which proof the checker found; and the evidence becomes either an extra run-time argument or a specialized copy of the code.

1. Problem and motivation¶

Instance resolution¶

The problem. Ad-hoc polymorphism — one name, different code per type — was handled by overloading resolved at each use (C++, Ada, Lesson 6.3), which does not combine with HM: an overloaded == inside a polymorphic member has no single type. Wadler and Blott [WB89] introduced type classes: a class declares the overloaded methods (class Eq a where (==) :: a -> a -> Bool), instances provide them per type, possibly under a context (instance Eq a => Eq [a]), and inference simply collects predicates Eq τ in the constraint. Deciding a predicate for a concrete type is a small logic program — instance heads are Horn clauses — and its proof tree is the dictionary. Rust's traits are the same idea with explicit bounds on generic parameters; rustc's trait selection plays the role of instance resolution.

Coherence¶

The problem. If two instances could prove Show [Char] (a general one for lists and a special one for strings), the meaning of show "abc" would depend on which proof the checker picked — possibly a different one in two modules that are compiled separately and later linked. Coherence is the property that every constraint has at most one proof, so the program's behavior is independent of the checker's search. Haskell 98 enforces it by forbidding overlapping instance heads; Rust enforces it globally with orphan rules (an impl must be in the crate of the trait or of the type) and an overlap check [RFC1023, RFC2451], because Rust links crates it cannot see together at type-checking time.

Dictionary passing vs monomorphization¶

The problem. After type checking, a function with a constraint Eq a must still get the right == at run time. Dictionary passing [WB89, HHPW96] turns each constraint into an extra parameter: member :: Eq a -> a -> [a] -> Bool receives a record (for a one-method class, just the method), and each call site builds the dictionary from instance functions ($fEq[] $fEqInt for Eq [Int]). One compiled copy serves all types, polymorphic recursion works, and separate compilation is easy; every method call is indirect. Monomorphization compiles a copy per instantiation, with the method calls resolved statically — Rust and C++ always, GHC when told to (SPECIALIZE) or when it can see the call site. Lesson 6.9 measured code size; here the question is how the evidence produced by resolution becomes code in each scheme.

2. Definitions and algorithms¶

Definition 7.7.1 (Classes, instances, programs of Horn clauses)

A class $C$ has one type parameter and a set of methods. An instance declaration $\forall\vec\alpha.\ P_1, \dots, P_k \Rightarrow C\ \tau$ has a head $C\ \tau$ ($\tau$ a type constructor applied to distinct variables, in Haskell 98) and a context $P_1, \dots, P_k$ of predicates on $\vec\alpha$. Read logically it is the Horn clause $P_1 \wedge \dots \wedge P_k \to C\ \tau$. A superclass declaration class Eq a => Ord a adds the clause $\mathrm{Ord}\ a \to \mathrm{Eq}\ a$ (used only to simplify constraints, never to search instances).

Definition 7.7.2 (Evidence)

Evidence for $C\ \tau$ is a term that computes the methods of $C$ at $\tau$: for a predicate $C\ \alpha$ on a quantified variable, a dictionary parameter $d$; for an instance $\forall\vec\alpha.\ \vec P \Rightarrow C\ (T\ \vec\alpha)$ applied at $\vec\alpha = \vec\tau$, the instance function applied to evidence for $[\vec\tau/\vec\alpha]\vec P$ (eqList eqInt for $\mathrm{Eq}\ [\mathsf{Int}]$).

Definition 7.7.3 (Coherence; orphans; overlap)

A program is coherent if every closed predicate has at most one evidence term up to observational equivalence. Two instance heads overlap if they unify. An instance of class $C$ for type constructor $T$ is an orphan in module (crate) $M$ if neither $C$ nor $T$ is defined in $M$ (Rust's precise rule allows local types behind uncovered parameters [RFC2451]).

Instance resolution¶

Algorithm 7.7.4 (Instance resolution with evidence: context reduction)

Input: a predicate $C\ \tau$, the instance clauses, the givens (dictionary parameters in scope for predicates on quantified variables).
Output: an evidence term, or "no instance", or a residual predicate on a type variable (to be quantified or reported as ambiguous).
Precondition: instance heads do not overlap (coherence), so at most one clause matches.
Postcondition: the evidence has type "dictionary of $C$ at $\tau$" (Theorem 7.7.7).
Invariant: each recursive call is on a strictly smaller type (Haskell 98's instance restrictions), so resolution terminates.

function Resolve(C τ, givens):
    τ ← dereference(τ)
    if τ is a type variable α:
        if some given d proves C α:  return d
        return residual(C α)                           # quantify at let, or ambiguity
    find the instance ∀ᾱ. P1…Pk ⇒ C (T ᾱ) whose head matches τ = T τ̄
    if none: fail "no instance C τ"                      # E0277 in rustc
    args ← [Resolve([τ̄/ᾱ] Pi, givens) for i = 1..k]      # the context, instantiated
    return InstanceFunction(C, T) applied to args

function Generalize-with-classes(Γ, τ, P):              # at a let (Lesson 7.4, Algorithm 7.4.4)
    P' ← context-reduce every predicate of P with Resolve (keeping residuals)
    for each residual C α:
        if α ∈ ftv(Γ):                     leave it to the enclosing binding
        elif α ∈ ftv(τ) and α generalized: add a dictionary parameter d_α
        else:                               fail "ambiguous"   (or default: Lesson 7.6)

Coherence¶

Algorithm 7.7.5 (Coherence checks: overlap and orphans)

Input: the instance (impl) declarations of a module (crate) and those visible from its dependencies.
Output: errors for overlapping heads and for orphan instances.
Precondition: instance heads are types with variables; matching is first-order unification (Lesson 7.1).
Postcondition: in an accepted program no two instances can prove the same closed predicate (Theorem 7.7.8), even across separately compiled modules.
Invariant: every instance is checked against every instance of the same class that is visible (local or from a dependency).

function CheckCoherence(M):
    for each instance I = (∀ᾱ. P ⇒ C τ) declared in M:
        if C is not defined in M and the head constructor of τ is not defined in M:
            error "orphan instance"                      # Rust E0117
        for each visible instance J = (∀β̄. Q ⇒ C σ), J ≠ I:
            rename β̄ apart from ᾱ
            if Unify(τ, σ) succeeds:                     # some type matches both heads
                error "overlapping instances" at I       # Rust E0119, GHC at use sites

Dictionary passing vs monomorphization¶

Algorithm 7.7.6 (The two translations of a constrained binding)

Input: a binding $f : \forall\vec\alpha.\ \vec P \Rightarrow \tau$ with body $e$, and its call sites with the evidence found by Algorithm 7.7.4.
Output: dictionary passing: one function with $\lvert\vec P\rvert$ extra parameters; monomorphization: one copy per distinct instantiation reached from the entry points.
Precondition: every constraint of $e$ was resolved to evidence mentioning only $f$'s dictionary parameters (or constants).
Postcondition: both translations compute the same values (Theorem 7.7.9); monomorphization needs the set of instantiations to be finite.
Invariant: dictionary passing: every method call reads its dictionary argument; monomorphization: every method call is resolved to one instance's code.

function DictTranslate(f, P̄ ⇒ τ, e):                    # the lab's L5, GHC's desugarer
    emit  f = fun d_1 -> … -> fun d_k -> ⟦e⟧
    where ⟦m⟧ for an overloaded method m at C τ' = Resolve(C τ', {d_i})   # the method itself
          ⟦g⟧ for a constrained g at instance θ   = g applied to Resolve(θ Q_j) for each Q_j
function Monomorphize(entry):                           # rustc_monomorphize's collector
    worklist ← [(entry, [])];  done ← {}
    while worklist not empty:
        (f, θ) ← pop;  if (f, θ) ∈ done: continue;  add it
        emit f_θ = θ(body of f) with every method call m at θ(C τ') replaced by the instance's code
        for each call g at instantiation θ' in θ(body of f): push (g, θ')

3. Worked example¶

The lab's ★ corpus program corpus-classes/04-member.mml, with the overloaded eq : Eq 'a => 'a -> 'a -> bool:

let rec member = fun x -> fun l ->
  if isnil l then false
  else if eq x (head l) then true
  else member x (tail l)
in (member 2 (cons 1 (cons 2 nil)), member true (cons false nil))

Instance resolution¶

step	where	constraint	resolution	evidence
1	`eq x (head l)` inside `member`	$\mathrm{Eq}\ \alpha$, $\alpha$ = the type of `x` (level 2)	variable: residual	—
2	generalizing `member`	residual $\mathrm{Eq}\ \alpha$, $\alpha \in \mathrm{ftv}(\tau)$, generalized	dictionary parameter	`_d1`
3	`member 2 …`	$\mathrm{Eq}\ \mathsf{int}$	instance `Eq int`, empty context	`eqInt`
4	`member true …`	$\mathrm{Eq}\ \mathsf{bool}$	instance `Eq bool`	`eqBool`

The recursive call member x (tail l) inside the body is at the same instance (monomorphic recursion), so it passes _d1 along. The reference elaborate (solutions/labs/ch07-hm/classes/Classes.cpp) prints the translation

let rec member = fun _d1 -> fun x -> fun l -> if isnil l then false
  else if _d1 x (head l) then true else member _d1 x (tail l)
in (member eqInt 2 (cons 1 (cons 2 nil)), member eqBool true (cons false nil))

and the provided evaluator runs it to (true, false), the corpus's # value. For a compound predicate — corpus-classes/06-neq.mml needs $\mathrm{Eq}\ ((\mathsf{int} \times \mathsf{bool})\ \mathsf{list})$ — the recursion of Algorithm 7.7.4 builds eqList (eqPair eqInt eqBool): one instance per level of the type.

Coherence¶

Suppose a second instance Eq 'a list existed beside Eq 'a => Eq ('a list). Algorithm 7.7.5 unifies the heads 'a list and 'b list (renamed apart): success with $\alpha = \beta$ — the instances overlap, and eq nil nil at int list would have two different evidence terms. GHC reports such overlap at the use site (§7), Rust at the second impl.

Dictionary passing vs monomorphization¶

instantiation	dictionary passing	monomorphization
`member` at `int`	the one `member`, called with `eqInt`	`member_int`, with `eqInt` inlined at the call of `eq`
`member` at `bool`	the same `member`, with `eqBool`	`member_bool`
code copies	1	2 (one per instantiation reached)
cost per `eq`	an indirect call through `_d1`	a direct (inlinable) comparison

4. Invariants and correctness¶

Instance resolution¶

Theorem 7.7.7 (Resolution is sound and terminates)

Under Haskell 98's instance restrictions (heads are constructors applied to distinct variables, contexts mention only those variables), Algorithm 7.7.4 terminates, and whenever it returns evidence $E$ for $C\ \tau$, $E$ has the type of a $C$-dictionary at $\tau$; if it fails with "no instance", no evidence exists.

Proof

Termination: each recursive call is on $[\vec\tau/\vec\alpha]P_i$ where $P_i$ is a predicate on one of the variables $\alpha_j$, so its type is $\tau_j$, a proper subterm of $T\ \vec\tau$; the size of the type decreases strictly. Soundness, by induction on the recursion: a given $d$ has the dictionary type by assumption; an instance function for $\forall\vec\alpha.\ \vec P \Rightarrow C\ (T\ \vec\alpha)$ has type $D_{P_1} \to \dots \to D_{P_k} \to D_{C (T \vec\alpha)}$, instantiated at $\vec\tau$, and the arguments have the instantiated $D_{P_i}$ types by the induction hypothesis. Completeness of failure: evidence for $C\ (T\ \vec\tau)$ can only be built from an instance whose head matches $T\ \vec\tau$ (instance functions are the only constructors of dictionaries); if none matches, none exists; if one matches (unique by coherence), its context must be proved, and the induction hypothesis covers the recursive failures.

Coherence¶

Theorem 7.7.8 (No overlap and no orphans give global coherence)

If no two visible instances of a class have unifiable heads, every closed predicate has at most one evidence term built by Algorithm 7.7.4. If moreover no module declares an orphan instance, this holds for any combination of separately checked modules.

Proof

Uniqueness: by induction on the type in the predicate. For $C\ (T\ \vec\tau)$, an evidence term starts with the instance function of an instance whose head matches $T\ \vec\tau$. If two instances $I, J$ matched, their heads would both have $T\ \vec\tau$ as an instance, so they would unify (the substitution sending each head to $T\ \vec\tau$, after renaming apart, is a unifier) — excluded. The arguments are evidence for smaller predicates, unique by the induction hypothesis. Across modules: an instance of $C$ for $T$ can only live in the module of $C$ or of $T$; any program that uses $C\ (T \dots)$ depends on both modules, so it sees every instance that could match, and the overlap check performed when the later of the two modules was compiled covers the pair. Without the orphan rule, two unrelated modules could each declare C T without seeing each other, and a third module importing both would be incoherent.

Dictionary passing vs monomorphization¶

Theorem 7.7.9 (The translations agree)

For a coherent program whose instantiations are finite, the dictionary-passing translation and the monomorphized program compute the same value; the dictionary translation of a well-typed program is itself well typed in the language without classes.

Proof sketch (full proof of the dictionary translation: [HHPW96, §5]; the course checks it on the lab corpus)

Typing of the translation: by induction on the typing derivation, replacing each constrained scheme $\forall\vec\alpha.\ \vec P \Rightarrow \tau$ by $\forall\vec\alpha.\ D_{\vec P} \to \tau$ and each Inst of such a scheme by an application to the evidence of Theorem 7.7.7. Agreement: monomorphization is dictionary passing followed by partial evaluation: each specialized copy $f_\theta$ is $f$ with its dictionary parameters bound to the (unique, by Theorem 7.7.8) closed evidence for $\theta\vec P$ and the resulting dictionary selections inlined — $\beta$-reduction, which preserves values in a pure language. Finiteness is needed only so that the specialization terminates (Lesson 6.9, Theorem 6.9.7 for polymorphic recursion). ch07.HM.L5_Classes_Corpus evaluates every translation and compares with the expected value.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Instance resolution	$O(\lvert\tau\rvert)$ per predicate under Haskell 98 rules; undecidable with unrestricted instances (bounded by GHC's reduction depth, rustc's `recursion_limit`)	a few steps per call site	evidence terms of size $O(\lvert\tau\rvert)$	$\tau$ the constrained type
Coherence checks	$O(i^2 \cdot s)$ pairwise overlap per class (indexed by head constructor in practice)	linear with indexing	none	$i$ instances, $s$ head size
Dictionary passing	one copy of each function; $O(1)$ extra argument per constraint, an indirect call per method	slower inner loops unless specialized	dictionaries at run time	$p$ constraints
Monomorphization	code size $\sum_f \lvert\mathrm{inst}(f)\rvert \cdot \lvert f \rvert$, exponential in the worst case	fast code, long compile times	copies	$\mathrm{inst}(f)$ instantiations of $f$

Justification. Resolution: Theorem 7.7.7's measure; each step does one head match ($O(s)$). Overlap: each pair of instances is unified once. Monomorphization: each reachable instantiation is emitted once by the collector's worklist.

Pathological families. (1) Evidence doubling: the x_i family of Lesson 7.4 §5 gives $x_n$ a scheme with $2^n$ Eq constraints, i.e. $2^n$ dictionary parameters — dictionary passing turns a type-level blow-up into an argument-list blow-up. (2) Instance explosion under monomorphization: f0 x = x == x; f1 x = f0 (x, x); …; fn x = f(n-1) (x, x) instantiates $f_0$ at a type of size $2^n$; each level adds one copy, but the Eq evidence for the nested pairs is a tree of $2^{n}$ eqPair applications that monomorphization turns into straight-line code of that size. (3) Non-termination: with UndecidableInstances, instance C [[a]] => C [a] makes resolution of C [Int] loop; GHC stops at its reduction depth.

Instance resolution¶

Multi-parameter classes and functional dependencies / associated types (Jones; Chakravarty et al.): classes over several types, with dependencies that let resolution improve (unify) type variables. Trade-off: more expressive; resolution can bind types, so termination and coherence need stronger conditions.
Defaulting (Haskell's default (Integer, Double); Pebble's literal defaulting, Lesson 7.6): pick a type for an ambiguous numeric constraint. Trade-off: fewer annotations; the chosen type can surprise (Integer vs Int).
Trait selection with auto traits and negative reasoning (rustc): Send/Sync are proved structurally. Trade-off: fewer impls to write; semver hazards when a field's type changes.

Coherence¶

Overlapping instances with most-specific selection (GHC {-# OVERLAPPING #-}, Rust's unstable specialization): allow overlap if one head is strictly more specific. Trade-off: useful (a fast path for String), but coherence then depends on which instances are visible where the constraint is solved.
Orphans allowed with warnings (GHC -Worphans): Haskell permits orphans and warns. Trade-off: flexibility for the library ecosystem; incoherence possible across packages.
Named or local instances (Scala implicits, OCaml modular implicits): several instances coexist and are chosen by scope. Trade-off: no global coherence, so data structures that rely on one Ord (sets) can break.

Dictionary passing vs monomorphization¶

Specialization in GHC (SPECIALIZE pragmas, -fspecialise across modules): generate monomorphic copies for chosen types and rewrite calls with rules. Trade-off: speed where it matters, one generic copy elsewhere.
Witness tables (Swift, Lesson 6.9): dictionaries plus type metadata, so unboxed values of unknown size can be handled generically. Trade-off: generic code works across library boundaries (ABI stability); specialization recovers speed within a module.
Trait objects (dyn Trait in Rust): a dictionary (vtable) attached to a value rather than passed per call. Trade-off: heterogeneous collections; one indirect call per method, no generics needed.

7. In real compilers¶

Instance resolution¶

GHC solves class constraints in its constraint solver; top-level instance lookup is matchGlobalInst in compiler/GHC/Tc/Instance/Class.hs [GHC-Class], and unsolved constraints on inferred bindings are quantified by simplifyInfer [GHC-Solver]. rustc's trait selection is SelectionContext::select in compiler/rustc_trait_selection/src/traits/select/mod.rs [RUSTC-Select].

A failed trait obligation in rustc 1.94

Reproduce (rustc 1.94.1):

mkdir -p rs && cat > rs/select.rs <<'EOF'
#[derive(Debug)]
struct Point { x: i32, y: i32 }

fn member<T: PartialEq>(x: &T, xs: &[T]) -> bool { xs.iter().any(|y| y == x) }

fn main() {
    let ok = member(&vec![1, 2], &[vec![1, 2]]);     // PartialEq for Vec<i32>: via PartialEq for i32
    let bad = member(&Point { x: 0, y: 0 }, &[]);    // no impl PartialEq for Point
    println!("{} {}", ok, bad);
}
EOF
rustc --edition 2021 rs/select.rs -o rs/select

Output (complete):

error[E0277]: can't compare `Point` with `Point`
 --> rs/select.rs:8:15
  |
8 |     let bad = member(&Point { x: 0, y: 0 }, &[]);    // no impl PartialEq for Point
  |               ^^^^^^ no implementation for `Point == Point`
  |
  = help: the trait `PartialEq` is not implemented for `Point`
note: required by a bound in `member`
 --> rs/select.rs:4:14
  |
4 | fn member<T: PartialEq>(x: &T, xs: &[T]) -> bool { xs.iter().any(|y| y == x) }
  |              ^^^^^^^^^ required by this bound in `member`
help: consider annotating `Point` with `#[derive(PartialEq)]`
  |
2 + #[derive(PartialEq)]
3 | struct Point { x: i32, y: i32 }
  |

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0277`.

What to notice: line 7's obligation Vec<i32>: PartialEq is proved by the impl for Vec<T> whose context requires i32: PartialEq — two steps of Algorithm 7.7.4, silently. Line 8's Point: PartialEq matches no impl head: "no instance", reported with the bound that created the obligation (the call's instantiation).

Coherence¶

rustc checks orphans in orphan_check_impl (compiler/rustc_hir_analysis/src/coherence/orphan.rs) and overlap with overlapping_trait_impls in compiler/rustc_trait_selection/src/traits/coherence.rs [RUSTC-Coherence]. GHC detects overlap lazily, when a constraint matches several instances.

Orphans and overlap in rustc 1.94; overlap at a use site in GHC 9.4

Reproduce (rustc 1.94.1, GHC 9.4.7):

mkdir -p rs hs && cat > rs/coherence.rs <<'EOF'
use std::fmt;

impl fmt::Display for Vec<u8> {                 // orphan: neither the trait nor the type is ours
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { write!(f, "bytes") }
}

trait Describe { fn describe(&self) -> String; }
impl<T: fmt::Debug> Describe for T {
    fn describe(&self) -> String { format!("{:?}", self) }
}
impl Describe for i32 {                          // overlaps the blanket impl
    fn describe(&self) -> String { String::from("an i32") }
}

fn main() {}
EOF
rustc --edition 2021 rs/coherence.rs -o rs/coh
cat > hs/Overlap.hs <<'EOF'
{-# LANGUAGE FlexibleInstances #-}
module Overlap where

class Describe a where describe :: a -> String
instance Describe [a] where describe _ = "a list"
instance Describe [Char] where describe s = "the string " ++ s

d :: String
d = describe "pebble"
EOF
LC_ALL=C ghc -fno-code hs/Overlap.hs

Output (the GHC [1 of 1] Compiling line removed):

error[E0117]: only traits defined in the current crate can be implemented for types defined outside of the crate
 --> rs/coherence.rs:3:1
  |
3 | impl fmt::Display for Vec<u8> {                 // orphan: neither the trait nor the type is ours
  | ^^^^^^^^^^^^^^^^^^^^^^-------
  |                       |
  |                       `Vec` is not defined in the current crate
  |
  = note: impl doesn't have any local type before any uncovered type parameters
  = note: for more information see https://doc.rust-lang.org/reference/items/implementations.html#orphan-rules
  = note: define and implement a trait or new type instead

error[E0119]: conflicting implementations of trait `Describe` for type `i32`
  --> rs/coherence.rs:11:1
   |
 8 | impl<T: fmt::Debug> Describe for T {
   | ---------------------------------- first implementation here
...
11 | impl Describe for i32 {                          // overlaps the blanket impl
   | ^^^^^^^^^^^^^^^^^^^^^ conflicting implementation for `i32`

error: aborting due to 2 previous errors

Some errors have detailed explanations: E0117, E0119.
For more information about an error, try `rustc --explain E0117`.
hs/Overlap.hs:9:5: error:
    * Overlapping instances for Describe String
        arising from a use of `describe'
      Matching instances:
        instance Describe [Char] -- Defined at hs/Overlap.hs:6:10
        instance Describe [a] -- Defined at hs/Overlap.hs:5:10
    * In the expression: describe "pebble"
      In an equation for `d': d = describe "pebble"
  |
9 | d = describe "pebble"
  |     ^^^^^^^^

What to notice: Rust applies Algorithm 7.7.5 eagerly: the orphan rule (E0117) and the head unification T vs i32 (E0119) are checked at the impls. GHC accepts both instance declarations and reports the overlap only when a constraint (Describe String) matches both heads — the same unification, performed at resolution time.

Dictionary passing vs monomorphization¶

GHC desugars evidence into Core arguments ($dEq parameters, $fEq[] instance functions) and specializes with SPECIALIZE rules; rustc's collector collect_crate_mono_items in compiler/rustc_monomorphize/src/collector.rs enumerates the instantiations to emit [RUSTC-Mono].

The same member in GHC 9.4 Core and in rustc 1.94 symbols

Reproduce (GHC 9.4.7, rustc 1.94.1):

mkdir -p hs rs && cat > hs/Dict.hs <<'EOF'
module Dict (member, useIt) where

member :: Eq a => a -> [a] -> Bool
member _ []     = False
member x (y:ys) = x == y || member x ys
{-# NOINLINE member #-}

useIt :: Bool
useIt = member [1 :: Int] [[2], [1]]
EOF
LC_ALL=C ghc -O0 -fforce-recomp -ddump-simpl -dsuppress-all -dsuppress-uniques -dno-typeable-binds hs/Dict.hs
cat > rs/mono.rs <<'EOF'
#[inline(never)]
fn member<T: PartialEq>(x: &T, xs: &[T]) -> bool {
    xs.iter().any(|y| y == x)
}

fn main() {
    let a = member(&1i32, &[2, 1]);
    let b = member(&"b", &["a", "b"]);
    let c = member(&vec![1u8], &[vec![2], vec![1]]);
    println!("{} {} {}", a, b, c);
}
EOF
rustc --edition 2021 -C opt-level=0 -C symbol-mangling-version=v0 rs/mono.rs -o rs/mono && ./rs/mono
nm -C rs/mono | grep ' mono::member' | cut -d' ' -f3- | sort

Output (the GHC [1 of 1] Compiling line removed):

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 38, types: 36, coercions: 0, joins: 0/0}

Rec {
member
  = \ @a $dEq ds ds1 ->
      case ds1 of {
        [] -> False;
        : y ys -> || (== $dEq ds y) (member $dEq ds ys)
      }
end Rec }

useIt
  = member
      ($fEq[] $fEqInt)
      (: (I# 1#) [])
      (: (: (I# 2#) []) (: (: (I# 1#) []) []))

true true true
mono::member::<&str>
mono::member::<&str>::{closure#0}
mono::member::<alloc::vec::Vec<u8>>
mono::member::<alloc::vec::Vec<u8>>::{closure#0}
mono::member::<i32>
mono::member::<i32>::{closure#0}

What to notice: GHC compiles one member that takes the dictionary $dEq and calls == through it; the call site builds Eq [Int] as $fEq[] $fEqInt — Algorithm 7.7.4's evidence term, exactly the lab's eqList eqInt. rustc emits three copies, one per instantiation the collector reached (Algorithm 7.7.6's Monomorphize). (Blank lines of GHC's dump are kept; an empty line separates the two tools' outputs.)

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Instance resolution	Overloading that composes with HM; evidence per predicate (Theorem 7.7.7); undecidable with unrestricted instances	$O(\lvert\tau\rvert)$ per predicate under H98 rules	"no instance" / E0277 with the originating bound; ambiguity errors	Medium: a small logic-program solver with evidence	Haskell, Rust, Scala, Swift, Lean
Coherence	At most one evidence per closed predicate, globally (Theorem 7.7.8)	pairwise head unification, indexed	Rust: errors at the impl (E0117, E0119); GHC: at the use site	Low for the checks; the orphan rule is a language-design decision	Rust (strict), Haskell (overlap check, orphans warned), not Scala
Dictionary passing	One copy; polymorphic recursion and separate compilation work (Theorem 7.7.9)	indirect call per method; GHC specializes hot paths	Generic code errors once, at the definition	Low: extra parameters in the translation	GHC by default, Swift witness tables, the lab's L5
Monomorphization	Fastest code; needs finitely many instantiations	code size grows with instantiations (§5)	Errors per generic definition (Rust) or per instance (C++)	Medium: a collector, symbol mangling	Rust, C++, GHC with `SPECIALIZE`

Choose type classes / traits with instance resolution whenever overloading must coexist with inference. Enforce coherence (no overlap, no orphans) if data structures rely on a unique instance — sets and maps do. Choose dictionary passing for separate compilation, polymorphic recursion and small binaries; monomorphization for inner-loop speed; production systems (GHC, Swift) combine them by specializing where it pays.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Instance resolution	`evidence-term`, `find-rustc-selection`	— (the ★ lab milestone L5 exercises resolution on a corpus; a drill would duplicate its oracle)	`instance-resolution`	lab L5
Coherence	`coherence-overlap`, `orphan-rule`	— (a yes/no property; the quiz computes overlaps)	`coherence`	—
Dictionary passing vs monomorphization	`dict-translation`, `mono-copies`	— (computational quiz items; Lesson 6.9's items cover code size)	`dictionary-passing`	lab L5

References¶

See the chapter references.

step	where	constraint	resolution	evidence
1	`eq x (head l)` inside `member`	\(\mathrm{Eq}\ \alpha\), \(\alpha\) = the type of `x` (level 2)	variable: residual	—
2	generalizing `member`	residual \(\mathrm{Eq}\ \alpha\), \(\alpha \in \mathrm{ftv}(\tau)\), generalized	dictionary parameter	`_d1`
3	`member 2 …`	\(\mathrm{Eq}\ \mathsf{int}\)	instance `Eq int`, empty context	`eqInt`
4	`member true …`	\(\mathrm{Eq}\ \mathsf{bool}\)	instance `Eq bool`	`eqBool`

Technique	Time (worst)	Time (typical)	Space	Variables
Instance resolution	\(O(\lvert\tau\rvert)\) per predicate under Haskell 98 rules; undecidable with unrestricted instances (bounded by GHC's reduction depth, rustc's `recursion_limit`)	a few steps per call site	evidence terms of size \(O(\lvert\tau\rvert)\)	\(\tau\) the constrained type
Coherence checks	\(O(i^2 \cdot s)\) pairwise overlap per class (indexed by head constructor in practice)	linear with indexing	none	\(i\) instances, \(s\) head size
Dictionary passing	one copy of each function; \(O(1)\) extra argument per constraint, an indirect call per method	slower inner loops unless specialized	dictionaries at run time	\(p\) constraints
Monomorphization	code size \(\sum_f \lvert\mathrm{inst}(f)\rvert \cdot \lvert f \rvert\), exponential in the worst case	fast code, long compile times	copies	\(\mathrm{inst}(f)\) instantiations of \(f\)

Lesson 7.7 — Type classes and traits: instance resolution, coherence, dictionaries vs monomorphization¶

1. Problem and motivation¶

Instance resolution¶

Coherence¶

Dictionary passing vs monomorphization¶

2. Definitions and algorithms¶

Instance resolution¶

Coherence¶

Dictionary passing vs monomorphization¶

3. Worked example¶

Instance resolution¶

Coherence¶

Dictionary passing vs monomorphization¶

4. Invariants and correctness¶

Instance resolution¶

Coherence¶

Dictionary passing vs monomorphization¶

5. Complexity¶

6. Variants and refinements¶

Instance resolution¶

Coherence¶

Dictionary passing vs monomorphization¶

7. In real compilers¶

Instance resolution¶

Coherence¶

Dictionary passing vs monomorphization¶

8. Comparison¶

9. Assessment¶

References¶