Wolfgang Jeltsch wrote,
I came across the following problem:I define a class with a functional dependency like so: class C a b | a -> bThen I want to define a datatype using the fact that the second argument of C is dependent on the first:data C a b => T a = MkT a b But unfortunately, this doesn’t work, at least not in GHC. I can try this: data T a = forall b. C a b => MkT a bBut if I do pattern matching on a value of T a, GHC doesn’t recognize that the type of MkT’s second argument is determined by the type of the first. For example, the following function definition is not accepted:useB :: C a b => T a -> (b -> ()) -> () useB (MkT a b) f = f bIn my opinion, the problem is that GHC doesn’t see that because of the functional dependency the type exists b. C a b => b is at least as general as the type forall b. C a b => b. Is there a solution to this problem?
You may want to have a look at Section 2.3 of "System F with Type Equality Coercions" <http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html>, which explains why GHC rejects the program.
The mentioned paper also outlines an alternative translation of FDs using System FC that does not suffer from this problem. Unfortunately, it is not quite clear how to extend type checking for FDs in such a way that the required System FC coercion-evidence types are produced by the type checker.
This is one of the reasons why I believe that we should use the type families mentioned by Stefan instead of functional dependencies. Type checker support for type synonym families (the flavour needed for your example) has been merged into GHC's development version a week ago. For more details, see
http://haskell.org/haskellwiki/GHC/Type_families Manuel _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
