6.4.16. Impredicative polymorphism


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 :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 ImpredicativeTypes GHC switches on Quick Look for applications of ($).