[Haskell-cafe] A question about functional dependencies and
existential quantification
oleg at pobox.com
oleg at pobox.com
Tue Mar 27 02:21:28 EDT 2007
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?
More information about the Haskell-Cafe
mailing list