Why is impredicative polymorphism allowed only for functions in Haskell?

Question

In Haskell I can't write

f :: [forall a. a -> a]
f = [id]

because

• Illegal polymorphic type: forall a. a -> a
  GHC doesn't yet support impredicative polymorphism

But I can happily do

f :: (forall a. a -> a) -> (a, b) -> (a, b)
f i (x, y) = (i x, i y)

So as I see GHC does support impredicative polymorphism which is contradict to the error message above. Why is the (->) type constructor treated specially in this case? What prevents GHC from having this feature generalized over all datatypes?

Answer 1

Higher-rank polymorphism is a special case of impredicative polymorphism, where the type constructor is (->) instead of any arbitrary constructor like [].

The basic problems with impredicativity are that it makes type checking hard and type inference impossible—and indeed we can’t infer types of a higher rank than 2: you have to provide a type annotation. This is the reason for the existence of the Rank2Types extension separate from RankNTypes. But for the restricted case of (->), there are simplified algorithms for checking these types and doing the necessary amount of inference along the way for the programmer’s convenience, such as Complete and Easy Bidirectional Type Checking for Higher-rank Polymorphism—compare that to the complexity of Boxy Types: Inference for Higher-rank Types and Impredicativity.

The actual reasons in GHC are partly historical: there was an ImpredicativeTypes extension, which is now deprecated, but it never worked properly or ergonomically. Part of the problem was that we didn’t yet have the TypeApplications extension, so there was no convenient way to explicitly supply a polymorphic type as a type argument, and the compiler attempted to do more inference than it ought to. Now that we have TypeApplications, a restricted form of ImpredicativeTypes may become possible in the future.

It’s not terribly pressing, however, since there have been workarounds for a while: with RankNTypes, you can “hide” other forms of impredicativity by wrapping the polymorphic type in a newtype and explicitly packing & unpacking it to tell the compiler exactly where you want to generalise and instantiate type variables.

newtype Id = Id { unId :: forall a. a -> a }

f :: [Id]
f = [Id id]  -- generalise

(unId (head f) (), unId (head f) 'x')  -- instantiate to () and Char