[GHC] #13370: exprIsBottom inconsistend with strictness analyser

[GHC]

#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