GitLab

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?