Type classes, as originally proposed, have a surprising feature: while they may appear to disallow some instance of polymorphic functions, they never actually preclude such instances from being valid. Type class errors arise in Haskell only through the use of explicit type signatures, or because of ad hoc syntactic restrictions on the form of types. The same does not hold for many extensions of the Haskell predicate system; for example, both equality constraints and functional dependencies make it possible for certain instantiations of polymorphic types to have entirely unsatisfiable predicates.

At the moment, Haskell compilers use the satisfiability of predicates in several ways. They reject (many) programs with provably unsatisfiable constraints. At ICFP this year, Richard Eisenberg and I argue that treating the termination of type family applications as a constraint simplifies the use of type families and improves their metatheory.

In this talk, I will propose that we should also take unsatisfiability seriously in Haskell’s type and class systems. For example, current compilers do not refine polymorphic type variables to rule out unsatisfiable constraint sets. I will claim that doing so would more accurately reflect the semantics of the type systems. More significantly, however, by recognizing that sets of constraints are unsatisfiable, we can give a more flexible notion of overlap among type class or type family instances, and hence to permit more expressive, modular, and easier-to-use type class programming, without compromising coherence or other semantic properties. Finally, I will relate satisfiability-aware overlap checks to my work with Mark Jones on instance chains, arguing that both the seemingly most palatable (alternative chaining) and least palatable (backtracking) aspects of instance chains follow inevitably from the attempt to make satisfiability-aware instances easier to use and more efficient to implement.