Re: [ghc-steering-committee] Mind the gap

Richard are you satisfied that my example program is invalid under PolyKinds?

On 6 Jul 2022, at 12:51, Richard Eisenberg wrote:

...

On Jul 6, 2022, at 4:35 AM, Simon Peyton Jones mailto: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