Why isn't this Typeable?

[Richard Eisenberg]

The problem is that to get Typeable (Foo 'Just), we need Typeable 'Just. However, the kind parameter for Typeable 'Just would be (forall a. a -> Maybe a), making the full constraint Typable (forall a. a -> Maybe a) 'Just. And saying that would be impredicative. In other contexts, 'Just *can* be Typeable, but it's 'Just invisibly instantiated at some monotype for `a`.

So I think that this boils down to impredicativity and that the implementation is doing the right thing here.

Richard

> On Sep 24, 2017, at 5:45 AM, David Feuer <david at well-typed.com> wrote:
> 
> data Foo :: (forall a. a -> Maybe a) -> Type
> 
> Neither Foo nor Foo 'Just is Typeable. There seems to be a certain sense to excluding Foo proper, because it can't be decomposed with Fun. But why not Foo 'Just? Is there a fundamental reason, or is that largely an implementation artifact?
> 
> David Feuer
> Well-Typed, LLP
> _______________________________________________
> 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/b55f2ba6/attachment.html>