Claus Reinke wrote:
overlapping instances with best-fit overlap resolution are useful because they give us an alternative way to write programs that we cannot write directly as long as current Haskell isn't expressive enough:
(a) we can't specify that two types in an instance are not equal;
but we can use overlap resolution to ensure that equal types are handled by another, more specific instance ...
permit type inequalities as guards in instance declarations:
<topdecls> -> .. | 'instance' [<ctxt> '=>'] <head> [ '|' <ineqs> ] [<body>]
<ineqs> -> <typevar> '/=' <type> [ ',' <ineqs>]
I'm afraid things might be a bit more complex. First of all, we may want several types of disequality (just as we want several equality relations on types). For example, let 'a' and 'b' be type variables. Does 'a' equal to 'b'? It depends. We may define two types t1 and t2 dis-equal if in any possible interpretation (for any assignment to type variables that may occur free in t1 and t2) the types are syntactically dissimilar. Under this definition, 'a' is not equal to 'b'. OTH, we may say that two types are disequal if there exists an interpretation (i.e., an assignment to type variables) that makes the types dissimilar. Both definitions can be useful, in different circumstances. Furthermore, sometimes we wish for a type equality constraint, sometimes we wish for a type equality predicate. The latter can be either total or partial. The type equality predicate typeEq in HList is partial: it can tell if two ground types are identical or not; in some situations, it can tell if two unground types are unequal (e.g., [a] is definitely not equal to Maybe a). OTH, it can't tell if [a] is equal to [a] -- until the type variable a is instantiated. For such unground types, the typeEq remains an unresolved constraint and floats out. Eventually the type variables get instantiated and the constraint is resolved. If they are not, we get the unresolved constraint type error (which often is the right thing). In addition to typeEq predicate (which instantiates no type variables), we often need (partial) type equality constraints that do instantiate type variables (typeCast in HList). The _full_ HList technical report discusses these issues in detail (Section 9 and Appendix D).