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 <[email protected]> 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
