[Git][ghc/ghc][wip/spj-try-opt-coercion] Comments -- almost all just about core invariants [skip ci]

Simon Peyton Jones pushed to branch wip/spj-try-opt-coercion at Glasgow Haskell Compiler / GHC Commits: 2b2ee165 by Simon Peyton Jones at 2026-01-12T17:31:42+00:00 Comments -- almost all just about core invariants [skip ci] - - - - - 18 changed files: - compiler/GHC/Builtin/PrimOps.hs - compiler/GHC/Core.hs - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Make.hs - compiler/GHC/Core/Opt/CSE.hs - compiler/GHC/Core/Opt/ConstantFold.hs - compiler/GHC/Core/Opt/FloatIn.hs - compiler/GHC/Core/Opt/SetLevels.hs - compiler/GHC/Core/Opt/Simplify/Env.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/Opt/Simplify/Utils.hs - compiler/GHC/Core/Opt/Specialise.hs - compiler/GHC/Core/SimpleOpt.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/Utils.hs - compiler/GHC/Stg/Lint.hs Changes: ===================================== compiler/GHC/Builtin/PrimOps.hs ===================================== @@ -435,12 +435,12 @@ follows, in decreasing order of permissiveness: NoEffect, we may float such an invalid call out of a dead branch and speculatively evaluate it. - In particular, we cannot safely rewrite such an invalid call to a - runtime error; we must emit code that produces a valid Word32#. - (If we're lucky, Core Lint may complain that the result of such a - rewrite violates the let-can-float invariant (#16742), but the - rewrite is always wrong!) See also Note [Guarding against silly shifts] - in GHC.Core.Opt.ConstantFold. + In particular, we cannot safely rewrite such an invalid call to a runtime + error; we must emit code that produces a valid Word32#. (If we're lucky, + Core Lint may complain that the result of such a rewrite violates + Note [Core binding invariants: nested non-rec] (#16742), but the rewrite + is always wrong!) See also Note [Guarding against silly shifts] in + GHC.Core.Opt.ConstantFold. Marking uncheckedShiftLWord32# as CanFail instead of NoEffect would give us the freedom to rewrite such invalid calls to runtime @@ -578,12 +578,12 @@ Several predicates on primops test this flag: where it is guarded by exprOkToDiscard, which in turn checks primOpOkToDiscard. - * The "no-float-out" thing is achieved by ensuring that we never - let-bind a saturated primop application unless it has NoEffect. - The RHS of a let-binding (which can float in and out freely) - satisfies exprOkForSpeculation; this is the let-can-float - invariant. And exprOkForSpeculation is false of a saturated - primop application unless it has NoEffect. + * The "no-float-out" thing is achieved by ensuring that we never let-bind a + saturated primop application unless it has NoEffect. The RHS of a + let-binding (which can float in and out freely) satisfies + exprOkForSpeculation; this is Note [Core binding invariants: nested non-rec]. + And exprOkForSpeculation is false of a saturated primop application unless it + has NoEffect. * So primops that aren't NoEffect will appear only as the scrutinees of cases, and that's why the FloatIn pass is capable ===================================== compiler/GHC/Core.hs ===================================== @@ -188,8 +188,7 @@ These data types are the heart of the compiler -- this corresponds to allocating a thunk for the things -- bound and then executing the sub-expression. -- --- See Note [Core letrec invariant] --- See Note [Core let-can-float invariant] +-- See Note [Core binding invariants] -- See Note [Representation polymorphism invariants] -- See Note [Core type and coercion invariant] -- @@ -393,25 +392,37 @@ extremely difficult to GUARANTEE it: * See Note [Shadowing in SpecConstr] in GHC.Core.Opt.SpecContr -Note [Core letrec invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The Core letrec invariant: +Note [Core binding invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A core binding, `CoreBind`, obeys these invariants: - The right hand sides of all /top-level/ or /recursive/ - bindings must be of lifted type +* For /top level/ or /recursive/ bindings, + see Note [Top-level binding invariants] -See "Type#type_classification" in GHC.Core.Type -for the meaning of "lifted" vs. "unlifted". +* For /nested/ (not top-level) /non-recursive/ bindings, + see Note [Nested binding invariants] + +Note [Top-level binding invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A /top-level/ or /recursive/ binding must -For the non-top-level, non-recursive case see -Note [Core let-can-float invariant]. + * be of lifted type +OR + * have a RHS that is a primitive string literal + (see Note [Core top-level string literals], or +OR + * have a rhs that is (Coercion co) +OR + * be a worker or wrapper for an unlifted non-newtype data constructor; see (TL1). -At top level, however, there are two exceptions to this rule: +For the non-top-level, non-recursive case see Note [Nested binding invariants]. +(NB: this Note applies to recursive as well as top-level bindings, but I wanted +a short title!) -(TL1) A top-level binding is allowed to bind primitive string literal, - (which is unlifted). See Note [Core top-level string literals]. +See "Type#type_classification" in GHC.Core.Type +for the meaning of "lifted" vs. "unlifted". -(TL2) In Core, we generate a top-level binding for every non-newtype data +(TL1) In Core, we generate a top-level binding for every non-newtype data constructor worker or wrapper e.g. data T = MkT Int we generate @@ -428,16 +439,17 @@ constructor worker or wrapper S1 = S1 We allow this top-level unlifted binding to exist. -Note [Core let-can-float invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The let-can-float invariant: - - The right hand side of a /non-top-level/, /non-recursive/ binding - may be of unlifted type, but only if - the expression is ok-for-speculation - or the 'Let' is for a join point. +Note [Nested binding invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A /non-top-level/, /non-recursive/ binding must + * Be a join point; see Note [Invariants on join points] +OR + * Be of lifted type +OR + * Have a RHS that is ok-for-speculation - (For top-level or recursive lets see Note [Core letrec invariant].) +NB: this only applies to /non-recursive/ bindings. For recursive +(or top-level) bindings see Note [Top-level binding invariants]. This means that the let can be floated around without difficulty. For example, this is OK: @@ -454,14 +466,14 @@ In this situation you should use @case@ rather than a @let@. The function alternatively use 'GHC.Core.Make.mkCoreLet' rather than this constructor directly, which will generate a @case@ if necessary -The let-can-float invariant is initially enforced by mkCoreLet in GHC.Core.Make. +The Core binding invariants are initially enforced by mkCoreLet in GHC.Core.Make. Historical Note [The let/app invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Before 2022 GHC used the "let/app invariant", which applied the let-can-float rules -to the argument of an application, as well as to the RHS of a let. This made some -kind of sense, because 'let' can always be encoded as application: - let x=rhs in b = (\x.b) rhs +Before 2022 GHC used the "let/app invariant", which applied +Note [Nested binding invariants] to the argument of an application, +as well as to the RHS of a let. This made some kind of sense, because 'let' can +always be encoded as application: let x=rhs in b = (\x.b) rhs But the let/app invariant got in the way of RULES; see #19313. For example up :: Int# -> Int# @@ -472,7 +484,7 @@ Indeed RULES is a big reason that GHC doesn't use ANF, where the argument of an application is always a variable or a constant. To allow RULES to work nicely we need to allow lots of things in the arguments of a call. -TL;DR: we relaxed the let/app invariant to become the let-can-float invariant. +TL;DR: we relaxed the let/app invariant to focus just on /bindings/. Note [Core top-level string literals] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -631,13 +643,33 @@ checked by Core Lint. Note [Core type and coercion invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We allow a /non-recursive/, /non-top-level/ let to bind type and -coercion variables. These can be very convenient for postponing type -substitutions until the next run of the simplifier. +We allow `let` to bind type and coercion variables. + +* A type or coercion binding is always /non-recursive/ + +* A type binding cannot be top level (yet) but a coercion binding + can be top-level. * A type variable binding must have a RHS of (Type ty) * A coercion variable binding must have a RHS of (Coercion co) + See Note [Coercion bindings] + + +Note [Coercion bindings] +~~~~~~~~~~~~~~~~~~~~~~~~ +We allow non-recursive let-bindings for coercion variables, CoVars, +of type (t1 ~r# t2). + +The /main motivation/ is to support sharing: + let g::T a ~# b + g = Coercion Expr b mkDoubleLit d = Lit (mkLitDouble d) mkDoubleLitDouble d = Lit (mkLitDouble (toRational d)) --- | Bind all supplied binding groups over an expression in a nested let expression. Assumes --- that the rhs satisfies the let-can-float invariant. Prefer to use +-- | Bind all supplied binding groups over an expression in a nested let expression. +-- Assumes that the rhs satisfies Note [Nested binding invariants]. Prefer to use -- 'GHC.Core.Make.mkCoreLets' if possible, which does guarantee the invariant mkLets :: [Bind b] -> Expr b -> Expr b -- | Bind all supplied binders over an expression in a nested lambda expression. Prefer to ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -46,7 +46,7 @@ Note [Coercion optimisation] This module does coercion optimisation. The purpose is to reduce the size of the coercions that the compiler carries around -- they are just proofs, and serve no runtime need. So the purpose of coercion optimisation is simply -to shrink coercions and thereby reduce compile time. +to shrink coercions and thereby reduce compile time and .hi file sizes. See the paper Evidence normalization in Systtem FV (RTA'13) @@ -57,7 +57,7 @@ However, although powerful and occasionally very effective, coercion optimisation can itself be very expensive (#26679). So we apply it sparingly: * In the Simplifier, function `rebuild_go`, we use `isReflexiveCo` (which - computes the type of the coercion) to eliminate reflexive coercion, just + computes the type of the coercion) to eliminate reflexive coercions, just before we build a cast (e |> co). (More precisely, we use `isReflexiveCoIgnoringMultiplicity; @@ -196,6 +196,10 @@ We use the following invariants: %********************************************************************* -} optCoProgram :: CoreProgram -> CoreProgram +-- Apply optCoercion to all coercions in /expressions/ +-- There may also be coercions in /types/ but we `optCoProgram` doesn't +-- look at them; they are typically fewer and smaller, and it doesn't seem +-- worth the cost of traversing and rebuilding all the types in the program. optCoProgram binds = map go binds where @@ -237,7 +241,24 @@ optCoAlt is (Alt k bs e) %* * %********************************************************************* -} +{- Note [optCoRefl] +~~~~~~~~~~~~~~~~~~~~ +`optCoRefl` is an experimental cheap-and-cheerful version of `optCoercion`. + +* It focuses entirely on chains of TransCo, thus + co1 ; co2 ; co3 ; ... ; con + +* It looks for sub-sequences in this chain that are Refl, based on their + types. The clever business is all in `gobble`, which springs into action + when we find a `TransCo`. + +* It can sometimes do a bit more than `optCoercion`. It'll eliminate /any/ + subsequence of co1..con that is reflexive, whereas `optCoercion` just works + left-to-right, and won't spot (co1 ; co2 ; sym co2) +-} + optCoRefl :: Coercion -> Coercion +-- See Note [optCoRefl] optCoRefl in_co #ifdef DEBUG -- Debug check that optCoRefl doesn't change the type ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -586,8 +586,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty ; checkL (not (isCoVar binder) || isCoArg rhs) (mkLetErr binder rhs) - -- Check the let-can-float invariant - -- See Note [Core let-can-float invariant] in GHC.Core + -- Check Note [Core binding invariants] in GHC.Core ; checkL (bindingIsOk top_lvl rec_flag binder binder_ty rhs) $ mkLetErr binder rhs @@ -647,6 +646,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty -- the unfolding is a SimplifiableCoreExpr. Give up for now. bindingIsOk :: TopLevelFlag -> RecFlag -> OutId -> OutType -> CoreExpr -> Bool +-- Checks the invariants of Note [Core binding invariants] in GHC.Core bindingIsOk top_lvl rec_flag binder binder_ty rhs | isCoVar binder = isCoArg rhs ===================================== compiler/GHC/Core/Make.hs ===================================== @@ -112,8 +112,9 @@ sortQuantVars vs = sorted_tcvs ++ ids -- | Bind a binding group over an expression, using a @let@ or @case@ as -- appropriate (see "GHC.Core#let_can_float_invariant") mkCoreLet :: HasDebugCallStack => CoreBind -> CoreExpr -> CoreExpr -mkCoreLet (NonRec bndr rhs) body -- See Note [Core let-can-float invariant] - = bindNonRec bndr rhs body +mkCoreLet (NonRec bndr rhs) body + = -- See Note [Core binding invariants: nested non-rec] + bindNonRec bndr rhs body mkCoreLet bind body = Let bind body ===================================== compiler/GHC/Core/Opt/CSE.hs ===================================== @@ -288,8 +288,8 @@ all trivial expressions. Consider case x |> co of (y::Array# Int) { ... } We do not want to extend the substitution with (y -> x |> co); since y -is of unlifted type, this would destroy the let-can-float invariant if -(x |> co) was not ok-for-speculation. +is of unlifted type, this would destroy Note [Nested binding invariants] +if (x |> co) was not ok-for-speculation. But surely (x |> co) is ok-for-speculation, because it's a trivial expression, and x's type is also unlifted, presumably. Well, maybe ===================================== compiler/GHC/Core/Opt/ConstantFold.hs ===================================== @@ -1606,11 +1606,11 @@ as follows: let x = I# (error "invalid shift") in ... -This was originally done in the fix to #16449 but this breaks the -let-can-float invariant (see Note [Core let-can-float invariant] in -GHC.Core) as noted in #16742. For the reasons discussed under -"NoEffect" in Note [Classifying primop effects] (in GHC.Builtin.PrimOps) -there is no safe way to rewrite the argument of I# such that it bottoms. +This was originally done in the fix to #16449 but this breaks +Note [Nested binding invariants] in GHC.Core, as noted in #16742. For the +reasons discussed under "NoEffect" in Note [Classifying primop effects] (in +GHC.Builtin.PrimOps) there is no safe way to rewrite the argument of I# such +that it bottoms. Consequently we instead take advantage of the fact that the result of a large shift is unspecified (see associated documentation in primops.txt.pp) @@ -2177,15 +2177,15 @@ BigNat). These rules implement the same kind of constant folding as we have for Int#/Word#/etc. primops. See builtinBignumRules. These rules are built-in because they can't be expressed as regular rules for -now. The reason is that due to the let-can-float invariant (see Note [Core -let-can-float invariant] in GHC.Core), GHC is too conservative with some bignum -operations and they don't match rules. For example: +now. The reason is that due to Note [Nested binding invariants] in GHC.Core, +GHC is too conservative with some bignum operations and they don't match rules. +For example: case integerAdd 1 x of r { _ -> integerAdd 1 r } doesn't constant-fold into `integerAdd 2 x` with a regular rule. That's because GHC never floats in `integerAdd 1 x` to form `integerAdd 1 (integerAdd 1 x)` -because of the let-can-float invariant (it doesn't know if `integerAdd` +because of Note [Nested binding invariants] (it doesn't know if `integerAdd` terminates). In the built-in rule for `integerAdd` we can access the unfolding of `r` and we ===================================== compiler/GHC/Core/Opt/FloatIn.hs ===================================== @@ -665,7 +665,8 @@ noFloatIntoRhs is_rec bndr rhs = isRec is_rec -- Joins are one-shot iff non-recursive | definitelyUnliftedType (idType bndr) - = True -- Preserve let-can-float invariant, see Note [noFloatInto considerations] + = True -- Preserve Note [Nested binding invariants], + -- see Note [noFloatInto considerations] | otherwise = noFloatIntoArg rhs @@ -690,7 +691,7 @@ When do we want to float bindings into - noFloatIntoArg: the argument of a function application Definitely don't float into RHS if it has unlifted type; -that would destroy the let-can-float invariant. +that would destroy Note [Nested binding invariants]. * Wrinkle 1: do not float in if (a) any non-one-shot value lambdas ===================================== compiler/GHC/Core/Opt/SetLevels.hs ===================================== @@ -1003,12 +1003,11 @@ Why? Because it's important /not/ to transform let x = a /# 3 to let x = case bx of I# a -> a /# 3 -because the let binding no -longer obeys the let-can-float invariant. But (a /# 3) is ok-for-spec -due to a special hack that says division operators can't fail -when the denominator is definitely non-zero. And yet that -same expression says False to exprIsCheap. Simplest way to -guarantee the let-can-float invariant is to use the same function! +because the let binding no longer obeys Note [Nested binding invariants]. +But (a /# 3) is ok-for-spec due to a special hack that says division operators +can't fail when the denominator is definitely non-zero. And yet that same +expression says False to exprIsCheap. Simplest way to guarantee +Note [Nested binding invariants] is to use the same function! If an expression is okay for speculation, we could also float it out *without* boxing and unboxing, since evaluating it early is okay. ===================================== compiler/GHC/Core/Opt/Simplify/Env.hs ===================================== @@ -749,8 +749,8 @@ Examples NonRec x# (y +# 3) FltOkSpec -- Unboxed, but ok-for-spec'n NonRec x* (f y) FltCareful -- Strict binding; might fail or diverge - NonRec x# (a /# b) FltCareful -- Might fail; does not satisfy let-can-float invariant - NonRec x# (f y) FltCareful -- Might diverge; does not satisfy let-can-float invariant + NonRec x# (a /# b) FltCareful -- Might fail; does not satisfy Note [Nested binding invariants] + NonRec x# (f y) FltCareful -- Might diverge; does not satisfy Note [Nested binding invariants] -} data LetFloats = LetFloats (OrdList OutBind) FloatFlag @@ -763,7 +763,7 @@ data FloatFlag = FltLifted -- All bindings are lifted and lazy *or* -- consist of a single primitive string literal -- Hence ok to float to top level, or recursive - -- NB: consequence: all bindings satisfy let-can-float invariant + -- NB: consequence: all bindings satisfy Note [Nested binding invariants] | FltOkSpec -- All bindings are FltLifted *or* -- strict (perhaps because unlifted, @@ -772,12 +772,12 @@ data FloatFlag -- Hence ok to float out of the RHS -- of a lazy non-recursive let binding -- (but not to top level, or into a rec group) - -- NB: consequence: all bindings satisfy let-can-float invariant + -- NB: consequence: all bindings satisfy Note [Nested binding invariants] | FltCareful -- At least one binding is strict (or unlifted) -- and not guaranteed cheap -- Do not float these bindings out of a lazy let! - -- NB: some bindings may not satisfy let-can-float + -- NB: some bindings may not satisfy Note [Nested binding invariants] instance Outputable LetFloats where ppr (LetFloats binds ff) = ppr ff $$ ppr (fromOL binds) @@ -962,8 +962,8 @@ wrapFloats (SimplFloats { sfLetFloats = LetFloats bs flag -- Note: Always safe to put the joins on the inside -- since the values can't refer to them where - mk_let | FltCareful <- flag = mkCoreLet -- need to enforce let-can-float-invariant - | otherwise = Let -- let-can-float invariant hold + mk_let | FltCareful <- flag = mkCoreLet -- Need to enforce Note [Nested binding invariants] + | otherwise = Let -- Note [Nested binding invariants] holds wrapJoinFloatsX :: SimplFloats -> OutExpr -> (SimplFloats, OutExpr) -- Wrap the sfJoinFloats of the env around the expression, ===================================== compiler/GHC/Core/Opt/Simplify/Iteration.hs ===================================== @@ -315,7 +315,7 @@ simplLazyBind :: TopLevelFlag -> RecFlag -> (InExpr, SimplEnv) -- The RHS and its static environment -> SimplM (SimplFloats, SimplEnv) -- Precondition: Ids only, no TyVars; not a JoinId --- Precondition: rhs obeys the let-can-float invariant +-- Precondition: rhs obeys Note [Nested binding invariants] simplLazyBind top_lvl is_rec (bndr,unf_se) (bndr1,env) (rhs,rhs_se) = assert (isId bndr ) assertPpr (not (isJoinId bndr)) (ppr bndr) $ @@ -397,7 +397,7 @@ simplAuxBind :: String -- The binder comes from a case expression (case binder or alternative) -- and so does not have rules, unfolding, inline pragmas etc. -- --- Precondition: rhs satisfies the let-can-float invariant +-- Precondition: rhs satisfies Note [Nested binding invariants] simplAuxBind _str env bndr new_rhs | assertPpr (isId bndr && not (isJoinId bndr)) (ppr bndr) $ @@ -950,7 +950,7 @@ completeBind :: BindContext -- * or by adding to the floats in the envt -- -- Binder /can/ be a JoinId --- Precondition: rhs obeys the let-can-float invariant +-- Precondition: rhs obeys Note [Nested binding invariants] completeBind bind_cxt (old_bndr, unf_se) (new_bndr, new_rhs, env) | isCoVar old_bndr = case new_rhs of @@ -1290,7 +1290,7 @@ simplExprF1 env (Let (NonRec bndr rhs) body) cont ; simplExprF (extendTvSubst env bndr ty') body cont } | Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs env - -- Because of the let-can-float invariant, it's ok to + -- Because of Note [Nested binding invariants], it's ok to -- inline freely, or to drop the binding if it is dead. = do { simplTrace "SimplBindr:inline-uncond2" (ppr bndr <+> ppr rhs) $ tick (PreInlineUnconditionally bndr) @@ -1594,13 +1594,13 @@ rebuild_go env expr cont completeBindX :: SimplEnv -> FromWhat -> InId -> OutExpr -- Non-recursively bind this Id to this (simplified) expression - -- (the let-can-float invariant may not be satisfied) + -- (Note [Nested binding invariants] may not be satisfied) -> InExpr -- In this body -> SimplCont -- Consumed by this continuation -> SimplM (SimplFloats, OutExpr) completeBindX env from_what bndr rhs body cont | FromBeta arg_levity <- from_what - , needsCaseBindingL arg_levity rhs -- Enforcing the let-can-float-invariant + , needsCaseBindingL arg_levity rhs -- Enforcing Note [Nested binding invariants] = do { (env1, bndr1) <- simplNonRecBndr env bndr -- Lambda binders don't have rules ; (floats, expr') <- simplNonRecBody env1 from_what body cont -- Do not float floats past the Case binder below @@ -1887,7 +1887,7 @@ simplNonRecE :: HasDebugCallStack -- It deals with strict bindings, via the StrictBind continuation, -- which may abort the whole process. -- --- from_what=FromLet => the RHS satisfies the let-can-float invariant +-- from_what=FromLet => the RHS satisfies Note [Nested binding invariants] -- Otherwise it may or may not satisfy it. simplNonRecE env from_what bndr (rhs, rhs_se) body cont @@ -1910,7 +1910,7 @@ simplNonRecE env from_what bndr (rhs, rhs_se) body cont is_strict_bind = case from_what of FromBeta Unlifted -> True -- If we are coming from a beta-reduction (FromBeta) we must - -- establish the let-can-float invariant, so go via StrictBind + -- establish Note [Nested binding invariants], so go via StrictBind -- If not, the invariant holds already, and it's optional. -- (FromBeta Lifted) or FromLet: look at the demand info @@ -2857,7 +2857,7 @@ this transformation: We treat the unlifted and lifted cases separately: * Unlifted case: 'e' satisfies exprOkForSpeculation - (ok-for-spec is needed to satisfy the let-can-float invariant). + (ok-for-spec is needed to satisfy Note [Nested binding invariants]. This turns case a +# b of r -> ...r... into let r = a +# b in ...r... and thence .....(a +# b).... @@ -3112,7 +3112,7 @@ rebuildCase env scrut case_bndr alts cont assert (null bs) $ do { (floats1, env') <- simplAuxBind "rebuildCase" env case_bndr case_bndr_rhs -- scrut is a constructor application, - -- hence satisfies let-can-float invariant + -- hence satisfies Note [Nested binding invariants] ; (floats2, expr') <- simplExprF env' rhs cont ; case wfloats of [] -> return (floats1 `addFloats` floats2, expr') @@ -3624,11 +3624,11 @@ We pin on a (OtherCon []) unfolding to the case-binder of a Case, even though it'll be over-ridden in every case alternative with a more informative unfolding. Why? Because suppose a later, less clever, pass simply replaces all occurrences of the case binder with the binder itself; -then Lint may complain about the let-can-float invariant. Example +then Lint may complain about failing Note [Nested binding invariants]. Example case e of b { DEFAULT -> let v = reallyUnsafePtrEquality# b y in .... ; K -> blah } -The let-can-float invariant requires that y is evaluated in the call to +Note [Nested binding invariants] requires that y is evaluated in the call to reallyUnsafePtrEquality#, which it is. But we still want that to be true if we propagate binders to occurrences. @@ -3732,7 +3732,8 @@ knownCon env scrut dc_floats dc dc_ty_args dc_args bndr bs rhs cont -- occur in the RHS; and simplAuxBind may therefore discard it. -- Nevertheless we must keep it if the case-binder is alive, -- because it may be used in the con_app. See Note [knownCon occ info] - ; (floats1, env2) <- simplAuxBind "knownCon" env' b' arg -- arg satisfies let-can-float invariant + -- NB: arg satisfies Note [Nested binding invariants] + ; (floats1, env2) <- simplAuxBind "knownCon" env' b' arg ; (floats2, env3) <- bind_args env2 bs' args ; return (floats1 `addFloats` floats2, env3) } ===================================== compiler/GHC/Core/Opt/Simplify/Utils.hs ===================================== @@ -1491,8 +1491,8 @@ preInlineUnconditionally :: SimplEnv -> TopLevelFlag -> InId -> InExpr -> StaticEnv -- These two go together -> Maybe SimplEnv -- Returned env has extended substitution --- Precondition: rhs satisfies the let-can-float invariant --- See Note [Core let-can-float invariant] in GHC.Core +-- Precondition: rhs satisfies Note [Nested binding invariants] +-- See Note [Nested binding invariants] in GHC.Core -- Reason: we don't want to inline single uses, or discard dead bindings, -- for unlifted, side-effect-ful bindings preInlineUnconditionally env top_lvl bndr rhs rhs_env @@ -1638,8 +1638,7 @@ postInlineUnconditionally -> InId -> OutId -- The binder (*not* a CoVar), including its unfolding -> OutExpr -> Bool --- Precondition: rhs satisfies the let-can-float invariant --- See Note [Core let-can-float invariant] in GHC.Core +-- Precondition: rhs satisfies Note [Nested binding invariants] in GHC.Core -- Reason: we don't want to inline single uses, or discard dead bindings, -- for unlifted, side-effect-ful bindings postInlineUnconditionally env bind_cxt old_bndr bndr rhs ===================================== compiler/GHC/Core/Opt/Specialise.hs ===================================== @@ -1944,7 +1944,7 @@ case) do not float the binding itself unless it satisfies exprIsTopLevelBindable This is conservative: maybe the RHS of `x` has a free var that would stop it floating to top level anyway; but that is hard to spot (since we don't know what the non-top-level in-scope binders are) and rare (since the binding must satisfy -Note [Core let-can-float invariant] in GHC.Core). +Note [Nested binding invariants] in GHC.Core). Note [Specialising Calls] ===================================== compiler/GHC/Core/SimpleOpt.hs ===================================== @@ -381,7 +381,7 @@ simple_app env e0@(Lam {}) as0@(_:_) -- See Note [Dark corner with representation polymorphism] needsCaseBinding (idType b') (snd a) -- This arg must not be inlined (side-effects) and cannot be let-bound, - -- due to the let-can-float invariant. So simply case-bind it here. + -- due to Note [Nested binding invariants]. So simply case-bind it here. , let a' = simple_opt_clo (soeInScope env) a = mkDefaultCase a' b' $ do_beta env' body as ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -350,7 +350,8 @@ deepTcvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synon where do_tcv is v = EndoOS do_it where - do_it acc | not (isLocalVar v) = acc + do_it acc | not (isLocalVar v) = acc -- A CoVar can be a GlobalId + -- See Note [Coercion bindings] in GHC.Core | v `elemVarSet` is = acc | v `elemVarSet` acc = acc | otherwise = appEndoOS (deep_ty (varType v)) $ ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -1040,7 +1040,7 @@ substTyCoBndr subst (Named (Bndr tv vis)) = (subst', Named (Bndr tv' vis)) {- Note [Keeping the substitution empty] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ A very common situation is where we run over a term doing no cloning, -no substitution, nothing. In that case the TCvSubst till be empty, and +no substitution, nothing. In that case the TCvSubst will be empty, and it is /very/ valuable to /keep/ it empty: * It's wasted effort to build up an identity substitution mapping ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -1813,13 +1813,11 @@ exprIsUnaryClassFun _ = False -- See also Note [Classifying primop effects] in "GHC.Builtin.PrimOps" -- and Note [Transformations affected by primop effects]. -- --- 'exprOkForSpeculation' is used to define Core's let-can-float --- invariant. (See Note [Core let-can-float invariant] in --- "GHC.Core".) It is therefore frequently called on arguments of --- unlifted type, especially via 'needsCaseBinding'. But it is --- sometimes called on expressions of lifted type as well. For --- example, see Note [Speculative evaluation] in "GHC.CoreToStg.Prep". - +-- 'exprOkForSpeculation' is used in the definition of Note [Nested binding +-- invariants]in GHC.Core. It is therefore frequently called on arguments of +-- unlifted type, especially via 'needsCaseBinding'. But it is sometimes +-- called on expressions of lifted type as well. For example, see +-- Note [Speculative evaluation] in "GHC.CoreToStg.Prep". exprOkForSpeculation, exprOkToDiscard :: CoreExpr -> Bool exprOkForSpeculation = expr_ok fun_always_ok primOpOkForSpeculation @@ -2044,12 +2042,14 @@ But we restrict it sharply: ; 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 + Does the RHS of v satisfy Note [Nested binding invariants]? + 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 + which does /not/ satisfy Note [Nested bindings invariants], 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 @@ -2134,7 +2134,7 @@ extremely useful for float-out, changes these expressions to 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. +and then it really, really doesn't obey Note [Nested binding invariants]. The solution is simple: exprOkForSpeculation does not try to take advantage of the evaluated-ness of (lifted) variables. And it returns @@ -2144,7 +2144,8 @@ by marking the relevant primops as "ThrowsException" or 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. +it doesn't have the trickiness of Note [Nested binding invariants] +to worry about. ************************************************************************ * * ===================================== compiler/GHC/Stg/Lint.hs ===================================== @@ -5,9 +5,8 @@ A lint pass to check basic STG invariants: - Variables should be defined before used. -- Let bindings should not have unboxed types (unboxed bindings should only - appear in case), except when they're join points (see Note [Core let-can-float - invariant] and #14117). +- Let bindings: see Note [Core binding invariants] in GHC.Core. + (See #14117). - If linting after unarisation, invariants listed in Note [Post-unarisation invariants]. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2b2ee16577b5bb5146bb48ab7156b84f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2b2ee16577b5bb5146bb48ab7156b84f... You're receiving this email because of your account on gitlab.haskell.org.