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