exprIsBottom inconsistent with strictness analyser

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.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture