Hi
Why is this a duplicate instance declaration:
class C a class D b data T a b instance (C (T a b), C a) => D b instance (C (T a b), C b) => D a
These are symmetric, but not duplicate, as I see it.
Suppose we add instance C () instance C (T () ()) Now there are two ways to build an instance of D (). The class mechanism is based on an open world assumption, hence declarations must be rejected if they can subsequently be made to overlap. If two instance `conclusions' unify, as (D a) and (D b) do, we can make them overlap by ensuring that both sets of `premises' hold. In general, instance inference amounts to proof search, or the execution of a logic program. It requires quite serious restrictions to ensure that a given set of instance declarations will always result in terminating and deterministic search. Relaxing those restrictions, as in ghc -fdont-tell-my-mum, leaves us able to write nonterminating compile-time programs. Indeed, we even find the compiler `deriving' them for us. By the way, critics of Cayenne should note that the only reason its typechecking is undecidable is that you can execute non-terminating programs at compile-time. Funny-type-class Haskell is just as bad. Just as I argue with respect to the type system (type-lambda etc), I'd suggest that extending the expressivity of the class system does no harm, provided we cease to presume that instance inference must always be fully automatic. If there is a way to give the construction of an instance explicitly, then we can always make clear those things the machine can't figure out for itself. Just like typechecking, instance-finding is a partnership between people and machines: the machines should figure out as much as possible, but the people should always be able to help. Cheers Conor