GADTs and functional dependencies

[Simon Peyton-Jones]

Wolfgang writes

| > data GADT a where
| >
| >     GADT :: GADT ()
| >
| > class Class a b | a -> b
| >
| > instance Class () ()
| >
| > fun :: (Class a b) => GADT a -> b
| > fun GADT = ()

You're right that this program should typecheck.  In the case branch we discover (locally) that a~(), and hence by the fundep, b~(), and away you go.

This has never worked with fundeps, because it involves a *local* type equality (one that holds in some places and not others) and my implementation of fundeps is fundamentally based on *global* equality.  Prior to GADTs that was fine!

By adding local type equalities, GADTs change the game, and associated types/type families change it even more.  (One reason that the game is different is that GHC has a typed intermediate language, so we need to maintain evidence of type equality throughout.  In contrast, global equalities can be handled by straightforward unification, that makes the two types *identical*.)  Our new implementation of type functions does, for the first time, a thorough principled job of handling arbitrary local type equalities.

But that still leaves fundeps.  Rather than try to fix fudeps directly (which would be a big job -- as I say, the current impl is fundamentally global) the best thing to do is to translate them into type equalities, thus:

        class (F a ~ b) => C a b
          type family F a

(Note for 6.10 users: type equalities in superclasses is the piece we still have not implemented.)  When you write an instance decl you add a type instance decl:

        instance C () ()
          type F () = ()

Now everything should be good.  Almost all fundep programs can be translated in this way.  (Maybe all, I'm not 100% certain.)   If you are doing this yourself, you can usually remove C's second parameter; but only if the fundep is unidirectional.

So, as of now (6.10), the fundep stuff is still handled exactly as before, using global unification, so your program isn't going to work in 6.10 either.  I'm frankly dubious about whether it's worth the effort of automatically performing the above translation from fundeps to type equalities; if you want this level of sophistication, you could just use type functions directly.

It's not really a lack of backward compat.  I think 6.10 will do all that 6.8 does; but if you want *more* you'll have to switch notation.  Does that help clear things up, and explain why things are the way they are?

Simon