Impredicative polymorphism
GHC does not (yet) support impredicative polymorphism, but it's a topic that comes up regularly, so this page collects the state of play.
See the new plan at ImpredicativePolymorphism/Impredicative2015
Tickets
See the ImpredicativeTypes label.
What is impredicative polymorphism?
Consider this
foo :: (forall a. a > a) > Int
bar :: forall b. Bool > b > b
test1 :: Bool > Int
test1 x = foo (bar x)
test2 :: Bool > Int
test2 = foo . bar
Should test1
typecheck? Yes: GHC can see that foo
's argument should have type forall a. a>a
, and indeed bar x
has that type. It involves higherrank type inference (see Practical type inference for higher rank types), but GHC has supported this for ages.
What about test2
? After all, it's just an etaabstracted version of test1
. No, test2
is rejected. Remember the type of (.)
:
(.) :: forall p q r. (q > r) > (p > q) > p > r
To make this work in test2
we must instantiate q := forall a. a>a
, to make the type of (.)
's first argument match foo
's type. So we have to instantiate a polymorphic type variable q
with a polymorphic type. This is called impredicative polymorphism, and GHC's type inference engine simply does not support it.
Constraints also trigger impredicative polymorhism
Although it does not appear to involve instantiating any polymorphic type variables with polymorphic types, instantiating a polymorphic type variable with qualified type will also trigger the "GHC doesn't yet support impredicative polymorphism" error.
For example
type Monadic m a = Monad m => m a
monadics :: [Monadic m a]
monadics = undefined
is not allowed.
A workaround for cases like this remove the constraint from the type synonym and add it at the use sites. I.e., the above example works if we change it to
type Monadic m a = m a
monadics :: Monad m => [Monadic m a]
monadics = undefined
($)
Special case for Consider
runST :: (forall s. ST s a) > a
foo = runST $ do { ...blah... }
Here again we need impredicative polymorphism, to instantiate ($)
's type, very much like (.)
above. So foo
would be rejected. But Haskell programmers use ($)
so much, to avoid writing parentheses, that GHC's type inference has an adhoc special case for ($)
that allows it to do type inference for (e1 $ e2)
, even when impredicative polymorphism is needed.
The internal language
All of this concerns the source language. GHC's internal language, System FC, is fully impredicative. This works fine because there is no type inference in System FC. It's only type inference that is the problem with impredicativity.
XImpredicativeTypes
?
What about We've made various attempts to support impredicativity, so there is a flag XImpredicativeTypes
. But it doesn't work, and is absolutely unsupported. If you use it, you are on your own; I make no promises about what will happen.
Workarounds
So if you need impredicativity and XImpredicativeTypes
doesn't work, what can you do? The main workaround is this: define a newtype to wrap the polymorphic function.
For example, you can't have a list of polymorphic functions, say [forall a. [a] > [a]]
. But you can wrap it like this:
newtype ListList = LL { unLL :: forall a. [a] > [a] }
Now [ListList]
is a perfectly fine type. The downside is that you have to wrap and unwrap, with LL
and unLL
, which is tiresome.
Reading
Here are some useful papers about type inference for impredicative polymorphism;
 FPH : Firstclass Polymorphism for Haskell (2008)
 Boxy types: type inference for higher rank and impredicativity (2006) We implemented this in GHC, but it was Just Too Complicated.
 QML: Explicit firstclass polymorphism for ML (2009) A much simpler, and less ambitious, approach.
 MLF: Raising ML to the power of System F (2003) The other end of the spectrum from QML: a very sophisticated approach.
The way forward
Personally I think there are two ways forward:

Add explicit type application in some shape or form. That is, tell GHC exactly how to instantiate those polymorphic type variables. Explicit type application is what happens in the intermediate language, System FC, and there are many reasons for wanting it in the source language. See the explicit type application wiki page.

Do something along the lines of QML.
The key is to be less ambitious than our previous attempts. Anything in FC should be expressible in source Haskell, but we may have to accept relativelyintrusive type annotations to achieve it.