So if we have polymorphic types, and now polymorphic kinds, if we call those first- and second-order polymorphism, why can't we extend this to higher orders? For instance, third-order would be when our kinds' types are also polymorphic.
[1] J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. (Shamelessly copied from Wikipedia)
What I'm getting at is that there are plenty of parts of GHC's flavor of Haskell that you can't depend on type inference for. You have to give type signatures for polymorphic recursion, for instance.