Opened 5 years ago

Last modified 4 years ago

#9792 new bug

map/coerce rule does not fire until the coercion is known

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Core Libraries Version: 7.9
Keywords: Cc: core-libraries-committee@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Runtime performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

If I write a nice, simple use, like:

myPotato = map coerce

or even

myPotato = Data.OldList.map coerce

the "map/coerce" rule does not fire.

It looks like there are two things getting in the way:

  1. The map rule fires first, turning map into a build/foldr form, which map/coerce does not recognize.
  1. Even if map gets written back, coerce has been expanded into something the rule doesn't recognize.

So we end up with something that looks like

myPotato =
  \ (@ a_are)
    (@ b_arf)
    ($dCoercible_arz :: Coercible a_are b_arf)
    (lst_aqx :: [a_are]) ->
    map
      @ a_are
      @ b_arf
      (\ (tpl_B2 [OS=ProbOneShot] :: a_are) ->
         case $dCoercible_arz
         of _ [Occ=Dead] { GHC.Types.MkCoercible tpl1_B3 ->
         tpl_B2 `cast` (tpl1_B3 :: a_are ~R# b_arf)
         })
      lst_aqx

Change History (17)

comment:1 Changed 5 years ago by dfeuer

I think the map rewrite probably isn't a big problem, because if map fuses with anything, the mapped coercion will become free (if a mapped coercion fuses with another mapped coercion, those will end up a mapped composed coercion—that might need some special treatment, but I'm not sure). The expansion of coerce, however, which seems to relate to the fact that Coercible has only one member, looks problematic.

comment:2 Changed 5 years ago by nomeata

We have a test case for this, T2110. I wonder why you observe something different.

My guess: Your code is polymorphic in the member of the list, and hence the code looks different and is no longer matched.

Now if GHC would float out the case $dCoercible_arz of, it would probably work. But of course it cannot, or we’d be stricter in the Coercible constraint than intended.

Ah: And in the polymorphic case, map coerce = coerce does not even hold! If the Coercible evidence is ⊥, then map coerce [] = [], but coerce [] = ⊥.

Given that high performance code is rarely polymorphic, I think we are fine.

comment:3 Changed 5 years ago by goldfire

But I thought Coercible evidence is never ⊥... unless you're thinking about deferred type errors?

comment:4 Changed 5 years ago by nomeata

But I thought Coercible evidence is never ⊥... unless you're thinking about deferred type errors?

It can be ⊥, just write coerceWith undefined using Data.Type.Coercion.

comment:5 Changed 5 years ago by goldfire

But that won't have a ⊥ Coercible evidence -- that will fail trying to get the Coercible evidence in the first place. Or am I confused?

comment:6 Changed 5 years ago by nomeata

I was confused. I thought for a moment that the type of $dCoercible_arz, i.e. Coercible is the same as the Coercion thingy, and the latter can be undefined. But they are not, Coercion adds another box around Coercible, I guess we avoid Coercion to be undefined.

But Coercible is a lifted type, so I’m not sure that we can guarantee that there is no way to produce a bottom here.

comment:7 Changed 5 years ago by goldfire

Depends on the meaning of "guarantee". You're right in that Coercible is lifted and can therefore, in theory, contain ⊥. However, as I understand it, we do some work to avoid ever creating ⊥ here. This is why we track stack depths (or some such) in the solver, right? Another way to say this is that we've designed the solver to avoid creating a ⊥ Coercible. So, if by "guarantee", we mean "If GHC is a bug-free implementation of its specification, then there are no ⊥ Coercibles", I think we're close. I believe the situation here is very close to that of ~, which is a lifted type but is supposedly never ⊥.

We're not quite there because of deferred type errors, which surely can create ⊥ Coercibles. But I'm personally OK with wonky semantics in this case, if the wonky semantics means real-world speedups in the vastly more common no-deferred-type-errors case.

comment:8 Changed 5 years ago by nomeata

Tracking the stack depths is to avoid generating looping code at runtime. But we don’t have this guarantee in Core, and the desugarer + typechecker is too large a beast to give any guarantees besides best-effort, I’d say.

Maybe it is possible to abstract over the constraints somehow, and write a constraint with value ⊥ in the general case, circumventing any special casing for Coercible?

(But even if it is possible it includes so much malice that whoever does that waives any right to complain about map coerce = coerce :-))

comment:9 Changed 5 years ago by dfeuer

Replying to nomeata:

Maybe it is possible to abstract over the constraints somehow, and write a constraint with value ⊥ in the general case, circumventing any special casing for Coercible?

(But even if it is possible it includes so much malice that whoever does that waives any right to complain about map coerce = coerce :-))

There's a lot I don't understand (including the two comments above), but here's what I think I do understand:

  1. Destroying the evidence: If GHC can get its hands on the concrete evidence, it will erase it, because it has the proof it needs. If it can't, it conservatively assumes that the evidence could be _|_, because getting this wrong would break the type system. This situation is somewhat unfortunate—if we can ensure the evidence is never bottom, we can be certain never to incur a runtime coercion cost. But without a proof the compiler gurus are unlikely to make that leap, and the people who've spoken up so far are not aware that anyone has proved it. One question in my mind is how this relates to #9701, and also whether GHC ensures that the evidence is as small as possible (coerce itself presumably can be a 0-size token, if it isn't already).
  1. Polymorphic map coerce, or more generally letting RULES get hold of a boxed up coerce: The situation here is far less dire. Replacing map coerce with coerce when coerce is bottom will turn a list of bottoms into bottom. Obviously, that wouldn't be wonderful, but it also wouldn't break the type system. I think that's the sort of thing that would be okay to implement optimistically and wait and see if anything breaks. What's involved in implementing it I wouldn't know. My understanding was that coerce is mostly about making things as efficient as possible in the face of lots of polymophism, so just accepting inefficiency because things are too polymorphic doesn't sound right here.

comment:10 Changed 5 years ago by nomeata

I think that's the sort of thing that would be okay to implement optimistically and wait and see if anything breaks

I wasn’t saying that we shouldn’t; I was just explaining why it is not.

I think one solution would be to assume everying is strict in values of type Coercible, so that the optimizer will move the case out as far as possible, outside the call to map, thus allowing the rule to match.

comment:11 Changed 5 years ago by simonpj

Tracking stack depths: this will go away when Richard completes his work of treating Coercible constraints more like nominal-equality constraints.

However, a value of type Coercible a b can certainly be bottom in Core, even if type inference engine will never produce it.

More promising is just to make functions strict in Coercible arguments. I should look again at -fdicts-strict.

Meanwhile Richard is also thinking about the whole lifted/unlifted equality thing, and I'd like to see how the dust settles there.

Simon

comment:12 Changed 5 years ago by goldfire

Forcing dictionary arguments to be strict helps here, but would that always work? For example, if we have

foo :: forall (c :: Constraint). c => Proxy c -> ()

would that still be inferred to be strict in its first (Core) parameter?

Separately, I don't think my lifted/unlifted thoughts will have impact here, although the rewrite of the Coercible solver may. That task will begin shortly.

comment:13 Changed 5 years ago by dfeuer

Summary: map/coerce rule never seems to firemap/coerce rule does not fire until the coercion is known

comment:14 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:15 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:16 Changed 4 years ago by thomie

Owner: ekmett deleted

comment:17 Changed 4 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.