On Jul 6, 2022, at 4:35 AM, Simon Peyton Jones <simon.peytonjones@gmail.com> wrote:

I sort of wonder: if we have (Typeable t) should that not give us (Typeable k) where (t :: k)?  That would require us to have a function typeRepKind :: TypeRep (a::k) -> TypeRep k, and I don't know how hard that is to get.

We have that function. It's called typeRepKind. What we need for this example is a superclass constraint:

class Typeable k => Typeable (a :: k)

which would probably require UndecidableSuperClasses, but otherwise might just work.

Richard