GADTs and functional dependencies
simonpj at microsoft.com
Mon Sep 29 07:59:50 EDT 2008
| 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.
More information about the Glasgow-haskell-users