Impredicative types

From HaskellWiki

Impredicative types are to be contrasted with rank-N types.

A standard Haskell type is universally quantified by default, and quantifiers can only appear at the top level of a type or to the right of function arrows.

A higher-rank polymorphic type allows universal quantifiers to appear to the left of function arrows as well, so that function arguments can be functions that are themselves polymorphic.

An impredicative type, on the other hand, allows universal quantifiers anywhere: in particular, may contain ordinary datatypes with polymorphic components. The GHC User's Guide gives the following example:

f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f (Just g) = Just (g [3], g "hello")
f Nothing  = Nothing

See also

* The GHC User's Guide on impredicative polymorphism.