overlapping instances and functional dependencies

[Simon Peyton-Jones]

|     class C a b c | a b -> c where
|         f :: a -> b -> c
|=20
|     instance C a b c =3D> C a (x,y,b) c where
|         f a (_,_,b) =3D f a b
|=20
|     instance C a (a,c,b) c where
|         f _ (_,c,_) =3D c
| ghci -fglasgow-exts -fallow-overlapping-instances compiles it without
| complaint but hugs -98 +o says:
|     ERROR "ClassProblem.hs":7 - Instances are not consistent with
dependencies
|     *** This instance    : C a (a,b,c) b
|     *** Conflicts with   : C a (b,c,d) e
|     *** For class        : C a b c
|     *** Under dependency : a b -> c

There are several things going on here.

1.  The functional dependency (a b -> c), together with an instance
declaration
	instance C <ta> <tb> <tc>
means that=20
	if you have a constraint (C <sa> <sb> <sc>),=20
	and <sa> matches <ta>
	and <sb> matches <tb>
then=09
	<sc> must look like <tc>

Here "matches" means "is a substitution instance of".

Mark Jones's original paper specified that=20
	the free variables of <tc> must be a subset of=20
	the free variable of <ta> and <tb>

Reason: then the matching of <sa> and <sb> generates a substitution that
covers all the free variables of <tc>, and then "<sc> must look like
<tc>" means exactly that "<sc> must be the same as <tc> instantiated by
the matches of <ta>/<sa> and <tb>/<sb>".

However, it seems that neither Hugs nor GHC make this test, which is
very naughty of them

2.  Having omitted this test, Hugs is complaining that a constraint
	C Int (Int,Bool,Bool) <sc>
would match both instance declarations, so it's not sure which <tc> to
make <sc> equal to.  I could check why GHC does not complain, but it may
be that the answer is the same in both cases (namely the unbound 'c').


3.  None of this has to do with overlapping instances per se.




I'm working with Martin Sulzmann on some ideas for loosening the
restriction (1) above, but it's all a bit vacuous in your example.  What
is the fundep is buying you?  It doesn't convey any information to say
that "<sc> must look like c", if c is completely unbound!

Simon