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... 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.