Kind variable would escape its scope [GHC-46956]
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 locally-bound kind, then the resulting program would contain an ill-scoped kind signature.
This situation can arise for multiple reasons.
- In the first example, the cause is a manually-specified type signature with the kind variable in the wrong position.
- In the second example, the cause is a pattern match on a GADT constructor in a let binding (use case instead).
Examples
An escaping kind variable
Error Message
Main.hs:9:49: error: [GHC-46956]
• 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:26-35
• 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 explicitly-provided 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 ()
Binding a `GADT` constructor in `let`
In this example, we use a let binding to unpack the constructor of a GADT. Naively, this should work fine, because there is only one constructor. Yet GHC does not accept this code!
The fix is to use pattern-matching, either with a case or by pattern-matching in a function argument.
For more details about why this is necessary, see the GHC user guide on ExistentialQuantification.
Note: this example generates GHC-46956 because the TypeFamilies extension is active. If it isn’t, GHC-25897 is generated instead.
Message
Let.hs:9:18: error: [GHC-46956]
• Couldn't match expected type ‘a0’ with actual type ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor:
MkShowable :: forall a. Show a => a -> Showable,
in a pattern binding
at Let.hs:9:7-18
• In the pattern: MkShowable x
In a pattern binding: MkShowable x = showable
In the expression: let MkShowable x = showable in show x
|
9 | let MkShowable x = showable
| ^Let.hs
{-# LANGUAGE TypeFamilies #-}
module Main where
data Showable where
MkShowable :: Show a => a -> Showable
showShowable :: Showable -> String
showShowable showable =
let MkShowable x = showable
in show x
main :: IO ()
main = putStrLn $ showShowable (MkShowable 42)
{-# LANGUAGE TypeFamilies #-}
module Main where
data Showable where
MkShowable :: Show a => a -> Showable
showShowable :: Showable -> String
showShowable showable =
case showable of
MkShowable x -> show x
main :: IO ()
main = putStrLn $ showShowable (MkShowable 42)