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 <[email protected]> wrote: > > 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
