[Haskell] dependent types, type class contexts

[Martin Sulzmann]

 > ...
 >   This gets at the crux of my questions:
 > 
 > - Why can't the compiler tell that (ListT a, Num b) is enough to figure 
 > out the additional context it seems to need?
 > 

Most likely, GHC won't "apply" 

 > instance (ListT a, Eq b) => Eq (a b)

cause of the overlap.

 > - Would it be possible to _exclude_ a type from a class, to aviod 
 > overlapping instances? Perhaps what I want is negation in a type class 
 > declaration:
 > 
 > < forall a . a /= [] => class ListT a
 > 
 > Alternatively, I'd like to state that the _only_ instances of ListT are 
 > NilT and ConsT.

You can't express the above in GHC at the moment. All what you might get is a "missing
instance" error.

Ok, you'd like to express

forall a. ListT a /\ a /= NilT /\ a /= ConsT -> False        (F)

There's no Haskell system (as far as I know) which allows for
disequality (negation).

In Chameleon (http://www.comp.nus.edu.sg/~sulzmann/chameleon/)
you can impose additional conditions on type classes.
E.g.

rule ListT Int ==> False
rule ListT Bool ==> False
rule ListT (a->b) ==> False
...

That is, you'd need to enumerate *all* false cases.

 > 
 > Are there definitive references on context resolution (aside from the 
 > compiler source, which I have not looked at)? Has anyone grappled with 
 > these problems and come up with satisfactory solutions?

A more satisfying solution would be to allow for

rule ListT a | a /=NilT, a /= ConsT ==> False

(the logical interpretation corresponds to formula (F))

The problem is that once you introduce disequality we might lose some
of the nice properties such as complete type inference etc.

There's also the issue of how to make use of disequalities to avoid
overlapping instances.
See "A Theory of Overloading" (journal version) Section 8.1
(http://www.comp.nus.edu.sg/~sulzmann/chr/publications.html) for
a (very) short discussion. The problem is that we might have to give
up separate compilation.

Martin