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

changed weight to 5

added Tbug Trac import labels

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.

changed title from exprIsBottom inconsistend with strictness analyser to exprIsBottom inconsistent with strictness analyser

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 (closed))
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)

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:

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.

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.

Trac metadata

Trac field	Value
CC	- → dfeuer

added exceptions label

added Pnormal label

marked this issue as related to #17999

mentioned in issue #24623 (closed)