| type Kind = Type | | What does this mean? It means that Kinds are represented by Types. Admittedly, Kinds only use a small fragment of what Types can represent, namely Arrow, and type constructor applications. So * is represented by a TyConApp with a TyCon that is called typeCon. The really annoying thing about Kinds is that there's occasionally a bit of sub-kinding. In particular error :: forall a. String -> a We want to allow error "foo" :: Int# so the kind of 'a' can't be *, nor # (the kind of unboxed types). It's an "open" kind, written "?"; both * and # are sub-kinds of ?. You should nevertheless be able to encode your kind system in the same way as GHC does. But I have been thinking that it's over-kill to use Types for Kinds, and leads to no real saving. I may well split the two types in the future. Simon