[Haskell-cafe] Re: A question about functional dependencies and existential quantification

[Jean-Marie Gaillourdet]

Hi,

oleg at pobox.com wrote:
> The problem is not related to existentials, so we just drop them
> 
>> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
>> module TestCase where
>>
>> data Any root = ANY
>>
>> class T root pos sel | pos -> root, root -> sel where
>>    f :: pos -> sel -> Bool
>> instance T root (Any root) sel
>>
>> test x = f ANY x
> 
> Hugs and GHC 6.4 both complain about the instance of T:
> Hush (September 2006 version) says
>   ERROR "/tmp/j.hs":9 - Instance is more general than a dependency allows
> 
> and GHC 6.4.2 says
> 
>  Illegal instance declaration for `T root (Any root) sel'
>    (the instance types do not agree with the functional dependencies 
>     of the class)
>   In the instance declaration for `T root (Any root) sel'
> 

As I understand functional dependencies, and I am definitely _not_ an
expert on them, they state, that given the lhs of a dependency is
instantiated, the type variables of the rhs are determined, too.
If that is correct, I don't understand why this instance should be to
general, as every instantiation of "root" exactly determines the
corresponding instantiation of "Any root".

> I concur. The class declares T as being a ternary relation such that
> the following holds
> 	forall r p p' s s'. T(r,p,s) && T(r,p',s') -> s = s'
> Now, the instance `T root (Any root) sel' is satisfied when
> root=Int, sel = Bool and when root=Int, sel = Int. Does it not? That
> falsifies the above proposition. In other words, the instance T is not
> functional with respect to the first and the third arguments.
> 
> That is not surprising. What is surprising is why GHC 6.6 accepts such
> an instance?

GHC 6.6 does not accept such instances. Add the following code to the
module TestCase

> instance T Int Int Int
> instance T Int Int Bool

and you get the following error:

TestCase.hs:10:0:
    Functional dependencies conflict between instance declarations:
      instance T Int Int Int -- Defined at TestCase.hs:10:0
      instance T Int Int Bool -- Defined at TestCase.hs:11:0

-- Jean-Marie