Why isn't this Typeable?

[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, 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 <david at well-typed.com> 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
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>