Dear Type Theory Experts, I’ve a broad question: in terms of expressivity, is there a difference between a type system that includes a third sort for managing kind-polymorphism (à la System U), and a type system that uses the Type : Type rule (à la GHC Haskell)?

I know that both are inconsistent as a logic, but I’m interested in their pragmatic application for type-level programming.