Kind variable would escape its scope [GHC46956]
This error occurs during kind inference. When inferring a kind for a type variable, GHC creates a fresh metavariable to stand for the kind. Later, if something forces this kind metavariable to be equal to some other kind, unification equates them. However, local kind quantification can lead to the existence of kinds that are only valid in the scope of the quantifier. If a kind metavariable that originated outside this scope were unified with the locallybound kind, then the resulting program would contain an illscoped kind signature.
Examples
An escaping kind variable
Error Message
Main.hs:9:49: error: [GHC46956]
• Expected kind ‘k’, but ‘b’ has kind ‘k0’
• because kind variable ‘k’ would escape its scope
This (rigid, skolem) kind variable is bound by
an explicit forall k (a :: k)
at Main.hs:9:2635
• In the second argument of ‘SameKind’, namely ‘b’
In the type signature:
foo :: forall b. (forall k (a :: k). SameKind a b) > ()

9  foo :: forall b. (forall k (a :: k). SameKind a b) > ()
 ^
Explanation
In this context, the SameKind
type requires that both of its arguments are types, and that those types have the same kind. In foo
’s type signature, the type b
does not have an explicitlyprovided kind, which means that GHC creates a fresh kind metavariable for it. The type a
does have an explicit kind, which is the variable k
. Because SameKind
is applied to both a
and b
, it causes b
’s kind metavariable to be unified with k
, but k
comes from an inner scope and is thus not available for unification.
The error can be fixed by extending k
’s scope to encompass b
’s binding site.
Main.hs
{# LANGUAGE PolyKinds, RankNTypes, ImpredicativeTypes #}
module Main where
import Data.Kind
data SameKind :: k > k > *
foo :: forall b. (forall k (a :: k). SameKind a b) > ()
foo = undefined
main :: IO ()
main = pure ()
{# LANGUAGE PolyKinds, RankNTypes, ImpredicativeTypes #}
module Main where
import Data.Kind
data SameKind :: k > k > *
foo :: forall k b. (forall (a :: k). SameKind a b) > ()
foo = undefined
main :: IO ()
main = pure ()