Make DataCon workers strict in strict fields (#20749)wip/T20749

This patch tweaks `exprIsConApp_maybe`, `exprIsHNF` and friends, and Demand
Analysis so that they exploit and maintain strictness of DataCon workers. See
`Note [Strict fields in Core]` for details.

Very little needed to change, and it puts field seq insertion done by Tag
Inference into a new perspective: That of *implementing* strict field semantics.
Before Tag Inference, DataCon workers are strict. Afterwards they are
effectively lazy and field seqs happen around use sites. History has shown
that there is no other way to guarantee taggedness and thus the STG Strict Field
Invariant.

Knock-on changes:

  * `exprIsHNF` previously used `exprOkForSpeculation` on unlifted arguments
    instead of recursing into `exprIsHNF`. That regressed the termination
    analysis in CPR analysis (which simply calls out to `exprIsHNF`), so I made
    it call `exprOkForSpeculation`, too.

  * There's a small regression in Demand Analysis, visible in the changed test
    output of T16859: Previously, a field seq on a variable would give that
    variable a "used exactly once" demand, now it's "used at least once",
    because `dmdTransformDataConSig` accounts for future uses of the field
    that actually all go through the case binder (and hence won't re-enter the
    potential thunk). The difference should hardly be observable.

  * The Simplifier's fast path for data constructors only applies to lazy
    data constructors now. I observed regressions involving Data.Binary.Put's
    `Pair` data type.

  * Unfortunately, T21392 does no longer reproduce after this patch, so I marked
    it as "not broken" in order to track whether we regress again in the future.

Fixes #20749, the satisfying conclusion of an annoying saga (cf. the ideas
in #21497 and #22475).

9 files changed, 289 insertions, 229 deletions

diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index f54f42d99d..61628962fb 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -48,7 +48,8 @@ module GHC.Core.DataCon (
         dataConIsInfix,
         dataConWorkId, dataConWrapId, dataConWrapId_maybe,
         dataConImplicitTyThings,
-        dataConRepStrictness, dataConImplBangs, dataConBoxer,
+        dataConRepStrictness, dataConRepStrictness_maybe,
+        dataConImplBangs, dataConBoxer,
 
         splitDataProductType_maybe,
 
@@ -59,7 +60,7 @@ module GHC.Core.DataCon (
         isVanillaDataCon, isNewDataCon, isTypeDataCon,
         classDataCon, dataConCannotMatch,
         dataConUserTyVarsNeedWrapper, checkDataConTyVars,
-        isBanged, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
+        isBanged, isUnpacked, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
         specialPromotedDc,
 
         -- ** Promotion related functions
@@ -95,6 +96,7 @@ import GHC.Types.Unique.FM ( UniqFM )
 import GHC.Types.Unique.Set
 import GHC.Builtin.Uniques( mkAlphaTyVarUnique )
 import GHC.Data.Graph.UnVar  -- UnVarSet and operations
+import GHC.Data.Maybe (orElse)
 
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
@@ -502,6 +504,18 @@ data DataCon
                 -- Matches 1-1 with dcOrigArgTys
                 -- Hence length = dataConSourceArity dataCon
 
+        dcImplBangs :: [HsImplBang],
+                -- The actual decisions made (including failures)
+                -- about the original arguments; 1-1 with orig_arg_tys
+                -- See Note [Bangs on data constructor arguments]
+
+        dcStricts :: [StrictnessMark],
+                -- One mark for every field of the DataCon worker;
+                -- if it's empty, then all fields are lazy,
+                -- otherwise it has the same length as dataConRepArgTys.
+                -- See also Note [Strict fields in Core] in GHC.Core
+                -- for the effect on the strictness signature
+
         dcFields  :: [FieldLabel],
                 -- Field labels for this constructor, in the
                 -- same order as the dcOrigArgTys;
@@ -777,13 +791,6 @@ data DataConRep
                                           -- after unboxing and flattening,
                                           -- and *including* all evidence args
 
-        , dcr_stricts :: [StrictnessMark]  -- 1-1 with dcr_arg_tys
-                -- See also Note [Data-con worker strictness]
-
-        , dcr_bangs :: [HsImplBang]  -- The actual decisions made (including failures)
-                                     -- about the original arguments; 1-1 with orig_arg_tys
-                                     -- See Note [Bangs on data constructor arguments]
-
     }
 
 type DataConEnv a = UniqFM DataCon a     -- Keyed by DataCon
@@ -852,43 +859,8 @@ eqSpecPreds spec = [ mkPrimEqPred (mkTyVarTy tv) ty
 instance Outputable EqSpec where
   ppr (EqSpec tv ty) = ppr (tv, ty)
 
-{- Note [Data-con worker strictness]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Notice that we do *not* say the worker Id is strict even if the data
-constructor is declared strict
-     e.g.    data T = MkT ![Int] Bool
-Even though most often the evals are done by the *wrapper* $WMkT, there are
-situations in which tag inference will re-insert evals around the worker.
-So for all intents and purposes the *worker* MkT is strict, too!
-
-Unfortunately, if we exposed accurate strictness of DataCon workers, we'd
-see the following transformation:
-
-  f xs = case xs of xs' { __DEFAULT -> ... case MkT xs b of x { __DEFAULT -> [x] } } -- DmdAnal: Strict in xs
-  ==> { drop-seq, binder swap on xs' }
-  f xs = case MkT xs b of x { __DEFAULT -> [x] } -- DmdAnal: Still strict in xs
-  ==> { case-to-let }
-  f xs = let x = MkT xs' b in [x] -- DmdAnal: No longer strict in xs!
-
-I.e., we are ironically losing strictness in `xs` by dropping the eval on `xs`
-and then doing case-to-let. The issue is that `exprIsHNF` currently says that
-every DataCon worker app is a value. The implicit assumption is that surrounding
-evals will have evaluated strict fields like `xs` before! But now that we had
-just dropped the eval on `xs`, that assumption is no longer valid.
-
-Long story short: By keeping the demand signature lazy, the Simplifier will not
-drop the eval on `xs` and using `exprIsHNF` to decide case-to-let and others
-remains sound.
-
-Similarly, during demand analysis in dmdTransformDataConSig, we bump up the
-field demand with `C_01`, *not* `C_11`, because the latter exposes too much
-strictness that will drop the eval on `xs` above.
-
-This issue is discussed at length in
-"Failed idea: no wrappers for strict data constructors" in #21497 and #22475.
-
-Note [Bangs on data constructor arguments]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Bangs on data constructor arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
   data T = MkT !Int {-# UNPACK #-} !Int Bool
 
@@ -914,8 +886,8 @@ Terminology:
   the flag settings in the importing module.
   Also see Note [Bangs on imported data constructors] in GHC.Types.Id.Make
 
-* The dcr_bangs field of the dcRep field records the [HsImplBang]
-  If T was defined in this module, Without -O the dcr_bangs might be
+* The dcImplBangs field records the [HsImplBang]
+  If T was defined in this module, Without -O the dcImplBangs might be
     [HsStrict _, HsStrict _, HsLazy]
   With -O it might be
     [HsStrict _, HsUnpack _, HsLazy]
@@ -959,6 +931,17 @@ we consult HsImplBang:
 The boolean flag is used only for this warning.
 See #11270 for motivation.
 
+* Core passes will often need to know whether the DataCon worker or wrapper in
+  an application is strict in some (lifted) field or not. This is tracked in the
+  demand signature attached to a DataCon's worker resp. wrapper Id.
+
+  So if you've got a DataCon dc, you can get the demand signature by
+  `idDmdSig (dataConWorkId dc)` and make out strict args by testing with
+  `isStrictDmd`. Similarly, `idDmdSig <$> dataConWrapId_maybe dc` gives
+  you the demand signature of the wrapper, if it exists.
+
+  These demand signatures are set in GHC.Types.Id.Make.
+
 Note [Data con representation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The dcRepType field contains the type of the representation of a constructor
@@ -974,14 +957,14 @@ what it means is the DataCon with all Unpacking having been applied.
 We can think of this as the Core representation.
 
 Here's an example illustrating the Core representation:
-        data Ord a => T a = MkT Int! a Void#
+        data Ord a => T a = MkT !Int a Void#
 Here
         T :: Ord a => Int -> a -> Void# -> T a
 but the rep type is
         Trep :: Int# -> a -> Void# -> T a
 Actually, the unboxed part isn't implemented yet!
 
-Not that this representation is still *different* from runtime
+Note that this representation is still *different* from runtime
 representation. (Which is what STG uses after unarise).
 
 This is how T would end up being used in STG post-unarise:
@@ -1106,6 +1089,11 @@ isBanged (HsUnpack {}) = True
 isBanged (HsStrict {}) = True
 isBanged HsLazy        = False
 
+isUnpacked :: HsImplBang -> Bool
+isUnpacked (HsUnpack {}) = True
+isUnpacked (HsStrict {}) = False
+isUnpacked HsLazy        = False
+
 isSrcStrict :: SrcStrictness -> Bool
 isSrcStrict SrcStrict = True
 isSrcStrict _ = False
@@ -1131,13 +1119,15 @@ cbvFromStrictMark MarkedStrict = MarkedCbv
 
 -- | Build a new data constructor
 mkDataCon :: Name
-          -> Bool           -- ^ Is the constructor declared infix?
-          -> TyConRepName   -- ^  TyConRepName for the promoted TyCon
-          -> [HsSrcBang]    -- ^ Strictness/unpack annotations, from user
-          -> [FieldLabel]   -- ^ Field labels for the constructor,
-                            -- if it is a record, otherwise empty
-          -> [TyVar]        -- ^ Universals.
-          -> [TyCoVar]      -- ^ Existentials.
+          -> Bool               -- ^ Is the constructor declared infix?
+          -> TyConRepName       -- ^  TyConRepName for the promoted TyCon
+          -> [HsSrcBang]        -- ^ Strictness/unpack annotations, from user
+          -> [HsImplBang]       -- ^ Strictness/unpack annotations, as inferred by the compiler
+          -> [StrictnessMark]   -- ^ Strictness marks for the DataCon worker's fields in Core
+          -> [FieldLabel]       -- ^ Field labels for the constructor,
+                                -- if it is a record, otherwise empty
+          -> [TyVar]            -- ^ Universals.
+          -> [TyCoVar]          -- ^ Existentials.
           -> [InvisTVBinder]    -- ^ User-written 'TyVarBinder's.
                                 --   These must be Inferred/Specified.
                                 --   See @Note [TyVarBinders in DataCons]@
@@ -1156,7 +1146,9 @@ mkDataCon :: Name
   -- Can get the tag from the TyCon
 
 mkDataCon name declared_infix prom_info
-          arg_stricts   -- Must match orig_arg_tys 1-1
+          arg_stricts  -- Must match orig_arg_tys 1-1
+          impl_bangs   -- Must match orig_arg_tys 1-1
+          str_marks    -- Must be empty or match dataConRepArgTys 1-1
           fields
           univ_tvs ex_tvs user_tvbs
           eq_spec theta
@@ -1173,6 +1165,8 @@ mkDataCon name declared_infix prom_info
   = con
   where
     is_vanilla = null ex_tvs && null eq_spec && null theta
+    str_marks' | not $ any isMarkedStrict str_marks = []
+               | otherwise                          = str_marks
 
     con = MkData {dcName = name, dcUnique = nameUnique name,
                   dcVanilla = is_vanilla, dcInfix = declared_infix,
@@ -1184,7 +1178,8 @@ mkDataCon name declared_infix prom_info
                   dcStupidTheta = stupid_theta,
                   dcOrigArgTys = orig_arg_tys, dcOrigResTy = orig_res_ty,
                   dcRepTyCon = rep_tycon,
-                  dcSrcBangs = arg_stricts,
+                  dcSrcBangs = arg_stricts, dcImplBangs = impl_bangs,
+                  dcStricts = str_marks',
                   dcFields = fields, dcTag = tag, dcRepType = rep_ty,
                   dcWorkId = work_id,
                   dcRep = rep,
@@ -1412,19 +1407,27 @@ isNullaryRepDataCon :: DataCon -> Bool
 isNullaryRepDataCon dc = dataConRepArity dc == 0
 
 dataConRepStrictness :: DataCon -> [StrictnessMark]
--- ^ Give the demands on the arguments of a
--- Core constructor application (Con dc args)
-dataConRepStrictness dc = case dcRep dc of
-                            NoDataConRep -> [NotMarkedStrict | _ <- dataConRepArgTys dc]
-                            DCR { dcr_stricts = strs } -> strs
+-- ^ Give the demands on the runtime arguments of a Core DataCon worker
+-- application.
+-- The length of the list matches `dataConRepArgTys` (e.g., the number
+-- of runtime arguments).
+dataConRepStrictness dc
+  = dataConRepStrictness_maybe dc
+    `orElse` map (const NotMarkedStrict) (dataConRepArgTys dc)
+
+dataConRepStrictness_maybe :: DataCon -> Maybe [StrictnessMark]
+-- ^ Give the demands on the runtime arguments of a Core DataCon worker
+-- application or `Nothing` if all of them are lazy.
+-- The length of the list matches `dataConRepArgTys` (e.g., the number
+-- of runtime arguments).
+dataConRepStrictness_maybe dc
+  | null (dcStricts dc) = Nothing
+  | otherwise           = Just (dcStricts dc)
 
 dataConImplBangs :: DataCon -> [HsImplBang]
 -- The implementation decisions about the strictness/unpack of each
 -- source program argument to the data constructor
-dataConImplBangs dc
-  = case dcRep dc of
-      NoDataConRep              -> replicate (dcSourceArity dc) HsLazy
-      DCR { dcr_bangs = bangs } -> bangs
+dataConImplBangs dc = dcImplBangs dc
 
 dataConBoxer :: DataCon -> Maybe DataConBoxer
 dataConBoxer (MkData { dcRep = DCR { dcr_boxer = boxer } }) = Just boxer
diff --git a/compiler/GHC/Core/Opt/Arity.hs b/compiler/GHC/Core/Opt/Arity.hs
index 3716dc6ea0..33abf5e640 100644
--- a/compiler/GHC/Core/Opt/Arity.hs
+++ b/compiler/GHC/Core/Opt/Arity.hs
@@ -1443,7 +1443,7 @@ myExprIsCheap (AE { am_opts = opts, am_sigs = sigs }) e mb_ty
         -- See Note [Eta expanding through dictionaries]
         -- See Note [Eta expanding through CallStacks]
 
-    cheap_fun e = exprIsCheapX (myIsCheapApp sigs) e
+    cheap_fun e = exprIsCheapX (myIsCheapApp sigs) False e
 
 -- | A version of 'isCheapApp' that considers results from arity analysis.
 -- See Note [Arity analysis] for what's in the signature environment and why
diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs
index 86fdc5cdb5..3c2c1348d1 100644
--- a/compiler/GHC/Core/Opt/ConstantFold.hs
+++ b/compiler/GHC/Core/Opt/ConstantFold.hs
@@ -46,7 +46,7 @@ import GHC.Core
 import GHC.Core.Make
 import GHC.Core.SimpleOpt (  exprIsConApp_maybe, exprIsLiteral_maybe )
 import GHC.Core.DataCon ( DataCon,dataConTagZ, dataConTyCon, dataConWrapId, dataConWorkId )
-import GHC.Core.Utils  ( cheapEqExpr, exprIsHNF
+import GHC.Core.Utils  ( cheapEqExpr, exprOkForSpeculation
                        , stripTicksTop, stripTicksTopT, mkTicks )
 import GHC.Core.Multiplicity
 import GHC.Core.Rules.Config
@@ -1932,7 +1932,7 @@ Things to note
 
 Implementing seq#.  The compiler has magic for SeqOp in
 
-- GHC.Core.Opt.ConstantFold.seqRule: eliminate (seq# <whnf> s)
+- GHC.Core.Opt.ConstantFold.seqRule: eliminate (seq# <ok-for-spec> s)
 
 - GHC.StgToCmm.Expr.cgExpr, and cgCase: special case for seq#
 
@@ -1947,7 +1947,7 @@ Implementing seq#.  The compiler has magic for SeqOp in
 seqRule :: RuleM CoreExpr
 seqRule = do
   [Type _ty_a, Type _ty_s, a, s] <- getArgs
-  guard $ exprIsHNF a
+  guard $ exprOkForSpeculation a
   return $ mkCoreUnboxedTuple [s, a]
 
 -- spark# :: forall a s . a -> State# s -> (# State# s, a #)
diff --git a/compiler/GHC/Core/Opt/CprAnal.hs b/compiler/GHC/Core/Opt/CprAnal.hs
index 87d9eb2ec7..5199635c4e 100644
--- a/compiler/GHC/Core/Opt/CprAnal.hs
+++ b/compiler/GHC/Core/Opt/CprAnal.hs
@@ -297,9 +297,16 @@ data TermFlag -- Better than using a Bool
 
 -- See Note [Nested CPR]
 exprTerminates :: CoreExpr -> TermFlag
+-- ^ A /very/ simple termination analysis.
 exprTerminates e
-  | exprIsHNF e = Terminates -- A /very/ simple termination analysis.
-  | otherwise   = MightDiverge
+  | exprIsHNF e            = Terminates
+  | exprOkForSpeculation e = Terminates
+  | otherwise              = MightDiverge
+  -- Annyingly, we have to check both for HNF and ok-for-spec.
+  --   * `I# (x# *# 2#)` is ok-for-spec, but not in HNF. Still worth CPR'ing!
+  --   * `lvl` is an HNF if its unfolding is evaluated
+  --     (perhaps `lvl = I# 0#` at top-level). But, tiresomely, it is never
+  --     ok-for-spec due to Note [exprOkForSpeculation and evaluated variables].
 
 cprAnalApp :: AnalEnv -> CoreExpr -> [(CprType, CoreArg)] -> (CprType, CoreExpr)
 -- Main function that takes care of /nested/ CPR. See Note [Nested CPR]
diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index 0bcabf55d3..d495d93245 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -814,6 +814,10 @@ 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.
 
+You might think that we should check for side-effects rather than just for
+precise exceptions. Right you are! See Note [Side-effects and strictness]
+for why we unfortunately do not.
+
 Note [Demand analysis for recursive data constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 T11545 features a single-product, recursive data type
diff --git a/compiler/GHC/Core/Opt/Simplify/Env.hs b/compiler/GHC/Core/Opt/Simplify/Env.hs
index 759f6e24fa..07f84cc7de 100644
--- a/compiler/GHC/Core/Opt/Simplify/Env.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Env.hs
@@ -8,14 +8,13 @@
 
 module GHC.Core.Opt.Simplify.Env (
         -- * The simplifier mode
-        SimplMode(..), updMode,
-        smPedanticBottoms, smPlatform,
+        SimplMode(..), updMode, smPlatform,
 
         -- * Environments
         SimplEnv(..), pprSimplEnv,   -- Temp not abstract
         seArityOpts, seCaseCase, seCaseFolding, seCaseMerge, seCastSwizzle,
         seDoEtaReduction, seEtaExpand, seFloatEnable, seInline, seNames,
-        seOptCoercionOpts, sePedanticBottoms, sePhase, sePlatform, sePreInline,
+        seOptCoercionOpts, sePhase, sePlatform, sePreInline,
         seRuleOpts, seRules, seUnfoldingOpts,
         mkSimplEnv, extendIdSubst,
         extendTvSubst, extendCvSubst,
@@ -216,9 +215,6 @@ seNames env = sm_names (seMode env)
 seOptCoercionOpts :: SimplEnv -> OptCoercionOpts
 seOptCoercionOpts env = sm_co_opt_opts (seMode env)
 
-sePedanticBottoms :: SimplEnv -> Bool
-sePedanticBottoms env = smPedanticBottoms (seMode env)
-
 sePhase :: SimplEnv -> CompilerPhase
 sePhase env = sm_phase (seMode env)
 
@@ -273,9 +269,6 @@ instance Outputable SimplMode where
          where
            pp_flag f s = ppUnless f (text "no") <+> s
 
-smPedanticBottoms :: SimplMode -> Bool
-smPedanticBottoms opts = ao_ped_bot (sm_arity_opts opts)
-
 smPlatform :: SimplMode -> Platform
 smPlatform opts = roPlatform (sm_rule_opts opts)
 
diff --git a/compiler/GHC/Core/Opt/Simplify/Iteration.hs b/compiler/GHC/Core/Opt/Simplify/Iteration.hs
index 07ea775fc0..cf83b44be9 100644
--- a/compiler/GHC/Core/Opt/Simplify/Iteration.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Iteration.hs
@@ -32,7 +32,7 @@ import GHC.Core.Reduction
 import GHC.Core.Coercion.Opt    ( optCoercion )
 import GHC.Core.FamInstEnv      ( FamInstEnv, topNormaliseType_maybe )
 import GHC.Core.DataCon
-   ( DataCon, dataConWorkId, dataConRepStrictness
+   ( DataCon, dataConWorkId, dataConRepStrictness, dataConRepStrictness_maybe
    , dataConRepArgTys, isUnboxedTupleDataCon
    , StrictnessMark (..) )
 import GHC.Core.Opt.Stats ( Tick(..) )
@@ -2094,14 +2094,14 @@ zap the SubstEnv.  This is VITAL.  Consider
 We'll clone the inner \x, adding x->x' in the id_subst Then when we
 inline y, we must *not* replace x by x' in the inlined copy!!
 
-Note [Fast path for data constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Fast path for lazy data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For applications of a data constructor worker, the full glory of
 rebuildCall is a waste of effort;
 * They never inline, obviously
 * They have no rewrite rules
-* They are not strict (see Note [Data-con worker strictness]
-  in GHC.Core.DataCon)
+* Though they might be strict (see Note [Strict fields in Core] in GHC.Core),
+  we will exploit that strictness through their demand signature
 So it's fine to zoom straight to `rebuild` which just rebuilds the
 call in a very straightforward way.
 
@@ -2125,7 +2125,8 @@ simplVar env var
 
 simplIdF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplFloats, OutExpr)
 simplIdF env var cont
-  | isDataConWorkId var         -- See Note [Fast path for data constructors]
+  | Just dc <- isDataConWorkId_maybe var      -- See Note [Fast path for lazy data constructors]
+  , Nothing <- dataConRepStrictness_maybe dc
   = rebuild env (Var var) cont
   | otherwise
   = case substId env var of
@@ -3304,7 +3305,7 @@ a case pattern.  This is *important*.  Consider
 
 We really must record that b is already evaluated so that we don't
 go and re-evaluate it when constructing the result.
-See Note [Data-con worker strictness] in GHC.Core.DataCon
+See Note [Strict fields in Core] in GHC.Core.
 
 NB: simplLamBndrs preserves this eval info
 
diff --git a/compiler/GHC/Core/SimpleOpt.hs b/compiler/GHC/Core/SimpleOpt.hs
index 609d007a5a..77ddde68a2 100644
--- a/compiler/GHC/Core/SimpleOpt.hs
+++ b/compiler/GHC/Core/SimpleOpt.hs
@@ -1219,11 +1219,8 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr
        --       simplifier produces rhs[exp/a], changing semantics if exp is not ok-for-spec
        -- Good: returning (Mk#, [x]) with a float of  case exp of x { DEFAULT -> [] }
        --       simplifier produces case exp of a { DEFAULT -> exp[x/a] }
-       = let arg' = subst_expr subst arg
-             bndr = uniqAway (subst_in_scope subst) (mkWildValBinder ManyTy arg_type)
-             float = FloatCase arg' bndr DEFAULT []
-             subst' = subst_extend_in_scope subst bndr
-         in go subst' (float:floats) fun (CC (Var bndr : args) co)
+       , (subst', float, bndr) <- case_bind subst arg arg_type
+       = go subst' (float:floats) fun (CC (Var bndr : args) co)
        | otherwise
        = go subst floats fun (CC (subst_expr subst arg : args) co)
 
@@ -1262,8 +1259,9 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr
 
         | Just con <- isDataConWorkId_maybe fun
         , count isValArg args == idArity fun
-        = succeedWith in_scope floats $
-          pushCoDataCon con args co
+        , (in_scope', seq_floats, args') <- mkFieldSeqFloats in_scope con args
+        = succeedWith in_scope' (seq_floats ++ floats) $
+          pushCoDataCon con args' co
 
         -- Look through data constructor wrappers: they inline late (See Note
         -- [Activation for data constructor wrappers]) but we want to do
@@ -1349,6 +1347,36 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr
     extend (Left in_scope) v e = Right (extendSubst (mkEmptySubst in_scope) v e)
     extend (Right s)       v e = Right (extendSubst s v e)
 
+    case_bind :: Either InScopeSet Subst -> CoreExpr -> Type -> (Either InScopeSet Subst, FloatBind, Id)
+    case_bind subst expr expr_ty = (subst', float, bndr)
+      where
+        bndr   = setCaseBndrEvald MarkedStrict $
+                 uniqAway (subst_in_scope subst) $
+                 mkWildValBinder ManyTy expr_ty
+        subst' = subst_extend_in_scope subst bndr
+        expr'  = subst_expr subst expr
+        float  = FloatCase expr' bndr DEFAULT []
+
+    mkFieldSeqFloats :: InScopeSet -> DataCon -> [CoreExpr] -> (InScopeSet, [FloatBind], [CoreExpr])
+    mkFieldSeqFloats in_scope dc args
+      | Nothing <- dataConRepStrictness_maybe dc
+      = (in_scope, [], args)
+      | otherwise
+      = (in_scope', floats', ty_args ++ val_args')
+      where
+        (ty_args, val_args) = splitAtList (dataConUnivAndExTyCoVars dc) args
+        (in_scope', floats', val_args') = foldr do_one (in_scope, [], []) $ zipEqual "mkFieldSeqFloats" str_marks val_args
+        str_marks = dataConRepStrictness dc
+        do_one (str, arg) (in_scope,floats,args)
+          | NotMarkedStrict <- str   = (in_scope, floats, arg:args)
+          | Var v <- arg, is_evald v = (in_scope, floats, arg:args)
+          | otherwise                = (in_scope', float:floats, Var bndr:args)
+          where
+            is_evald v = isId v && isEvaldUnfolding (idUnfolding v)
+            (in_scope', float, bndr) =
+               case case_bind (Left in_scope) arg (exprType arg) of
+                 (Left in_scope', float, bndr) -> (in_scope', float, bndr)
+                 (right, _, _) -> pprPanic "case_bind did not preserve Left" (ppr in_scope $$ ppr arg $$ ppr right)
 
 -- See Note [exprIsConApp_maybe on literal strings]
 dealWithStringLiteral :: Var -> BS.ByteString -> Coercion
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index 21ceb2a7bb..72d7fc4e0f 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -1253,18 +1253,23 @@ in this (which it previously was):
             in \w. v True
 -}
 
---------------------
-exprIsWorkFree :: CoreExpr -> Bool   -- See Note [exprIsWorkFree]
-exprIsWorkFree e = exprIsCheapX isWorkFreeApp e
-
-exprIsCheap :: CoreExpr -> Bool
-exprIsCheap e = exprIsCheapX isCheapApp e
+-------------------------------------
+type CheapAppFun = Id -> Arity -> Bool
+  -- Is an application of this function to n *value* args
+  -- always cheap, assuming the arguments are cheap?
+  -- True mainly of data constructors, partial applications;
+  -- but with minor variations:
+  --    isWorkFreeApp
+  --    isCheapApp
+  --    isExpandableApp
 
-exprIsCheapX :: CheapAppFun -> CoreExpr -> Bool
+exprIsCheapX :: CheapAppFun -> Bool -> CoreExpr -> Bool
 {-# INLINE exprIsCheapX #-}
--- allow specialization of exprIsCheap and exprIsWorkFree
+-- allow specialization of exprIsCheap, exprIsWorkFree and exprIsExpandable
 -- instead of having an unknown call to ok_app
-exprIsCheapX ok_app e
+-- expandable: Only True for exprIsExpandable, where Case and Let are never
+--             expandable.
+exprIsCheapX ok_app expandable e
   = ok e
   where
     ok e = go 0 e
@@ -1275,98 +1280,34 @@ exprIsCheapX ok_app e
     go _ (Type {})                    = True
     go _ (Coercion {})                = True
     go n (Cast e _)                   = go n e
-    go n (Case scrut _ _ alts)        = ok scrut &&
-                                        and [ go n rhs | Alt _ _ rhs <- alts ]
     go n (Tick t e) | tickishCounts t = False
                     | otherwise       = go n e
     go n (Lam x e)  | isRuntimeVar x  = n==0 || go (n-1) e
                     | otherwise       = go n e
     go n (App f e)  | isRuntimeArg e  = go (n+1) f && ok e
                     | otherwise       = go n f
-    go n (Let (NonRec _ r) e)         = go n e && ok r
-    go n (Let (Rec prs) e)            = go n e && all (ok . snd) prs
+    go n (Case scrut _ _ alts)        = not expandable && ok scrut &&
+                                        and [ go n rhs | Alt _ _ rhs <- alts ]
+    go n (Let (NonRec _ r) e)         = not expandable && go n e && ok r
+    go n (Let (Rec prs) e)            = not expandable && go n e && all (ok . snd) prs
 
       -- Case: see Note [Case expressions are work-free]
       -- App, Let: see Note [Arguments and let-bindings exprIsCheapX]
 
+--------------------
+exprIsWorkFree :: CoreExpr -> Bool
+-- See Note [exprIsWorkFree]
+exprIsWorkFree e = exprIsCheapX isWorkFreeApp False e
 
-{- Note [exprIsExpandable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-An expression is "expandable" if we are willing to duplicate it, if doing
-so might make a RULE or case-of-constructor fire.  Consider
-   let x = (a,b)
-       y = build g
-   in ....(case x of (p,q) -> rhs)....(foldr k z y)....
-
-We don't inline 'x' or 'y' (see Note [Lone variables] in GHC.Core.Unfold),
-but we do want
-
- * the case-expression to simplify
-   (via exprIsConApp_maybe, exprIsLiteral_maybe)
-
- * the foldr/build RULE to fire
-   (by expanding the unfolding during rule matching)
-
-So we classify the unfolding of a let-binding as "expandable" (via the
-uf_expandable field) if we want to do this kind of on-the-fly
-expansion.  Specifically:
-
-* True of constructor applications (K a b)
-
-* True of applications of a "CONLIKE" Id; see Note [CONLIKE pragma] in GHC.Types.Basic.
-  (NB: exprIsCheap might not be true of this)
-
-* False of case-expressions.  If we have
-    let x = case ... in ...(case x of ...)...
-  we won't simplify.  We have to inline x.  See #14688.
-
-* False of let-expressions (same reason); and in any case we
-  float lets out of an RHS if doing so will reveal an expandable
-  application (see SimplEnv.doFloatFromRhs).
-
-* Take care: exprIsExpandable should /not/ be true of primops.  I
-  found this in test T5623a:
-    let q = /\a. Ptr a (a +# b)
-    in case q @ Float of Ptr v -> ...q...
-
-  q's inlining should not be expandable, else exprIsConApp_maybe will
-  say that (q @ Float) expands to (Ptr a (a +# b)), and that will
-  duplicate the (a +# b) primop, which we should not do lightly.
-  (It's quite hard to trigger this bug, but T13155 does so for GHC 8.0.)
--}
+--------------------
+exprIsCheap :: CoreExpr -> Bool
+-- See Note [exprIsCheap]
+exprIsCheap e = exprIsCheapX isCheapApp False e
 
--------------------------------------
+--------------------
 exprIsExpandable :: CoreExpr -> Bool
 -- See Note [exprIsExpandable]
-exprIsExpandable e
-  = ok e
-  where
-    ok e = go 0 e
-
-    -- n is the number of value arguments
-    go n (Var v)                      = isExpandableApp v n
-    go _ (Lit {})                     = True
-    go _ (Type {})                    = True
-    go _ (Coercion {})                = True
-    go n (Cast e _)                   = go n e
-    go n (Tick t e) | tickishCounts t = False
-                    | otherwise       = go n e
-    go n (Lam x e)  | isRuntimeVar x  = n==0 || go (n-1) e
-                    | otherwise       = go n e
-    go n (App f e)  | isRuntimeArg e  = go (n+1) f && ok e
-                    | otherwise       = go n f
-    go _ (Case {})                    = False
-    go _ (Let {})                     = False
-
-
--------------------------------------
-type CheapAppFun = Id -> Arity -> Bool
-  -- Is an application of this function to n *value* args
-  -- always cheap, assuming the arguments are cheap?
-  -- True mainly of data constructors, partial applications;
-  -- but with minor variations:
-  --    isWorkFreeApp
-  --    isCheapApp
+exprIsExpandable e = exprIsCheapX isExpandableApp True e
 
 isWorkFreeApp :: CheapAppFun
 isWorkFreeApp fn n_val_args
@@ -1385,7 +1326,7 @@ isCheapApp fn n_val_args
   | isDeadEndId fn              = True  -- See Note [isCheapApp: bottoming functions]
   | otherwise
   = case idDetails fn of
-      DataConWorkId {} -> True  -- Actually handled by isWorkFreeApp
+      -- DataConWorkId {} -> _  -- Handled by isWorkFreeApp
       RecSelId {}      -> n_val_args == 1  -- See Note [Record selection]
       ClassOpId {}     -> n_val_args == 1
       PrimOpId op _    -> primOpIsCheap op
@@ -1400,6 +1341,7 @@ isExpandableApp fn n_val_args
   | isWorkFreeApp fn n_val_args = True
   | otherwise
   = case idDetails fn of
+      -- DataConWorkId {} -> _  -- Handled by isWorkFreeApp
       RecSelId {}  -> n_val_args == 1  -- See Note [Record selection]
       ClassOpId {} -> n_val_args == 1
       PrimOpId {}  -> False
@@ -1431,6 +1373,50 @@ isExpandableApp fn n_val_args
 I'm not sure why we have a special case for bottoming
 functions in isCheapApp.  Maybe we don't need it.
 
+Note [exprIsExpandable]
+~~~~~~~~~~~~~~~~~~~~~~~
+An expression is "expandable" if we are willing to duplicate it, if doing
+so might make a RULE or case-of-constructor fire.  Consider
+   let x = (a,b)
+       y = build g
+   in ....(case x of (p,q) -> rhs)....(foldr k z y)....
+
+We don't inline 'x' or 'y' (see Note [Lone variables] in GHC.Core.Unfold),
+but we do want
+
+ * the case-expression to simplify
+   (via exprIsConApp_maybe, exprIsLiteral_maybe)
+
+ * the foldr/build RULE to fire
+   (by expanding the unfolding during rule matching)
+
+So we classify the unfolding of a let-binding as "expandable" (via the
+uf_expandable field) if we want to do this kind of on-the-fly
+expansion.  Specifically:
+
+* True of constructor applications (K a b)
+
+* True of applications of a "CONLIKE" Id; see Note [CONLIKE pragma] in GHC.Types.Basic.
+  (NB: exprIsCheap might not be true of this)
+
+* False of case-expressions.  If we have
+    let x = case ... in ...(case x of ...)...
+  we won't simplify.  We have to inline x.  See #14688.
+
+* False of let-expressions (same reason); and in any case we
+  float lets out of an RHS if doing so will reveal an expandable
+  application (see SimplEnv.doFloatFromRhs).
+
+* Take care: exprIsExpandable should /not/ be true of primops.  I
+  found this in test T5623a:
+    let q = /\a. Ptr a (a +# b)
+    in case q @ Float of Ptr v -> ...q...
+
+  q's inlining should not be expandable, else exprIsConApp_maybe will
+  say that (q @ Float) expands to (Ptr a (a +# b)), and that will
+  duplicate the (a +# b) primop, which we should not do lightly.
+  (It's quite hard to trigger this bug, but T13155 does so for GHC 8.0.)
+
 Note [isExpandableApp: bottoming functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's important that isExpandableApp does not respond True to bottoming
@@ -1574,10 +1560,10 @@ expr_ok fun_ok primop_ok (Case scrut bndr _ alts)
   && altsAreExhaustive alts
 
 expr_ok fun_ok primop_ok other_expr
-  | (expr, args) <- collectArgs other_expr
+  | (expr, val_args) <- collectValArgs other_expr
   = case stripTicksTopE (not . tickishCounts) expr of
         Var f ->
-           app_ok fun_ok primop_ok f args
+           app_ok fun_ok primop_ok f val_args
 
         -- 'LitRubbish' is the only literal that can occur in the head of an
         -- application and will not be matched by the above case (Var /= Lit).
@@ -1591,8 +1577,8 @@ expr_ok fun_ok primop_ok other_expr
         _ -> False
 
 -----------------------------
-app_ok :: (Id -> Bool) -> (PrimOp -> Bool) -> Id -> [CoreExpr] -> Bool
-app_ok fun_ok primop_ok fun args
+app_ok :: (Id -> Bool) -> (PrimOp -> Bool) -> Id -> [CoreArg] -> Bool
+app_ok fun_ok primop_ok fun val_args
   | not (fun_ok fun)
   = False -- This code path is only taken for Note [Speculative evaluation]
   | otherwise
@@ -1601,21 +1587,22 @@ app_ok fun_ok primop_ok fun args
          -- DFuns terminate, unless the dict is implemented
          -- with a newtype in which case they may not
 
-      DataConWorkId {} -> True
-                -- The strictness of the constructor has already
-                -- been expressed by its "wrapper", so we don't need
-                -- to take the arguments into account
+      DataConWorkId dc
+        | Just str_marks <- dataConRepStrictness_maybe dc
+        -> all3Prefix field_ok str_marks val_arg_tys val_args
+        | otherwise
+        -> all2Prefix arg_ok val_arg_tys val_args
 
       ClassOpId _ is_terminating_result
         | is_terminating_result -- See Note [exprOkForSpeculation and type classes]
-        -> assertPpr (n_val_args == 1) (ppr fun $$ ppr args) $
+        -> assertPpr (n_val_args == 1) (ppr fun $$ ppr val_args) $
            True
            -- assert: terminating result type => can't be applied;
            -- c.f the _other case below
 
       PrimOpId op _
         | primOpIsDiv op
-        , [arg1, Lit lit] <- args
+        , [arg1, Lit lit] <- val_args
         -> not (isZeroLit lit) && expr_ok fun_ok primop_ok arg1
               -- Special case for dividing operations that fail
               -- In general they are NOT ok-for-speculation
@@ -1633,13 +1620,13 @@ app_ok fun_ok primop_ok fun args
 
         | otherwise
         -> primop_ok op  -- Check the primop itself
-        && and (zipWith arg_ok arg_tys args)  -- Check the arguments
+        && all2Prefix arg_ok val_arg_tys val_args  -- Check the arguments
 
       _other  -- Unlifted and terminating types;
               -- Also c.f. the Var case of exprIsHNF
          |  isTerminatingType fun_ty  -- See Note [exprOkForSpeculation and type classes]
          || definitelyUnliftedType fun_ty
-         -> assertPpr (n_val_args == 0) (ppr fun $$ ppr args)
+         -> assertPpr (n_val_args == 0) (ppr fun $$ ppr val_args)
             True  -- Both terminating types (e.g. Eq a), and unlifted types (e.g. Int#)
                   -- are non-functions and so will have no value args.  The assert is
                   -- just to check this.
@@ -1648,7 +1635,7 @@ app_ok fun_ok primop_ok fun args
 
          -- Partial applications
          | idArity fun > n_val_args ->
-           and (zipWith arg_ok arg_tys args)  -- Check the arguments
+           all2Prefix arg_ok val_arg_tys val_args  -- Check the arguments
 
          -- Functions that terminate fast without raising exceptions etc
          -- See Note [Discarding unnecessary unsafeEqualityProofs]
@@ -1660,18 +1647,27 @@ app_ok fun_ok primop_ok fun args
              --     see Note [exprOkForSpeculation and evaluated variables]
   where
     fun_ty       = idType fun
-    n_val_args   = valArgCount args
+    n_val_args   = length val_args
     (arg_tys, _) = splitPiTys fun_ty
+    val_arg_tys  = mapMaybe anonPiTyBinderType_maybe arg_tys
 
     -- Used for arguments to primops and to partial applications
-    arg_ok :: PiTyVarBinder -> CoreExpr -> Bool
-    arg_ok (Named _) _ = True   -- A type argument
-    arg_ok (Anon ty _) arg      -- A term argument
-       | definitelyLiftedType (scaledThing ty)
+    arg_ok :: Type -> CoreExpr -> Bool
+    arg_ok ty arg
+       | definitelyLiftedType ty
        = True -- See Note [Primops with lifted arguments]
        | otherwise
        = expr_ok fun_ok primop_ok arg
 
+    -- Used for DataCon worker arguments
+    field_ok :: StrictnessMark -> Type -> CoreExpr -> Bool
+    field_ok str ty arg      -- A term argument
+       | NotMarkedStrict <- str   -- iff it's a lazy field
+       , definitelyLiftedType ty  -- and its type is lifted
+       = True                     -- then the worker app does not eval
+       | otherwise
+       = expr_ok fun_ok primop_ok arg
+
 -----------------------------
 altsAreExhaustive :: [Alt b] -> Bool
 -- True  <=> the case alternatives are definitely exhaustive
@@ -1938,12 +1934,14 @@ exprIsConLike = exprIsHNFlike isConLikeId isConLikeUnfolding
 -- or PAPs.
 --
 exprIsHNFlike :: HasDebugCallStack => (Var -> Bool) -> (Unfolding -> Bool) -> CoreExpr -> Bool
-exprIsHNFlike is_con is_con_unf = is_hnf_like
+exprIsHNFlike is_con is_con_unf e
+  = -- pprTraceWith "hnf" (\r -> ppr r <+> ppr e) $
+    is_hnf_like e
   where
     is_hnf_like (Var v) -- NB: There are no value args at this point
-      =  id_app_is_value v 0 -- Catches nullary constructors,
-                             --      so that [] and () are values, for example
-                             -- and (e.g.) primops that don't have unfoldings
+      =  id_app_is_value v [] -- Catches nullary constructors,
+                              --      so that [] and () are values, for example
+                              -- and (e.g.) primops that don't have unfoldings
       || is_con_unf (idUnfolding v)
         -- Check the thing's unfolding; it might be bound to a value
         --   or to a guaranteed-evaluated variable (isEvaldUnfolding)
@@ -1967,31 +1965,57 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like
                                       -- See Note [exprIsHNF Tick]
     is_hnf_like (Cast e _)       = is_hnf_like e
     is_hnf_like (App e a)
-      | isValArg a               = app_is_value e 1
+      | isValArg a               = app_is_value e [a]
       | otherwise                = is_hnf_like e
     is_hnf_like (Let _ e)        = is_hnf_like e  -- Lazy let(rec)s don't affect us
     is_hnf_like _                = False
 
-    -- 'n' is the number of value args to which the expression is applied
-    -- And n>0: there is at least one value argument
-    app_is_value :: CoreExpr -> Int -> Bool
-    app_is_value (Var f)    nva = id_app_is_value f nva
-    app_is_value (Tick _ f) nva = app_is_value f nva
-    app_is_value (Cast f _) nva = app_is_value f nva
-    app_is_value (App f a)  nva
-      | isValArg a              =
-        app_is_value f (nva + 1) &&
-        not (needsCaseBinding (exprType a) a)
-          -- For example  f (x /# y)  where f has arity two, and the first
-          -- argument is unboxed. This is not a value!
-          -- But  f 34#  is a value.
-          -- NB: Check app_is_value first, the arity check is cheaper
-      | otherwise               = app_is_value f nva
-    app_is_value _          _   = False
-
-    id_app_is_value id n_val_args
-       = is_con id
-       || idArity id > n_val_args
+    -- Collect arguments through Casts and Ticks and call id_app_is_value
+    app_is_value :: CoreExpr -> [CoreArg] -> Bool
+    app_is_value (Var f)    as = id_app_is_value f as
+    app_is_value (Tick _ f) as = app_is_value f as
+    app_is_value (Cast f _) as = app_is_value f as
+    app_is_value (App f a)  as | isValArg a = app_is_value f (a:as)
+                               | otherwise  = app_is_value f as
+    app_is_value _          _  = False
+
+    id_app_is_value id val_args
+       -- First handle saturated applications of DataCons with strict fields
+       | Just dc <- isDataConWorkId_maybe id              -- DataCon
+       , Just str_marks <- dataConRepStrictness_maybe dc  -- with strict fields
+       , assert (val_args `leLength` str_marks) True
+       , val_args `equalLength` str_marks                 -- in a saturated app
+       = all3Prefix check_field str_marks val_arg_tys val_args
+
+       -- Now all applications except saturated DataCon apps with strict fields
+       |  idArity id > length val_args
+            -- PAP: Check unlifted val_args
+       || is_con id && isNothing (isDataConWorkId_maybe id >>= dataConRepStrictness_maybe)
+            -- Either a lazy DataCon or a CONLIKE.
+            -- Hence we only need to check unlifted val_args here.
+            -- NB: We assume that CONLIKEs are lazy, which is their entire
+            --     point.
+       = all2Prefix check_arg val_arg_tys val_args
+
+       | otherwise
+       = False
+       where
+         fun_ty      = idType id
+         (arg_tys,_) = splitPiTys fun_ty
+         val_arg_tys = mapMaybe anonPiTyBinderType_maybe  arg_tys
+         -- val_arg_tys = map exprType val_args, but much less costly.
+         -- The obvious definition regresses T16577 by 30% so we don't do it.
+
+         check_arg a_ty a = mightBeUnliftedType a_ty ==> is_hnf_like a
+          -- Check unliftedness; for example f (x /# 12#) where f has arity two,
+          -- and the first argument is unboxed. This is not a value!
+          -- But  f 34#  is a value, so check args for HNFs.
+          -- NB: We check arity (and CONLIKEness) first because it's cheaper
+          --     and we reject quickly on saturated apps.
+         check_field str a_ty a
+           = isMarkedStrict str || mightBeUnliftedType a_ty ==> is_hnf_like a
+         a ==> b = not a || b
+         infixr 1 ==>
 
 {-
 Note [exprIsHNF Tick]
@@ -2552,7 +2576,7 @@ This means the seqs on x and y both become no-ops and compared to the first vers
 
 The downside is that the caller of $wfoo potentially has to evaluate `y` once if we can't prove it isn't already evaluated.
 But y coming out of a strict field is in WHNF so safe to evaluated. And most of the time it will be properly tagged+evaluated
-already at the call site because of the Strict Field Invariant! See Note [Strict Field Invariant] for more in this.
+already at the call site because of the Strict Field Invariant! See Note [STG Strict Field Invariant] for more in this.
 This makes GHC itself around 1% faster despite doing slightly more work! So this is generally quite good.
 
 We only apply this when we think there is a benefit in doing so however. There are a number of cases in which