GADTs and functional dependencies

[Simon Peyton-Jones]

| while both GHC and Hugs accept this variation:
|
|     class FD a b | a -> b
|     f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
|     f x y = undefined
|
| and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'.
|
| So they use the FD globally (when checking use of 'f'), but not locally
| (when checking the definition of 'f'). Is that interpretation correct, or is
| there another bug involved?

No, by "globally" I meant "throughout the scope of a type variable".  I'm surprised GHC accepts the program you give, because it should unify two skolems.  With a minor change it fails

     f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3
     f x y = y

As I say, GHC's implementation of FDs is flaky and inconsistent; and that is not just because I'm lazy but because it is hard to know just what to do, most especially in situations like this when there is no System F translation. That is why I've been working so hard on FC.

Simon