To derive Data for Const, we need

deriving instance (Typeable k, Data a, Typeable (b :: k)) => Data (Const a b)

Where's that Typeable k constraint come from? It turns out that for reasons I haven't looked into, we can only obtain Typeable (Const a (b :: k)) if we have Typeable k; (Typeable a, Typeable b) is insufficient. Is there a reason for that?

Annoyingly, we can actually get that:

weGotThat :: forall k (a :: k). Typeable a :- Typeable k
weGotThat = Sub $ withTypeable (typeRepKind (typeRep :: TypeRep a)) Dict

But of course that doesn't help us.

Could we use UndecidableSuperClasses to work around this problem? I think we likely can, although I'm concerned about the performance implications:

class (Typeable a, Typeable' k) => Typeable' (a :: k)
instance (Typeable a, Typeable' k) => Typeable' (a :: k)

withTypeable' :: forall k (a :: k) r. TypeRep a -> (Typeable' a => r) -> r
withTypeable' tr f = withTypeable tr $ withTypeable (typeRepKind (typeRep @a)) f