[Haskell] functional dependencies not satisfactory?

[Manuel M T Chakravarty]

Wolfgang Jeltsch wrote,
> I came across the following problem:
> 
> I define a class with a functional dependency like so:
> 
>     class C a b | a -> b
> 
> Then 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 b
> 
> But 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 b
> 
> In 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