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

[oleg at pobox.com]

Jean-Marie Gaillourdet wrote
> I am trying to do something like the following:

> > {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
> > module TestCase where
> >
> > data Any root = forall pos sel . T root pos sel => ANY pos
> >
> > class T root pos sel | pos -> root, root -> sel where
> >    f :: pos -> sel -> Bool
> >
> > instance T root (Any root) sel where
> >    f (ANY p) s = f p s

The code as posted seems to have a problem. The problem is noted by
GHC 6.4 and hugs but is accepted by GHC 6.6. Such a change in GHC
seems strange.

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'

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?