Unification and impl search

July 31, 2026 - Tagged as: en, haskell, rust.

At a high level Haskell’s typeclasses and Rust’s traits are the same feature, but they also differ quite a bit in details. Here’s an example:

struct A;

trait C<T> {}

impl<T> C<T> for Option<T> {}   // ∀ T . C<Option<T>,   T>

fn f<P, Q>(p: P, q: Q) where P: C<Q> {}

fn main() {
    f(None, A);
}

-

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

data A = A

class C a b

instance C (Maybe t) t

f :: C p q => p -> q -> ()
f _ _ = ()

main :: IO ()
main = pure (f Nothing A)

The Rust code type checks, but Haskell code fails with an error saying that the constraint generated by the application of f cannot be solved.

The reason is because of a difference in how they match instance heads against constraints. In Haskell syntax, type checking of main goes like this:

• A : A
• Nothing : Maybe a0 (where a0 is a fresh unification variable)
• f : p0 -> q0 -> () (where p0 and q0 are fresh unification variables)
  • f also generates the constraint C p0 q0
• f Nothing A unifies p0 ~ Maybe a0 and q0 ~ A and gets type ()

The pure ... part is not important. The last unification above makes the constraint C (Maybe a0) A. Now how do we resolve this constraint?

The only instance we have has the head ∀ t . C (Maybe t) t. To match this against the constraint we first instantiate it as C (Maybe t0) t0 (where t0 is fresh unification variable). After this part Haskell and Rust do different things:

• Haskell only allows updating the instance head’s unification variables (matching, aka. one-way unification). The second parameter unifies with A (t0 ~ A), which makes the instance head C (Maybe A) A and the constraint stays as C (Maybe a0) A. If we unify a0 ~ A, the instance head matches and the program type checks, but that would update the constraint, which Haskell doesn’t do. So we’re stuck here with this type error:

  Ambiguous type variable ‘a0’ arising from a use of ‘f’
  prevents the constraint ‘(C (Maybe a0) A)’ from being solved.

• Rust allows updating constraint variables. Instantiation of the instance head happens the same way, but when matching, we allow the unification a0 ~ A that Haskell doesn’t allow, and this program type checks.

Two-way unification allows matching in more cases, but when there are multiple matches, Rust fails the same way as Haskell:

struct A;

trait C<T> {}

impl<T> C<T> for Option<T> {}   // ∀ T . C<Option<T>,   T>
impl C<A> for Option<u32> {}    //       C<Option<u32>, A>  (new)

fn f<P, Q>(p: P, q: Q) where P: C<Q> {}

fn main() {
    f(None, A);
}

-

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

data A = A

class C a b

instance C (Maybe t) t

instance C (Maybe Int) A    -- new

f :: C p q => p -> q -> ()
f _ _ = ()

main :: IO ()
main = pure (f Nothing A)

The Haskell version fails the same way (and fixed the same way, by annotating Nothing), but now Rust version fails (and fixed) the same way too:

error[E0283]: type annotations needed
  --> test.rs:12:5
   |
12 |     f(None, A);
   |     ^ ---- type must be known at this point
   |     |
   |     cannot infer type of the type parameter `P` declared on the function `f`
   |

Implementation-wise, two-way unification for instance search requires that the constraint unification variables are saved before matching, and restored afterwards to continue searching for more solutions¹. Only when we have just one matching instance we actually do the unifications and continue type checking².

---

1. Or another implementation that achieves the same, e.g. by cloning the unification variables in a way that breaks sharing, instead of e.g. copying mutable cells or reference counted heap structures.↩︎

2. Typeclass constraint solving often enables more type checking by e.g. allowing associated type selections to be evaluated, and so unlike in tutorials, in real implementation you often need to eagerly solve constraints to be able to fully type check function bodies.↩︎