Unification and impl search

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…