eck first how much that matters.
>
>
> David Feuer
> Well-Typed, LLP
>
> Original message
> From: Richard Eisenberg
> Date: 9/25/17 2:42 PM (GMT-05:00)
> To: David Feuer
> Cc: Ben Gamari , ghc-devs@haskell.org
> Subject: Re: Why isn't this Type
the
generalization I describe, so I wanted to check first how much that matters.
David FeuerWell-Typed, LLP
Original message From: Richard Eisenberg
Date: 9/25/17 2:42 PM (GMT-05:00) To: David Feuer
Cc: Ben Gamari ,
ghc-devs@haskell.org Subject: Re: Why isn't this Typ
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 should
> work as well, and
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, t
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
0) 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 polymorp
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 examp
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