Typeable imposes seemingly redundant constraints on polykinded instances
Const, we need
deriving instance (Typeable k, Data a, Typeable (b :: k)) => Data (Const a b)
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 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
|Component||Compiler (Type checker)|