[hiker]

Going further one will need a word for "the kind of a kind", "the kind of a kind of a kind" and so on.

One solution is TypeInType, that is the type of a type is another type (not kind or something else). That's where Haskell is going with the work of adding Dependent Types to the language.

The problem with TypeInType is that it is logically inconsistent - it leads to Girard's paradox, analog to Russel's paradox in set theory.

The correct solution is type universes where every type lives in some type universe indexed by a natural number. For example terms are of type 'Type 1', 'Type 1' types are of type 'Type 2' and so on. The usual 'Type' is then just the first universe level 'Type 1' and 'Kind' is 'Type 2'.

Type universes is what most proof assistants employ, e.g. Agda, Coq, Lean. Idris uses TypeInType which is easier to use and there's no need to massage your program until all type universes type check but is logically inconsistent so one has to be careful to not reproduce Girard's paradox in some form or another.