<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">I think we're a long way off from supporting Typeable for higher-kinded types, so I wouldn't worry about that dark, spider-ridden corner.</div><div class=""><br class=""></div><div class="">Richard</div><br class=""><div><blockquote type="cite" class=""><div class="">On Sep 25, 2017, at 3:00 PM, David Feuer <<a href="mailto:david@well-typed.com" class="">david@well-typed.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class=""><div class=""><div class="">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 class=""><br class=""></div><div class=""><br class=""></div><div id="composer_signature" class=""><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class=""><div style="font-size:85%;color:#575757" class="">David Feuer</div><div style="font-size:85%;color:#575757" class="">Well-Typed, LLP</div></div><div class=""><br class=""></div><div style="font-size: 100%;" class=""><!-- originalMessage --><div class="">-------- Original message --------</div><div class="">From: Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" class="">rae@cs.brynmawr.edu</a>> </div><div class="">Date: 9/25/17 2:42 PM (GMT-05:00) </div><div class="">To: David Feuer <<a href="mailto:david@well-typed.com" class="">david@well-typed.com</a>> </div><div class="">Cc: Ben Gamari <<a href="mailto:ben@smart-cactus.org" class="">ben@smart-cactus.org</a>>, <a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a> </div><div class="">Subject: Re: Why isn't this Typeable? </div><div class=""><br class=""></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 class=""><br class="">Richard<br class=""><br class="">> On Sep 25, 2017, at 2:28 PM, David Feuer <<a href="mailto:david@well-typed.com" class="">david@well-typed.com</a>> wrote:<br class="">> <br class="">> My example wasn't quite the one I intended (although I think it should<br class="">> work as well, and it's simpler). Here's the sort of example I really intended:<br class="">> <br class="">> data Bar :: forall (j :: forall k. k -> Maybe k) (a :: Type). Proxy (j a) -> Type<br class="">> <br class="">> I would expect<br class="">> <br class="">> Bar :: Proxy ('Just Int) -> Type<br class="">> <br class="">> or, to abuse notation a bit,<br class="">> <br class="">> Bar @'Just @Int<br class="">> <br class="">> to be Typeable. What I'm really suggesting is that we should distinguish between things that are typeable and<br class="">> things that can be decomposed into typeable components. We already make a limited distinction<br class="">> here. For example, we have<br class="">> <br class="">> 'Just :: forall a. a -> Maybe a<br class="">> <br class="">> 'Just itself cannot be Typeable, but once it's applied to a kind variable, it is Typeable.<br class="">> 'Just @Int is Typeable even though that (kind) application cannot be broken with App. Similarly, I'd expect<br class="">> Foo 'Just to be Typeable even though that (type) application cannot be broken with App (or Fun).<br class="">> <br class="">> Putting things in terms of fingerprints, we can offer type-indexed fingerprints<br class="">> <br class="">> newtype Finger a = Finger Fingerprint<br class="">> <br class="">> for anything we can fingerprint. Is there any difficulty fingerprinting types like Foo 'Just and<br class="">> Bar @'Just @Int? Fingerprints are useful for lots of applications where decomposition isn't<br class="">> necessary.<br class="">> <br class="">> On Sunday, September 24, 2017 1:16:37 PM EDT Richard Eisenberg wrote:<br class="">>> 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 class="">>> <br class="">>> So I think that this boils down to impredicativity and that the implementation is doing the right thing here.<br class="">>> <br class="">>> Richard<br class="">>> <br class="">>>> On Sep 24, 2017, at 5:45 AM, David Feuer <<a href="mailto:david@well-typed.com" class="">david@well-typed.com</a>> wrote:<br class="">>>> <br class="">>>> data Foo :: (forall a. a -> Maybe a) -> Type<br class="">>>> <br class="">>>> 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 class="">>>> <br class="">>>> David Feuer<br class="">>>> Well-Typed, LLP<br class="">>>> _______________________________________________<br class="">>>> ghc-devs mailing list<br class="">>>> <a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a><br class="">>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br class="">>> <br class="">> <br class="">> <br class=""><br class=""></div></div></blockquote></div><br class=""></body></html>