Why isn't this Typeable?
ryan.gl.scott at gmail.com
Sun Sep 24 14:08:49 UTC 2017
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  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 ,
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 .
More information about the ghc-devs