[GHC] #9792: map/coerce rule never seems to fire
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core Libraries | Version: 7.9 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Runtime Blocked By: | performance bug Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- If I write a nice, simple use, like: {{{#!hs myPotato = map coerce }}} or even {{{#!hs 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. 2. 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 {{{#!hs 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): But I thought `Coercible` evidence is ''never'' ⊥... unless you're thinking about deferred type errors? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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 ⊥ `Coercible`s", 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 ⊥ `Coercible`s. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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` :-)) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
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
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:8 nomeata]: 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). 2. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule never seems to fire -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9792: map/coerce rule does not fire until the coercion is known -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: ekmett Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Core | Version: 7.9 Libraries | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Runtime | Related Tickets: performance bug | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9792#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC