Kinds of types in functions

Question

Take the following code:

{-# LANGUAGE KindSignatures, DataKinds #-}

data Nat = O | S Nat

class NatToInt (n :: Nat) where
    natToInt :: n -> Int

instance NatToInt O where
    natToInt _ = 0

instance (NatToInt n) => NatToInt (S n) where
    natToInt _ = 1 + natToInt (undefined :: n)

GHC informs us that it expects an OpenKind in the type specification of natToInt instead of a Nat and thus refuses to compile. This can be remedied by some kind casting:

data NatToOpen :: Nat -> *

and then replacing n with NatToOpen n in t the natToInt-s.

Question 1: is there some way to specify kinds other than * in any function without using type-level wrappers?

Question 2: It appears to me that non-class functions will happily work with types of any kind, for example:

foo :: (a :: *) -> (a :: *)
foo = id

bar = foo (S O)

but inside classes the compiler will complain about kind mismatches, as I described above. Why is that? It doesn't seem that non-class functions are properly polymorphic in kinds, because above I actually specified *, and it still works with Nat-s, as if the kinds were simply ignored.

Answer 1

Values always have types of kind * (possibly with some weird exceptions involving unboxing?), so there's nothing you can apply a function to or take as an argument that would have some other kind.

In your final example, you're applying foo to the unlifted version of Nat: the values are S and O, and their type is Nat, which has kind *. In the class definition, you give Nat as a kind using a signature, which means the lifted version, where S and O are types.

The NatToOpen type is just using phantom types in the usual way, but with a phantom type parameter of a non-* kind.

This distinction is not new with DataKinds, either. For example, there are no values whose type is Maybe :: * -> *, as distinct from the type forall a. Maybe a :: *, which is the type of Nothing.