Kinds of types in functions
haskell
Solution
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`.
Problem
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.