Why does the kind of my type have '-> Constraint' at the end?

Question

The Haskell tutorial I'm reading has a section introducing the basics of type kinds, and describes a type class

class Tofu t where  
    tofu :: j a -> t a j 

as having the kind

* -> (* -> *) -> *

I understand that, but when I enter :k Tofu in GHCi, I get

Tofu :: (* -> (* -> *) -> *) -> GHC.Prim.Constraint

What is GHC.Prim.Constraint and why does the kind of Tofu have this form rather than simply * -> (* -> *) -> *?

Answer 1

t is a type parameter of the class Tofu of kind * -> (* -> *) -> * (written t :: * -> (* -> *) -> *). This is the inferred type of t by GHC because in the absence of -XPolyKinds, GHC tries to default all type parameters to kind *. Thus GHC assumes a has kind * (though nothing in your signature makes this the only choice).

The type constructor (->) has kind * -> * -> *. Since j a appears as a parameter to (->), j a must have kind *. Since GHC has assumed that a has kind *, j is a type that takes something of kind * and returns something of kind *. Thus:

j :: * -> *

Since t is applied to both a and j, t has the kind * -> (* -> *) -> *, because the first argument a has kind * and the second argument j has kind *->*, and the overall type t a j must have kind * since it is also a parameter of the type (->).

Classes are just types taking type parameters (just like data Foo a b), except Foo a b has kind * while Tofu t has kind a special kind Constraint. Thus the kind of Tofu is:

(* -> (* -> *) -> *) -> Constraint

as GHC indicates. Constraint is just the kind given to constraints. In the signature

(Num a) => a -> a -> a

(Num a) is a type of kind Constraint.