duplicate instance declarations

[C T McBride]

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