Re: Why isn't this Typeable?

2017-09-25 Thread Richard Eisenberg
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

Re: Why isn't this Typeable?

2017-09-25 Thread David Feuer
<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

Re: Why isn't this Typeable?

2017-09-25 Thread Richard Eisenberg
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

Re: Why isn't this Typeable?

2017-09-25 Thread David Feuer
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,

Re: Why isn't this Typeable?

2017-09-24 Thread 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

Re: Why isn't this Typeable?

2017-09-24 Thread David Feuer
: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

Re: Why isn't this Typeable?

2017-09-24 Thread Ryan Scott
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

Why isn't this Typeable?

2017-09-24 Thread David Feuer
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