[Git][ghc/ghc][wip/hnf-spec] Make exprIsHNF imply exprOkForSpeculation

Sebastian Graf (@sgraf812) gitlab at gitlab.haskell.org
Sun Oct 27 23:24:50 UTC 2024



Sebastian Graf pushed to branch wip/hnf-spec at Glasgow Haskell Compiler / GHC


Commits:
1f37d307 by Sebastian Graf at 2024-10-28T00:23:54+01:00
Make exprIsHNF imply exprOkForSpeculation

Fixes #23256 because SetLevels and CSE no longer do a reverse binder
swap.
Furthermore, we no longer need to check for exprIsHNF when
exprOkForSpeculation fails.

- - - - -


7 changed files:

- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/CSE.hs
- compiler/GHC/Core/Opt/CprAnal.hs
- compiler/GHC/Core/Opt/SetLevels.hs
- compiler/GHC/Core/Subst.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/Utils.hs


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -592,7 +592,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty
                || (isNonRec rec_flag && exprOkForSpeculation rhs)
                || isDataConWorkId binder || isDataConWrapId binder -- until #17521 is fixed
                || exprIsTickedString rhs)
-           (badBndrTyMsg binder (text "unlifted"))
+           (badUnliftedBndrTyMsg binder rhs)
 
         -- Check that if the binder is at the top level and has type Addr#,
         -- that it is a string literal.
@@ -3741,10 +3741,11 @@ mkRhsMsg binder what ty
      hsep [text "Binder's type:", ppr (idType binder)],
      hsep [text "Rhs type:", ppr ty]]
 
-badBndrTyMsg :: Id -> SDoc -> SDoc
-badBndrTyMsg binder what
-  = vcat [ text "The type of this binder is" <+> what <> colon <+> ppr binder
-         , text "Binder's type:" <+> ppr (idType binder) ]
+badUnliftedBndrTyMsg :: Id -> CoreExpr -> SDoc
+badUnliftedBndrTyMsg bndr rhs
+  = vcat [ text "The let binder" <+> ppr bndr <+> text "does not satisfy the let-can-float invariant"
+         , text "Type:" <+> ppr (idType bndr)
+         , text "RHS:" <+> ppr rhs ]
 
 mkNonTopExportedMsg :: Id -> SDoc
 mkNonTopExportedMsg binder


=====================================
compiler/GHC/Core/Opt/CSE.hs
=====================================
@@ -498,7 +498,9 @@ extendCSEnvWithBinding env in_id out_id rhs' cse_done
 
     -- Should we use SUBSTITUTE or EXTEND?
     -- See Note [CSE for bindings]
-    use_subst | Var {} <- rhs' = True
+    use_subst | Var v <- rhs'
+              , isEvaldUnfolding (idUnfolding v) == isEvaldUnfolding (idUnfolding in_id)
+              = True
               | otherwise      = False
 
 -- | Given a binder `let x = e`, this function


=====================================
compiler/GHC/Core/Opt/CprAnal.hs
=====================================
@@ -298,14 +298,8 @@ data TermFlag -- Better than using a Bool
 exprTerminates :: CoreExpr -> TermFlag
 -- ^ A /very/ simple termination analysis.
 exprTerminates e
-  | exprIsHNF e            = Terminates
   | exprOkForSpeculation e = Terminates
   | otherwise              = MightDiverge
-  -- Annoyingly, 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]


=====================================
compiler/GHC/Core/Opt/SetLevels.hs
=====================================
@@ -127,6 +127,7 @@ import GHC.Utils.Outputable
 import GHC.Utils.Panic
 
 import Data.Maybe
+import Data.Either
 
 {-
 ************************************************************************
@@ -452,14 +453,14 @@ lvlCase env scrut_fvs scrut' case_bndr ty alts
   =     -- Always float the case if possible
         -- Unlike lets we don't insist that it escapes a value lambda
     do { (env1, (case_bndr' : bs')) <- cloneCaseBndrs env dest_lvl (case_bndr : bs)
-       ; let rhs_env = extendCaseBndrEnv env1 case_bndr scrut'
+       ; let rhs_env = rememberEval env1 case_bndr' scrut'
        ; body' <- lvlMFE rhs_env True body
        ; let alt' = Alt con (map (stayPut dest_lvl) bs') body'
        ; return (Case scrut' (TB case_bndr' (FloatMe dest_lvl)) ty' [alt']) }
 
   | otherwise     -- Stays put
