[GHC] #13370: exprIsBottom inconsistend with strictness analyser

#13370: exprIsBottom inconsistend with strictness analyser -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Because of `Note [IO hack in the demand analyser]` (which I hate), an expression like {{{ f :: Int -> State# RealWorld -> (# State# RealWorld, Int #) f x s = case blah of (# s::State# RealWorld, r::() #) -> error (show x) }}} is not reported as a bottoming function by the strictness analyser. But `exprBotStrictness_maybe` will say that the RHS ''is'' bottoming. That ultimately comes from `CoreArity.arityType` which has no analogous hack to the demand analyser. These can't both be right! We could * Cripple `exprBotStrictness_maybe` a bit by adding the hack there too. * Weaken the hack so that it propagates divergence. The demand-analyser hack note says {{{ {- Note [IO hack in the demand analyser] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ There's a hack here for I/O operations. Consider case foo x s of { (# s, r #) -> y } Is this strict in 'y'? Normally yes, but what if 'foo' is an I/O operation that simply terminates the program (not in an erroneous way)? In that case we should not evaluate 'y' before the call to 'foo'. Hackish solution: spot the IO-like situation and add a virtual branch, as if we had case foo x s of (# s, r #) -> y other -> return () So the 'y' isn't necessarily going to be evaluated A more complete example (Trac #148, #1592) where this shows up is: do { let len = <expensive> ; ; when (...) (exitWith ExitSuccess) ; print len } }}} I wonder if we could weaken the hack so that it propagated divergence /exception-thowing, while still making mentioned variables lazy. The big reason I'd like to do this is if we have {{{ case f x s of (# s',r #) -> BIG }}} then I really want to discard the alternative (since `f x s` is guaranteed to throw an exception) to give {{{ case f x s of {} }}} This is absolutely kosher; no change in evaluation order or anything. But weakening the IO hack in this way can change strictness. For example {{{ g A x y z s = x `seq` y `seq` (# s, () #) g B x y z s = x `seq` case blah2 of (# s', _ #) -> y `seq` (# s', () #) g C x y z s = case blah of (# s', _ #) -> error (show z) }}} Currently we treat this as lazy in x,y and z. With the above change, it'd become strict in `x` but not `y` or `z`, which is a little weird. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13370 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13370: exprIsBottom inconsistend with strictness analyser -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): PS: the inconsistency actually appears as lint warnings {{{ No alternatives for a case scrutinee not known to diverge for sure: tcGetDefaultTys6 }}} This happens because `FloatOut` hoist an expression like the RHS of `f` above to top level; and then uses `exprBotStrictness_maybe` to give it a cheap-and-cheerful strictness signature, one that says it diverges. That sig enables GHC to discard case alternatives. But then the final demand- analysis phase, just before CoreTidy, returns a more conservative verdict, after which the lint warnings appear. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13370#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13370: exprIsBottom inconsistent with strictness analyser -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13370#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13370: exprIsBottom inconsistent with strictness analyser -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): All this looks to me like a piece of a bigger puzzle we need to solve relating to strictness in the presence of: 1. Imprecise exceptions (which we have a whole paper about) 2. Precise exceptions (which I think we ''don't'' have a good story around at all--see #13380) 3. `catch` and friends. I had a (crazy?) thought last night. This may or may not make any sense at all, but it's driven by the fundamentally simple idea that ''precise'' exceptions should be modeled by something that looks vaguely similar to `ExceptT SomeException (State (State# RealWorld))`, but that fits into the `IO` type we're pretty much stuck with. Right now, `State# RealWorld` is terrifically boring for its entire life. But I don't know if it needs to be. Imagine if we had instead (very, very approximately) {{{#!hs data OK = OK State# RealWorld = (# OK | SomeException #) }}} where the "state of the real world" includes what precise exception (if any) we have encountered. Now we could talk about ''precise'' exceptions in Core in an entirely different fashion: {{{#!hs instance Monad IO where return x = IO $ \s -> (# s, x #) -- If the state has become exceptional, then performing additional -- actions is useless. m >>= f = IO $ \s -> case unIO m s of (# (# | e #), _ #) -> (# (# | e #), undefined #) (# s', r #) -> unIO (f r) s' throwIO e = IO $ \s -> (# (# | e #), undefined #) -- Function for catching only precise exceptions catchIO m f = IO $ \s -> case unIO m s of (# (# | e #), _ #) -> unIO (f e) realWorld# }}} Then `seq#` could take on the "magical" job of turning imprecise exceptions into precise ones, allowing us to implement `catch`. {{{#!hs catch# m f s = case seq# (m s) of (# (# | e #), _ #) -> f e realWorld# --Imprecise exception executing (m s) (# _, (# (# | e #), _ #) #) -> f e realWorld# --Precise exception executing (m s) (# _, res #) -> res }}} We'd need to perform some sort of magic in code generation to get rid of this wacky `State#` and implement exceptions in the usual fashion (I have no idea what that would look like myself). But in Core, I think we'd greatly confine the weirdness. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13370#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13370: exprIsBottom inconsistent with strictness analyser -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13370#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13370: exprIsBottom inconsistent with strictness analyser -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Exceptions Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * keywords: => Exceptions -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13370#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC