Foralls, Redexes, and Type Lambdas

In my last post about universally quantified types, I was asking why GHC disallows datatypes like Evil while allowing datatypes like Fine:

data OK (x :: * -> *) where
   OK :: OK x
type Fine = OK Maybe
type Evil = OK (forall (f  :: * -> *) . f)

This seems more confusing when Evil' is just fine:

data OK' (x :: *) where
   OK' :: OK' x
type Fine' = OK' Int
type Evil' = OK' (forall (f  :: *) . f)

Ken Shan answered my question: In the static semantics of the typed lambda calculus, only forms like (Λt:k.r) @ s are redexes. This makes sense to me, but it seems like it's so for simplicity reasons. I expect that this makes the metatheory simpler.

Unfortunately, this makes some things in GHC a pain, since GHC doesn't have type lambdas. SPJ suggests that this is because it makes unification for type inference impossible, but I don't yet understand why. The feature list for EHC indicates that it does support type lambdas, though I haven't tested this.

Update: (29 Jan 2007)

A History of Haskell points to A system of constructor classes (mirror) regarding unification and type lambdas.