Why is Type the kind of types with values?

Question

If I enable MagicHash, then I have unlifted values such as 42# with type Int#.

Now if Type is the kind of types with values, then the kind of Int# should be Type, but it isn't because Type is a synonym for TYPE 'LiftedRep whereas the kind of Int# is TYPE 'IntRep. We can easily confirm this in ghci,

Prelude> :set -XMagicHash -XKindSignatures
Prelude> :m +Data.Kind GHC.Prim
Prelude Data.Kind GHC.Prim> :k (Int# :: Type)

<interactive>:1:2: error:
    • Expecting a lifted type, but ‘Int#’ is unlifted
    • In the type ‘(Int# :: Type)’

So is it just the case that we don't regard magic literals such as 42# as values?

Answer 1

Just elide the type signature and GHCI will happily tell you:

Prelude Data.Kind GHC.Prim> :k Int#
Int# :: TYPE 'GHC.Types.IntRep

It's an unlifted Int, which is about what we'd expect from the name Int#.

Answer 2

This indeed turned out to be a deficiency in the documentation and is now fixed in GHC's HEAD.

To sum up, Type is the kind of types with lifted values because there are other values with differently kinded types such as 42# :: (Int# :: TYPE 'IntRep)).