In my last post about universally quantified types, I was asking why GHC disallows datatypes like
Evil while allowing datatypes like
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.