Major type-class overhaul

[Simon Peyton-Jones]

Dear GHC users,

For some time I have been promising an overhaul of GHC's type inference machinery to fix the interactions between type classes and GADTs.  I've just completed it (or at least I hope so).

This message is just to summarise the programmer-visible changes, and to encourage you to give them a whirl.  Of course, you'll need to compile the HEAD to do this; or get a nightly-build snapshot in a day or two's time.

Needless to say, if you are using the HEAD for mission-critical stuff, proceed with caution. I don't guaranteed bug-free-ness.

Simon

This major patch adds implication constraints to GHC's type inference
mechanism.  (The name "implication constraint" is due to Martin
Sulzmann.)

>From a programmer point of view, there are several improvements

1. Complete(r) type inference
~~~~~~~~~~~~~~~~~~
GHC's type inference becomes complete (or perhaps more complete!)
Particularly, Karl-Filip Faxen's famous example in "Haskell and principal
types" (Haskell workshop 2003) would type check when the program text
was written in one order, and then fail when the text was re-ordered.
Now it works regardless.  The test is tc218.

2. Lifting the "quantified-here" restriction
~~~~~~~~~~~~~~~~~~~~~~~~~
The restriction that every constraint in a type signature must mention
at least one of the quantified type variables is lifted. So you can write
        f :: C Int => ...
or      g :: forall b. Eq a => ...
This may seem odd, but the former was recently requested by a Haskell
user; see this message:
http://www.haskell.org/pipermail/glasgow-haskell-users/2006-September/011137.html

3. Dictionaries are packaged in data constructors
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A very useful new feature is this.  When a data type is declared in in
GADT syntax, the context of the constructor is
        *required* when constructing
        *available* when matching

For example
        data T a where
          T1 :: Num a => a -> T a
          T2 :: Bounded a => T a

        f :: T a -> a
        f (T1 x) = x+1
        f T2     = maxBound

Notice that f is not overloaded.  The Num needed in the first branch
is satisfied by the T1 pattern match; and similarly for the T2 pattern
match.

This feature has been often requested, becuase it allows you to
package a dictionary into an ordinary (non-existential) data type, and
be able to use it.

NOTE: the Haskell 98 syntax for data type declarations
        data Num a => T a = T1 a
behaves exactly as specified in H98, and *not* in the new way.
The Num dictionary is
        *required* when constructing, and
        *required* when matching
I think this is stupid, but it's what H98 says.  To get the new
behaviour, use GADT-style syntax, even though the data type being
defined is does not use the GADT-ness.

4. Type classes and GADTs
~~~~~~~~~~~~~~~~~
The proper interaction between GADTs and type classes is now
respected.  For example:

        data GADT a where
          MkG :: Num a => a -> GADT [a]

        g :: forall b. Read b => GADT b -> String -> b
        g (MkG n) s = n : read s

Inside the branch we know that b=[a], so the (Read b)
dictionary is a (Read [a]) dictionary, which is why we can
use the result of read in the tail of a cons.


Functional dependencies and equality predicates
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The treatment of functional dependencies is still ad hoc
and unsatisfactory.  I do not promise that they will work
nicely in conjunction with GADTs.  Trac #345 has a good
example.

More generally, we want to add
        - indexed type synonyms
          (aka associated type synonyms)
        - equality constraints in contexts

Both will require us to furher overhaul constraint
handling.  So this patch is just a (big) step on the way.