Cannot equate polymorphic types with type variables [GHC91028]
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: [GHC91028]
• 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: [GHC91028]
• 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 higherrank polymorphism, and impredicativity removes restrictions from the uses of higherrank 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
{# LANGUAGE RankNTypes #}
module Impred where
import Control.Monad.ST
test :: (forall s. ST s a) > a
test = id runST
{# 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: [GHC91028]
• 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 fprintexplicitkinds
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
{# LANGUAGE ImpredicativeTypes #}
module PredKinds where
import Data.Proxy
t :: Proxy (z :: forall k. a)
t = Proxy
{# LANGUAGE ImpredicativeTypes #}
module PredKinds where
import Data.Proxy
t :: forall a (z :: forall k. a). Proxy z
t = Proxy