Arcane interaction of RuntimeRep with StandaloneKindSignatures
Consider this program:
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
data R
type TY :: R -> Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
We can discover the inferred kind of A
in GHCi:
ghci> :k A
A :: forall (r :: R). TY r -> Type
And then, sure enough, we can copy this signature into the original program:
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
data R
type TY :: R -> Type
data TY r
type A :: forall (r :: R). TY r -> Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
This compiles fine. Now, let's repeat the experiment using RuntimeRep
instead of a new data type R
:
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R -> Type
data TY r
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
To check the kind of A
in GHCi, let's not forget -fprint-explicit-runtime-reps
:
ghci> :set -fprint-explicit-runtime-reps
ghci> :k A
A :: forall (r :: R). TY r -> Type
This time, if we paste this signature into the original program, we get a kind error:
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, StandaloneKindSignatures #-}
import Data.Kind
import GHC.Exts
type R = RuntimeRep
type TY :: R -> Type
data TY r
type A :: forall (r :: R). TY r -> Type
data A (a :: TY r) = MkA (B a)
data B a = MkB (A a)
Test.hs:12:29: error:
• Expected kind ‘TY 'LiftedRep’, but ‘a’ has kind ‘TY r’
• In the first argument of ‘B’, namely ‘a’
In the type ‘(B a)’
In the definition of data constructor ‘MkA’
|
12 | data A (a :: TY r) = MkA (B a)
|
How come?