Preserve precise exceptions in strictness analysis

The "IO hack" (which is a fallback to preserve precise exceptions
semantics and thus *soundness*, rather than some smart thing that
increases *precision*) always was quite hard to understand. That led to
a misguided effort to simplify it (!1829), because the Note wasn't
particularly clear about what kinds of side-effects it cares about.

The implementation seemed to care about preserving precise exception
semantics, but failed to deliver for the central case of `raiseIO#`
(#17676), which is in stark contrast to one of the motivating examples
in the Note (the one about `exitWith ExitSuccess`).

This patch rewords the Note to apply to IO actions throwing precise
exceptions, rather than all side-effecting IO actions (such as write
effects) in general. Also it makes this clear in the implementation by
extracting the rather opaque `io_hack_reqd` into
`CoreUtils.exprMightThrowPreciseException`.

In fact, that alone wasn't enough to fix #17676. It actually turned out
to be a duplicate of #13380, for which we had a fix in 7b087aeb, making
`catchIO#` have `topDiv` from `botDiv`. But that was reverted on the
grounds of regressing dead code elimination too much. In this patch
we introduce `exnDiv` for `raiseIO#`, the `defaultDmd` of which acts
like `topDiv`s (which was the key point which fixed #13380), but
otherwise acts like `botDiv` in terms of dead code elimination.

Fixes #13380 and #17676.

12 files changed, 362 insertions, 181 deletions

diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index d84bcdd774..c3f92f37d6 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -24,7 +24,7 @@ module GHC.Core.Utils (
         -- * Properties of expressions
         exprType, coreAltType, coreAltsType, isExprLevPoly,
         exprIsDupable, exprIsTrivial, getIdFromTrivialExpr, exprIsBottom,
-        getIdFromTrivialExpr_maybe,
+        exprMayThrowPreciseException, getIdFromTrivialExpr_maybe,
         exprIsCheap, exprIsExpandable, exprIsCheapX, CheapAppFun,
         exprIsHNF, exprOkForSpeculation, exprOkForSideEffects, exprIsWorkFree,
         exprIsConLike,
@@ -88,10 +88,11 @@ import Unique
 import Outputable
 import TysPrim
 import GHC.Driver.Session
+import TysWiredIn
 import FastString
 import Maybes
 import ListSetOps       ( minusList )
-import BasicTypes       ( Arity, isConLike )
+import BasicTypes       ( Arity, isConLike, Boxity(..) )
 import Util
 import Pair
 import Data.ByteString     ( ByteString )
@@ -1026,6 +1027,39 @@ exprIsTrivial (Cast e _)       = exprIsTrivial e
 exprIsTrivial (Case e _ _ [])  = exprIsTrivial e  -- See Note [Empty case is trivial]
 exprIsTrivial _                = False
 
+-- | Whether an expression might throw a precise exception when evaluated.
+-- Only true for an IO action that is not a 'PrimOp' application other than
+-- 'raiseIO#'.
+--
+-- See Note [Precise exceptions and strictness analysis] in Demand.
+exprMayThrowPreciseException :: CoreExpr -> Bool
+exprMayThrowPreciseException e
+  -- No precise exception without IO. We give no guarantees wrt. to
+  -- unsafePerformIO!
+  | not (is_io_action e)
+  = False
+
+  -- The only IO PrimOp that throws a precise exception is RaiseIOOp.
+  | (Var f, _) <- collectArgs e
+  , Just op    <- isPrimOpId_maybe f
+  = op == RaiseIOOp
+
+  -- A conservative default for all the other cases. Even a simple wrapper
+  -- around a non-RaiseIOOp will default to this! However, being more precise
+  -- would require a program analysis.
+  | otherwise
+  = True
+  where
+    is_io_action e
+      | Just (tc, [_rep1, _rep2, rw, _a]) <- splitTyConApp_maybe (exprType e)
+      , Just dc <- tyConSingleAlgDataCon_maybe tc
+      , dc == tupleDataCon Unboxed 2
+      , rw `eqType` realWorldStatePrimTy
+      = True
+      | otherwise
+      = False
+
+
 {-
 Note [getIdFromTrivialExpr]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/basicTypes/Demand.hs b/compiler/basicTypes/Demand.hs
index 26452721b2..085bc9c868 100644
--- a/compiler/basicTypes/Demand.hs
+++ b/compiler/basicTypes/Demand.hs
@@ -29,7 +29,7 @@ module Demand (
         DmdEnv, emptyDmdEnv,
         peelFV, findIdDemand,
 
-        Divergence(..), lubDivergence, isBotDiv, isTopDiv, topDiv, botDiv,
+        Divergence(..), lubDivergence, isBotDiv, isTopDiv, topDiv, botDiv, exnDiv,
         appIsBottom, isBottomingSig, pprIfaceStrictSig,
         StrictSig(..), mkStrictSigForArity, mkClosedStrictSig,
         nopSig, botSig, cprProdSig,
@@ -41,7 +41,7 @@ module Demand (
 
         evalDmd, cleanEvalDmd, cleanEvalProdDmd, isStrictDmd,
         splitDmdTy, splitFVs,
-        deferAfterIO,
+        deferAfterPreciseException,
         postProcessUnsat, postProcessDmdType,
 
         splitProdDmd_maybe, peelCallDmd, peelManyCalls, mkCallDmd, mkCallDmds,
@@ -180,6 +180,129 @@ is not strict in its argument: Just try this in GHCi
 
 Any analysis that assumes otherwise will be broken in some way or another
 (beyond `-fno-pendantic-bottoms`).
+
+But then #13380 and #17676 suggest (in Mar 20) that we need to re-introduce a
+subtly different variant of `ThrowsExn` (which we call `ExnOrDiv` now) that is
+only used by `raiseIO#` in order to preserve precise exceptions by strictness
+analysis, while not impacting the ability to eliminate dead code.
+See Note [Precise exceptions and strictness analysis].
+
+Note [Precise exceptions and strictness analysis]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have to take care to preserve precise exception semantics (#17676).
+There are two scenarios that need careful hacks.
+
+Scenario 1: Precise exceptions in case scrutinees
+-------------------------------------------------
+Consider
+
+     case foo x s of { (# s', r #) -> y }
+
+Is this strict in 'y'? Often not! If @foo x s@ might throw a precise exception
+(ultimately via the 'raiseIO#' PrimOp), then we must not force 'y' (which may
+fail to terminate or throw an imprecise exception) until we have performed
+@foo x s@.
+
+Hackish solution: spot the exceptional 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.
+
+The function that spots this situation is
+'CoreUtils.exprMayThrowPreciseException', and
+'Demand.deferAfterPreciseException' will lub with the strictness analysis
+results of the virtual branch.
+
+A more complete example (#148, #1592) where this shows up is:
+     do { let len = <expensive> ;
+        ; when (...) (exitWith ExitSuccess)
+        ; print len }
+Here, we want to defer, because @when (...) (exitWith ExitSuccess)@ might throw
+a precise exception.
+
+However, consider
+  f x s = case getMaskingState# s of
+            (# s, r #) ->
+          case x of I# x2 -> ...
+
+Here it is terribly sad to make 'f' lazy in 'x'.  After all,
+getMaskingState# is not going throw a precise exception! And
+'exprMayThrowPreciseException' recognises that.
+This situation actually arises in GHC.IO.Handle.Internals.wantReadableHandle
+(on an MVar not an Int), and made a material difference.
+
+Scenario 2: Precise exceptions in case alternatives
+---------------------------------------------------
+The motivating example for #13380 is the following:
+    f x y | x>0       = raiseIO blah
+          | y>0       = return 1
+          | otherwise = return 2
+If 'f' was inferred to be strict in 'y', WW would turn a precise into an
+imprecise exception in the call site @f 1 (error "boom")@.
+
+The solution is to give 'raiseIO#' 'topDiv' instead of 'botDiv', so that its
+'Demand.defaultDmd' is lazy. But then the simplifier fails to eliminate a lot of
+dead code, namely when 'raiseIO#' occurs in a case scrutinee. Hence we need to
+give it 'exnDiv', which was conceived entirely for this reason. The default
+demand of 'exnDiv' is lazy, but otherwise (in terms of 'Demand.isBotDiv') it
+behaves exactly as 'botDiv', so that dead code elimination works as expected.
+
+Note [Demand on the scrutinee of a product case]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When figuring out the demand on the scrutinee of a product case,
+we use the demands of the case alternative, i.e. id_dmds.
+But note that these include the demand on the case binder;
+see Note [Demand on case-alternative binders] in Demand.hs.
+This is crucial. Example:
+   f x = case x of y { (a,b) -> k y a }
+If we just take scrut_demand = U(L,A), then we won't pass x to the
+worker, so the worker will rebuild
+     x = (a, absent-error)
+and that'll crash.
+
+Note [Aggregated demand for cardinality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We use different strategies for strictness and usage/cardinality to
+"unleash" demands captured on free variables by bindings. Let us
+consider the example:
+
+f1 y = let {-# NOINLINE h #-}
+           h = y
+       in  (h, h)
+
+We are interested in obtaining cardinality demand U1 on |y|, as it is
+used only in a thunk, and, therefore, is not going to be updated any
+more. Therefore, the demand on |y|, captured and unleashed by usage of
+|h| is U1. However, if we unleash this demand every time |h| is used,
+and then sum up the effects, the ultimate demand on |y| will be U1 +
+U1 = U. In order to avoid it, we *first* collect the aggregate demand
+on |h| in the body of let-expression, and only then apply the demand
+transformer:
+
+transf[x](U) = {y |-> U1}
+
+so the resulting demand on |y| is U1.
+
+The situation is, however, different for strictness, where this
+aggregating approach exhibits worse results because of the nature of
+|both| operation for strictness. Consider the example:
+
+f y c =
+  let h x = y |seq| x
+   in case of
+        True  -> h True
+        False -> y
+
+It is clear that |f| is strict in |y|, however, the suggested analysis
+will infer from the body of |let| that |h| is used lazily (as it is
+used in one branch only), therefore lazy demand will be put on its
+free variable |y|. Conversely, if the demand on |h| is unleashed right
+on the spot, we will get the desired result, namely, that |f| is
+strict in |y|.
+
+
 -}
 
 -- | Vanilla strictness domain
@@ -896,40 +1019,55 @@ splitProdDmd_maybe (JD { sd = s, ud = u })
 {-
 ************************************************************************
 *                                                                      *
-                   Termination
+                   Divergence
 *                                                                      *
 ************************************************************************
-
-Divergence:     Dunno
-               /
-          Diverges
-
-In a fixpoint iteration, start from Diverges
 -}
 
+-- | Divergence lattice.
+--
+-- @
+--         Dunno
+--           |
+-- ThrowsExceptionOrDiverges
+--           |
+--        Diverges
+-- @
+--
+-- See Note [Precise exceptions and strictness analysis] for why we have that
+-- additional bottom-like element.
 data Divergence
-  = Diverges    -- Definitely diverges
-  | Dunno       -- Might diverge or converge
+  = Diverges -- ^ Definitely throws an imprecise exception or diverges.
+  | ExnOrDiv -- ^ Definitely throws a *precise* exception, an imprecise
+             --   exception or diverges.
+             --   See Note [Precise exceptions and strictness analysis].
+  | Dunno    -- ^ Might diverge or converge.
   deriving( Eq, Show )
 
 lubDivergence :: Divergence -> Divergence ->Divergence
 lubDivergence Diverges r        = r
 lubDivergence r        Diverges = r
-lubDivergence Dunno    Dunno    = Dunno
+lubDivergence Dunno    _        = Dunno
+lubDivergence _        Dunno    = Dunno
+lubDivergence ExnOrDiv ExnOrDiv = ExnOrDiv
 -- This needs to commute with defaultDmd, i.e.
 -- defaultDmd (r1 `lubDivergence` r2) = defaultDmd r1 `lubDmd` defaultDmd r2
 -- (See Note [Default demand on free variables] for why)
 
 bothDivergence :: Divergence -> Divergence -> Divergence
 -- See Note [Asymmetry of 'both' for DmdType and Divergence]
-bothDivergence _ Diverges = Diverges
-bothDivergence r Dunno    = r
+bothDivergence _        Diverges = Diverges
+bothDivergence Diverges _        = Diverges
+bothDivergence r        Dunno    = r
+bothDivergence Dunno    r        = r
+bothDivergence ExnOrDiv ExnOrDiv = ExnOrDiv
 -- This needs to commute with defaultDmd, i.e.
 -- defaultDmd (r1 `bothDivergence` r2) = defaultDmd r1 `bothDmd` defaultDmd r2
 -- (See Note [Default demand on free variables] for why)
 
 instance Outputable Divergence where
   ppr Diverges      = char 'b'
+  ppr ExnOrDiv      = char 'x'
   ppr Dunno         = empty
 
 ------------------------------------------------------------------------
@@ -938,8 +1076,9 @@ instance Outputable Divergence where
 
 -- [cprRes] lets us switch off CPR analysis
 -- by making sure that everything uses TopRes
-topDiv, botDiv :: Divergence
+topDiv, exnDiv, botDiv :: Divergence
 topDiv = Dunno
+exnDiv = ExnOrDiv
 botDiv = Diverges
 
 isTopDiv :: Divergence -> Bool
@@ -949,13 +1088,16 @@ isTopDiv _     = False
 -- | True if the result diverges or throws an exception
 isBotDiv :: Divergence -> Bool
 isBotDiv Diverges = True
+isBotDiv ExnOrDiv = True
 isBotDiv _        = False
 
 -- See Notes [Default demand on free variables]
 -- and [defaultDmd vs. resTypeArgDmd]
+-- and Scenario 2 in [Precise exceptions and strictness analysis]
 defaultDmd :: Divergence -> Demand
-defaultDmd Dunno = absDmd
-defaultDmd _     = botDmd  -- Diverges
+defaultDmd Dunno    = absDmd
+defaultDmd ExnOrDiv = absDmd -- This is the whole point of ExnOrDiv!
+defaultDmd Diverges = botDmd -- Diverges
 
 resTypeArgDmd :: Divergence -> Demand
 -- TopRes and BotRes are polymorphic, so that
@@ -1090,10 +1232,7 @@ mkBothDmdArg :: DmdEnv -> BothDmdArg
 mkBothDmdArg env = (env, Dunno)
 
 toBothDmdArg :: DmdType -> BothDmdArg
-toBothDmdArg (DmdType fv _ r) = (fv, go r)
-  where
-    go Dunno    = Dunno
-    go Diverges = Diverges
+toBothDmdArg (DmdType fv _ r) = (fv, r)
 
 bothDmdType :: DmdType -> BothDmdArg -> DmdType
 bothDmdType (DmdType fv1 ds1 r1) (fv2, t2)
@@ -1167,16 +1306,15 @@ splitDmdTy :: DmdType -> (Demand, DmdType)
 splitDmdTy (DmdType fv (dmd:dmds) res_ty) = (dmd, DmdType fv dmds res_ty)
 splitDmdTy ty@(DmdType _ [] res_ty)       = (resTypeArgDmd res_ty, ty)
 
--- When e is evaluated after executing an IO action, and d is e's demand, then
--- what of this demand should we consider, given that the IO action can cleanly
--- exit?
+-- When e is evaluated after executing an IO action that may throw a precise
+-- exception, and d is e's demand, then what of this demand should we consider?
 -- * We have to kill all strictness demands (i.e. lub with a lazy demand)
 -- * We can keep usage information (i.e. lub with an absent demand)
 -- * We have to kill definite divergence
 -- * We can keep CPR information.
--- See Note [IO hack in the demand analyser] in DmdAnal
-deferAfterIO :: DmdType -> DmdType
-deferAfterIO d@(DmdType _ _ res) =
+-- See Note [Precise exceptions and strictness analysis] in Demand
+deferAfterPreciseException :: DmdType -> DmdType
+deferAfterPreciseException d@(DmdType _ _ res) =
     case d `lubDmdType` nopDmdType of
         DmdType fv ds _ -> DmdType fv ds (defer_res res)
   where
@@ -1997,9 +2135,11 @@ instance Binary DmdType where
 
 instance Binary Divergence where
   put_ bh Dunno    = putByte bh 0
-  put_ bh Diverges = putByte bh 1
+  put_ bh ExnOrDiv = putByte bh 1
+  put_ bh Diverges = putByte bh 2
 
   get bh = do { h <- getByte bh
               ; case h of
                   0 -> return Dunno
+                  1 -> return ExnOrDiv
                   _ -> return Diverges }
diff --git a/compiler/prelude/PrimOp.hs b/compiler/prelude/PrimOp.hs
index 4d0bbcee66..a0491975a6 100644
--- a/compiler/prelude/PrimOp.hs
+++ b/compiler/prelude/PrimOp.hs
@@ -337,7 +337,10 @@ A primop "has_side_effects" if it has some *write* effect, visible
 elsewhere
     - writing to the world (I/O)
     - writing to a mutable data structure (writeIORef)
-    - throwing a synchronous Haskell exception
+    - throwing a *precise* exception
+
+BUT since #3207, we also have to mark read effects as "has_side_effects".
+See NB3 below.
 
 Often such primops have a type like
    State -> input -> (State, output)
@@ -351,24 +354,29 @@ data dependencies of the state token to enforce write-effect ordering
    primops even if both their state and result is discarded.
 
  * NB2: We consider primops, such as raiseIO#, that can raise a
-   (Haskell) synchronous exception to "have_side_effects" but not
-   "can_fail".  We must be careful about not discarding such things;
+   precise exception to "have_side_effects" but not "can_fail".
+   We must be careful about not discarding such things;
    see the paper "A semantics for imprecise exceptions".
 
- * NB3: *Read* effects (like reading an IORef) don't count here,
-   because it doesn't matter if we don't do them, or do them more than
-   once.  *Sequencing* is maintained by the data dependency of the state
-   token.
+ * NB3: *Read* effects (like reading an IORef) shouldn't count here,
+   because it doesn't matter if we don't do them, or do them more than once.
+   *Sequencing* is maintained by the linear consumption of the state token.
+   However, duplicating a read-effect violates that premise. This happened in
+   #3207, where a write effect is then performed before the duplicated read
+   effect. A few alternatives to the current design of marking them as
+   "has_side_effects" are outlined in
+   https://gitlab.haskell.org/ghc/ghc/issues/3207#note_257470.
 
 ----------  can_fail ----------------------------
-A primop "can_fail" if it can fail with an *unchecked* exception on
+A primop "can_fail" if it can fail with an *imprecise* exception on
 some elements of its input domain. Main examples:
    division (fails on zero denominator)
    array indexing (fails if the index is out of bounds)
+   raise# (always throws an imprecise exception)
 
-An "unchecked exception" is one that is an outright error, (not
-turned into a Haskell exception,) such as seg-fault or
-divide-by-zero error.  Such can_fail primops are ALWAYS surrounded
+An "imprecise exception" is one that is an outright error, (which can't be
+reliably caught with 'catch#',) such as seg-fault or divide-by-zero error.
+Such can_fail primops are ALWAYS surrounded
 with a test that checks for the bad cases, but we need to be
 very careful about code motion that might move it out of
 the scope of the test.
diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index 7361c4bea8..685a867b0d 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -2595,20 +2595,23 @@ primop  RaiseOp "raise#" GenPrimOp
    with
    strictness  = { \ _arity -> mkClosedStrictSig [topDmd] botDiv }
    out_of_line = True
-   has_side_effects = True
-     -- raise# certainly throws a Haskell exception and hence has_side_effects
-     -- It doesn't actually make much difference because the fact that it
-     -- returns bottom independently ensures that we are careful not to discard
-     -- it.  But still, it's better to say the Right Thing.
+   can_fail = True
+     -- In contrast to 'raiseIO#', which throws a *precise* exception,
+     -- exceptions thrown by 'raise#' are considered *imprecise*.
+     -- Hence 'raise#' is marked as "can_fail" (which 'raiseIO#' is not), but
+     -- not as "has_side_effects" (which 'raiseIO#' is).
+     -- See Note [PrimOp can_fail and has_side_effects] in PrimOp.hs.
+     -- For the same reasons, it has 'botDiv', not 'exnDiv'.
 
 -- Note [Arithmetic exception primops]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 --
--- The RTS provides several primops to raise specific exceptions (raiseDivZero#,
--- raiseUnderflow#, raiseOverflow#). These primops are meant to be used by the
--- package implementing arbitrary precision numbers (Natural,Integer). It can't
--- depend on `base` package to raise exceptions in a normal way because it would
--- create a package dependency circle (base <-> bignum package).
+-- The RTS provides several primops to raise specific imprecise exceptions
+-- (raiseDivZero#, raiseUnderflow#, raiseOverflow#). These primops are meant to
+-- be used by the package implementing arbitrary precision numbers
+-- (Natural,Integer). It can't depend on `base` package to raise exceptions in a
+-- normal way because it would create a package dependency circle
+-- (base <-> bignum package).
 --
 -- See #14664
 
@@ -2646,25 +2649,27 @@ primop  RaiseOverflowOp "raiseOverflow#" GenPrimOp
 
 -- raiseIO# needs to be a primop, because exceptions in the IO monad
 -- must be *precise* - we don't want the strictness analyser turning
--- one kind of bottom into another, as it is allowed to do in pure code.
+-- one kind of bottom into another, as it is allowed to do with imprecise
+-- exceptions. For the same reason it doesn't return botRes, either.
+--
+-- Take the following function as an example. It should *not* be strict in @y@,
+-- because that would turn a precise into an imprecise exception for the call
+-- site @f 1 (error "boom")@ (see #13380):
 --
--- But we *do* want to know that it returns bottom after
--- being applied to two arguments, so that this function is strict in y
 --     f x y | x>0       = raiseIO blah
 --           | y>0       = return 1
 --           | otherwise = return 2
 --
--- TODO Check that the above notes on @f@ are valid. The function successfully
--- produces an IO exception when compiled without optimization. If we analyze
--- it as strict in @y@, won't we change that behavior under optimization?
--- I thought the rule was that it was okay to replace one valid imprecise
--- exception with another, but not to replace a precise exception with
--- an imprecise one (dfeuer, 2017-03-05).
+-- This is scenario 2 in Note [Precise exceptions and strictness analysis] in
+-- Demand. For this reason, 'raiseIO#' should have @topDiv@, but that would
+-- entail not being able to eliminate a lot of dead code. Hence it is the only
+-- primitive to introduce @exnDiv@, which differs from @botDiv@ only in its
+-- 'defaultDmd'.
 
 primop  RaiseIOOp "raiseIO#" GenPrimOp
    a -> State# RealWorld -> (# State# RealWorld, b #)
    with
-   strictness  = { \ _arity -> mkClosedStrictSig [topDmd, topDmd] botDiv }
+   strictness  = { \ _arity -> mkClosedStrictSig [topDmd, topDmd] exnDiv }
    out_of_line = True
    has_side_effects = True
 
diff --git a/compiler/simplCore/FloatIn.hs b/compiler/simplCore/FloatIn.hs
index c1121e16e2..25d8aaa742 100644
--- a/compiler/simplCore/FloatIn.hs
+++ b/compiler/simplCore/FloatIn.hs
@@ -405,10 +405,15 @@ But there are wrinkles
 
 * Which unlifted cases do we float? See PrimOp.hs
   Note [PrimOp can_fail and has_side_effects] which explains:
-   - We can float-in can_fail primops, but we can't float them out.
+   - We can float-in can_fail primops (which concerns imprecise exceptions),
+     but we can't float them out.
    - But we can float a has_side_effects primop, but NOT inside a lambda,
-     so for now we don't float them at all.
-  Hence exprOkForSideEffects
+     so for now we don't float them at all. Hence exprOkForSideEffects.
+   - Throwing precise exceptions is a special case of the previous point: We
+     may /never/ float in a call to (something that ultimately calls)
+     'raiseIO#'. This can be detected with exprMayThrowPreciseException.
+     Note that exprOkForSideEffects implies @not exprMayThrowPreciseException@.
+
 
 * Because we can float can-fail primops (array indexing, division) inwards
   but not outwards, we must be careful not to transform
diff --git a/compiler/stranal/DmdAnal.hs b/compiler/stranal/DmdAnal.hs
index 8f5cb6ddea..792ab9e4fa 100644
--- a/compiler/stranal/DmdAnal.hs
+++ b/compiler/stranal/DmdAnal.hs
@@ -34,8 +34,6 @@ import GHC.Core.Coercion ( Coercion, coVarsOfCo )
 import GHC.Core.FamInstEnv
 import Util
 import Maybes           ( isJust )
-import TysWiredIn
-import TysPrim          ( realWorldStatePrimTy )
 import ErrUtils         ( dumpIfSet_dyn, DumpFormat (..) )
 import UniqSet
 
@@ -222,8 +220,9 @@ dmdAnal' env dmd (Case scrut case_bndr ty [(DataAlt dc, bndrs, rhs)])
         (alt_ty1, dmds)          = findBndrsDmds env rhs_ty bndrs
         (alt_ty2, case_bndr_dmd) = findBndrDmd env False alt_ty1 case_bndr
         id_dmds                  = addCaseBndrDmd case_bndr_dmd dmds
-        alt_ty3 | io_hack_reqd scrut dc bndrs = deferAfterIO alt_ty2
-                | otherwise                   = alt_ty2
+        -- See Note [Precise exceptions and strictness analysis] in Demand
+        alt_ty3 | exprMayThrowPreciseException scrut = deferAfterPreciseException alt_ty2
+                | otherwise                          = alt_ty2
 
         -- Compute demand on the scrutinee
         -- See Note [Demand on scrutinee of a product case]
@@ -314,19 +313,6 @@ dmdAnal' env dmd (Let (Rec pairs) body)
     body_ty2 `seq`
     (body_ty2,  Let (Rec pairs') body')
 
-io_hack_reqd :: CoreExpr -> DataCon -> [Var] -> Bool
--- See Note [IO hack in the demand analyser]
-io_hack_reqd scrut con bndrs
-  | (bndr:_) <- bndrs
-  , con == tupleDataCon Unboxed 2
-  , idType bndr `eqType` realWorldStatePrimTy
-  , (fun, _) <- collectArgs scrut
-  = case fun of
-      Var f -> not (isPrimOpId f)
-      _     -> True
-  | otherwise
-  = False
-
 dmdAnalAlt :: AnalEnv -> CleanDemand -> Id -> Alt Var -> (DmdType, Alt Var)
 dmdAnalAlt env dmd case_bndr (con,bndrs,rhs)
   | null bndrs    -- Literals, DEFAULT, and nullary constructors
@@ -341,103 +327,7 @@ dmdAnalAlt env dmd case_bndr (con,bndrs,rhs)
   = (alt_ty, (con, setBndrsDemandInfo bndrs id_dmds, rhs'))
 
 
-{- 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'? Often not! If foo x s performs some observable action
-(including raising an exception with raiseIO#, modifying a mutable variable, or
-even ending the program normally), then we must not force 'y' (which may fail
-to terminate) until we have performed foo x s.
-
-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 (#148, #1592) where this shows up is:
-     do { let len = <expensive> ;
-        ; when (...) (exitWith ExitSuccess)
-        ; print len }
-
-However, consider
-  f x s = case getMaskingState# s of
-            (# s, r #) ->
-          case x of I# x2 -> ...
-
-Here it is terribly sad to make 'f' lazy in 's'.  After all,
-getMaskingState# is not going to diverge or throw an exception!  This
-situation actually arises in GHC.IO.Handle.Internals.wantReadableHandle
-(on an MVar not an Int), and made a material difference.
-
-So if the scrutinee is a primop call, we *don't* apply the
-state hack:
-  - If it is a simple, terminating one like getMaskingState,
-    applying the hack is over-conservative.
-  - If the primop is raise# then it returns bottom, so
-    the case alternatives are already discarded.
-  - If the primop can raise a non-IO exception, like
-    divide by zero or seg-fault (eg writing an array
-    out of bounds) then we don't mind evaluating 'x' first.
-
-Note [Demand on the scrutinee of a product case]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When figuring out the demand on the scrutinee of a product case,
-we use the demands of the case alternative, i.e. id_dmds.
-But note that these include the demand on the case binder;
-see Note [Demand on case-alternative binders] in Demand.hs.
-This is crucial. Example:
-   f x = case x of y { (a,b) -> k y a }
-If we just take scrut_demand = U(L,A), then we won't pass x to the
-worker, so the worker will rebuild
-     x = (a, absent-error)
-and that'll crash.
-
-Note [Aggregated demand for cardinality]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We use different strategies for strictness and usage/cardinality to
-"unleash" demands captured on free variables by bindings. Let us
-consider the example:
-
-f1 y = let {-# NOINLINE h #-}
-           h = y
-       in  (h, h)
-
-We are interested in obtaining cardinality demand U1 on |y|, as it is
-used only in a thunk, and, therefore, is not going to be updated any
-more. Therefore, the demand on |y|, captured and unleashed by usage of
-|h| is U1. However, if we unleash this demand every time |h| is used,
-and then sum up the effects, the ultimate demand on |y| will be U1 +
-U1 = U. In order to avoid it, we *first* collect the aggregate demand
-on |h| in the body of let-expression, and only then apply the demand
-transformer:
-
-transf[x](U) = {y |-> U1}
-
-so the resulting demand on |y| is U1.
-
-The situation is, however, different for strictness, where this
-aggregating approach exhibits worse results because of the nature of
-|both| operation for strictness. Consider the example:
-
-f y c =
-  let h x = y |seq| x
-   in case of
-        True  -> h True
-        False -> y
-
-It is clear that |f| is strict in |y|, however, the suggested analysis
-will infer from the body of |let| that |h| is used lazily (as it is
-used in one branch only), therefore lazy demand will be put on its
-free variable |y|. Conversely, if the demand on |h| is unleashed right
-on the spot, we will get the desired result, namely, that |f| is
-strict in |y|.
-
-
+{-
 ************************************************************************
 *                                                                      *
                     Demand transformer
diff --git a/testsuite/tests/stranal/should_compile/T5775.hs b/testsuite/tests/stranal/should_compile/T5775.hs
new file mode 100644
index 0000000000..ec385c028e
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T5775.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE MagicHash, UnboxedTuples #-}
+module U where
+import GHC.Prim
+import GHC.Types
+
+idx :: Addr# -> Int -> Int
+{-# INLINE idx #-}
+idx a (I# i) = case readIntOffAddr# a i realWorld# of (# _, y #) -> I# y
+
+f :: Int -> Int -> Int
+{-# INLINE f #-}
+f x y = y + x
+
+foo :: Addr# -> Int -> Int
+foo a n = n `seq` loop (idx a 0) 1
+  where
+    loop x i = case i >= n of
+      False -> loop (f x (idx a i)) (i+1)
+      True  -> x
diff --git a/testsuite/tests/stranal/should_compile/T5775.stderr b/testsuite/tests/stranal/should_compile/T5775.stderr
new file mode 100644
index 0000000000..b8f38eb980
--- /dev/null
+++ b/testsuite/tests/stranal/should_compile/T5775.stderr
@@ -0,0 +1,58 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core = {terms: 73, types: 66, coercions: 0, joins: 1/1}
+
+-- RHS size: {terms: 13, types: 16, coercions: 0, joins: 0/0}
+idx :: Addr# -> Int -> Int
+idx
+  = \ (a_atJ :: Addr#) (ds_d1mx :: Int) ->
+      case ds_d1mx of { I# i_atK ->
+      case readIntOffAddr# @RealWorld a_atJ i_atK realWorld# of { (# ipv_s1mT, ipv1_s1mU #) -> GHC.Types.I# ipv1_s1mU }
+      }
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+U.$trModule4 :: Addr#
+U.$trModule4 = "main"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+U.$trModule3 :: TrName
+U.$trModule3 = GHC.Types.TrNameS U.$trModule4
+
+-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+U.$trModule2 :: Addr#
+U.$trModule2 = "U"#
+
+-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
+U.$trModule1 :: TrName
+U.$trModule1 = GHC.Types.TrNameS U.$trModule2
+
+-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
+U.$trModule :: Module
+U.$trModule = GHC.Types.Module U.$trModule3 U.$trModule1
+
+-- RHS size: {terms: 5, types: 2, coercions: 0, joins: 0/0}
+f :: Int -> Int -> Int
+f = \ (x_atM :: Int) (y_atN :: Int) -> GHC.Num.$fNumInt_$c+ y_atN x_atM
+
+-- RHS size: {terms: 38, types: 34, coercions: 0, joins: 1/1}
+foo :: Addr# -> Int -> Int
+foo
+  = \ (w_s1oZ :: Addr#) (w1_s1p0 :: Int) ->
+      case w1_s1p0 of { I# ww1_s1p3 ->
+      case readIntOffAddr# @RealWorld w_s1oZ 0# realWorld# of { (# ipv_s1mY, ipv1_s1mZ #) ->
+      joinrec {
+        $wloop_s1oY :: Int# -> Int# -> Int
+        $wloop (ww2 :: Int#) (ww3 :: Int#)
+          = case >=# ww3_s1oW ww1_s1p3 of {
+              __DEFAULT ->
+                case readIntOffAddr# @RealWorld w_s1oZ ww3_s1oW realWorld# of { (# ipv2_X2, ipv3_X3 #) ->
+                jump $wloop_s1oY (+# ipv3_X3 ww2_s1oS) (+# ww3_s1oW 1#)
+                };
+              1# -> GHC.Types.I# ww2_s1oS
+            }; } in
+      jump $wloop_s1oY ipv1_s1mZ 1#
+      }
+      }
+
+
+
diff --git a/testsuite/tests/stranal/should_compile/all.T b/testsuite/tests/stranal/should_compile/all.T
index 012d3170e2..8a1dcc24bf 100644
--- a/testsuite/tests/stranal/should_compile/all.T
+++ b/testsuite/tests/stranal/should_compile/all.T
@@ -28,6 +28,8 @@ test('T8743', [], multimod_compile, ['T8743', '-v0'])
 # Set -dppr-cols to ensure output doesn't wrap
 test('T10482',  [ grep_errmsg(r'wfoo.*Int#') ], compile, ['-dppr-cols=200 -ddump-simpl'])
 test('T10482a', [ grep_errmsg(r'wf.*Int#') ],   compile, ['-dppr-cols=200 -ddump-simpl'])
+# T5775: There should be $wloop :: Int# -> Int# -> Int
+test('T5775',  [ grep_errmsg(r'wloop.*:: Int#.*:: Int#') ], compile, ['-dppr-cols=200 -ddump-simpl -dsuppress-idinfo -dsuppress-uniques'])
 
 test('T9208', when(compiler_debugged(), expect_broken(9208)), compile, [''])
 # T9208 fails (and should do so) if you have assertion checking on in the compiler
diff --git a/testsuite/tests/stranal/should_run/T17676.hs b/testsuite/tests/stranal/should_run/T17676.hs
new file mode 100644
index 0000000000..d0fa4cf661
--- /dev/null
+++ b/testsuite/tests/stranal/should_run/T17676.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+import Data.IORef
+import Control.Exception
+import Control.Monad
+
+data Exc = Exc deriving Show
+
+instance Exception Exc
+
+-- Recursive instead of NOINLINE because of #17673
+f :: Int -> Int -> IO ()
+f 0 x = do
+  let true = sum [0..4] == 10
+  when true $ throwIO Exc
+  x `seq` return ()
+f n x = f (n-1) (x+1)
+
+main = f 1 (error "expensive computation") `catch` \(_ :: Exc) -> return ()
diff --git a/testsuite/tests/stranal/should_run/all.T b/testsuite/tests/stranal/should_run/all.T
index 278b91b292..d822e482dd 100644
--- a/testsuite/tests/stranal/should_run/all.T
+++ b/testsuite/tests/stranal/should_run/all.T
@@ -19,7 +19,8 @@ test('T11076', normal, multimod_compile_and_run, ['T11076.hs', 'T11076_prim.cmm'
 test('T11555a', normal, compile_and_run, [''])
 test('T12368', exit_code(1), compile_and_run, [''])
 test('T12368a', exit_code(1), compile_and_run, [''])
-test('T13380', [expect_broken(13380), exit_code(1)], compile_and_run, [''])
+test('T13380', exit_code(1), compile_and_run, [''])
 test('T14171', [expect_broken(14171), exit_code(1)], compile_and_run, [''])
 test('T14290', normal, compile_and_run, [''])
 test('T14285', normal, multimod_compile_and_run, ['T14285', ''])
+test('T17676', normal, compile_and_run, [''])
diff --git a/testsuite/tests/stranal/should_run/strun003.hs b/testsuite/tests/stranal/should_run/strun003.hs
index 3240ab272a..7b12e7fac3 100644
--- a/testsuite/tests/stranal/should_run/strun003.hs
+++ b/testsuite/tests/stranal/should_run/strun003.hs
@@ -1,8 +1,9 @@
 -- This module should run fine with an empty argument list
--- But it won't if the strictness analyser thinks that 'len' is use
+-- But it won't if the strictness analyser thinks that 'len' is used
 -- strictly, which was the case in GHC 6.0
 
--- See the io_hack_reqd in DmdAnal.lhs
+-- See Note [Precise exceptions and strictness analysis] in Demand.hs
+-- This is similar to T17676, but with an extra putStrLn.
 
 module Main where