Suggestion: refine overlap handling for instance declarations

Wed Mar 15 00:04:23 EST 2006

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).