Why isn't this Typeable?

[David Feuer]

I don't see why Typeable (Foo 'Just) requires that. I'd expect to get back a TrTyCon, not a TrApp. Some modifications to the structure of TrTyCon might be required.


David FeuerWell-Typed, LLP
-------- Original message --------From: Ryan Scott <ryan.gl.scott at gmail.com> Date: 9/24/17  10:08 AM  (GMT-05:00) To: ghc-devs at haskell.org Subject: Re: Why isn't this Typeable? 
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
_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170924/1ac68145/attachment.html>