# 6.4.20. Impredicative polymorphism¶

- ImpredicativeTypes¶
- Implies:
- 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 so-called 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 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

`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`

.

Note that the treatment of type-class 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.