-  = do { let (alts_env1, [case_bndr']) = substAndLvlBndrs NonRecursive env incd_lvl [case_bndr]
-             alts_env = extendCaseBndrEnv alts_env1 case_bndr scrut'
+  = do { let (alts_env1, [case_bndr'@(TB case_bndrr _)]) = substAndLvlBndrs NonRecursive env incd_lvl [case_bndr]
+             alts_env = rememberEval alts_env1 case_bndrr scrut'
        ; alts' <- mapM (lvl_alt alts_env) alts
        ; return (Case scrut' case_bndr' ty' alts') }
   where
@@ -632,7 +633,7 @@ lvlMFE env strict_ctxt ann_expr
   |  float_is_new_lam || exprIsTopLevelBindable expr expr_ty
          -- No wrapping needed if the type is lifted, or is a literal string
          -- or if we are wrapping it in one or more value lambdas
-  = do { expr1 <- lvlFloatRhs abs_vars dest_lvl rhs_env NonRecursive
+  = do { expr1 <- lvlFloatRhs abs_vars eval_vars dest_lvl rhs_env NonRecursive
                               is_bot_lam NotJoinPoint ann_expr
                   -- Treat the expr just like a right-hand side
        ; var <- newLvlVar expr1 NotJoinPoint is_mk_static
@@ -653,6 +654,7 @@ lvlMFE env strict_ctxt ann_expr
   = do { expr1 <- lvlExpr rhs_env ann_expr
        ; let l1r       = incMinorLvlFrom rhs_env
              float_rhs = mkLams abs_vars_w_lvls $
+                         flip (foldr (wrapEval l1r)) eval_vars $
                          Case expr1 (stayPut l1r ubx_bndr) box_ty
                              [Alt DEFAULT [] (App boxing_expr (Var ubx_bndr))]
 
@@ -678,7 +680,8 @@ lvlMFE env strict_ctxt ann_expr
                            -- See Note [Bottoming floats]
                            -- esp Bottoming floats (2)
     expr_ok_for_spec = exprOkForSpeculation expr
-    abs_vars = abstractVars dest_lvl env fvs
+    (abs_vars, eval_vars) = eliminateAbsCaseBndrs dest_lvl env $
+                            abstractVars dest_lvl env fvs
     dest_lvl = destLevel env fvs fvs_ty is_function is_bot_lam
                -- NB: is_bot_lam not is_bot; see (3) in
                --     Note [Bottoming floats]
@@ -1233,7 +1236,7 @@ lvlBind env (AnnNonRec bndr rhs)
   -- Otherwise we are going to float
   | null abs_vars
   = do {  -- No type abstraction; clone existing binder
-         rhs' <- lvlFloatRhs [] dest_lvl env NonRecursive
+         rhs' <- lvlFloatRhs [] [] dest_lvl env NonRecursive
                              is_bot_lam NotJoinPoint rhs
        ; (env', [bndr']) <- cloneLetVars NonRecursive env dest_lvl [bndr]
        ; let bndr2 = annotateBotStr bndr' 0 mb_bot_str
@@ -1241,7 +1244,7 @@ lvlBind env (AnnNonRec bndr rhs)
 
   | otherwise
   = do {  -- Yes, type abstraction; create a new binder, extend substitution, etc
-         rhs' <- lvlFloatRhs abs_vars dest_lvl env NonRecursive
+         rhs' <- lvlFloatRhs abs_vars eval_vars dest_lvl env NonRecursive
                              is_bot_lam NotJoinPoint rhs
        ; (env', [bndr']) <- newPolyBndrs dest_lvl env abs_vars [bndr]
        ; let bndr2 = annotateBotStr bndr' n_extra mb_bot_str
@@ -1252,7 +1255,8 @@ lvlBind env (AnnNonRec bndr rhs)
     ty_fvs     = tyCoVarsOfType bndr_ty
     rhs_fvs    = freeVarsOf rhs
     bind_fvs   = rhs_fvs `unionDVarSet` dIdFreeVars bndr
-    abs_vars   = abstractVars dest_lvl env bind_fvs
+    (abs_vars, eval_vars) = eliminateAbsCaseBndrs dest_lvl env $
+                            abstractVars dest_lvl env bind_fvs
     dest_lvl   = destLevel env bind_fvs ty_fvs (isFunction rhs) is_bot_lam
 
     deann_rhs  = deAnnotate rhs
@@ -1332,9 +1336,8 @@ lvlBind env (AnnRec pairs)
                       -- function in a Rec, and we don't much care what
                       -- happens to it.  False is simple!
 
-    do_rhs env (_,rhs) = lvlFloatRhs abs_vars dest_lvl env Recursive
-                                     is_bot NotJoinPoint
-                                     rhs
+    do_rhs env (_,rhs) = lvlFloatRhs abs_vars eval_vars dest_lvl env Recursive
+                                     is_bot NotJoinPoint rhs
 
         -- Finding the free vars of the binding group is annoying
     bind_fvs = ((unionDVarSets [ freeVarsOf rhs | (_, rhs) <- pairs])
@@ -1346,7 +1349,8 @@ lvlBind env (AnnRec pairs)
 
     ty_fvs   = foldr (unionVarSet . tyCoVarsOfType . idType) emptyVarSet bndrs
     dest_lvl = destLevel env bind_fvs ty_fvs is_fun is_bot
-    abs_vars = abstractVars dest_lvl env bind_fvs
+    (abs_vars, eval_vars) = eliminateAbsCaseBndrs dest_lvl env $
+                            abstractVars dest_lvl env bind_fvs
 
     is_top_bindable = not (any (mightBeUnliftedType . idType) bndrs)
        -- This mightBeUnliftedType stuff is the same test as in the non-rec case
@@ -1396,21 +1400,28 @@ lvlRhs :: LevelEnv
        -> CoreExprWithFVs
        -> LvlM LevelledExpr
 lvlRhs env rec_flag is_bot mb_join_arity expr
-  = lvlFloatRhs [] (le_ctxt_lvl env) env
+  = lvlFloatRhs [] [] (le_ctxt_lvl env) env
                 rec_flag is_bot mb_join_arity expr
 
-lvlFloatRhs :: [OutVar] -> Level -> LevelEnv -> RecFlag
+wrapEval :: Level -> (OutId, OutId) -> Expr LevelledBndr -> Expr LevelledBndr
+-- A bit like GHC.Core.Utils.mkDefaultCase, but `Expr LevelledBndr`
+wrapEval dest_lvl (scrut_v, case_bndr) body
+  = Case (Var scrut_v) (TB case_bndr (StayPut dest_lvl))
+         (exprType $ deTagExpr body) [Alt DEFAULT [] body]
+
+lvlFloatRhs :: [OutVar] -> [(OutId,OutId)] -> Level -> LevelEnv -> RecFlag
             -> Bool   -- Binding is for a bottoming function
             -> JoinPointHood
             -> CoreExprWithFVs
             -> LvlM (Expr LevelledBndr)
 -- Ignores the le_ctxt_lvl in env; treats dest_lvl as the baseline
-lvlFloatRhs abs_vars dest_lvl env rec is_bot mb_join_arity rhs
-  = do { body' <- if not is_bot  -- See Note [Floating from a RHS]
+lvlFloatRhs abs_vars eval_vars dest_lvl env rec is_bot mb_join_arity rhs
+  = do { body1 <- if not is_bot  -- See Note [Floating from a RHS]
                      && any isId bndrs
                   then lvlMFE  body_env True body
                   else lvlExpr body_env      body
-       ; return (mkLams bndrs' body') }
+       ; let body2 = foldr (wrapEval dest_lvl) body1 eval_vars
+       ; return (mkLams bndrs' body2) }
   where
     (bndrs, body)     | JoinPoint join_arity <- mb_join_arity
                       = collectNAnnBndrs join_arity rhs
@@ -1633,14 +1644,20 @@ countFreeIds = nonDetStrictFoldUDFM add 0 . getUniqDSet
 
 data LevelEnv
   = LE { le_switches :: FloatOutSwitches
-       , le_ctxt_lvl :: Level           -- The current level
-       , le_lvl_env  :: VarEnv Level    -- Domain is *post-cloned* TyVars and Ids
+       , le_ctxt_lvl :: Level
+       -- ^ The current level
+       , le_lvl_env  :: VarEnv (Level, Maybe OutId)
+       -- ^ Domain is *post-cloned* TyVars and Ids.
+       -- If `Just scrut`, then the var mapping belongs to a case binder with
+       -- variable scrutinee `scrut`.
+       -- This is to support Note [Duplicate evals into float].
 
        -- See Note [le_subst and le_env]
-       , le_subst    :: Subst           -- Domain is pre-cloned TyVars and Ids
-                                        -- The Id -> CoreExpr in the Subst is ignored
-                                        -- (since we want to substitute a LevelledExpr for
-                                        -- an Id via le_env) but we do use the Co/TyVar substs
+       , le_subst    :: Subst
+       -- ^ Domain is pre-cloned TyVars and Ids.
+       -- The Id -> CoreExpr in the Subst is ignored
+       -- (since we want to substitute a LevelledExpr for
+       -- an Id via le_env) but we do use the Co/TyVar substs
        , le_env      :: IdEnv ([OutVar], LevelledExpr)  -- Domain is pre-cloned Ids
     }
 
@@ -1690,10 +1707,10 @@ initialEnv float_lams binds
       -- to a later one.  So here we put all the top-level binders in scope before
       -- we start, to satisfy the lookupIdSubst invariants (#20200 and #20294)
 
-addLvl :: Level -> VarEnv Level -> OutVar -> VarEnv Level
-addLvl dest_lvl env v' = extendVarEnv env v' dest_lvl
+addLvl :: Level -> VarEnv (Level, Maybe OutId) -> OutVar -> VarEnv (Level, Maybe OutId)
+addLvl dest_lvl env v' = extendVarEnv env v' (dest_lvl, Nothing)
 
-addLvls :: Level -> VarEnv Level -> [OutVar] -> VarEnv Level
+addLvls :: Level -> VarEnv (Level, Maybe OutId) -> [OutVar] -> VarEnv (Level, Maybe OutId)
 addLvls dest_lvl env vs = foldl' (addLvl dest_lvl) env vs
 
 floatLams :: LevelEnv -> Maybe Int
@@ -1711,20 +1728,19 @@ floatTopLvlOnly le = floatToTopLevelOnly (le_switches le)
 incMinorLvlFrom :: LevelEnv -> Level
 incMinorLvlFrom env = incMinorLvl (le_ctxt_lvl env)
 
--- extendCaseBndrEnv adds the mapping case-bndr->scrut-var if it can
+-- rememberEval adds the mapping case-bndr->scrut-var if it can
 -- See Note [Binder-swap during float-out]
-extendCaseBndrEnv :: LevelEnv
-                  -> Id                 -- Pre-cloned case binder
-                  -> Expr LevelledBndr  -- Post-cloned scrutinee
-                  -> LevelEnv
-extendCaseBndrEnv le@(LE { le_subst = subst, le_env = id_env })
+rememberEval :: LevelEnv
+             -> OutId              -- Post-cloned case binder
+             -> Expr LevelledBndr  -- Post-cloned scrutinee
+             -> LevelEnv
+rememberEval le@(LE { le_lvl_env = lvl_env })
                   case_bndr (Var scrut_var)
   -- We could use OccurAnal. scrutOkForBinderSwap here, and perhaps
   -- get a bit more floating.  But we didn't in the past and it's
   -- an unforced change, so I'm leaving it.
-  = le { le_subst   = extendSubstWithVar subst case_bndr scrut_var
-       , le_env     = add_id id_env (case_bndr, scrut_var) }
-extendCaseBndrEnv env _ _ = env
+  = le { le_lvl_env = modifyVarEnv (\(lvl,_) -> (lvl, Just scrut_var)) lvl_env case_bndr }
+rememberEval env _ _ = env
 
 maxFvLevel :: (Var -> Bool) -> LevelEnv -> DVarSet -> Level
 maxFvLevel max_me env var_set
@@ -1745,8 +1761,8 @@ maxIn max_me (LE { le_lvl_env = lvl_env, le_env = id_env }) in_var lvl
   where
     max_out out_var lvl
         | max_me out_var = case lookupVarEnv lvl_env out_var of
-                                Just lvl' -> maxLvl lvl' lvl
-                                Nothing   -> lvl
+                                Just (lvl',_) -> maxLvl lvl' lvl
+                                Nothing       -> lvl
         | otherwise = lvl       -- Ignore some vars depending on max_me
 
 lookupVar :: LevelEnv -> Id -> LevelledExpr
@@ -1765,20 +1781,16 @@ abstractVars :: Level -> LevelEnv -> DVarSet -> [OutVar]
         -- variable computation and deterministic sort.
         -- See Note [Unique Determinism] in GHC.Types.Unique for explanation of why
         -- Uniques are not deterministic.
-abstractVars dest_lvl (LE { le_subst = subst, le_lvl_env = lvl_env }) in_fvs
+abstractVars dest_lvl le@(LE { le_subst = subst }) in_fvs
   =  -- NB: sortQuantVars might not put duplicates next to each other
-    map zap $ sortQuantVars $
-    filter abstract_me      $
-    dVarSetElems            $
-    closeOverKindsDSet      $
+    map zap $ sortQuantVars         $
+    filter (abstractMe dest_lvl le) $
+    dVarSetElems                    $
+    closeOverKindsDSet              $
     substDVarSet subst in_fvs
         -- NB: it's important to call abstract_me only on the OutIds the
         -- come from substDVarSet (not on fv, which is an InId)
   where
-    abstract_me v = case lookupVarEnv lvl_env v of
-                        Just lvl -> dest_lvl `ltLvl` lvl
-                        Nothing  -> False
-
         -- We are going to lambda-abstract, so nuke any IdInfo,
         -- and add the tyvars of the Id (if necessary)
     zap v | isId v = warnPprTrace (isStableUnfolding (idUnfolding v) ||
@@ -1787,6 +1799,23 @@ abstractVars dest_lvl (LE { le_subst = subst, le_lvl_env = lvl_env }) in_fvs
                      setIdInfo v vanillaIdInfo
           | otherwise = v
 
+abstractMe :: Level -> LevelEnv -> Var -> Bool
+abstractMe dest_lvl (LE { le_lvl_env = lvl_env }) v
+  | Just (lvl, _) <- lookupVarEnv lvl_env v
+  = dest_lvl `ltLvl` lvl
+  | otherwise
+  = False
+
+eliminateAbsCaseBndrs :: Level -> LevelEnv -> [OutVar] -> ([OutVar], [(OutId,OutId)])
+eliminateAbsCaseBndrs dest_lvl le@(LE { le_lvl_env = lvl_env })
+  = partitionEithers . map try_elim
+  where
+    try_elim v = case lookupVarEnv lvl_env v of
+      Just (_, Just scrut_id)
+        | not (abstractMe dest_lvl le scrut_id) -- would not abstract scrut_id
+        -> Right (scrut_id, v) -- turn abs_var v into an eval on scrut_id!
+      _ -> Left v              -- retain as an abs_var
+
 type LvlM result = UniqSM result
 
 initLvl :: UniqSupply -> UniqSM a -> a
@@ -1835,9 +1864,12 @@ newLvlVar :: LevelledExpr        -- The RHS of the new binding
           -> LvlM Id
 newLvlVar lvld_rhs join_arity_maybe is_mk_static
   = do { uniq <- getUniqueM
-       ; return (add_join_info (mk_id uniq rhs_ty))
+       ; return (add_evald $ add_join_info $ mk_id uniq rhs_ty)
        }
   where
+    add_evald var
+      | exprIsHNF de_tagged_rhs = var `setIdUnfolding` evaldUnfolding
+      | otherwise               = var
     add_join_info var = var `asJoinId_maybe` join_arity_maybe
     de_tagged_rhs = deTagExpr lvld_rhs
     rhs_ty        = exprType de_tagged_rhs


=====================================
compiler/GHC/Core/Subst.hs
=====================================
@@ -519,7 +519,9 @@ substUnfolding subst df@(DFunUnfolding { df_bndrs = bndrs, df_args = args })
 substUnfolding subst unf@(CoreUnfolding { uf_tmpl = tmpl, uf_src = src })
   -- Retain stable unfoldings
   | not (isStableSource src)  -- Zap an unstable unfolding, to save substitution work
-  = NoUnfolding
+  = if isEvaldUnfolding unf
+    then evaldUnfolding
+    else NoUnfolding
   | otherwise                 -- But keep a stable one!
   = seqExpr new_tmpl `seq`
     unf { uf_tmpl = new_tmpl }


=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -22,6 +22,7 @@ module GHC.Core.TyCo.Subst
         extendCvSubst, extendCvSubstWithClone,
         extendTvSubst, extendTvSubstWithClone,
         extendTvSubstList, extendTvSubstAndInScope,
+        extendCvSubstAndInScope,
         extendTCvSubstList,
         unionSubst, zipTyEnv, zipCoEnv,
         zipTvSubst, zipCvSubst,
@@ -408,6 +409,14 @@ extendTvSubstAndInScope (Subst in_scope ids tenv cenv) tv ty
              (extendVarEnv tenv tv ty)
              cenv
 
+extendCvSubstAndInScope :: Subst -> CoVar -> Coercion -> Subst
+-- Also extends the in-scope set
+extendCvSubstAndInScope (Subst in_scope ids tenv cenv) cv co
+  = Subst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co)
+             ids
+             tenv
+             (extendVarEnv cenv cv co)
+
 -- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTvSubst'
 extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst
 extendTvSubstList subst vrs


=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -74,9 +74,11 @@ import GHC.Core.Ppr
 import GHC.Core.FVs( bindFreeVars )
 import GHC.Core.DataCon
 import GHC.Core.Type as Type
+import GHC.Core.TyCo.Rep as Type
 import GHC.Core.Predicate( isCoVarType )
 import GHC.Core.FamInstEnv
 import GHC.Core.TyCo.Compare( eqType, eqTypeX )
+import GHC.Core.TyCo.Subst
 import GHC.Core.Coercion
 import GHC.Core.Reduction
 import GHC.Core.TyCon
@@ -1814,11 +1816,9 @@ expr_ok fun_ok primop_ok (Tick tickish e)
 expr_ok _ _ (Let {}) = False
 -- See W3 in the Haddock comment for exprOkForSpeculation
 
-expr_ok fun_ok primop_ok (Case scrut bndr _ alts)
+expr_ok fun_ok primop_ok (Case scrut _ _ alts)
   =  -- See Note [exprOkForSpeculation: case expressions]
      expr_ok fun_ok primop_ok scrut
-  && isUnliftedType (idType bndr)
-      -- OK to call isUnliftedType: binders always have a fixed RuntimeRep
   && all (\(Alt _ _ rhs) -> expr_ok fun_ok primop_ok rhs) alts
   && altsAreExhaustive alts
 
@@ -1847,7 +1847,7 @@ app_ok fun_ok primop_ok fun args
 
   | idArity fun > n_val_args
   -- Partial application: just check passing the arguments is OK
-  = args_ok
+  = args_ok notCBV
 
   | otherwise
   = case idDetails fun of
@@ -1857,9 +1857,10 @@ app_ok fun_ok primop_ok fun args
 
       DataConWorkId dc
         | isLazyDataConRep dc
-        -> args_ok
+        -> args_ok notCBV
         | otherwise
-        -> fields_ok (dataConRepStrictness dc)
+        -> args_ok (dataConRepStrictness dc)
+            -- See (SFC1) of Note [Strict fields in Core]
 
       ClassOpId _ is_terminating_result
         | is_terminating_result -- See Note [exprOkForSpeculation and type classes]
@@ -1881,7 +1882,7 @@ app_ok fun_ok primop_ok fun args
               -- Often there is a literal divisor, and this
               -- can get rid of a thunk in an inner loop
 
-        | otherwise -> primop_ok op && args_ok
+        | otherwise -> primop_ok op && args_ok notCBV
 
       _other  -- Unlifted and terminating types;
               -- Also c.f. the Var case of exprIsHNF
@@ -1898,37 +1899,54 @@ app_ok fun_ok primop_ok fun args
          -- See (U12) of Note [Implementing unsafeCoerce]
          | fun `hasKey` unsafeEqualityProofIdKey -> True
 
-         | otherwise -> False
-             -- NB: even in the nullary case, do /not/ check
-             --     for evaluated-ness of the fun;
-             --     see Note [exprOkForSpeculation and evaluated variables]
+         | 0 <- n_val_args
+         , isEvaldUnfolding (idUnfolding fun)
+         -> -- pprTrace "yes" (ppr fun)
+            True
+
+         | otherwise -> -- pprTrace "no" (ppr fun <+> ppr args)
+                        False
   where
     fun_ty       = idType fun
     n_val_args   = valArgCount args
-    (arg_tys, _) = splitPiTys fun_ty
 
     -- Even if a function call itself is OK, any unlifted
-    -- args are still evaluated eagerly and must be checked
-    args_ok = all2Prefix arg_ok arg_tys args
-    arg_ok :: PiTyVarBinder -> CoreExpr -> Bool
-    arg_ok (Named _) _ = True   -- A type argument
-    arg_ok (Anon ty _) arg      -- A term argument
-       | definitelyLiftedType (scaledThing ty)
-       = True -- lifted args are not evaluated eagerly
+    -- args are still evaluated eagerly and must be checked.
+    -- Furthermore, for saturated calls, we must check CBV args (strict fields
+    -- of DataCons!)
+    args_ok str_marks = relevantAppArgsSatisfy arg_ok fun_ty args str_marks
+    arg_ok :: Type -> CoreExpr -> StrictnessMark -> Bool
+    arg_ok ty arg str
+       | NotMarkedStrict <- str   -- iff it's not a CBV arg
+       , definitelyLiftedType ty  -- and its type is lifted
+       = True                     -- then the worker app does not eval
        | otherwise
        = expr_ok fun_ok primop_ok arg
 
-    -- Used for strict DataCon worker arguments
-    -- See (SFC1) of Note [Strict fields in Core]
-    fields_ok str_marks = all3Prefix field_ok arg_tys str_marks args
-    field_ok :: PiTyVarBinder -> StrictnessMark -> CoreExpr -> Bool
-    field_ok (Named _)   _   _ = True
-    field_ok (Anon ty _) str arg
-       | NotMarkedStrict <- str                 -- iff it's a lazy field
-       , definitelyLiftedType (scaledThing ty)  -- and its type is lifted
-       = True                                   -- then the worker app does not eval
-       | otherwise
-       = expr_ok fun_ok primop_ok arg
+notCBV :: [StrictnessMark]
+notCBV = repeat NotMarkedStrict
+
+relevantAppArgsSatisfy :: (Type -> CoreExpr -> StrictnessMark -> Bool) -> Type -> [CoreExpr] -> [StrictnessMark] -> Bool
+-- This calls the predicate on every non-Type CoreExpr arg.
+-- We could just do `exprType arg` for every such arg, but carrying around a
+-- substitution is much more efficient.
+-- The obvious definition regresses T16577 by 30% so we don't do it.
+relevantAppArgsSatisfy p ty = go (mkEmptySubst in_scope) ty
+  where
+    in_scope = mkInScopeSet (tyCoVarsOfType ty)
+    go subst (ForAllTy b res) (Type ty : args) strs
+      = go (extendTvSubstAndInScope subst (binderVar b) ty) res args strs
+    go subst (ForAllTy b res) (Coercion co : args) strs
+      = go (extendCvSubstAndInScope subst (binderVar b) co) res args strs
+    go subst (FunTy { ft_arg = arg, ft_res = res }) (e : args) (str : strs)
+      = p (substTy subst arg) e str && go subst res args strs
+    go subst ty args@(_:_) strs@(_:_)
+      | Just ty' <- coreView (substTy subst ty)
+      = go (mkEmptySubst (getSubstInScope subst)) ty' args strs
+      | otherwise
+      = pprPanic "Should see more argument tys" (ppr ty $$ ppr subst $$ ppr args $$ ppr (take 10 strs))
+    go _ _ _ _ = True
+{-# INLINE relevantAppArgsSatisfy #-}
 
 -----------------------------
 altsAreExhaustive :: [Alt b] -> Bool
@@ -1985,6 +2003,8 @@ GHC.Types.Id.Make.mkDictSelId for where this field is initialised.
 
 Note [exprOkForSpeculation: case expressions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+SG: I don't get what is so "very special" about this case. I find it very reasonable.
+
 exprOkForSpeculation accepts very special case expressions.
 Reason: (a ==# b) is ok-for-speculation, but the litEq rules
 in GHC.Core.Opt.ConstantFold convert it (a ==# 3#) to
@@ -1994,39 +2014,22 @@ for excellent reasons described in
 So, annoyingly, we want that case expression to be
 ok-for-speculation too. Bother.
 
-But we restrict it sharply:
-
-* We restrict it to unlifted scrutinees. Consider this:
-     case x of y {
-       DEFAULT -> ... (let v::Int# = case y of { True  -> e1
-                                               ; False -> e2 }
-                       in ...) ...
-
-  Does the RHS of v satisfy the let-can-float invariant?  Previously we said
-  yes, on the grounds that y is evaluated.  But the binder-swap done
-  by GHC.Core.Opt.SetLevels would transform the inner alternative to
-     DEFAULT -> ... (let v::Int# = case x of { ... }
-                     in ...) ....
-  which does /not/ satisfy the let-can-float invariant, because x is
-  not evaluated. See Note [Binder-swap during float-out]
-  in GHC.Core.Opt.SetLevels.  To avoid this awkwardness it seems simpler
-  to stick to unlifted scrutinees where the issue does not
-  arise.
-
-* We restrict it to exhaustive alternatives. A non-exhaustive
-  case manifestly isn't ok-for-speculation. for example,
-  this is a valid program (albeit a slightly dodgy one)
-    let v = case x of { B -> ...; C -> ... }
-    in case x of
-         A -> ...
-         _ ->  ...v...v....
-  Should v be considered ok-for-speculation?  Its scrutinee may be
-  evaluated, but the alternatives are incomplete so we should not
-  evaluate it strictly.
-
-  Now, all this is for lifted types, but it'd be the same for any
-  finite unlifted type. We don't have many of them, but we might
-  add unlifted algebraic types in due course.
+SG: Again, I don't see why we need to list a specific example.
+Clearly, we want to detect as many expressions as ok-for-spec as possible!
+
+But we restrict it to exhaustive alternatives. A non-exhaustive
+case manifestly isn't ok-for-speculation. For example,
+this is a valid program (albeit a slightly dodgy one)
+  let v = case x of { B -> ...; C -> ... }
+  in case x of
+       A -> ...
+       _ ->  ...v...v....
+Should v be considered ok-for-speculation?  Its scrutinee may be
+evaluated, but the alternatives are incomplete so we should not
+evaluate it strictly.
+
+Now, all this is for lifted types, but it'd be the same for any
+finite unlifted type.
 
 
 ----- Historical note: #15696: --------
@@ -2073,37 +2076,6 @@ points do the job nicely.
 ------- End of historical note ------------
 
 
-Note [exprOkForSpeculation and evaluated variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider these examples:
- * case x of y { DEFAULT -> ....y.... }
-   Should 'y' (alone) be considered ok-for-speculation?
-
- * case x of y { DEFAULT -> ....let z = dataToTagLarge# y... }
-   Should (dataToTagLarge# y) be considered ok-for-spec? Recall that
-     dataToTagLarge# :: forall a. a -> Int#
-   must always evaluate its argument. (See also Note [DataToTag overview].)
-
-You could argue 'yes', because in the case alternative we know that
-'y' is evaluated.  But the binder-swap transformation, which is
-extremely useful for float-out, changes these expressions to
-   case x of y { DEFAULT -> ....x.... }
-   case x of y { DEFAULT -> ....let z = dataToTagLarge# x... }
-
-And now the expression does not obey the let-can-float invariant!  Yikes!
-Moreover we really might float (dataToTagLarge# x) outside the case,
-and then it really, really doesn't obey the let-can-float invariant.
-
-The solution is simple: exprOkForSpeculation does not try to take
-advantage of the evaluated-ness of (lifted) variables.  And it returns
-False (always) for primops that perform evaluation.  We achieve the latter
-by marking the relevant primops as "ThrowsException" or
-"ReadWriteEffect"; see also Note [Classifying primop effects] in
-GHC.Builtin.PrimOps.
-
-Note that exprIsHNF /can/ and does take advantage of evaluated-ness;
-it doesn't have the trickiness of the let-can-float invariant to worry about.
-
 ************************************************************************
 *                                                                      *
              exprIsHNF, exprIsConLike
@@ -2185,66 +2157,59 @@ exprIsHNFlike is_con is_con_unf e
                                    && is_hnf_like e
                                       -- 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 [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 (Case e b _ as)
       | Just rhs <- isUnsafeEqualityCase e b as
       = is_hnf_like rhs
-    is_hnf_like _                = False
-
-    -- 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 =
+    is_hnf_like e
+      | (fun, args) <- collectArgs e
+      = case stripTicksTopE (not . tickishCounts) fun of
+            Var f -> id_app_is_value f 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).
+            -- See Note [How a rubbish literal can be the head of an application]
+            -- in GHC.Types.Literal
+            Lit lit | debugIsOn, not (isLitRubbish lit)
+                     -> pprPanic "Non-rubbish lit in app head" (ppr lit)
+                     | otherwise
+                     -> True
+
+            _ -> False
+
+    id_app_is_value id args =
       -- See Note [exprIsHNF for function applications]
       --   for the specification and examples
-      case compare (idArity id) (length val_args) of
+      case compare (idArity id) n_val_args of
         EQ | is_con id ->      -- Saturated app of a DataCon/CONLIKE Id
           case mb_str_marks id of
             Just str_marks ->  -- with strict fields; see (SFC1) of Note [Strict fields in Core]
-              assert (val_args `equalLength` str_marks) $
-              fields_hnf str_marks
+              args_hnf str_marks
             Nothing ->         -- without strict fields: like PAP
-              args_hnf         -- NB: CONLIKEs are lazy!
+              args_hnf notCBV  -- NB: CONLIKEs are lazy!
 
-        GT ->                  -- PAP: Check unlifted val_args
-          args_hnf
+        GT ->                  -- PAP: Check unlifted args
+          args_hnf notCBV
 
         _  -> False
 
       where
-        -- Saturated, Strict DataCon: Check unlifted val_args and strict fields
-        fields_hnf str_marks = all3Prefix check_field val_arg_tys str_marks val_args
-
-        -- PAP: Check unlifted val_args
-        args_hnf             = all2Prefix check_arg   val_arg_tys           val_args
-
         fun_ty = idType id
-        val_arg_tys = mapMaybe anonPiTyBinderType_maybe (collectPiTyBinders fun_ty)
-          -- 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
+        n_val_args   = valArgCount args
+        -- Check the args for HNFness.
+        args_hnf str_marks = relevantAppArgsSatisfy check_arg fun_ty args str_marks
+        --   * Unlifted args must always be HNF
+        --   * CBV args (strict fields!) must be HNF for saturated calls,
+        --     indicated by str_marks
+        check_arg a_ty a str
           | mightBeUnliftedType a_ty = is_hnf_like a
+          | isMarkedStrict str       = is_hnf_like a
           | otherwise                = True
          -- 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 a_ty str a
-          | mightBeUnliftedType a_ty = is_hnf_like a
-          | isMarkedStrict str       = is_hnf_like a
-          | otherwise                = True
-          -- isMarkedStrict: Respect Note [Strict fields in Core]
 
         mb_str_marks id
           | Just dc <- isDataConWorkId_maybe id



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1f37d307ca17c6cd1e680fb569fbb714fecf6070

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1f37d307ca17c6cd1e680fb569fbb714fecf6070
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20241027/baddfae1/attachment-0001.html>


More information about the ghc-commits mailing list