<html><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"></head><body><div>No. What led me down this path is that I was thinking about whether we could simplify the representation and reduce the TCB. The as-yet-incomplete ideas I had (largely based on the concept of using a constructor name as a singletons-style defunctionalization symbol) seem difficult to adapt to the generalization I describe, so I wanted to check first how much that matters.</div><div><br></div><div><br></div><div id="composer_signature"><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"><div style="font-size:85%;color:#575757">David Feuer</div><div style="font-size:85%;color:#575757">Well-Typed, LLP</div></div><div><br></div><div style="font-size:100%;color:#000000"><!-- originalMessage --><div>-------- Original message --------</div><div>From: Richard Eisenberg <rae@cs.brynmawr.edu> </div><div>Date: 9/25/17 2:42 PM (GMT-05:00) </div><div>To: David Feuer <david@well-typed.com> </div><div>Cc: Ben Gamari <ben@smart-cactus.org>, ghc-devs@haskell.org </div><div>Subject: Re: Why isn't this Typeable? </div><div><br></div></div>I suppose this is conceivable, but it would complicate the representation and solver for TypeReps considerably. Do you have a real use case?<br><br>Richard<br><br>> On Sep 25, 2017, at 2:28 PM, David Feuer <david@well-typed.com> wrote:<br>> <br>> My example wasn't quite the one I intended (although I think it should<br>> work as well, and it's simpler). Here's the sort of example I really intended:<br>> <br>> data Bar :: forall (j :: forall k. k -> Maybe k) (a :: Type). Proxy (j a) -> Type<br>> <br>> I would expect<br>> <br>> Bar :: Proxy ('Just Int) -> Type<br>> <br>> or, to abuse notation a bit,<br>> <br>> Bar @'Just @Int<br>> <br>> to be Typeable. What I'm really suggesting is that we should distinguish between things that are typeable and<br>> things that can be decomposed into typeable components. We already make a limited distinction<br>> here. For example, we have<br>> <br>> 'Just :: forall a. a -> Maybe a<br>> <br>> 'Just itself cannot be Typeable, but once it's applied to a kind variable, it is Typeable.<br>> 'Just @Int is Typeable even though that (kind) application cannot be broken with App. Similarly, I'd expect<br>> Foo 'Just to be Typeable even though that (type) application cannot be broken with App (or Fun).<br>> <br>> Putting things in terms of fingerprints, we can offer type-indexed fingerprints<br>> <br>> newtype Finger a = Finger Fingerprint<br>> <br>> for anything we can fingerprint. Is there any difficulty fingerprinting types like Foo 'Just and<br>> Bar @'Just @Int? Fingerprints are useful for lots of applications where decomposition isn't<br>> necessary.<br>> <br>> On Sunday, September 24, 2017 1:16:37 PM EDT Richard Eisenberg wrote:<br>>> 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`.<br>>> <br>>> So I think that this boils down to impredicativity and that the implementation is doing the right thing here.<br>>> <br>>> Richard<br>>> <br>>>> On Sep 24, 2017, at 5:45 AM, David Feuer <david@well-typed.com> wrote:<br>>>> <br>>>> data Foo :: (forall a. a -> Maybe a) -> Type<br>>>> <br>>>> 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?<br>>>> <br>>>> David Feuer<br>>>> Well-Typed, LLP<br>>>> _______________________________________________<br>>>> ghc-devs mailing list<br>>>> ghc-devs@haskell.org<br>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br>>> <br>> <br>> <br><br></body></html>