DmdAnal: Improve handling of precise exceptions

This patch does two things: Fix possible unsoundness in what was called
the "IO hack" and implement part 2.1 of the "fixing precise exceptions"
plan in
https://gitlab.haskell.org/ghc/ghc/wikis/fixing-precise-exceptions,
which, in combination with !2956, supersedes !3014 and !2525.

**IO hack**

The "IO hack" (which is a fallback to preserve precise exceptions
semantics and thus soundness, rather than some smart thing that
increases precision) is called `exprMayThrowPreciseException` now.
I came up with two testcases exemplifying possible unsoundness (if
twisted enough) in the old approach:

- `T13380d`: Demonstrating unsoundness of the "IO hack" when resorting
             to manual state token threading and direct use of primops.
             More details below.
- `T13380e`: Demonstrating unsoundness of the "IO hack" when we have
             Nested CPR. Not currently relevant, as we don't have Nested
             CPR yet.
- `T13380f`: Demonstrating unsoundness of the "IO hack" for safe FFI
             calls.

Basically, the IO hack assumed that precise exceptions can only be
thrown from a case scrutinee of type `(# State# RealWorld, _ #)`. I
couldn't come up with a program using the `IO` abstraction that violates
this assumption. But it's easy to do so via manual state token threading
and direct use of primops, see `T13380d`. Also similar code might be
generated by Nested CPR in the (hopefully not too) distant future, see
`T13380e`. Hence, we now have a more careful test in `forcesRealWorld`
that passes `T13380{d,e}` (and will hopefully be robust to Nested CPR).

**Precise exceptions**

In #13380 and #17676 we saw that we didn't preserve precise exception
semantics in demand analysis. We fixed that with minimal changes in
!2956, but that was terribly unprincipled.

That unprincipledness resulted in a loss of precision, which is tracked
by these new test cases:

- `T13380b`: Regression in dead code elimination, because !2956 was too
             syntactic about `raiseIO#`
- `T13380c`: No need to apply the "IO hack" when the IO action may not
             throw a precise exception (and the existing IO hack doesn't
             detect that)

Fixing both issues in !3014 turned out to be too complicated and had
the potential to regress in the future. Hence we decided to only fix
`T13380b` and augment the `Divergence` lattice with a new middle-layer
element, `ExnOrDiv`, which means either `Diverges` (, throws an
imprecise exception) or throws a *precise* exception.

See the wiki page on Step 2.1 for more implementational details:
https://gitlab.haskell.org/ghc/ghc/wikis/fixing-precise-exceptions#dead-code-elimination-for-raiseio-with-isdeadenddiv-introducing-exnordiv-step-21

21 files changed, 532 insertions, 420 deletions

diff --git a/compiler/GHC/Builtin/primops.txt.pp b/compiler/GHC/Builtin/primops.txt.pp
index a29fbf48d7..0928f8ed61 100644
--- a/compiler/GHC/Builtin/primops.txt.pp
+++ b/compiler/GHC/Builtin/primops.txt.pp
@@ -2567,14 +2567,17 @@ section "Exceptions"
 ------------------------------------------------------------------------
 
 -- Note [Strictness for mask/unmask/catch]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -- Consider this example, which comes from GHC.IO.Handle.Internals:
 --    wantReadableHandle3 f ma b st
 --      = case ... of
 --          DEFAULT -> case ma of MVar a -> ...
---          0#      -> maskAsynchExceptions# (\st -> case ma of MVar a -> ...)
+--          0#      -> maskAsyncExceptions# (\st -> case ma of MVar a -> ...)
 -- The outer case just decides whether to mask exceptions, but we don't want
--- thereby to hide the strictness in 'ma'!  Hence the use of strictApply1Dmd.
+-- thereby to hide the strictness in 'ma'!  Hence the use of strictApply1Dmd
+-- in mask and unmask. But catch really is lazy in its first argument, see
+-- #11555. So for IO actions 'ma' we often use a wrapper around it that is
+-- head-strict in 'ma': GHC.IO.catchException.
 
 primop  CatchOp "catch#" GenPrimOp
           (State# RealWorld -> (# State# RealWorld, a #) )
@@ -2593,13 +2596,16 @@ primop  RaiseOp "raise#" GenPrimOp
    b -> o
       -- NB: the type variable "o" is "a", but with OpenKind
    with
+   -- In contrast to 'raiseIO#', which throws a *precise* exception,
+   -- exceptions thrown by 'raise#' are considered *imprecise*.
+   -- See Note [Precise vs imprecise exceptions] in GHC.Types.Demand.
+   -- Hence, it has 'botDiv', not 'exnDiv'.
+   -- For the same reasons, '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.
    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
 
 -- Note [Arithmetic exception primops]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2648,8 +2654,8 @@ primop  RaiseIOOp "raiseIO#" GenPrimOp
    a -> State# RealWorld -> (# State# RealWorld, b #)
    with
    -- See Note [Precise exceptions and strictness analysis] in Demand.hs
-   -- for why we give it topDiv
-   -- strictness  = { \ _arity -> mkClosedStrictSig [topDmd, topDmd] topDiv }
+   -- for why this is the *only* primop that has 'exnDiv'
+   strictness  = { \ _arity -> mkClosedStrictSig [topDmd, topDmd] exnDiv }
    out_of_line = True
    has_side_effects = True
 
diff --git a/compiler/GHC/Core/Arity.hs b/compiler/GHC/Core/Arity.hs
index 53e47d9746..935fd7a67b 100644
--- a/compiler/GHC/Core/Arity.hs
+++ b/compiler/GHC/Core/Arity.hs
@@ -759,8 +759,8 @@ arityType _ (Var v)
   , not $ isTopSig strict_sig
   , (ds, res) <- splitStrictSig strict_sig
   , let arity = length ds
-  = if isBotDiv res then ABot arity
-                    else ATop (take arity one_shots)
+  = if isDeadEndDiv res then ABot arity
+                        else ATop (take arity one_shots)
   | otherwise
   = ATop (take (idArity v) one_shots)
   where
@@ -787,7 +787,7 @@ arityType env (App fun arg )
         -- The difference is observable using 'seq'
         --
 arityType env (Case scrut _ _ alts)
-  | exprIsBottom scrut || null alts
+  | exprIsDeadEnd scrut || null alts
   = ABot 0     -- Do not eta expand
                -- See Note [Dealing with bottom (1)]
   | otherwise
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index b1f0e8eece..872a081f47 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -64,7 +64,7 @@ import GHC.Utils.Misc
 import GHC.Core.InstEnv      ( instanceDFunId )
 import GHC.Core.Coercion.Opt ( checkAxInstCo )
 import GHC.Core.Arity        ( typeArity )
-import GHC.Types.Demand ( splitStrictSig, isBotDiv )
+import GHC.Types.Demand ( splitStrictSig, isDeadEndDiv )
 
 import GHC.Driver.Types
 import GHC.Driver.Session
@@ -651,7 +651,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty
            ppr binder)
 
        ; case splitStrictSig (idStrictness binder) of
