overlapping instances and functional dependencies

[oleg@pobox.com]

Wolfgang Jeltsch has observed:
> I have this code:
>     class C a b c | a b -> c where
>         f :: a -> b -> c
>
>     instance C a b c => C a (x,y,b) c where
>         f a (_,_,b) = f a b
>
>     instance C a (a,c,b) c where
>         f _ (_,c,_) = 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
> Can anyone tell me what the reason for this is and, maybe, how to avoid
> these problems with Hugs?

I believe it's helpful to think about this problem in terms of logical
programming, and proceed in phases.

Phase 1. The compiler sees the instances of a class C and compiles
them into a database of instances. In Prolog terms, given the
instances

	instance C a b c => C a (x,y,b) c
	instance C a (a,c,b) c

the compiler asserts

	c(A,tuple(A,C,B),C,dict2).
	c(A,tuple(X,Y,B),C,dict1) :- c(A,B,C,_).

In Haskell, lower-case type identifiers are variables and upper-case
one are type constants. In Prolog, it's the other way around:
lower-cased identifiers are constants and upper-cased are variables. I
hope that won't cause too much confusion.

I happen to have SWI-Prolog handy, in which I assert the above two
facts.

Phase 2. Suppose the compiler sees a type with a class constraint ``C Int
(Int,Char,Bool) t'' The compiler can determine the appropriate instance
by issuing a query:

?- bagof(Dict,c(int,tuple(int,char,bool),T,Dict),Dicts).

Dict = _G158
T = char
Dicts = [dict2] 
Yes

In our case, only one instance matched, and we found the corresponding
dictionary. If Dicts were a list of two or more dictionaries, we would
have needed to choose the most specific, if any.

Phase 1a.
Before we get to Phase 2 however, we have to take care of one more
problem. The class declaration specified a dependency:
	class C a b c | a b -> c

which all members of that class must satisfy. The instances (which
define the membership) must be consistent with the dependency "a b -> c".
The consistency would be violated if there were two types "C a b c1"
and "C a b c2" such that c1 /== c2. Thus we can check the
consistency of the instances by searching for a counter-example:

?- c(A,B,C1,_), c(A,B,C2,_), \+ C1 == C2.

A = _G151
B = tuple(_G151, _G153, tuple(_G151, _G158, _G302))
C1 = _G153
C2 = _G158 
Yes

Alas, in this case we found a counter-example: types
	C a (a,c,(a,c',d)) c
	C a (a,c,(a,c',d)) c'

with c' /= c match some instance but contradict the functional
dependency. Therefore, the compiler complaints.