en Gamari <b...@smart-cactus.org>, ghc-devs@haskell.org
> Subject: Re: Why isn't this Typeable?
>
> I suppose this is conceivable, but it would complicate the representation and
> solver for TypeReps considerably. Do you have a real use case?
>
> Richard
>
> > O
<b...@smart-cactus.org>,
ghc-devs@haskell.org Subject: Re: Why isn't this Typeable?
I suppose this is conceivable, but it would complicate the representation and
solver for TypeReps considerably. Do you have a real use case?
Richard
> On Sep 25, 2017, at 2:28 PM, David Feuer <da...@well-t
I suppose this is conceivable, but it would complicate the representation and
solver for TypeReps considerably. Do you have a real use case?
Richard
> On Sep 25, 2017, at 2:28 PM, David Feuer wrote:
>
> My example wasn't quite the one I intended (although I think it
My example wasn't quite the one I intended (although I think it should
work as well, and it's simpler). Here's the sort of example I really intended:
data Bar :: forall (j :: forall k. k -> Maybe k) (a :: Type). Proxy (j a)
-> Type
I would expect
Bar :: Proxy ('Just Int) -> Type
or,
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
:08 AM (GMT-05:00) To: ghc-devs@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
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
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