This extension (together with the type-level built-in literals, described in section 8.3 of the paper) looks like it will address the major remaining wart I've observed in Haskell: the widespread use of complex type-level programming to make up for deficiencies in the type system. Many packages on Hackage have deep type-level hackery under the surface, and that hackery often creates subtle differences and incompatibilities.
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.
Interesting. The extensions to the type system remind me of Ωmega (<a href="http://code.google.com/p/omega/" rel="nofollow">http://code.google.com/p/omega/</a>), though without higher-order kinds.<p>EDIT: Turns out "Programming in Omega" is cited by the section on related work. No wonder the mention of proving red-black trees using type-level computation seemed familiar...
It sounds pretty neat, but how could all this intimidating-looking type theory this be made useful for ordinary programmers who don't know what a monad is?