To respond to your original point:
Morally I think that
class Typeable (a :: k)
should have been
class Typeable k => Typeable (a :: k)
This has been considered before, although it is not entirely straightforward to implement. See [1] and [2], which track the idea of having GHC solve these constraints automatically, without the need for users to explicitly reach for `typeRepKind`.
Best,
Ryan
-----