Opened 2 years ago
Last modified 10 months ago
#14190 patch bug
Typeable imposes seemingly redundant constraints on polykinded instances
Reported by: | dfeuer | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.10.1 |
Component: | Compiler (Type checker) | Version: | 8.2.1 |
Keywords: | Typeable | Cc: | bgamari, Iceland_jack, RyanGlScott |
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: |
Description
To derive Data
for Const
, we need
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:
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:
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
Change History (18)
comment:1 Changed 2 years ago by
Cc: | Iceland_jack added |
---|
comment:2 Changed 2 years ago by
comment:3 Changed 2 years ago by
Ryan, my point is that the TypeRep k
can be extracted from the TypeRep b
to simplify the constraint.
comment:4 Changed 2 years ago by
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:
{-# 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 discussion about this on the corresponding GHC proposal, but it didn't seem to make it into GHC's implementation of it.
Ben, do you know what became of this idea?
comment:5 Changed 2 years ago by
Cc: | RyanGlScott added |
---|---|
Keywords: | Typeable added; TypeableReflection removed |
(Changing to the much more frequently used "Typeable" keyword.)
comment:6 Changed 2 years ago by
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.
comment:7 Changed 2 years ago by
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)
.
comment:8 Changed 2 years ago by
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.
comment:9 Changed 2 years ago by
Here's how I think of it:
- Given
r :: TypeRep (t :: k)
, can I somehow obtainrk :: TypeRep k
? The current answer is "yes": usetypeRepKind r
.
- Given
d :: Typeable (t :: k)
, can I somehow obtaindk :: Typeable k
? The answer clearly should be "yes of course", because aTypeable
dictionary is no more than a wrapper around aTypeRep
.
- One way to achieve (2) would to make
Typeable k
a superclass ofTypeable (a::k)
. But that would be stupid.- It'd mean that every
Typeable (t::k)
dictionary was represented as a pair of a dictionary forTypeable k
and aTypeRep 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.
- It'd mean that every
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.
comment:10 Changed 2 years ago by
Differential Rev(s): | → Phab:D4000 |
---|---|
Status: | new → patch |
See Phab:D4000 for an implementation of comment:9. It currently doesn't validate but I'll try to finish it up tonight.
comment:11 Changed 2 years ago by
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.
comment:12 follow-up: 13 Changed 2 years ago by
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.
comment:13 Changed 2 years ago by
Replying to 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.
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.
comment:14 Changed 2 years ago by
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?
comment:15 Changed 2 years ago by
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.
comment:16 Changed 20 months ago by
Milestone: | 8.4.1 → 8.6.1 |
---|
This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.
The reason you need a
Typeable k
constraint is quite simple:k
is just as much of a type asa
orb
, so in order to obtain a properTypeRep
forConst
, you need to also obtain theTypeRep
s fora
,b
, andk
, requiring them all to beTypeable
instances:I don't see a bug here.