GADTs and functional dependencies

[Simon Peyton-Jones]

By "global" I really meant "throughout the scope of the type variable concerned.

Nevertheless, the program you give is rejected, even though the scope is global:

  class FD a b | a -> b

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

Both GHC and Hugs erroneously reject the program, just as they do this one
  instance FD Int Bool
  g :: FD Int b => ...

The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job.  That is what we are fixing with type functions.  I do not know how to fix it for FDs (except by way of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language.  This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to.

Simon

| -----Original Message-----
| From: Claus Reinke [mailto:claus.reinke at talk21.com]
| Sent: 24 September 2008 19:27
| To: Simon Peyton-Jones; glasgow-haskell-users at haskell.org
| Subject: Re: GADTs and functional dependencies
|
| >> 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!
|
| Actually, how does that relate to reasoning under assumptions?
|
|     class FD a b | a -> b
|
|     f :: (FD t1 t2, FD t1 t3) => ..
|     f = ..
|
| There is no instance of 'FD', so no equalities can be derived from there
| outside of 'f', and no equalities should be derived globally from instances
| that are only local hypotheses in 'f' . But inside 'f', we assume that those
| two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of
| the implication.
|
| Isn't that decidedly local?
| Claus
|
|