-           (demands, result_info) | isBotDiv result_info ->
+           (demands, result_info) | isDeadEndDiv result_info ->
              checkL (demands `lengthAtLeast` idArity binder)
                (text "idArity" <+> ppr (idArity binder) <+>
                text "exceeds arity imposed by the strictness signature" <+>
@@ -986,7 +986,7 @@ used to check two things:
 * exprIsHNF is false: it would *seem* to be terribly wrong if
   the scrutinee was already in head normal form.
 
-* exprIsBottom is true: we should be able to see why GHC believes the
+* exprIsDeadEnd is true: we should be able to see why GHC believes the
   scrutinee is diverging for sure.
 
 It was already known that the second test was not entirely reliable.
@@ -1182,7 +1182,7 @@ lintCaseExpr scrut var alt_ty alts =
               , isAlgTyCon tycon
               , not (isAbstractTyCon tycon)
               , null (tyConDataCons tycon)
-              , not (exprIsBottom scrut)
+              , not (exprIsDeadEnd scrut)
               -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
                         -- This can legitimately happen for type families
                       $ return ()
diff --git a/compiler/GHC/Core/Opt/CallArity.hs b/compiler/GHC/Core/Opt/CallArity.hs
index ef5bb94b23..250942e0f6 100644
--- a/compiler/GHC/Core/Opt/CallArity.hs
+++ b/compiler/GHC/Core/Opt/CallArity.hs
@@ -701,7 +701,7 @@ trimArity v a = minimum [a, max_arity_by_type, max_arity_by_strsig]
   where
     max_arity_by_type = length (typeArity (idType v))
     max_arity_by_strsig
-        | isBotDiv result_info = length demands
+        | isDeadEndDiv result_info = length demands
         | otherwise = a
 
     (demands, result_info) = splitStrictSig (idStrictness v)
diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index 5d4e650564..b1fcc227ef 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -16,7 +16,7 @@ module GHC.Core.Opt.DmdAnal ( dmdAnalProgram ) where
 import GHC.Prelude
 
 import GHC.Driver.Session
-import GHC.Core.Opt.WorkWrap.Utils ( findTypeShape )
+import GHC.Core.Opt.WorkWrap.Utils
 import GHC.Types.Demand   -- All of it
 import GHC.Core
 import GHC.Core.Seq     ( seqBinds )
@@ -25,6 +25,7 @@ import GHC.Types.Var.Env
 import GHC.Types.Basic
 import Data.List        ( mapAccumL )
 import GHC.Core.DataCon
+import GHC.Types.ForeignCall ( isSafeForeignCall )
 import GHC.Types.Id
 import GHC.Types.Id.Info
 import GHC.Core.Utils
@@ -34,7 +35,7 @@ import GHC.Core.Coercion ( Coercion, coVarsOfCo )
 import GHC.Core.FamInstEnv
 import GHC.Utils.Misc
 import GHC.Data.Maybe         ( isJust )
-import GHC.Builtin.Types
+import GHC.Builtin.PrimOps
 import GHC.Builtin.Types.Prim ( realWorldStatePrimTy )
 import GHC.Utils.Error        ( dumpIfSet_dyn, DumpFormat (..) )
 import GHC.Types.Unique.Set
@@ -151,7 +152,7 @@ dmdAnal env d e = -- pprTrace "dmdAnal" (ppr d <+> ppr e) $
                   dmdAnal' env d e
 
 dmdAnal' _ _ (Lit lit)     = (nopDmdType, Lit lit)
-dmdAnal' _ _ (Type ty)     = (nopDmdType, Type ty)      -- Doesn't happen, in fact
+dmdAnal' _ _ (Type ty)     = (nopDmdType, Type ty) -- Doesn't happen, in fact
 dmdAnal' _ _ (Coercion co)
   = (unitDmdType (coercionDmdEnv co), Coercion co)
 
@@ -222,8 +223,13 @@ 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
+        fam_envs                 = ae_fam_envs env
+        alt_ty3
+          -- See Note [Precise exceptions and strictness analysis] in Demand
+          | exprMayThrowPreciseException fam_envs scrut
+          = deferAfterPreciseException alt_ty2
+          | otherwise
+          = alt_ty2
 
         -- Compute demand on the scrutinee
         -- See Note [Demand on scrutinee of a product case]
@@ -251,12 +257,20 @@ dmdAnal' env dmd (Case scrut case_bndr ty alts)
                                -- NB: Base case is botDmdType, for empty case alternatives
                                --     This is a unit for lubDmdType, and the right result
                                --     when there really are no alternatives
-        res_ty               = alt_ty `bothDmdType` toBothDmdArg scrut_ty
+        fam_envs             = ae_fam_envs env
+        alt_ty2
+          -- See Note [Precise exceptions and strictness analysis] in Demand
+          | exprMayThrowPreciseException fam_envs scrut
+          = deferAfterPreciseException alt_ty
+          | otherwise
+          = alt_ty
+        res_ty               = alt_ty2 `bothDmdType` toBothDmdArg scrut_ty
+
     in
 --    pprTrace "dmdAnal:Case2" (vcat [ text "scrut" <+> ppr scrut
 --                                   , text "scrut_ty" <+> ppr scrut_ty
 --                                   , text "alt_tys" <+> ppr alt_tys
---                                   , text "alt_ty" <+> ppr alt_ty
+--                                   , text "alt_ty2" <+> ppr alt_ty2
 --                                   , text "res_ty" <+> ppr res_ty ]) $
     (res_ty, Case scrut' case_bndr' ty alts')
 
@@ -314,16 +328,37 @@ 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
+-- | A simple, syntactic analysis of whether an expression MAY throw a precise
+-- exception when evaluated. It's always sound to return 'True'.
+-- See Note [Which scrutinees may throw precise exceptions].
+exprMayThrowPreciseException :: FamInstEnvs -> CoreExpr -> Bool
+exprMayThrowPreciseException envs e
+  | not (forcesRealWorld envs (exprType e))
+  = False -- 1. in the Note
+  | (Var f, _) <- collectArgs e
+  , Just op    <- isPrimOpId_maybe f
+  , op /= RaiseIOOp
+  = False -- 2. in the Note
+  | (Var f, _) <- collectArgs e
+  , Just fcall <- isFCallId_maybe f
+  , not (isSafeForeignCall fcall)
+  = False -- 3. in the Note
+  | otherwise
+  = True  -- _. in the Note
+
+-- | Recognises types that are
+--    * @State# RealWorld@
+--    * Unboxed tuples with a @State# RealWorld@ field
+-- modulo coercions. This will detect 'IO' actions (even post Nested CPR! See
+-- T13380e) and user-written variants thereof by their type.
+forcesRealWorld :: FamInstEnvs -> Type -> Bool
+forcesRealWorld fam_envs ty
+  | ty `eqType` realWorldStatePrimTy
+  = True
+  | Just DataConAppContext{ dcac_dc = dc, dcac_arg_tys = field_tys }
+      <- deepSplitProductType_maybe fam_envs ty
+  , isUnboxedTupleCon dc
+  = any (\(ty,_) -> ty `eqType` realWorldStatePrimTy) field_tys
   | otherwise
   = False
 
@@ -340,49 +375,42 @@ dmdAnalAlt env dmd case_bndr (con,bndrs,rhs)
         id_dmds       = addCaseBndrDmd case_bndr_dmd dmds
   = (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 [Which scrutinees may throw precise exceptions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This is the specification of 'exprMayThrowPreciseExceptions',
+which is important for Scenario 2 of
+Note [Precise exceptions and strictness analysis] in GHC.Types.Demand.
+
+For an expression @f a1 ... an :: ty@ we determine that
+  1. False  If ty is *not* @State# RealWorld@ or an unboxed tuple thereof.
+            This check is done by 'forcesRealWorld'.
+            (Why not simply unboxed pairs as above? This is motivated by
+            T13380{d,e}.)
+  2. False  If f is a PrimOp, and it is *not* raiseIO#
+  3. False  If f is an unsafe FFI call ('PlayRisky')
+  _. True   Otherwise "give up".
+
+It is sound to return False in those cases, because
+  1. We don't give any guarantees for unsafePerformIO, so no precise exceptions
+     from pure code.
+  2. raiseIO# is the only primop that may throw a precise exception.
+  3. Unsafe FFI calls may not interact with the RTS (to throw, for example).
+     See haddock on GHC.Types.ForeignCall.PlayRisky.
+
+We *need* to return False in those cases, because
+  1. We would lose too much strictness in pure code, all over the place.
+  2. We would lose strictness for primops like getMaskingState#, which
+     introduces a substantial regression in
+     GHC.IO.Handle.Internals.wantReadableHandle.
+  3. We would lose strictness for code like GHC.Fingerprint.fingerprintData,
+     where an intermittent FFI call to c_MD5Init would otherwise lose
+     strictness on the arguments len and buf, leading to regressions in T9203
+     (2%) and i386's haddock.base (5%). Tested by T13380f.
+
+In !3014 we tried a more sophisticated analysis by introducing ConOrDiv (nic)
+to the Divergence lattice, but in practice it turned out to be hard to untaint
+from 'topDiv' to 'conDiv', leading to bugs, performance regressions and
+complexity that didn't justify the single fixed testcase T13380c.
 
 Note [Demand on the scrutinee of a product case]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -453,27 +481,33 @@ dmdTransform :: AnalEnv         -- The strictness environment
         -- this function plus demand on its free variables
 
 dmdTransform env var dmd
-  | isDataConWorkId var                          -- Data constructor
+  -- Data constructors
+  | isDataConWorkId var
   = dmdTransformDataConSig (idArity var) dmd
-
+  -- Dictionary component selectors
   | gopt Opt_DmdTxDictSel (ae_dflags env),
-    Just _ <- isClassOpId_maybe var -- Dictionary component selector
+    Just _ <- isClassOpId_maybe var
   = dmdTransformDictSelSig (idStrictness var) dmd
-
-  | isGlobalId var                               -- Imported function
+  -- Imported functions
+  | isGlobalId var
   , let res = dmdTransformSig (idStrictness var) dmd
-  = -- pprTrace "dmdTransform" (vcat [ppr var, ppr (idStrictness var), ppr dmd, ppr res])
+  = -- pprTrace "dmdTransform:import" (vcat [ppr var, ppr (idStrictness var), ppr dmd, ppr res])
     res
-
-  | Just (sig, top_lvl) <- lookupSigEnv env var  -- Local letrec bound thing
+  -- Top-level or local let-bound thing for which we use LetDown ('useLetUp').
+  -- In that case, we have a strictness signature to unleash in our AnalEnv.
+  | Just (sig, top_lvl) <- lookupSigEnv env var
   , let fn_ty = dmdTransformSig sig dmd
-  = -- pprTrace "dmdTransform" (vcat [ppr var, ppr sig, ppr dmd, ppr fn_ty]) $
+  = -- pprTrace "dmdTransform:LetDown" (vcat [ppr var, ppr sig, ppr dmd, ppr fn_ty]) $
     if isTopLevel top_lvl
-    then fn_ty   -- Don't record top level things
+    then fn_ty   -- Don't record demand on top-level things
     else addVarDmd fn_ty var (mkOnceUsedDmd dmd)
-
-  | otherwise                                    -- Local non-letrec-bound thing
-  = unitDmdType (unitVarEnv var (mkOnceUsedDmd dmd))
+  -- Everything else:
+  --   * Local let binders for which we use LetUp (cf. 'useLetUp')
+  --   * Lambda binders
+  --   * Case and constructor field binders
+  | otherwise
+  = -- pprTrace "dmdTransform:other" (vcat [ppr var, ppr sig, ppr dmd, ppr res]) $
+    unitDmdType (unitVarEnv var (mkOnceUsedDmd dmd))
 
 {-
 ************************************************************************
@@ -600,10 +634,9 @@ dmdAnalRhsLetDown rec_flag env let_dmd id rhs
       = mkRhsDmd env rhs_arity rhs
     (DmdType rhs_fv rhs_dmds rhs_div, rhs')
                    = dmdAnal env rhs_dmd rhs
-    -- TODO: Won't the following line unnecessarily trim down arity for join
-    --       points returning a lambda in a C(S) context?
-    sig            = mkStrictSigForArity rhs_arity (mkDmdType sig_fv rhs_dmds rhs_div)
-    id'            = setIdStrictness id sig
+    sig            = mkStrictSigForArity rhs_arity (DmdType sig_fv rhs_dmds rhs_div)
+    id'            = -- pprTrace "dmdAnalRhsLetDown" (ppr id <+> ppr sig) $
+                     setIdStrictness id sig
         -- See Note [NOINLINE and strictness]
 
 
diff --git a/compiler/GHC/Core/Opt/FloatIn.hs b/compiler/GHC/Core/Opt/FloatIn.hs
index 4d759a47bc..9398435ee5 100644
--- a/compiler/GHC/Core/Opt/FloatIn.hs
+++ b/compiler/GHC/Core/Opt/FloatIn.hs
@@ -407,12 +407,17 @@ floating in cases with a single alternative that may bind values.
 
 But there are wrinkles
 
-* Which unlifted cases do we float? See GHC.Builtin.PrimOps
-  Note [PrimOp can_fail and has_side_effects] which explains:
-   - We can float-in can_fail primops, but we can't float them out.
+* Which unlifted cases do we float?
+  See Note [PrimOp can_fail and has_side_effects] in GHC.Builtin.PrimOps which
+  explains:
+   - 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#'.
+     See Note [Precise exceptions and strictness analysis] in GHC.Types.Demand.
 
 * 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/GHC/Core/Opt/FloatOut.hs b/compiler/GHC/Core/Opt/FloatOut.hs
index 92a747424f..7bb7acafb0 100644
--- a/compiler/GHC/Core/Opt/FloatOut.hs
+++ b/compiler/GHC/Core/Opt/FloatOut.hs
@@ -20,7 +20,7 @@ import GHC.Core.Opt.Monad ( FloatOutSwitches(..) )
 
 import GHC.Driver.Session
 import GHC.Utils.Error   ( dumpIfSet_dyn, DumpFormat (..) )
-import GHC.Types.Id      ( Id, idArity, idType, isBottomingId,
+import GHC.Types.Id      ( Id, idArity, idType, isDeadEndId,
                            isJoinId, isJoinId_maybe )
 import GHC.Core.Opt.SetLevels
 import GHC.Types.Unique.Supply ( UniqSupply )
@@ -221,7 +221,7 @@ floatBind (NonRec (TB var _) rhs)
 
         -- A tiresome hack:
         -- see Note [Bottoming floats: eta expansion] in GHC.Core.Opt.SetLevels
-    let rhs'' | isBottomingId var = etaExpand (idArity var) rhs'
+    let rhs'' | isDeadEndId var   = etaExpand (idArity var) rhs'
               | otherwise         = rhs'
 
     in (fs, rhs_floats, [NonRec var rhs'']) }
diff --git a/compiler/GHC/Core/Opt/LiberateCase.hs b/compiler/GHC/Core/Opt/LiberateCase.hs
index 7a28abce20..211fc39920 100644
--- a/compiler/GHC/Core/Opt/LiberateCase.hs
+++ b/compiler/GHC/Core/Opt/LiberateCase.hs
@@ -158,8 +158,8 @@ libCaseBind env (Rec pairs)
                                    Let (Rec dup_pairs) (Var unitDataConId)
 
     ok_pair (id,_)
-        =  idArity id > 0          -- Note [Only functions!]
-        && not (isBottomingId id)  -- Note [Not bottoming ids]
+        =  idArity id > 0       -- Note [Only functions!]
+        && not (isDeadEndId id) -- Note [Not bottoming ids]
 
 {- Note [Not bottoming Ids]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Core/Opt/SetLevels.hs b/compiler/GHC/Core/Opt/SetLevels.hs
index ed6f4c61fe..0a1395a432 100644
--- a/compiler/GHC/Core/Opt/SetLevels.hs
+++ b/compiler/GHC/Core/Opt/SetLevels.hs
@@ -87,7 +87,7 @@ import GHC.Types.Unique.Set   ( nonDetStrictFoldUniqSet )
 import GHC.Types.Unique.DSet  ( getUniqDSet )
 import GHC.Types.Var.Env
 import GHC.Types.Literal      ( litIsTrivial )
-import GHC.Types.Demand       ( StrictSig, Demand, isStrictDmd, splitStrictSig, increaseStrictSigArity )
+import GHC.Types.Demand       ( StrictSig, Demand, isStrictDmd, splitStrictSig, prependArgsStrictSig )
 import GHC.Types.Cpr          ( mkCprSig, botCpr )
 import GHC.Types.Name         ( getOccName, mkSystemVarName )
 import GHC.Types.Name.Occurrence ( occNameString )
@@ -293,7 +293,7 @@ lvlTopBind env (Rec pairs)
 lvl_top :: LevelEnv -> RecFlag -> Id -> CoreExpr -> LvlM LevelledExpr
 lvl_top env is_rec bndr rhs
   = lvlRhs env is_rec
-           (isBottomingId bndr)
+           (isDeadEndId bndr)
            Nothing  -- Not a join point
            (freeVars rhs)
 
@@ -943,7 +943,7 @@ Id, *immediately*, for three reasons:
     Lint complains unless the scrutinee of such a case is clearly bottom.
 
     This was reported in #11290.   But since the whole bottoming-float
-    thing is based on the cheap-and-cheerful exprIsBottom, I'm not sure
+    thing is based on the cheap-and-cheerful exprIsDeadEnd, I'm not sure
     that it'll nail all such cases.
 
 Note [Bottoming floats: eta expansion] c.f Note [Bottoming floats]
@@ -983,7 +983,7 @@ annotateBotStr id n_extra mb_str
   = case mb_str of
       Nothing           -> id
       Just (arity, sig) -> id `setIdArity`      (arity + n_extra)
-                              `setIdStrictness` (increaseStrictSigArity n_extra sig)
+                              `setIdStrictness` (prependArgsStrictSig n_extra sig)
                               `setIdCprInfo`    mkCprSig (arity + n_extra) botCpr
 
 notWorthFloating :: CoreExpr -> [Var] -> Bool
diff --git a/compiler/GHC/Core/Opt/Simplify.hs b/compiler/GHC/Core/Opt/Simplify.hs
index 340efd2c9c..154b15e9d8 100644
--- a/compiler/GHC/Core/Opt/Simplify.hs
+++ b/compiler/GHC/Core/Opt/Simplify.hs
@@ -3058,7 +3058,7 @@ altsWouldDup (alt:alts)
   | is_bot_alt alt = altsWouldDup alts
   | otherwise      = not (all is_bot_alt alts)
   where
-    is_bot_alt (_,_,rhs) = exprIsBottom rhs
+    is_bot_alt (_,_,rhs) = exprIsDeadEnd rhs
 
 -------------------------
 mkDupableCont :: SimplEnv -> SimplCont
@@ -3515,7 +3515,7 @@ mkLetUnfolding dflags top_lvl src id new_rhs
             --             we don't.)  The simple thing is always to have one.
   where
     is_top_lvl   = isTopLevel top_lvl
-    is_bottoming = isBottomingId id
+    is_bottoming = isDeadEndId id
 
 -------------------
 simplStableUnfolding :: SimplEnv -> TopLevelFlag
diff --git a/compiler/GHC/Core/Opt/Simplify/Utils.hs b/compiler/GHC/Core/Opt/Simplify/Utils.hs
index 14e1a08fe0..87948ff6c1 100644
--- a/compiler/GHC/Core/Opt/Simplify/Utils.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Utils.hs
@@ -58,7 +58,6 @@ import GHC.Types.Var
 import GHC.Types.Demand
 import GHC.Types.Var.Set
 import GHC.Types.Basic
-import GHC.Builtin.PrimOps
 import GHC.Core.Opt.Simplify.Monad
 import GHC.Core.Type     hiding( substTy )
 import GHC.Core.Coercion hiding( substCo )
@@ -499,11 +498,9 @@ mkArgInfo env fun rules n_val_args call_cont
                         -- interesting context.  This avoids substituting
                         -- top-level bindings for (say) strings into
                         -- calls to error.  But now we are more careful about
-                        -- inlining lone variables, so it's ok
-                        -- (see GHC.Core.Opt.Simplify.Utils.analyseCont)
-                        -- See Note [Precise exceptions and strictness analysis] in Demand.hs
-                        -- for the special case on raiseIO#
-                   if isBotDiv result_info || isPrimOpId_maybe fun == Just RaiseIOOp then
+                        -- inlining lone variables, so its ok
+                        -- (see GHC.Core.Op.Simplify.Utils.analyseCont)
+                   if isDeadEndDiv result_info then
                         map isStrictDmd demands         -- Finite => result is bottom
                    else
                         map isStrictDmd demands ++ vanilla_stricts
@@ -1145,7 +1142,7 @@ preInlineUnconditionally
 preInlineUnconditionally env top_lvl bndr rhs rhs_env
   | not pre_inline_unconditionally           = Nothing
   | not active                               = Nothing
-  | isTopLevel top_lvl && isBottomingId bndr = Nothing -- Note [Top-level bottoming Ids]
+  | isTopLevel top_lvl && isDeadEndId bndr   = Nothing -- Note [Top-level bottoming Ids]
   | isCoVar bndr                             = Nothing -- Note [Do not inline CoVars unconditionally]
   | isExitJoinId bndr                        = Nothing -- Note [Do not inline exit join points]
                                                        -- in module Exitify
@@ -1517,7 +1514,7 @@ tryEtaExpandRhs :: SimplMode -> OutId -> OutExpr
 tryEtaExpandRhs mode bndr rhs
   | Just join_arity <- isJoinId_maybe bndr
   = do { let (join_bndrs, join_body) = collectNBinders join_arity rhs
-       ; return (count isId join_bndrs, exprIsBottom join_body, rhs) }
+       ; return (count isId join_bndrs, exprIsDeadEnd join_body, rhs) }
          -- Note [Do not eta-expand join points]
          -- But do return the correct arity and bottom-ness, because
          -- these are used to set the bndr's IdInfo (#15517)
diff --git a/compiler/GHC/Core/Opt/SpecConstr.hs b/compiler/GHC/Core/Opt/SpecConstr.hs
index 780c115857..d2c431765b 100644
--- a/compiler/GHC/Core/Opt/SpecConstr.hs
+++ b/compiler/GHC/Core/Opt/SpecConstr.hs
@@ -1551,8 +1551,8 @@ specialise env bind_calls (RI { ri_fn = fn, ri_lam_bndrs = arg_bndrs
                               , ri_lam_body = body, ri_arg_occs = arg_occs })
                spec_info@(SI { si_specs = specs, si_n_specs = spec_count
                              , si_mb_unspec = mb_unspec })
-  | isBottomingId fn      -- Note [Do not specialise diverging functions]
-                          -- and do not generate specialisation seeds from its RHS
+  | isDeadEndId fn  -- Note [Do not specialise diverging functions]
+                    -- and do not generate specialisation seeds from its RHS
   = -- pprTrace "specialise bot" (ppr fn) $
     return (nullUsage, spec_info)
 
@@ -1713,10 +1713,10 @@ calcSpecStrictness :: Id                     -- The original function
                    -> StrictSig              -- Strictness of specialised thing
 -- See Note [Transfer strictness]
 calcSpecStrictness fn qvars pats
-  = mkClosedStrictSig spec_dmds topDiv
+  = mkClosedStrictSig spec_dmds div
   where
     spec_dmds = [ lookupVarEnv dmd_env qv `orElse` topDmd | qv <- qvars, isId qv ]
-    StrictSig (DmdType _ dmds _) = idStrictness fn
+    StrictSig (DmdType _ dmds div) = idStrictness fn
 
     dmd_env = go emptyVarEnv dmds pats
 
@@ -1776,10 +1776,10 @@ Note [Transfer strictness]
 We must transfer strictness information from the original function to
 the specialised one.  Suppose, for example
 
-  f has strictness     SS
+  f has strictness     SSx
         and a RULE     f (a:as) b = f_spec a as b
 
-Now we want f_spec to have strictness  LLS, otherwise we'll use call-by-need
+Now we want f_spec to have strictness  LLSx, otherwise we'll use call-by-need
 when calling f_spec instead of call-by-value.  And that can result in
 unbounded worsening in space (cf the classic foldl vs foldl')
 
diff --git a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
index 4c4c3dc5e7..5ea719ac5b 100644
--- a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
+++ b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
@@ -1228,7 +1228,10 @@ mk_absent_let dflags fam_envs arg
 
     abs_rhs      = mkAbsentErrorApp arg_ty msg
     msg          = showSDoc (gopt_set dflags Opt_SuppressUniques)
-                          (ppr arg <+> ppr (idType arg))
+                            (ppr arg <+> ppr (idType arg) <+> file_msg)
+    file_msg     = case outputFile dflags of
+                     Nothing -> empty
+                     Just f  -> text "in output file " <+> quotes (text f)
               -- We need to suppress uniques here because otherwise they'd
               -- end up in the generated code as strings. This is bad for
               -- determinism, because with different uniques the strings
diff --git a/compiler/GHC/Core/SimpleOpt.hs b/compiler/GHC/Core/SimpleOpt.hs
index 3e55600461..e8a4e86af1 100644
--- a/compiler/GHC/Core/SimpleOpt.hs
+++ b/compiler/GHC/Core/SimpleOpt.hs
@@ -39,7 +39,7 @@ import GHC.Types.Var      ( isNonCoVarId )
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
 import GHC.Core.DataCon
-import GHC.Types.Demand( etaExpandStrictSig )
+import GHC.Types.Demand( etaConvertStrictSig )
 import GHC.Core.Coercion.Opt ( optCoercion )
 import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
                             , isInScope, substTyVarBndr, cloneTyVarBndr )
@@ -767,7 +767,7 @@ joinPointBinding_maybe bndr rhs
   , let str_sig   = idStrictness bndr
         str_arity = count isId bndrs  -- Strictness demands are for Ids only
         join_bndr = bndr `asJoinId`        join_arity
-                         `setIdStrictness` etaExpandStrictSig str_arity str_sig
+                         `setIdStrictness` etaConvertStrictSig str_arity str_sig
   = Just (join_bndr, mkLams bndrs body)
 
   | otherwise
diff --git a/compiler/GHC/Core/Unfold.hs b/compiler/GHC/Core/Unfold.hs
index 42a8974b54..bf281e7246 100644
--- a/compiler/GHC/Core/Unfold.hs
+++ b/compiler/GHC/Core/Unfold.hs
@@ -53,7 +53,7 @@ import GHC.Core.SimpleOpt
 import GHC.Core.Arity   ( manifestArity )
 import GHC.Core.Utils
 import GHC.Types.Id
-import GHC.Types.Demand ( StrictSig, isBottomingSig )
+import GHC.Types.Demand ( StrictSig, isDeadEndSig )
 import GHC.Core.DataCon
 import GHC.Types.Literal
 import GHC.Builtin.PrimOps
@@ -86,7 +86,7 @@ mkFinalUnfolding :: DynFlags -> UnfoldingSource -> StrictSig -> CoreExpr -> Unfo
 mkFinalUnfolding dflags src strict_sig expr
   = mkUnfolding dflags src
                 True {- Top level -}
-                (isBottomingSig strict_sig)
+                (isDeadEndSig strict_sig)
                 expr
 
 mkCompulsoryUnfolding :: CoreExpr -> Unfolding
@@ -1150,7 +1150,7 @@ certainlyWillInline dflags fn_info
         --    See Note [certainlyWillInline: INLINABLE]
     do_cunf expr (UnfIfGoodArgs { ug_size = size, ug_args = args })
       | arityInfo fn_info > 0  -- See Note [certainlyWillInline: be careful of thunks]
-      , not (isBottomingSig (strictnessInfo fn_info))
+      , not (isDeadEndSig (strictnessInfo fn_info))
               -- Do not unconditionally inline a bottoming functions even if
               -- it seems smallish. We've carefully lifted it out to top level,
               -- so we don't want to re-inline it.
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 6faf179489..b9f4a63eb5 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -23,7 +23,7 @@ module GHC.Core.Utils (
 
         -- * Properties of expressions
         exprType, coreAltType, coreAltsType, isExprLevPoly,
-        exprIsDupable, exprIsTrivial, getIdFromTrivialExpr, exprIsBottom,
+        exprIsDupable, exprIsTrivial, getIdFromTrivialExpr, exprIsDeadEnd,
         getIdFromTrivialExpr_maybe,
         exprIsCheap, exprIsExpandable, exprIsCheapX, CheapAppFun,
         exprIsHNF, exprOkForSpeculation, exprOkForSideEffects, exprIsWorkFree,
@@ -1031,21 +1031,21 @@ getIdFromTrivialExpr_maybe e
     go _       = Nothing
 
 {-
-exprIsBottom is a very cheap and cheerful function; it may return
+exprIsDeadEnd is a very cheap and cheerful function; it may return
 False for bottoming expressions, but it never costs much to ask.  See
 also GHC.Core.Arity.exprBotStrictness_maybe, but that's a bit more
 expensive.
 -}
 
-exprIsBottom :: CoreExpr -> Bool
+exprIsDeadEnd :: CoreExpr -> Bool
 -- See Note [Bottoming expressions]
-exprIsBottom e
+exprIsDeadEnd e
   | isEmptyTy (exprType e)
   = True
   | otherwise
   = go 0 e
   where
-    go n (Var v) = isBottomingId v &&  n >= idArity v
+    go n (Var v)                 = isDeadEndId v &&  n >= idArity v
     go n (App e a) | isTypeArg a = go n e
                    | otherwise   = go (n+1) e
     go n (Tick _ e)              = go n e
@@ -1059,7 +1059,7 @@ exprIsBottom e
 {- Note [Bottoming expressions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 A bottoming expression is guaranteed to diverge, or raise an
-exception.  We can test for it in two different ways, and exprIsBottom
+exception.  We can test for it in two different ways, and exprIsDeadEnd
 checks for both of these situations:
 
 * Visibly-bottom computations.  For example
@@ -1353,7 +1353,6 @@ type CheapAppFun = Id -> Arity -> Bool
   -- but with minor variations:
   --    isWorkFreeApp
   --    isCheapApp
-  --    isExpandableApp
 
 isWorkFreeApp :: CheapAppFun
 isWorkFreeApp fn n_val_args
@@ -1369,7 +1368,7 @@ isWorkFreeApp fn n_val_args
 isCheapApp :: CheapAppFun
 isCheapApp fn n_val_args
   | isWorkFreeApp fn n_val_args = True
-  | isBottomingId fn            = True  -- See Note [isCheapApp: bottoming functions]
+  | isDeadEndId fn              = True  -- See Note [isCheapApp: bottoming functions]
   | otherwise
   = case idDetails fn of
       DataConWorkId {} -> True  -- Actually handled by isWorkFreeApp
@@ -1390,7 +1389,7 @@ isExpandableApp fn n_val_args
       RecSelId {}  -> n_val_args == 1  -- See Note [Record selection]
       ClassOpId {} -> n_val_args == 1
       PrimOpId {}  -> False
-      _ | isBottomingId fn   -> False
+      _ | isDeadEndId fn     -> False
           -- See Note [isExpandableApp: bottoming functions]
         | isConLikeId fn     -> True
         | all_args_are_preds -> True
@@ -2136,7 +2135,7 @@ diffExpr top env (Tick n1 e1)   (Tick n2 e2)
  -- generated names, which are allowed to differ.
 diffExpr _   _   (App (App (Var absent) _) _)
                  (App (App (Var absent2) _) _)
-  | isBottomingId absent && isBottomingId absent2 = []
+  | isDeadEndId absent && isDeadEndId absent2 = []
 diffExpr top env (App f1 a1)    (App f2 a2)
   = diffExpr top env f1 f2 ++ diffExpr top env a1 a2
 diffExpr top env (Lam b1 e1)  (Lam b2 e2)
diff --git a/compiler/GHC/Iface/Tidy.hs b/compiler/GHC/Iface/Tidy.hs
index 430ef5ac7c..455b0824e1 100644
--- a/compiler/GHC/Iface/Tidy.hs
+++ b/compiler/GHC/Iface/Tidy.hs
@@ -39,7 +39,7 @@ import GHC.Types.Id.Make ( mkDictSelRhs )
 import GHC.Types.Id.Info
 import GHC.Core.InstEnv
 import GHC.Core.Type     ( tidyTopType )
-import GHC.Types.Demand  ( appIsBottom, isTopSig, isBottomingSig )
+import GHC.Types.Demand  ( appIsDeadEnd, isTopSig, isDeadEndSig )
 import GHC.Types.Cpr     ( mkCprSig, botCpr )
 import GHC.Types.Basic
 import GHC.Types.Name hiding (varName)
@@ -726,7 +726,7 @@ addExternal omit_prags expose_all id
     show_unfold    = show_unfolding unfolding
     never_active   = isNeverActive (inlinePragmaActivation (inlinePragInfo idinfo))
     loop_breaker   = isStrongLoopBreaker (occInfo idinfo)
-    bottoming_fn   = isBottomingSig (strictnessInfo idinfo)
+    bottoming_fn   = isDeadEndSig (strictnessInfo idinfo)
 
         -- Stuff to do with the Id's unfolding
         -- We leave the unfolding there even if there is a worker
@@ -1229,7 +1229,7 @@ tidyTopIdInfo dflags rhs_tidy_env name orig_rhs tidy_rhs idinfo show_unfold
 
     _bottom_hidden id_sig = case mb_bot_str of
                                   Nothing         -> False
-                                  Just (arity, _) -> not (appIsBottom id_sig arity)
+                                  Just (arity, _) -> not (appIsDeadEnd id_sig arity)
 
     --------- Unfolding ------------
     unf_info = unfoldingInfo idinfo
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs
index f36889444c..416eff9f4a 100644
--- a/compiler/GHC/Types/Demand.hs
+++ b/compiler/GHC/Types/Demand.hs
@@ -22,26 +22,25 @@ module GHC.Types.Demand (
         addCaseBndrDmd,
 
         DmdType(..), dmdTypeDepth, lubDmdType, bothDmdType,
-        nopDmdType, botDmdType, mkDmdType,
-        addDemand, ensureArgs,
         BothDmdArg, mkBothDmdArg, toBothDmdArg,
+        nopDmdType, botDmdType, addDemand,
 
         DmdEnv, emptyDmdEnv,
         peelFV, findIdDemand,
 
-        Divergence(..), lubDivergence, isBotDiv, isTopDiv, topDiv, botDiv,
-        appIsBottom, isBottomingSig, pprIfaceStrictSig,
+        Divergence(..), lubDivergence, isDeadEndDiv,
+        topDiv, botDiv, exnDiv,
+        appIsDeadEnd, isDeadEndSig, pprIfaceStrictSig,
         StrictSig(..), mkStrictSigForArity, mkClosedStrictSig,
-        nopSig, botSig, cprProdSig,
+        nopSig, botSig,
         isTopSig, hasDemandEnvSig,
         splitStrictSig, strictSigDmdEnv,
-        increaseStrictSigArity, etaExpandStrictSig,
+        prependArgsStrictSig, etaConvertStrictSig,
 
         seqDemand, seqDemandList, seqDmdType, seqStrictSig,
 
         evalDmd, cleanEvalDmd, cleanEvalProdDmd, isStrictDmd,
-        splitDmdTy, splitFVs,
-        deferAfterIO,
+        splitDmdTy, splitFVs, deferAfterPreciseException,
         postProcessUnsat, postProcessDmdType,
 
         splitProdDmd_maybe, peelCallDmd, peelManyCalls, mkCallDmd, mkCallDmds,
@@ -125,7 +124,7 @@ See #14998 for the way it's resolved at the moment.
 Here's a historic breakdown:
 
 Apparently, exception handling prim-ops didn't use to have any special
-strictness signatures, thus defaulting to topSig, which assumes they use their
+strictness signatures, thus defaulting to nopSig, which assumes they use their
 arguments lazily. Joachim was the first to realise that we could provide richer
 information. Thus, in 0558911f91c (Dec 13), he added signatures to
 primops.txt.pp indicating that functions like `catch#` and `catchRetry#` call
@@ -179,6 +178,13 @@ 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].
+
 -}
 
 -- | Vanilla strictness domain
@@ -913,30 +919,63 @@ Divergence:     Dunno
 In a fixpoint iteration, start from Diverges
 -}
 
+-- | Divergence lattice. Models a subset lattice of the following exhaustive
+-- set of divergence results:
+--
+-- [n] nontermination (e.g. loops)
+-- [i] throws imprecise exception
+-- [p] throws precise exception
+-- [c] converges (reduces to WHNF)
+--
+-- The different lattice elements correspond to different subsets, indicated by
+-- juxtaposition of indicators (e.g. __nc__ definitely doesn't throw an
+-- exception, and may or may not reduce to WHNF).
+--
+-- @
+--             Dunno (nipc)
+--                  |
+--            ExnOrDiv (nip)
+--                  |
+--            Diverges (ni)
+-- @
+--
+-- As you can see, we don't distinguish __n__ and __i__.
+-- See Note [Precise exceptions and strictness analysis] for why __p__ is so
+-- special compared to __i__.
 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. Never converges, hence 'isDeadEndDiv'!
+             --   See scenario 1 in Note [Precise exceptions and strictness analysis].
+  | Dunno    -- ^ Might diverge, throw any kind of exception or converge.
   deriving( Eq, Show )
 
-lubDivergence :: Divergence -> Divergence ->Divergence
-lubDivergence Diverges r        = r
-lubDivergence r        Diverges = r
-lubDivergence Dunno    Dunno    = Dunno
--- 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)
+lubDivergence :: Divergence -> Divergence -> Divergence
+lubDivergence Diverges div      = div
+lubDivergence div      Diverges = div
+lubDivergence ExnOrDiv ExnOrDiv = ExnOrDiv
+lubDivergence _        _        = Dunno
+-- This needs to commute with defaultFvDmd, i.e.
+-- defaultFvDmd (r1 `lubDivergence` r2) = defaultFvDmd r1 `lubDmd` defaultFvDmd r2
+-- (See Note [Default demand on free variables and arguments] for why)
 
 bothDivergence :: Divergence -> Divergence -> Divergence
--- See Note [Asymmetry of 'both' for DmdType and Divergence]
-bothDivergence _ Diverges = Diverges
-bothDivergence r Dunno    = r
--- 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)
+-- See Note [Asymmetry of 'both*'], which concludes that 'bothDivergence' needs
+-- to be symmetric.
+-- Strictly speaking, we should have @bothDivergence Dunno Diverges = ExnOrDiv@.
+-- But that regresses in too many places (every infinite loop, basically) to be
+-- worth it and is only relevant in higher-order scenarios
+-- (e.g. Divergence of @f (throwIO blah)@).
+-- So 'bothDivergence' currently is 'glbDivergence', really.
+bothDivergence Dunno    Dunno    = Dunno
+bothDivergence Diverges _        = Diverges
+bothDivergence _        Diverges = Diverges
+bothDivergence _        _        = ExnOrDiv
 
 instance Outputable Divergence where
-  ppr Diverges      = char 'b'
-  ppr Dunno         = empty
+  ppr Diverges = char 'b' -- for (b)ottom
+  ppr ExnOrDiv = char 'x' -- for e(x)ception
+  ppr Dunno    = empty
 
 {- Note [Precise vs imprecise exceptions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -958,78 +997,132 @@ Imprecise exceptions are actually more interesting than precise ones (which are
 fairly standard) from the perspective of semantics. See the paper "A Semantics
 for Imprecise Exceptions" for more details.
 
+Note [Dead ends]
+~~~~~~~~~~~~~~~~
+We call an expression that either diverges or throws a precise or imprecise
+exception a "dead end". We used to call such an expression just "bottoming",
+but with the measures we take to preserve precise exception semantics
+(see Note [Precise exceptions and strictness analysis]), that is no longer
+accurate: 'exnDiv' is no longer the bottom of the Divergence lattice.
+
+Yet externally to demand analysis, we mostly care about being able to drop dead
+code etc., which is all due to the property that such an expression never
+returns, hence we consider throwing a precise exception to be a dead end.
+See also 'isDeadEndDiv'.
+
 Note [Precise exceptions and strictness analysis]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-raiseIO# raises a *precise* exception, in contrast to raise# which
-raise an *imprecise* exception.  See Note [Precise vs imprecise exceptions]
-in XXXX.
+We have to take care to preserve precise exception semantics in strictness
+analysis (#17676). There are two scenarios that need careful treatment.
+
+The fixes were discussed at
+https://gitlab.haskell.org/ghc/ghc/wikis/fixing-precise-exceptions
 
-Unlike raise# (which returns botDiv), we want raiseIO# to return topDiv.
+Recall that raiseIO# raises a *precise* exception, in contrast to raise# which
+raises an *imprecise* exception. See Note [Precise vs imprecise exceptions].
+
+Scenario 1: Precise exceptions in case alternatives
+---------------------------------------------------
+Unlike raise# (which returns botDiv), we want raiseIO# to return exnDiv.
 Here's why. Consider this example from #13380 (similarly #17676):
-    f x y | x>0       = raiseIO Exc
-          | y>0       = return 1
-          | otherwise = return 2
+  f x y | x>0       = raiseIO# Exc
+        | y>0       = return 1
+        | otherwise = return 2
 Is 'f' strict in 'y'? One might be tempted to say yes! But that plays fast and
 loose with the precise exception; after optimisation, (f 42 (error "boom"))
 turns from throwing the precise Exc to throwing the imprecise user error
-"boom". So, the defaultDmd of raiseIO# should be lazy (topDmd), which can be
-achieved by giving it divergence topDiv.
+"boom". So, the defaultFvDmd of raiseIO# should be lazy (topDmd), which can be
+achieved by giving it divergence exnDiv.
+See Note [Default demand on free variables and arguments].
 
-But if it returns topDiv, the simplifier will fail to discard raiseIO#'s
-continuation in
-   case raiseIO# x s of { (# s', r #) -> <BIG> }
+Why don't we just give it topDiv instead of introducing exnDiv?
+Because then the simplifier will fail to discard raiseIO#'s continuation in
+  case raiseIO# x s of { (# s', r #) -> <BIG> }
 which we'd like to optimise to
-   raiseIO# x s
-Temporary hack solution: special treatment for raiseIO# in
-Simplifier.Utils.mkArgInfo. For the non-hack solution, see
-https://gitlab.haskell.org/ghc/ghc/wikis/fixing-precise-exceptions#replacing-hacks-by-principled-program-analyses
+  case raiseIO# x s of {}
+Hence we came up with exnDiv. The default FV demand of exnDiv is lazy (and
+its default arg dmd is absent), but otherwise (in terms of 'isDeadEndDiv') it
+behaves exactly as botDiv, so that dead code elimination works as expected.
+This is tracked by T13380b.
+
+Scenario 2: Precise exceptions in case scrutinees
+-------------------------------------------------
+Consider (more complete examples in #148, #1592, testcase strun003)
+
+  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 raiseIO#), then we must not force 'y', which may fail to
+terminate or throw an imprecise exception, until we have performed @foo x s@.
+
+So we have to 'Demand.deferAfterPreciseException' (which just 'lub's with
+'nopDmdType' to model the exceptional control flow) when @foo x s@
+may throw a precise exception. Motivated by T13380{d,e,f}.
+See Note [Which scrutinees may throw precise exceptions] in DmdAnal.
+
+Historical Note: This used to be called the "IO hack". But that term is rather
+a bad fit because
+1. It's easily confused with the "State hack", which also affects IO.
+2. Neither "IO" nor "hack" is a good description of what goes on here, which
+   is deferring strictness results after possibly throwing a precise exception.
+   The "hack" is probably not having to defer when we can prove that the
+   expression may not throw a precise exception (increasing precision of the
+   analysis), but that's just a favourable guess.
 -}
 
-
 ------------------------------------------------------------------------
 -- Combined demand result                                             --
 ------------------------------------------------------------------------
 
--- [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
-isTopDiv Dunno = True
-isTopDiv _     = False
-
--- | True if the result diverges or throws an exception
-isBotDiv :: Divergence -> Bool
-isBotDiv Diverges = True
-isBotDiv _        = False
-
--- See Notes [Default demand on free variables]
--- and [defaultDmd vs. resTypeArgDmd]
-defaultDmd :: Divergence -> Demand
-defaultDmd Dunno = absDmd
-defaultDmd _     = botDmd  -- Diverges
-
-resTypeArgDmd :: Divergence -> Demand
+-- | True if the result indicates that evaluation will not return.
+-- See Note [Dead ends].
+isDeadEndDiv :: Divergence -> Bool
+isDeadEndDiv Diverges = True
+isDeadEndDiv ExnOrDiv = True
+isDeadEndDiv Dunno    = False
+
+-- See Notes [Default demand on free variables and arguments]
+-- and Scenario 1 in [Precise exceptions and strictness analysis]
+defaultFvDmd :: Divergence -> Demand
+defaultFvDmd Dunno    = absDmd
+defaultFvDmd ExnOrDiv = absDmd -- This is the whole point of ExnOrDiv!
+defaultFvDmd Diverges = botDmd -- Diverges
+
+defaultArgDmd :: Divergence -> Demand
 -- TopRes and BotRes are polymorphic, so that
 --      BotRes === (Bot -> BotRes) === ...
 --      TopRes === (Top -> TopRes) === ...
 -- This function makes that concrete
--- Also see Note [defaultDmd vs. resTypeArgDmd]
-resTypeArgDmd Dunno = topDmd
-resTypeArgDmd _     = botDmd   -- Diverges
-
-{-
-Note [defaultDmd and resTypeArgDmd]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-These functions are similar: They express the demand on something not
-explicitly mentioned in the environment resp. the argument list. Yet they are
-different:
- * Variables not mentioned in the free variables environment are definitely
-   unused, so we can use absDmd there.
- * Further arguments *can* be used, of course. Hence topDmd is used.
+-- Also see Note [Default demand on free variables and arguments]
+defaultArgDmd Dunno    = topDmd
+-- NB: not botDmd! We don't want to mask the precise exception by forcing the
+-- argument. But it is still absent.
+defaultArgDmd ExnOrDiv = absDmd
+defaultArgDmd Diverges = botDmd
+
+{- Note [Default demand on free variables and arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Free variables not mentioned in the environment of a 'DmdType'
+are demanded according to the demand type's Divergence:
+  * In a Diverges (botDiv) context, that demand is botDmd
+    (HyperStr and Absent).
+  * In all other contexts, the demand is absDmd (Lazy and Absent).
+This is recorded in 'defaultFvDmd'.
+
+Similarly, we can eta-expand demand types to get demands on excess arguments
+not accounted for in the type, by consulting 'defaultArgDmd':
+  * In a Diverges (botDiv) context, that demand is again botDmd.
+  * In a ExnOrDiv (exnDiv) context, that demand is absDmd: We surely diverge
+    before evaluating the excess argument, but don't want to eagerly evaluate
+    it (cf. Note [Precise exceptions and strictness analysis]).
+  * In a Dunno context (topDiv), the demand is topDmd, because
+    it's perfectly possible to enter the additional lambda and evaluate it
+    in unforeseen ways (so, not Absent).
 
 
 ************************************************************************
@@ -1039,61 +1132,46 @@ different:
 ************************************************************************
 -}
 
-type DmdEnv = VarEnv Demand   -- See Note [Default demand on free variables]
+type DmdEnv = VarEnv Demand   -- See Note [Default demand on free variables and arguments]
 
 data DmdType = DmdType
                   DmdEnv        -- Demand on explicitly-mentioned
                                 --      free variables
                   [Demand]      -- Demand on arguments
-                  Divergence     -- See [Nature of result demand]
+                  Divergence     -- See [Demand type Divergence]
 
 {-
-Note [Nature of result demand]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A Divergence contains information about termination (currently distinguishing
-definite divergence and no information; it is possible to include definite
-convergence here), and CPR information about the result.
-
-The semantics of this depends on whether we are looking at a DmdType, i.e. the
-demand put on by an expression _under a specific incoming demand_ on its
-environment, or at a StrictSig describing a demand transformer.
-
-For a
- * DmdType, the termination information is true given the demand it was
-   generated with, while for
- * a StrictSig it holds after applying enough arguments.
-
-The CPR information, though, is valid after the number of arguments mentioned
-in the type is given. Therefore, when forgetting the demand on arguments, as in
-dmdAnalRhs, this needs to be considered (via removeDmdTyArgs).
+Note [Demand type Divergence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In contrast to StrictSigs, DmdTypes are elicited under a specific incoming demand.
+This is described in detail in Note [Understanding DmdType and StrictSig].
+Here, we'll focus on what that means for a DmdType's Divergence in a higher-order
+scenario.
 
 Consider
-  b2 x y = x `seq` y `seq` error (show x)
+  err x y = x `seq` y `seq` error (show x)
 this has a strictness signature of
   <S><S>b
-meaning that "b2 `seq` ()" and "b2 1 `seq` ()" might well terminate, but
-for "b2 1 2 `seq` ()" we get definite divergence.
-
-For comparison,
-  b1 x = x `seq` error (show x)
-has a strictness signature of
-  <S>b
-and "b1 1 `seq` ()" is known to terminate.
-
-Now consider a function h with signature "<C(S)>", and the expression
-  e1 = h b1
-now h puts a demand of <C(S)> onto its argument, and the demand transformer
-turns it into
-  <S>b
-Now the Divergence "b" does apply to us, even though "b1 `seq` ()" does not
-diverge, and we do not anything being passed to b.
-
-Note [Asymmetry of 'both' for DmdType and Divergence]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-'both' for DmdTypes is *asymmetrical*, because there is only one
-result!  For example, given (e1 e2), we get a DmdType dt1 for e1, use
-its arg demand to analyse e2 giving dt2, and then do (dt1 `bothType` dt2).
-Similarly with
+meaning that we don't know what happens when we call errin weaker contexts than
+C(C(S)), like @err `seq` ()@ (S) and @err 1 `seq` ()@ (C(S)). We may not unleash
+the botDiv, hence assume topDiv. Of course, in @err 1 2 `seq` ()@ the incoming
+demand C(C(S)) is strong enough and we see that the expression diverges.
+
+Now consider a function
+  f g = g 1 2
+with signature <C(S)>, and the expression
+  f err `seq` ()
+now f puts a strictness demand of C(C(S)) onto its argument, which is unleashed
+on err via the App rule. In contrast to weaker head strictness, this demand is
+strong enough to unleash err's signature and hence we see that the whole
+expression diverges!
+
+Note [Asymmetry of 'both*']
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+'both' for DmdTypes is *asymmetrical*, because there can only one
+be one type contributing argument demands!  For example, given (e1 e2), we get
+a DmdType dt1 for e1, use its arg demand to analyse e2 giving dt2, and then do
+(dt1 `bothType` dt2). Similarly with
   case e of { p -> rhs }
 we get dt_scrut from the scrutinee and dt_rhs from the RHS, and then
 compute (dt_rhs `bothType` dt_scrut).
@@ -1101,10 +1179,18 @@ compute (dt_rhs `bothType` dt_scrut).
 We
  1. combine the information on the free variables,
  2. take the demand on arguments from the first argument
- 3. combine the termination results, but
- 4. take CPR info from the first argument.
-
-3 and 4 are implemented in bothDivergence.
+ 3. combine the termination results, as in bothDivergence.
+
+Since we don't use argument demands of the second argument anyway, 'both's
+second argument is just a 'BothDmdType'.
+
+But note that the argument demand types are not guaranteed to be observed in
+left to right order. For example, analysis of a case expression will pass the
+demand type for the alts as the left argument and the type for the scrutinee as
+the right argument. Also, it is not at all clear if there is such an order;
+consider the LetUp case, where the RHS might be forced at any point while
+evaluating the let body.
+Therefore, it is crucial that 'bothDivergence' is symmetric!
 -}
 
 -- Equality needed for fixpoints in GHC.Core.Opt.DmdAnal
@@ -1116,45 +1202,34 @@ instance Eq DmdType where
          -- Unique order, it is the same order for both
                               && ds1 == ds2 && div1 == div2
 
+-- | Compute the least upper bound of two 'DmdType's elicited /by the same
+-- incoming demand/!
 lubDmdType :: DmdType -> DmdType -> DmdType
 lubDmdType d1 d2
   = DmdType lub_fv lub_ds lub_div
   where
     n = max (dmdTypeDepth d1) (dmdTypeDepth d2)
-    (DmdType fv1 ds1 r1) = ensureArgs n d1
-    (DmdType fv2 ds2 r2) = ensureArgs n d2
+    (DmdType fv1 ds1 r1) = etaExpandDmdType n d1
+    (DmdType fv2 ds2 r2) = etaExpandDmdType n d2
 
-    lub_fv  = plusVarEnv_CD lubDmd fv1 (defaultDmd r1) fv2 (defaultDmd r2)
+    lub_fv  = plusVarEnv_CD lubDmd fv1 (defaultFvDmd r1) fv2 (defaultFvDmd r2)
     lub_ds  = zipWithEqual "lubDmdType" lubDmd ds1 ds2
     lub_div = lubDivergence r1 r2
 
-{-
-Note [The need for BothDmdArg]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Previously, the right argument to bothDmdType, as well as the return value of
-dmdAnalStar via postProcessDmdType, was a DmdType. But bothDmdType only needs
-to know about the free variables and termination information, but nothing about
-the demand put on arguments, nor cpr information. So we make that explicit by
-only passing the relevant information.
--}
-
 type BothDmdArg = (DmdEnv, Divergence)
 
 mkBothDmdArg :: DmdEnv -> BothDmdArg
-mkBothDmdArg env = (env, Dunno)
+mkBothDmdArg env = (env, topDiv)
 
 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)
-    -- See Note [Asymmetry of 'both' for DmdType and Divergence]
+    -- See Note [Asymmetry of 'both*']
     -- 'both' takes the argument/result info from its *first* arg,
     -- using its second arg just for its free-var info.
-  = DmdType (plusVarEnv_CD bothDmd fv1 (defaultDmd r1) fv2 (defaultDmd t2))
+  = DmdType (plusVarEnv_CD bothDmd fv1 (defaultFvDmd r1) fv2 (defaultFvDmd t2))
             ds1
             (r1 `bothDivergence` t2)
 
@@ -1172,40 +1247,46 @@ instance Outputable DmdType where
 emptyDmdEnv :: VarEnv Demand
 emptyDmdEnv = emptyVarEnv
 
--- nopDmdType is the demand of doing nothing
--- (lazy, absent, no CPR information, no termination information).
--- Note that it is ''not'' the top of the lattice (which would be "may use everything"),
--- so it is (no longer) called topDmd
-nopDmdType, botDmdType :: DmdType
-nopDmdType = DmdType emptyDmdEnv [] topDiv
+botDmdType :: DmdType
 botDmdType = DmdType emptyDmdEnv [] botDiv
 
-isTopDmdType :: DmdType -> Bool
-isTopDmdType (DmdType env [] res)
-  | isTopDiv res && isEmptyVarEnv env = True
-isTopDmdType _                        = False
+-- | The demand type of doing nothing (lazy, absent, no Divergence
+-- information). Note that it is ''not'' the top of the lattice (which would be
+-- "may use everything"), so it is (no longer) called topDmdType.
+-- (SG: I agree, but why is it still 'topDmd' then?)
+nopDmdType :: DmdType
+nopDmdType = DmdType emptyDmdEnv [] topDiv
 
-mkDmdType :: DmdEnv -> [Demand] -> Divergence -> DmdType
-mkDmdType fv ds res = DmdType fv ds res
+isTopDmdType :: DmdType -> Bool
+isTopDmdType (DmdType env args div)
+  = div == topDiv && null args && isEmptyVarEnv env
 
 dmdTypeDepth :: DmdType -> Arity
 dmdTypeDepth (DmdType _ ds _) = length ds
 
--- | This makes sure we can use the demand type with n arguments.
--- It extends the argument list with the correct resTypeArgDmd.
--- It also adjusts the Divergence: Divergence survives additional arguments,
--- CPR information does not (and definite converge also would not).
-ensureArgs :: Arity -> DmdType -> DmdType
-ensureArgs n d | n == depth = d
-               | otherwise  = DmdType fv ds' r'
+-- | This makes sure we can use the demand type with n arguments after eta
+-- expansion, where n must not be lower than the demand types depth.
+-- It appends the argument list with the correct 'defaultArgDmd'.
+etaExpandDmdType :: Arity -> DmdType -> DmdType
+etaExpandDmdType n d
+  | n == depth = d
+  | n >  depth = DmdType fv inc_ds div
+  | otherwise  = pprPanic "etaExpandDmdType: arity decrease" (ppr n $$ ppr d)
   where depth = dmdTypeDepth d
-        DmdType fv ds r = d
-
-        ds' = take n (ds ++ repeat (resTypeArgDmd r))
-        r' = case r of    -- See [Nature of result demand]
-              Dunno -> topDiv
-              _     -> r
-
+        DmdType fv ds div = d
+        -- Arity increase:
+        --  * Demands on FVs are still valid
+        --  * Demands on args also valid, plus we can extend with defaultArgDmd
+        --    as appropriate for the given Divergence
+        --  * Divergence is still valid:
+        --    - A dead end after 2 arguments stays a dead end after 3 arguments
+        --    - The remaining case is Dunno, which is already topDiv
+        inc_ds  = take n (ds ++ repeat (defaultArgDmd div))
+
+-- | A conservative approximation for a given 'DmdType' in case of an arity
+-- decrease. Currently, it's just nopDmdType.
+decreaseArityDmdType :: DmdType -> DmdType
+decreaseArityDmdType _ = nopDmdType
 
 seqDmdType :: DmdType -> ()
 seqDmdType (DmdType env ds res) =
@@ -1219,23 +1300,16 @@ splitDmdTy :: DmdType -> (Demand, DmdType)
 -- We already have a suitable demand on all
 -- free vars, so no need to add more!
 splitDmdTy (DmdType fv (dmd:dmds) res_ty) = (dmd, DmdType fv dmds res_ty)
-splitDmdTy ty@(DmdType _ [] res_ty)       = (resTypeArgDmd res_ty, ty)
+splitDmdTy ty@(DmdType _ [] res_ty)       = (defaultArgDmd 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 GHC.Core.Opt.DmdAnal
-deferAfterIO :: DmdType -> DmdType
-deferAfterIO d@(DmdType _ _ res) =
-    case d `lubDmdType` nopDmdType of
-        DmdType fv ds _ -> DmdType fv ds (defer_res res)
-  where
-  defer_res r@(Dunno {}) = r
-  defer_res _            = topDiv  -- Diverges
+-- See Note [Precise exceptions and strictness analysis]
+deferAfterPreciseException :: DmdType -> DmdType
+deferAfterPreciseException d = lubDmdType d nopDmdType
 
 strictenDmd :: Demand -> CleanDemand
 strictenDmd (JD { sd = s, ud = u})
@@ -1270,14 +1344,16 @@ toCleanDmd (JD { sd = s, ud = u })
 -- This is used in dmdAnalStar when post-processing
 -- a function's argument demand. So we only care about what
 -- does to free variables, and whether it terminates.
--- see Note [The need for BothDmdArg]
+-- see Note [Asymmetry of 'both*']
 postProcessDmdType :: DmdShell -> DmdType -> BothDmdArg
 postProcessDmdType du@(JD { sd = ss }) (DmdType fv _ res_ty)
     = (postProcessDmdEnv du fv, postProcessDivergence ss res_ty)
 
 postProcessDivergence :: Str () -> Divergence -> Divergence
-postProcessDivergence Lazy _   = topDiv
-postProcessDivergence _    res = res
+-- In a Lazy scenario, we might not force the Divergence, in which case we
+-- converge, hence Dunno.
+postProcessDivergence Lazy _ = Dunno
+postProcessDivergence _    d = d
 
 postProcessDmdEnv :: DmdShell -> DmdEnv -> DmdEnv
 postProcessDmdEnv ds@(JD { sd = ss, ud = us }) env
@@ -1355,7 +1431,6 @@ peelManyCalls n (JD { sd = str, ud = abs })
 {-
 Note [Demands from unsaturated function calls]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Consider a demand transformer d1 -> d2 -> r for f.
 If a sufficiently detailed demand is fed into this transformer,
 e.g <C(C(S)), C1(C1(S))> arising from "f x1 x2" in a strict, use-once context,
@@ -1370,9 +1445,7 @@ But the demand fed into f might be less than <C(C(S)), C1(C1(S))>. There are a f
  * Not enough demand on the strictness side:
    - In that case, we need to zap all strictness in the demand on arguments and
      free variables.
-   - Furthermore, we remove CPR information. It could be left, but given the incoming
-     demand is not enough to evaluate so far we just do not bother.
-   - And finally termination information: If r says that f diverges for sure,
+   - And finally Divergence information: If r says that f Diverges for sure,
      then this holds when the demand guarantees that two arguments are going to
      be passed. If the demand is lower, we may just as well converge.
      If we were tracking definite convegence, than that would still hold under
@@ -1397,29 +1470,17 @@ peelFV (DmdType fv ds res) id = -- pprTrace "rfv" (ppr id <+> ppr dmd $$ ppr fv)
                                (DmdType fv' ds res, dmd)
   where
   fv' = fv `delVarEnv` id
-  -- See Note [Default demand on free variables]
-  dmd  = lookupVarEnv fv id `orElse` defaultDmd res
+  -- See Note [Default demand on free variables and arguments]
+  dmd  = lookupVarEnv fv id `orElse` defaultFvDmd res
 
 addDemand :: Demand -> DmdType -> DmdType
 addDemand dmd (DmdType fv ds res) = DmdType fv (dmd:ds) res
 
 findIdDemand :: DmdType -> Var -> Demand
 findIdDemand (DmdType fv _ res) id
-  = lookupVarEnv fv id `orElse` defaultDmd res
+  = lookupVarEnv fv id `orElse` defaultFvDmd res
 
 {-
-Note [Default demand on free variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the variable is not mentioned in the environment of a demand type,
-its demand is taken to be a result demand of the type.
-    For the strictness component,
-     if the result demand is a Diverges, then we use HyperStr
-                                         else we use Lazy
-    For the usage component, we use Absent.
-So we use either absDmd or botDmd.
-
-Also note the equations for lubDivergence (resp. bothDivergence) noted there.
-
 Note [Always analyse in virgin pass]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Tricky point: make sure that we analyse in the 'virgin' pass. Consider
@@ -1526,7 +1587,7 @@ transfomer, namely
 
 This DmdType gives the demands unleashed by the Id when it is applied
 to as many arguments as are given in by the arg demands in the DmdType.
-Also see Note [Nature of result demand] for the meaning of a Divergence in a
+Also see Note [Demand type Divergence] for the meaning of a Divergence in a
 strictness signature.
 
 If an Id is applied to less arguments than its arity, it means that
@@ -1585,9 +1646,6 @@ type's depth! So in mkStrictSigForArity we make sure to trim the list of
 argument demands to the given threshold arity. Call sites will make sure that
 this corresponds to the arity of the call demand that elicited the wrapped
 demand type. See also Note [What are demand signatures?] in GHC.Core.Opt.DmdAnal.
-
-Besides trimming argument demands, mkStrictSigForArity will also trim CPR
-information if necessary.
 -}
 
 -- | The depth of the wrapped 'DmdType' encodes the arity at which it is safe
@@ -1607,7 +1665,9 @@ pprIfaceStrictSig (StrictSig (DmdType _ dmds res))
 -- | Turns a 'DmdType' computed for the particular 'Arity' into a 'StrictSig'
 -- unleashable at that arity. See Note [Understanding DmdType and StrictSig]
 mkStrictSigForArity :: Arity -> DmdType -> StrictSig
-mkStrictSigForArity arity dmd_ty = StrictSig (ensureArgs arity dmd_ty)
+mkStrictSigForArity arity dmd_ty@(DmdType fvs args div)
+  | arity < dmdTypeDepth dmd_ty = StrictSig (DmdType fvs (take arity args) div)
+  | otherwise                   = StrictSig (etaExpandDmdType arity dmd_ty)
 
 mkClosedStrictSig :: [Demand] -> Divergence -> StrictSig
 mkClosedStrictSig ds res = mkStrictSigForArity (length ds) (DmdType emptyDmdEnv ds res)
@@ -1615,32 +1675,33 @@ mkClosedStrictSig ds res = mkStrictSigForArity (length ds) (DmdType emptyDmdEnv
 splitStrictSig :: StrictSig -> ([Demand], Divergence)
 splitStrictSig (StrictSig (DmdType _ dmds res)) = (dmds, res)
 
-increaseStrictSigArity :: Int -> StrictSig -> StrictSig
--- ^ Add extra arguments to a strictness signature.
--- In contrast to 'etaExpandStrictSig', this /prepends/ additional argument
--- demands and leaves CPR info intact.
-increaseStrictSigArity arity_increase sig@(StrictSig dmd_ty@(DmdType env dmds res))
+prependArgsStrictSig :: Int -> StrictSig -> StrictSig
+-- ^ Add extra ('topDmd') arguments to a strictness signature.
+-- In contrast to 'etaConvertStrictSig', this /prepends/ additional argument
+-- demands. This is used by FloatOut.
+prependArgsStrictSig new_args sig@(StrictSig dmd_ty@(DmdType env dmds res))
+  | new_args == 0       = sig
   | isTopDmdType dmd_ty = sig
-  | arity_increase == 0 = sig
-  | arity_increase < 0  = WARN( True, text "increaseStrictSigArity:"
-                                  <+> text "negative arity increase"
-                                  <+> ppr arity_increase )
-                          nopSig
+  | new_args < 0        = pprPanic "prependArgsStrictSig: negative new_args"
+                                   (ppr new_args $$ ppr sig)
   | otherwise           = StrictSig (DmdType env dmds' res)
   where
-    dmds' = replicate arity_increase topDmd ++ dmds
-
-etaExpandStrictSig :: Arity -> StrictSig -> StrictSig
--- ^ We are expanding (\x y. e) to (\x y z. e z).
--- In contrast to 'increaseStrictSigArity', this /appends/ extra arg demands if
--- necessary, potentially destroying the signature's CPR property.
-etaExpandStrictSig arity (StrictSig dmd_ty)
-  | arity < dmdTypeDepth dmd_ty
-  -- an arity decrease must zap the whole signature, because it was possibly
-  -- computed for a higher incoming call demand.
-  = nopSig
-  | otherwise
-  = StrictSig $ ensureArgs arity dmd_ty
+    dmds' = replicate new_args topDmd ++ dmds
+
+etaConvertStrictSig :: Arity -> StrictSig -> StrictSig
+-- ^ We are expanding (\x y. e) to (\x y z. e z) or reducing from the latter to
+-- the former (when the Simplifier identifies a new join points, for example).
+-- In contrast to 'prependArgsStrictSig', this /appends/ extra arg demands if
+-- necessary.
+-- This works by looking at the 'DmdType' (which was produced under a call
+-- demand for the old arity) and trying to transfer as many facts as we can to
+-- the call demand of new arity.
+-- An arity increase (resulting in a stronger incoming demand) can retain much
+-- of the info, while an arity decrease (a weakening of the incoming demand)
+-- must fall back to a conservative default.
+etaConvertStrictSig arity (StrictSig dmd_ty)
+  | arity < dmdTypeDepth dmd_ty = StrictSig $ decreaseArityDmdType dmd_ty
+  | otherwise                   = StrictSig $ etaExpandDmdType arity dmd_ty
 
 isTopSig :: StrictSig -> Bool
 isTopSig (StrictSig ty) = isTopDmdType ty
@@ -1651,16 +1712,16 @@ hasDemandEnvSig (StrictSig (DmdType env _ _)) = not (isEmptyVarEnv env)
 strictSigDmdEnv :: StrictSig -> DmdEnv
 strictSigDmdEnv (StrictSig (DmdType env _ _)) = env
 
--- | True if the signature diverges or throws an exception
-isBottomingSig :: StrictSig -> Bool
-isBottomingSig (StrictSig (DmdType _ _ res)) = isBotDiv res
+-- | True if the signature diverges or throws an exception in a saturated call.
+-- See Note [Dead ends].
+isDeadEndSig :: StrictSig -> Bool
+isDeadEndSig (StrictSig (DmdType _ _ res)) = isDeadEndDiv res
 
-nopSig, botSig :: StrictSig
-nopSig = StrictSig nopDmdType
+botSig :: StrictSig
 botSig = StrictSig botDmdType
 
-cprProdSig :: Arity -> StrictSig
-cprProdSig _arity = nopSig
+nopSig :: StrictSig
+nopSig = StrictSig nopDmdType
 
 seqStrictSig :: StrictSig -> ()
 seqStrictSig (StrictSig ty) = seqDmdType ty
@@ -1706,7 +1767,7 @@ dmdTransformDictSelSig (StrictSig (DmdType _ [dict_dmd] _)) cd
    = postProcessUnsat defer_use $
      DmdType emptyDmdEnv [mkOnceUsedDmd $ mkProdDmd $ map (enhance cd') jds] topDiv
    | otherwise
-   = nopDmdType              -- See Note [Demand transformer for a dictionary selector]
+   = nopDmdType -- See Note [Demand transformer for a dictionary selector]
   where
     enhance cd old | isAbsDmd old = old
                    | otherwise    = mkOnceUsedDmd cd  -- This is the one!
@@ -1789,13 +1850,11 @@ The occurrence analyser propagates this one-shot infor to the
 binders \pqr and \xyz; see Note [Use one-shot information] in OccurAnal.
 -}
 
--- | Returns true if an application to n args
--- would diverge or throw an exception
--- See Note [Unsaturated applications]
-appIsBottom :: StrictSig -> Int -> Bool
-appIsBottom (StrictSig (DmdType _ ds res)) n
-            | isBotDiv res                   = not $ lengthExceeds ds n
-appIsBottom _                              _ = False
+-- | Returns true if an application to n args would diverge or throw an
+-- exception. See Note [Unsaturated applications] and Note [Dead ends].
+appIsDeadEnd :: StrictSig -> Int -> Bool
+appIsDeadEnd (StrictSig (DmdType _ ds res)) n
+  = isDeadEndDiv res && not (lengthExceeds ds n)
 
 {-
 Note [Unsaturated applications]
@@ -1803,9 +1862,9 @@ Note [Unsaturated applications]
 If a function having bottom as its demand result is applied to a less
 number of arguments than its syntactic arity, we cannot say for sure
 that it is going to diverge. This is the reason why we use the
-function appIsBottom, which, given a strictness signature and a number
-of arguments, says conservatively if the function is going to diverge
-or not.
+function appIsDeadEnd, which, given a strictness signature and a number
+of arguments, says conservatively if the function is never going to return.
+See Note [Dead ends].
 -}
 
 zapUsageEnvSig :: StrictSig -> StrictSig
@@ -2019,9 +2078,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/GHC/Types/ForeignCall.hs b/compiler/GHC/Types/ForeignCall.hs
index 2a42a2b51e..cf3739bfca 100644
--- a/compiler/GHC/Types/ForeignCall.hs
+++ b/compiler/GHC/Types/ForeignCall.hs
@@ -49,20 +49,27 @@ instance Outputable ForeignCall where
   ppr (CCall cc)  = ppr cc
 
 data Safety
-  = PlaySafe            -- Might invoke Haskell GC, or do a call back, or
-                        -- switch threads, etc.  So make sure things are
-                        -- tidy before the call. Additionally, in the threaded
-                        -- RTS we arrange for the external call to be executed
-                        -- by a separate OS thread, i.e., _concurrently_ to the
-                        -- execution of other Haskell threads.
-
-  | PlayInterruptible   -- Like PlaySafe, but additionally
-                        -- the worker thread running this foreign call may
-                        -- be unceremoniously killed, so it must be scheduled
-                        -- on an unbound thread.
-
-  | PlayRisky           -- None of the above can happen; the call will return
-                        -- without interacting with the runtime system at all
+  = PlaySafe          -- ^ Might invoke Haskell GC, or do a call back, or
+                      --   switch threads, etc.  So make sure things are
+                      --   tidy before the call. Additionally, in the threaded
+                      --   RTS we arrange for the external call to be executed
+                      --   by a separate OS thread, i.e., _concurrently_ to the
+                      --   execution of other Haskell threads.
+
+  | PlayInterruptible -- ^ Like PlaySafe, but additionally
+                      --   the worker thread running this foreign call may
+                      --   be unceremoniously killed, so it must be scheduled
+                      --   on an unbound thread.
+
+  | PlayRisky         -- ^ None of the above can happen; the call will return
+                      --   without interacting with the runtime system at all.
+                      --   Specifically:
+                      --
+                      --     * No GC
+                      --     * No call backs
+                      --     * No blocking
+                      --     * No precise exceptions
+                      --
   deriving ( Eq, Show, Data )
         -- Show used just for Show Lex.Token, I think
 
diff --git a/compiler/GHC/Types/Id.hs b/compiler/GHC/Types/Id.hs
index 028bfd45f0..3d9d9c3f40 100644
--- a/compiler/GHC/Types/Id.hs
+++ b/compiler/GHC/Types/Id.hs
@@ -70,7 +70,7 @@ module GHC.Types.Id (
         isDataConWrapId, isDataConWrapId_maybe,
         isDataConId_maybe,
         idDataCon,
-        isConLikeId, isBottomingId, idIsFrom,
+        isConLikeId, isDeadEndId, idIsFrom,
         hasNoBinding,
 
         -- ** Join variables
@@ -637,10 +637,11 @@ setIdCallArity id arity = modifyIdInfo (`setCallArityInfo` arity) id
 idFunRepArity :: Id -> RepArity
 idFunRepArity x = countFunRepArgs (idArity x) (idType x)
 
--- | Returns true if an application to n args would diverge
-isBottomingId :: Var -> Bool
-isBottomingId v
-  | isId v    = isBottomingSig (idStrictness v)
+-- | Returns true if an application to n args diverges or throws an exception
+-- See Note [Dead ends] in GHC.Types.Demand.
+isDeadEndId :: Var -> Bool
+isDeadEndId v
+  | isId v    = isDeadEndSig (idStrictness v)
   | otherwise = False
 
 -- | Accesses the 'Id''s 'strictnessInfo'.
@@ -958,7 +959,7 @@ transferPolyIdInfo old_id abstract_wrt new_id
     new_occ_info    = zapOccTailCallInfo old_occ_info
 
     old_strictness  = strictnessInfo old_info
-    new_strictness  = increaseStrictSigArity arity_increase old_strictness
+    new_strictness  = prependArgsStrictSig arity_increase old_strictness
     old_cpr         = cprInfo old_info
 
     transfer new_info = new_info `setArityInfo` new_arity
diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index df62ad5469..910d738a8e 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -1245,8 +1245,8 @@ mkPrimOpId prim_op
 
     -- PrimOps don't ever construct a product, but we want to preserve bottoms
     cpr
-      | isBotDiv (snd (splitStrictSig strict_sig)) = botCpr
-      | otherwise                                  = topCpr
+      | isDeadEndDiv (snd (splitStrictSig strict_sig)) = botCpr
+      | otherwise                                      = topCpr
 
     info = noCafIdInfo
            `setRuleInfo`           mkRuleInfo (maybeToList $ primOpRules name prim_op)
@@ -1372,7 +1372,7 @@ proxyHashId :: Id
 proxyHashId
   = pcMiscPrelId proxyName ty
        (noCafIdInfo `setUnfoldingInfo` evaldUnfolding -- Note [evaldUnfoldings]
-                    `setNeverLevPoly`  ty )
+                    `setNeverLevPoly`  ty)
   where
     -- proxy# :: forall {k} (a:k). Proxy# k a
     --
@@ -1699,8 +1699,8 @@ inlined.
 realWorldPrimId :: Id   -- :: State# RealWorld
 realWorldPrimId = pcMiscPrelId realWorldName realWorldStatePrimTy
                      (noCafIdInfo `setUnfoldingInfo` evaldUnfolding    -- Note [evaldUnfoldings]
-                                  `setOneShotInfo` stateHackOneShot
-                                  `setNeverLevPoly` realWorldStatePrimTy)
+                                  `setOneShotInfo`   stateHackOneShot
+                                  `setNeverLevPoly`  realWorldStatePrimTy)
 
 voidPrimId :: Id     -- Global constant :: Void#
 voidPrimId  = pcMiscPrelId voidPrimIdName voidPrimTy