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 Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 2 years ago 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 TypeReps 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.

comment:3 Changed 2 years ago by dfeuer

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 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:

{-# 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 RyanGlScott

Cc: RyanGlScott added
Keywords: Typeable added; TypeableReflection removed

(Changing to the much more frequently used "Typeable" keyword.)

comment:6 Changed 2 years ago 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 DFuns.

comment:7 Changed 2 years ago 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 DFuns, and hack the constraint solver to let it solve Typeable k from Typeable (a :: k).

comment:8 Changed 2 years ago 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.

comment:9 Changed 2 years ago 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.
  1. 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.
  1. 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.

comment:10 Changed 2 years ago by bgamari

Differential Rev(s): Phab:D4000
Status: newpatch

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 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.

comment:12 Changed 2 years ago 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.

comment:13 in reply to:  12 Changed 2 years ago by dfeuer

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 Apps 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 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?

comment:15 Changed 2 years ago 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.

comment:16 Changed 20 months ago by bgamari

Milestone: 8.4.18.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.

comment:17 Changed 15 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be addressed by GHC 8.6.

comment:18 Changed 10 months ago by bgamari

Milestone: 8.8.18.10.1

This won't happen for 8.8.

Note: See TracTickets for help on using tickets.