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

[Jean-Marie Gaillourdet]

Hi,

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

There is a multi-parameter type class T with some functional
dependencies. And I want do define an almost general type for T, Any
root. I would like to have that type in T as well. But ghc is not able
to type check f. It gives:

> TestCase.hs:10:7:
>     Couldn't match expected type `sel1' (a rigid variable)
>            against inferred type `sel' (a rigid variable)
>       `sel1' is bound by the pattern for `ANY' at TestCase.hs:10:7-11
>       `sel' is bound by the instance declaration at TestCase.hs:9:0
>     When using functional dependencies to combine
>       T root pos sel, arising from use of `f' at TestCase.hs:10:18-22
>       T root pos sel1,
>         arising from is bound by the pattern for `ANY'
>                        at TestCase.hs:10:7-11
>         at TestCase.hs:10:7-11
>     In the pattern: ANY p
>     In the definition of `f': f (ANY p) s = f p s

I think sel1 and sel are equal, because the root in the type of "(ANY
p)" on the left side is the same as the root of the type of "f p s" on
the right side. From that should follow with help of the functional
dependency that sel1 and sel are the same types. Do I misunderstand the
type system or is that a weakness of GHC? Or am I trying to do something
silly?

I have a solution that involves requiring sel to be in Typeable and
using cast and I never came across a runtime error, so far. Is there a
better way to express that?

Any enlightenment is appreciated.

Regards,
  Jean-Marie