[GHC] #14190: Typeable imposes seemingly redundant constraints on polykinded instances
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeableReflection | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- To derive `Data` for `Const`, we need {{{#!hs deriving instance (Typeable k, Data a, Typeable (b :: k)) => Data (Const a b) }}} Where's that `Typeable k` constraint come from? It turns out that for reasons I haven't looked into, we can only obtain `Typeable (Const a (b :: k))` if we have `Typeable k`; `(Typeable a, Typeable b)` is insufficient. Is there a reason for that? Annoyingly, we can actually ''get'' that: {{{#!hs weGotThat :: forall k (a :: k). Typeable a :- Typeable k weGotThat = Sub $ withTypeable (typeRepKind (typeRep :: TypeRep a)) Dict }}} But of course that doesn't help us. Could we use `UndecidableSuperClasses` to work around this problem? I think we likely can, although I'm concerned about the performance implications: {{{#!hs class (Typeable a, Typeable' k) => Typeable' (a :: k) instance (Typeable a, Typeable' k) => Typeable' (a :: k) withTypeable' :: forall k (a :: k) r. TypeRep a -> (Typeable' a => r) -> r withTypeable' tr f = withTypeable tr $ withTypeable (typeRepKind (typeRep @a)) f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | TypeableReflection Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | TypeableReflection Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The reason you need a `Typeable k` constraint is quite simple: `k` is just as much of a type as `a` or `b`, so in order to obtain a proper `TypeRep` for `Const`, you need to also obtain the `TypeRep`s for `a`, `b`, and `k`, requiring them all to be `Typeable` instances: {{{ λ> typeRep :: TypeRep (Const String Type) Const * [Char] * λ> typeRep :: TypeRep (Const String (Nothing :: Maybe Bool)) Const (Maybe Bool) [Char] ('Nothing Bool) }}} I don't see a bug here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | TypeableReflection Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Ryan, my point is that the `TypeRep k` can be extracted from the `TypeRep b` to simplify the constraint. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | TypeableReflection Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Sorry, I think I woefully misunderstood the point you were making. You're not arguing that we shouldn't require `k` to be a `Typeable` instance, but rather than if you have `Typeable (a :: k)`, then that //implies// `Typeable k`. I must admit I wasn't aware of the `weGotThis` trick you showed off above. Here's a version that doesn't depend on the `constraints` library: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} import Type.Reflection hm :: forall k (a :: k). Typeable a => TypeRep k hm = withTypeable (typeRepKind (typeRep @a)) (typeRep @k) }}} In light of this, your suggestion to make `Typeable k` a superclass of `Typeable (a :: k)` makes much more sense. In fact, there was some [https://github.com/ghc-proposals/ghc- proposals/pull/16#issuecomment-255645119 discussion] about this on the corresponding GHC proposal, but it didn't seem to make it into [http://git.haskell.org/ghc.git/blob/055d73c6576bed2affaf96ef6a6b89aeb2cd2e9f... GHC's implementation] of it. Ben, do you know what became of this idea? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeableReflection => Typeable * cc: RyanGlScott (added) Comment: (Changing to the much more frequently used "Typeable" keyword.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): While the superclass approach probably has the best ergonomics, it makes the dictionary heavier. My suggestion was to extract the typerep-of-kind information as required in the `DFun`s. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I think the ideal ergonomics with the best performance would likely be to leave the class as it is, extract the typerep-of-kind info as needed in the `DFun`s, and hack the constraint solver to let it solve `Typeable k` from `Typeable (a :: k)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Regarding comment:7, I'm not sure how easy it would be to implement this. Goldfire will need to comment here, but it seems like this may be hard as there is nothing tying `k` back to `a`. One way of hacking around this might be to add `Typeable k` evidence to the solved dictionary cache every time we solve for `Typeable (a :: k)`. However, this would lead to the production of lots of redundant evidence and just feels terribly wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Here's how I think of it: 1. Given `r :: TypeRep (t :: k)`, can I somehow obtain `rk :: TypeRep k`? The current answer is "yes": use `typeRepKind r`. 2. Given `d :: Typeable (t :: k)`, can I somehow obtain `dk :: Typeable k`? The answer clearly should be "yes of course", because a `Typeable` dictionary is no more than a wrapper around a `TypeRep`. 3. One way to achieve (2) would to make `Typeable k` a superclass of `Typeable (a::k)`. But that would be stupid. * It'd mean that every `Typeable (t::k)` dictionary was represented as a pair of a dictionary for `Typeable k` and a `TypeRep t`. * But the latter already can provide a `TypeRep k`, via (1) * Moreover that `Typeable k` dictionary would itself be a pair, and so on infinitely. So, assuming we want to continue to have `typeRepKind`, the obvious way forward is to teach the solver that it behaves as a kind of virtual superclass of `Typeable`. That is, if you have `[G] Typeable (t::k)` then, when expanding superclasses, you can extract `Typeable k`. Not terribly hard; we'd need a new `EvTerm` to express that extraction. As with undecidable superclasses we'd only want to do one step at a time. Then, quite separately, we might like to think about how to make `typeRepKind` more efficient. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => patch * differential: => Phab:D4000 Comment: See Phab:D4000 for an implementation of comment:9. It currently doesn't validate but I'll try to finish it up tonight. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I guess we really do want `typeRepKind`. Without it, we have no way to get the kinds of the pieces once we decompose. This doesn't seem to have been considered in the original paper, perhaps because the authors were thinking of `TypeInType` only as part of the solution, and not as part of the problem. I think we almost certainly want to expand the data constructors (probably all of them) to accommodate typereps of kinds. One thing I'm rather unclear on is just what information is stored in a `TyCon` (most particularly, what a `KindRep` is about) and whether we really need all that information in that form in the typerep of a tycon. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Without it, we have no way to get the kinds of the pieces once we decompose
I think it would be useful to give a concrete example of this, and put that example in a Note with the code for `typeRepKind`. So far I have always supposed that it's a convenience mechanism: you can always pass a `TypeRep` for the kind separately. But maybe I'm wrong. I'm not against `typeRepKind`, just wanting a slam-dunk argument that we need it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Without it, we have no way to get the kinds of the pieces once we decompose
I think it would be useful to give a concrete example of this, and put
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:12 simonpj]: that example in a Note with the code for `typeRepKind`.
So far I have always supposed that it's a convenience mechanism: you can
always pass a `TypeRep` for the kind separately. But maybe I'm wrong.
I'm not against `typeRepKind`, just wanting a slam-dunk argument that we
need it. I haven't dug into enough examples of type reflection to know how often this is important. The one place I've seen so far is in de/serialization, where we need it if we want to check well-kindedness of deserialized typereps. Richard's suggestion that we dig into nested `App`s to find the constructor and build from there seems likely to be a good way to avoid needing a general `typeRepKind` there. For `dynApply`, storing the representation of the kind separately is sufficient, I think. But I don't know if some more sophisticated use of `Typeable` will really need kinds of deconstructed typereps. Ben: when we serialize a nest of applications, I think we probably don't want to emit a tag for each `App`. Use an `Apps` tag instead. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I like comment:7 and Simon's suggested implementation of comment:7 in comment:9. Ben's worry about redundant constraints floating around (comment:8) is a valid concern, but GHC already worries about this with any superclass constraints (as comment:9 hints). Re Simon's comment:12: You can't always pass the `TypeRep` for a kind separately. If you have the `TypeRep` for `(a :: k -> Type) (b :: k)`, then you don't always have the `TypeRep` for `k` to hand. `typeRepKind` allows you to get the kind once you've decompose an application. Also, while we're thinking about changing the concrete representation of `TypeRep`, might we consider getting rid of `TrFun`? GHC has very good reasons for having a streamlined representation for functions, but `TypeRep` doesn't have as clear-cut a use-case for this. Getting rid of `TrFun` would greatly simplify, e.g., `splitApp`. Was it motivated directly by performance (or other) problems? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Getting rid of `TrFun` does seem to simplify the story substantially. If we end up keeping it, by the way, I think we should really have a `Note` explaining why the fingerprinting is safe. It's because whenever `p q` is well-kinded, `p -> q` is not. Not a complicated matter, but I think one worth mentioning. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14190: Typeable imposes seemingly redundant constraints on polykinded instances -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4000 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.8.1 => 8.10.1 Comment: This won't happen for 8.8. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14190#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC