Trying to conclude Typeable Foo (or, if expanded with -fprint-explicit-kinds, Typeable ((forall a. a -> Maybe a) -> Type) Foo) is beyond GHC's capabilities at the moment, as that would require impredicative polymorphism. This problem has arose in other contexts too—see Trac #13895 [1] for one example. I don't think you can conclude Typeable (Foo 'Just) either, since that requires concluding both Typeable Foo and Typeable 'Just, so you ultimately run into the same problem. While there an in-the-works plan to allow a limited form of impredicativity through explicit use of visible type application [2], my fear is that that wouldn't be enough to address the problem you've encountered, since there's no way to visibly apply @((forall a. a -> Maybe a) -> Type) to Typeable at the moment. To accomplish this, you would need visible kind application [3]. Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/ticket/13895 [2] https://ghc.haskell.org/trac/ghc/ticket/11319#comment:11 [3] https://ghc.haskell.org/trac/ghc/ticket/12045