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, to abuse notation a bit,
Bar @'Just @Int
to be Typeable. What I'm really suggesting is that we should distinguish
between things that are typeable and
things that can be decomposed into typeable components. We already make a
limited distinction
here. For example, we have
'Just :: forall a. a -> Maybe a
'Just itself cannot be Typeable, but once it's applied to a kind variable, it
is Typeable.
'Just @Int is Typeable even though that (kind) application cannot be broken
with App. Similarly, I'd expect
Foo 'Just to be Typeable even though that (type) application cannot be broken
with App (or Fun).
Putting things in terms of fingerprints, we can offer type-indexed fingerprints
newtype Finger a = Finger Fingerprint
for anything we can fingerprint. Is there any difficulty fingerprinting types
like Foo 'Just and
Bar @'Just @Int? Fingerprints are useful for lots of applications where
decomposition isn't
necessary.
On Sunday, September 24, 2017 1:16:37 PM EDT Richard Eisenberg wrote:
> 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
