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