Changes between Initial Version and Version 1 of Ticket #7411, comment 31


Ignore:
Timestamp:
May 14, 2018 1:52:58 PM (16 months ago)
Author:
tdammers
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #7411, comment 31

    initial v1  
    1212For the second one, let me summarize what I think the core of the problem is: The equational reasoning strategies behind this eta expansion and `seq` are at odds. The eta expansion assumes that floating bottoms around will not make an effective difference (as per fast-and-loose reasoning), but this assumption doesn't hold when `seq` is involved, because `seq` is like this magical backdoor to bottoms. Eta expansion says that `case x of { _ -> f }` is equivalent to `\eta -> case x of { _ -> f eta }`, even if there are bottoms involved. But this breaks when `seq` is involved, because the eta expansion allows the argument to slip past `seq`.
    1313
    14 So what we would need to fix this "properly" would be a way to mark the relevant code sections as "here be dragons", and make the state hack skip over those. But I suspect this would be a rather invasive change (extending Core with such markers), and detecting such sections correctly could be tricky. Or maybe not, I really don't know.
     14So what we would need to fix this "properly" would be a way to mark the relevant code sections as "here be dragons", and make the state hack skip over those. E.g., in the example program discussed earlier:
     15{{{
     16import Control.Exception
     17
     18dslist :: [a] -> b -> b
     19dslist [] b = b
     20dslist (x:xs) b = x `seq` dslist xs b
     21
     22main = evaluate (('a':undefined) `dslist` return () :: IO ())
     23}}}
     24...we would mark the {{{x `seq` dslist xs b}}} part as "dangerous", and forbid eta-expanding across this boundary.
     25
     26Or rather, in this bit here:
     27{{{
     28lvl_s2Yn [Occ=Once]   -- Comes from 'return ()'
     29  :: GHC.Prim.State# GHC.Prim.RealWorld -> (# GHC.Prim.State# GHC.Prim.RealWorld, () #)
     30[LclId]
     31lvl_s2Yn
     32  = \ (s_a2z6 [Occ=Once, Dmd=<S,U>]
     33         :: GHC.Prim.State# GHC.Prim.RealWorld) ->
     34      (# s_a2z6, GHC.Tuple.() #)
     35
     36lvl_s2Yo [Occ=Once] :: GHC.Types.IO ()
     37[LclId]  -- Comes from (('a':undefined) `dslist` return ())
     38lvl_s2Yo
     39  = case go_s2WQ lvl_s2Ym of { __DEFAULT ->
     40    lvl_s2Yn
     41    `cast` (Sym (GHC.Types.N:IO[0] <()>_R)
     42            :: (GHC.Prim.State# GHC.Prim.RealWorld
     43                -> (# GHC.Prim.State# GHC.Prim.RealWorld, () #) :: *)
     44               ~R# (GHC.Types.IO () :: *))
     45    }
     46
     47main_s2z7
     48  = \ (s_a2yI [Occ=Once, Dmd=<S,U>]
     49         :: GHC.Prim.State# GHC.Prim.RealWorld) ->
     50      GHC.Prim.seq#
     51        @ (GHC.Types.IO ()) @ GHC.Prim.RealWorld lvl_s2Yo s_a2yI
     52}}}
     53...we would have to drag along the information that `go_s2WQ` is dangerous, and infer from that that we cannot eta-expand `lvl_s2Yo`.
     54
     55But I suspect this would be a rather invasive change (extending Core with such markers), and detecting such sections correctly could be tricky. Or maybe not, I really don't know.