6.4.16. Impredicative polymorphism¶

ImpredicativeTypes
¶ Implies: RankNTypes
Since: 9.2.1 (unreliable in 6.10  9.0) Allow impredicative polymorphic types.
In general, GHC will only instantiate a polymorphic function at a monomorphic type (one with no foralls). For example,
runST :: (forall s. ST s a) > a
id :: forall b. b > b
foo = id runST  Rejected
The definition of foo
is rejected because one would have to
instantiate id
‘s type with b := (forall s. ST s a) > a
, and
that is not allowed. Instantiating polymorphic type variables with
polymorphic types is called impredicative polymorphism.
GHC has robust support for impredicative polymorphism,
enabled with ImpredicativeTypes
, using the socalled Quick Look
inference algorithm. It is described in the paper
A quick look at impredicativity
(Serrano et al, ICFP 2020).
Switching on ImpredicativeTypes
 Switches on
RankNTypes
 Allows userwritten types to have foralls under type constructors, not just under arrows.
For example
f :: Maybe (forall a. [a] > [a])
is a legal type signature.  Allows polymorphic types in Visible Type Application
(when
TypeApplications
is enabled). For example, you can writereverse @(forall b. b>b) xs
. Using VTA with a polymorphic type argument is useful in cases when Quick Look cannot infer the correct instantiation.  Switches on the Quick Look type inference algorithm, as described
in the paper. This allows the compiler to infer impredicative instantiations of polymorphic
functions in many cases. For example,
reverse xs
will typecheck even ifxs :: [forall a. a>a]
, by instantiatingreverse
at typeforall a. a>a
.
Note that the treatment of typeclass constraints and implicit parameters remains entirely monomorphic, even with ImpredicativeTypes. Specifically:
 You cannot apply a type class to a polymorphic type. This is illegal:
f :: C (forall a. a>a) => [a] > [a]
 You cannot give an instance declaration with a polymorphic argument. This is illegal:
instance C (forall a. a>a)
 An implicit parameter cannot have a polymorphic type:
g :: (?x :: forall a. a>a) => [a] > [a]
For many years GHC has a special case for the function ($)
, that allows it
to typecheck an application like runST $ (do { ... })
, even though that
instantiation may be impredicative. This special case remains: even without
ImpredicativeTypes
GHC switches on Quick Look for applications of ($)
.
This flag was available in earlier versions of GHC (6.10.1  9.0), but the behavior was unpredictable and not officially supported.