Cannot equate polymorphic types with type variables [GHC-91028]

During the type checking process, type variables are replaced with actual types. For example, the function id has type a -> a, which is a shorter way of writing forall a. a -> a. When id is applied to an argument, the variable a is instantiated with the argument’s type, causing id’s return type (and thus the whole expression) to be the same as the argument’s type. This is because id’s type is polymorphic - it contains variables that can be instantiated with many different types.

For technical reasons, type variables cannot be instantiated with types that are themselves polymorphic in Haskell. This kind of instantiation is referred to as impredicative, borrowing a term from logic that describes terms with quantifiers where the variable ranges over the same set as the one in which the quantifier is being used. Haskell is predicative, meaning that the variables of the forall quantifier do not range over types that themselves contain forall. Predicativity makes a type system much less expressive, which means that implementations are able to be more predictable for users, run faster, and give better error messages. Impredicativity is sometimes very useful, but predicativity is usually strong enough.

This error occurs when GHC is asked to instantiate a type variable with a polymorphic type, which would require impredicativity.

Enabling Impredicativity

For some time, GHC has supported an extension called ImpredicativeTypes, but it was unreliable for many years. Starting in version 9.2, GHC uses a new implementation of type inference with impredicativity called Quick Look that is more robust than previous implementations, so ImpredicativeTypes is now considered suitable for serious use. If your application does require the additional power provided by impredicativity, then enabling this extension may resolve this error message. Code that uses ImpredicativeTypes is likely to be less compatible with GHC 9.0 and earlier due to the revamping of this extension.

Impredicative Kinds

Types and kinds are unified into a single entity in GHC, with typing rules rather than a separate grammar being used to track the difference between them. GHC’s kind system thus supports many features of the type system, including polymorphism. A definition may be polymorphic over both types and kinds. This error can also occur when GHC attempts to instantiate a kind variable with a polymorphic kind.

However, even when ImpredicativeTypes is enabled, GHC requires that kind polymorphism be predicative.

Examples

Enabling Impredicativity

Error

Impred.hs:7:8: error: [GHC-91028]
    • Couldn't match expected type ‘(forall s. ST s a) -> a’
                  with actual type ‘a0’
      Cannot instantiate unification variable ‘a0’
      with a type involving polytypes: (forall s. ST s a) -> a
    • In the expression: id runST
      In an equation for ‘test’: test = id runST
    • Relevant bindings include
        test :: (forall s. ST s a) -> a (bound at Impred.hs:7:1)
  |
7 | test = id runST
  |        ^^^^^^^^

Impred.hs:7:11: error: [GHC-91028]
    • Couldn't match expected type ‘a0’
                  with actual type ‘(forall s. ST s a1) -> a1’
      Cannot instantiate unification variable ‘a0’
      with a type involving polytypes: (forall s. ST s a1) -> a1
    • In the first argument of ‘id’, namely ‘runST’
      In the expression: id runST
      In an equation for ‘test’: test = id runST
  |
7 | test = id runST
  |           ^^^^^

Explanation

Some code truly needs impredicativity. In this example, runST has the type (forall s. ST s a) -> a. Because the forall is nested underneath the arrow, GHC can’t just provide it with a type argument - indeed, runST is one of the motivating examples for the utility of higher-rank polymorphism, and impredicativity removes restrictions from the uses of higher-rank functions. But applying id to runST requires instantiating the type variable in id to (forall s. ST s a) -> a, which is polymorphic.

Here, the error occurs twice: once when GHC attempts to match the type of id’s argument to the type of runST, and again when it attempts to match id’s return type to the type signature on test. In each case, the type variable a0 from id’s type forall a0. a0 -> a0 is needed.

This code can be fixed by turning on impredicative polymorphism, which implies RankNTypes.

Impred.hs
Before
{-# LANGUAGE RankNTypes #-}
module Impred where

import Control.Monad.ST

test :: (forall s. ST s a) -> a
test = id runST
After
{-# LANGUAGE ImpredicativeTypes #-}
module Impred where

import Control.Monad.ST

test :: (forall s. ST s a) -> a
test = id runST
Impredicative Kind Polymorphism

Error

PredKinds.hs:6:13: error: [GHC-91028]
    • Expected kind ‘forall (k :: k1). a’, but ‘z’ has kind ‘k0’
      Cannot instantiate unification variable ‘k0’
      with a kind involving polytypes: forall (k2 :: k1). a
    • In the first argument of ‘Proxy’, namely ‘(z :: forall k. a)’
      In the type signature: t :: Proxy (z :: forall k. a)
  |
6 | t :: Proxy (z :: forall k. a)
  |             ^

Explanation

Even when impredicative types are enabled, polymorphic kinds remain predicative. In this case, the type constructor Proxy has the kind forall k. k -> Type. This allows its argument to be any type, no matter its kind. Applying it to the type (z :: forall k. a) would require instantiating Proxy’s kind argument k with the polymorphic kind forall k. a, but this is not allowed.

The only way to fix this error is to rewrite the code so that impredicative polymorphism is not required. One way to do this is to lift the polymorphism outward, so that GHC will suitably instantiate the type z’s polymorphic arguments in the argument position to Proxy. After performing this transformation, the fully explicit type of t can be seen in GHCI:

ghci> :l PredKinds.hs
[1 of 1] Compiling PredKinds        ( PredKinds.hs, interpreted )
Ok, one module loaded.
ghci> :set -fprint-explicit-kinds
ghci> :t t
t :: forall {k1} {k2 :: k1} a (z :: forall (k3 :: k1). a).
     Proxy @{a} (z @k2)

Here, GHC has provided the argument k2 to z, resulting in a type with a monomorphic kind a.

PredKinds.hs
Before
{-# LANGUAGE ImpredicativeTypes #-}
module PredKinds where

import Data.Proxy

t :: Proxy (z :: forall k. a)
t = Proxy
After
{-# LANGUAGE ImpredicativeTypes #-}
module PredKinds where

import Data.Proxy

t :: forall a (z :: forall k. a). Proxy z
t = Proxy