.. _impredicative-polymorphism:
Impredicative polymorphism
==========================
.. extension:: ImpredicativeTypes
:shortdesc: Enable impredicative types.
Implies :extension:`RankNTypes`.
:implies: :extension:`RankNTypes`
:since: 6.10.1
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 :extension:`ImpredicativeTypes`, using the so-called Quick Look
inference algorithm. It is described in the paper
`A quick look at impredicativity
`__
(Serrano et al, ICFP 2020).
Switching on :extension:`ImpredicativeTypes`
- Switches on :extension: `RankNTypes`
- Allows user-written 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 :extension: `TypeApplications` is enabled). For example, you
can write ``reverse @(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 if ``xs :: [forall a. a->a]``,
by instantiating ``reverse`` at type ``forall 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
:extension:`ImpredicativeTypes` GHC switches on Quick Look for applications of ``($)``.