[Git][ghc/ghc][master] Fix four bug in handling of (forall cv. body_ty)

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Thu Jan 18 10:23:16 UTC 2024



Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
c4078f2f by Simon Peyton Jones at 2024-01-18T05:22:25-05:00
Fix four bug in handling of (forall cv. body_ty)

These bugs are all described in #24335

It's not easy to provoke the bug, hence no test case.

- - - - -


6 changed files:

- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/Opt/Simplify/Utils.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Utils.hs


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -822,7 +822,27 @@ special behaviour.  For example, this is /not/ fine:
     join j = ...
     in runRW# @r @ty (jump j)
 
+Note [Coercions in terms]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+The expression (Type ty) can occur only as the argument of an application,
+or the RHS of a non-recursive Let.  But what about (Coercion co)?
 
+Currently it appears in ghc-prim:GHC.Types.coercible_sel, a WiredInId whose
+definition is:
+   coercible_sel :: Coercible a b => (a ~R# b)
+   coercible_sel d = case d of
+                         MkCoercibleDict (co :: a ~# b) -> Coercion co
+
+So this function has a (Coercion co) in the alternative of a case.
+
+Richard says (!11908): it shouldn't appear outside of arguments, but we've been
+loose about this. coercible_sel is some thin ice. Really we should be unpacking
+Coercible using case, not a selector. I recall looking into this a few years
+back and coming to the conclusion that the fix was worse than the disease. Don't
+remember the details, but could probably recover it if we want to revisit.
+
+So Lint current accepts (Coercion co) in arbitrary places.  There is no harm in
+that: it really is a value, albeit a zero-bit value.
 
 ************************************************************************
 *                                                                      *
@@ -996,6 +1016,7 @@ lintCoreExpr (Type ty)
   = failWithL (text "Type found as expression" <+> ppr ty)
 
 lintCoreExpr (Coercion co)
+  -- See Note [Coercions in terms]
   = do { co' <- addLoc (InCo co) $
                 lintCoercion co
        ; return (coercionType co', zeroUE) }
@@ -1438,6 +1459,8 @@ lintCoreArgs  :: (LintedType, UsageEnv) -> [CoreArg] -> LintM (LintedType, Usage
 lintCoreArgs (fun_ty, fun_ue) args = foldM lintCoreArg (fun_ty, fun_ue) args
 
 lintCoreArg  :: (LintedType, UsageEnv) -> CoreArg -> LintM (LintedType, UsageEnv)
+
+-- Type argument
 lintCoreArg (fun_ty, ue) (Type arg_ty)
   = do { checkL (not (isCoercionTy arg_ty))
                 (text "Unnecessary coercion-to-type injection:"
@@ -1446,6 +1469,14 @@ lintCoreArg (fun_ty, ue) (Type arg_ty)
        ; res <- lintTyApp fun_ty arg_ty'
        ; return (res, ue) }
 
+-- Coercion argument
+lintCoreArg (fun_ty, ue) (Coercion co)
+  = do { co' <- addLoc (InCo co) $
+                lintCoercion co
+       ; res <- lintCoApp fun_ty co'
+       ; return (res, ue) }
+
+-- Other value argument
 lintCoreArg (fun_ty, fun_ue) arg
   = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg
            -- See Note [Representation polymorphism invariants] in GHC.Core
@@ -1510,7 +1541,7 @@ checkCaseLinearity ue case_bndr var_w bndr = do
 -----------------
 lintTyApp :: LintedType -> LintedType -> LintM LintedType
 lintTyApp fun_ty arg_ty
-  | Just (tv,body_ty) <- splitForAllTyCoVar_maybe fun_ty
+  | Just (tv,body_ty) <- splitForAllTyVar_maybe fun_ty
   = do  { lintTyKind tv arg_ty
         ; in_scope <- getInScope
         -- substTy needs the set of tyvars in scope to avoid generating
@@ -1521,12 +1552,35 @@ lintTyApp fun_ty arg_ty
   | otherwise
   = failWithL (mkTyAppMsg fun_ty arg_ty)
 
+-----------------
+lintCoApp :: LintedType -> LintedCoercion -> LintM LintedType
+lintCoApp fun_ty co
+  | Just (cv,body_ty) <- splitForAllCoVar_maybe fun_ty
+  , let co_ty = coercionType co
+        cv_ty = idType cv
+  , cv_ty `eqType` co_ty
+  = do { in_scope <- getInScope
+       ; let init_subst = mkEmptySubst in_scope
+             subst = extendCvSubst init_subst cv co
+       ; return (substTy subst body_ty) }
+
+  | Just (_, _, arg_ty', res_ty') <- splitFunTy_maybe fun_ty
+  , co_ty `eqType` arg_ty'
+  = return (res_ty')
+
+  | otherwise
+  = failWithL (mkCoAppMsg fun_ty co)
+
+  where
+    co_ty = coercionType co
+
 -----------------
 
 -- | @lintValApp arg fun_ty arg_ty@ lints an application of @fun arg@
 -- where @fun :: fun_ty@ and @arg :: arg_ty@, returning the type of the
 -- application.
-lintValApp :: CoreExpr -> LintedType -> LintedType -> UsageEnv -> UsageEnv -> LintM (LintedType, UsageEnv)
+lintValApp :: CoreExpr -> LintedType -> LintedType -> UsageEnv -> UsageEnv
+           -> LintM (LintedType, UsageEnv)
 lintValApp arg fun_ty arg_ty fun_ue arg_ue
   | Just (_, w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty
   = do { ensureEqTys arg_ty' arg_ty (mkAppMsg arg_ty' arg_ty arg)
@@ -3627,11 +3681,19 @@ mkLetErr bndr rhs
 mkTyAppMsg :: Type -> Type -> SDoc
 mkTyAppMsg ty arg_ty
   = vcat [text "Illegal type application:",
-              hang (text "Exp type:")
+              hang (text "Function type:")
                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
-              hang (text "Arg type:")
+              hang (text "Type argument:")
                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 
+mkCoAppMsg :: Type -> Coercion -> SDoc
+mkCoAppMsg fun_ty co
+  = vcat [ text "Illegal coercion application:"
+         , hang (text "Function type:")
+              4 (ppr fun_ty)
+         , hang (text "Coercion argument:")
+              4 (ppr co <+> dcolon <+> ppr (coercionType co))]
+
 emptyRec :: CoreExpr -> SDoc
 emptyRec e = hang (text "Empty Rec binding:") 2 (ppr e)
 


=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -198,8 +198,10 @@ typeOneShots ty
   = go initRecTc ty
   where
     go rec_nts ty
-      | Just (_, ty')  <- splitForAllTyCoVar_maybe ty
-      = go rec_nts ty'
+      | Just (tcv, ty')  <- splitForAllTyCoVar_maybe ty
+      = if isCoVar tcv
+        then idOneShotInfo tcv : go rec_nts ty'
+        else go rec_nts ty'
 
       | Just (_,_,arg,res) <- splitFunTy_maybe ty
       = typeOneShot arg : go rec_nts res


=====================================
compiler/GHC/Core/Opt/Simplify/Iteration.hs
=====================================
@@ -20,7 +20,7 @@ import GHC.Driver.Flags
 import GHC.Core
 import GHC.Core.Opt.Simplify.Monad
 import GHC.Core.Opt.ConstantFold
-import GHC.Core.Type hiding ( substTy, substTyVar, extendTvSubst, extendCvSubst )
+import GHC.Core.Type hiding ( substTy, substCo, substTyVar, extendTvSubst, extendCvSubst )
 import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.Opt.Simplify.Env
 import GHC.Core.Opt.Simplify.Inline
@@ -1551,8 +1551,8 @@ completeBindX :: SimplEnv
               -> SimplCont         -- Consumed by this continuation
               -> SimplM (SimplFloats, OutExpr)
 completeBindX env from_what bndr rhs body cont
-  | FromBeta arg_ty <- from_what
-  , needsCaseBinding arg_ty rhs -- Enforcing the let-can-float-invariant
+  | FromBeta arg_levity <- from_what
+  , needsCaseBindingL arg_levity rhs -- Enforcing the let-can-float-invariant
   = 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
@@ -1753,26 +1753,47 @@ simpl_lam env bndr body (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = cont })
   = do { tick (BetaReduction bndr)
        ; simplLam (extendTvSubst env bndr arg_ty) body cont }
 
+-- Coercion beta-reduction
+simpl_lam env bndr body (ApplyToVal { sc_arg = Coercion arg_co, sc_env = arg_se
+                                    , sc_cont = cont })
+  = assertPpr (isCoVar bndr) (ppr bndr) $
+    do { tick (BetaReduction bndr)
+       ; let arg_co' = substCo (arg_se `setInScopeFromE` env) arg_co
+       ; simplLam (extendCvSubst env bndr arg_co') body cont }
+
 -- Value beta-reduction
+-- This works for /coercion/ lambdas too
 simpl_lam env bndr body (ApplyToVal { sc_arg = arg, sc_env = arg_se
                                     , sc_cont = cont, sc_dup = dup
                                     , sc_hole_ty = fun_ty})
   = do { tick (BetaReduction bndr)
-       ; let arg_ty = funArgTy fun_ty
+       ; let from_what = FromBeta arg_levity
+             arg_levity
+               | isForAllTy fun_ty = assertPpr (isCoVar bndr) (ppr bndr) Unlifted
+               | otherwise         = typeLevity (funArgTy fun_ty)
+             -- Example:  (\(cv::a ~# b). blah) co
+             -- The type of (\cv.blah) can be (forall cv. ty); see GHC.Core.Utils.mkLamType
+
+             -- Using fun_ty: see Note [Dark corner with representation polymorphism]
+             -- e.g  (\r \(a::TYPE r) \(x::a). blah) @LiftedRep @Int arg
+             --      When we come to `x=arg` we must choose lazy/strict correctly
+             --      It's wrong to err in either direction
+             --      But fun_ty is an OutType, so is fully substituted
+
        ; if | isSimplified dup  -- Don't re-simplify if we've simplified it once
                                 -- Including don't preInlineUnconditionally
                                 -- See Note [Avoiding exponential behaviour]
-            -> completeBindX env (FromBeta arg_ty) bndr arg body cont
+            -> completeBindX env from_what bndr arg body cont
 
             | Just env' <- preInlineUnconditionally env NotTopLevel bndr arg arg_se
-            , not (needsCaseBinding arg_ty arg)
+            , not (needsCaseBindingL arg_levity arg)
               -- Ok to test arg::InExpr in needsCaseBinding because
               -- exprOkForSpeculation is stable under simplification
             -> do { tick (PreInlineUnconditionally bndr)
                   ; simplLam env' body cont }
 
             | otherwise
-            -> simplNonRecE env (FromBeta arg_ty) bndr (arg, arg_se) body cont }
+            -> simplNonRecE env from_what bndr (arg, arg_se) body cont }
 
 -- Discard a non-counting tick on a lambda.  This may change the
 -- cost attribution slightly (moving the allocation of the
@@ -1846,15 +1867,12 @@ simplNonRecE env from_what bndr (rhs, rhs_se) body cont
 
   where
     is_strict_bind = case from_what of
-       FromBeta arg_ty | isUnliftedType arg_ty -> True
-         -- If we are coming from a beta-reduction (FromBeta) we must
-         -- establish the let-can-float invariant, so go via StrictBind
-         -- If not, the invariant holds already, and it's optional.
-         -- Using arg_ty: see Note [Dark corner with representation polymorphism]
-         -- e.g  (\r \(a::TYPE r) \(x::a). blah) @LiftedRep @Int arg
-         --      When we come to `x=arg` we myst choose lazy/strict correctly
-         --      It's wrong to err in either directly
+       FromBeta Unlifted -> True
+       -- If we are coming from a beta-reduction (FromBeta) we must
+       -- establish the let-can-float invariant, so go via StrictBind
+       -- If not, the invariant holds already, and it's optional.
 
+       -- (FromBeta Lifted) or FromLet: look at the demand info
        _ -> seCaseCase env && isStrUsedDmd (idDemandInfo bndr)
 
 


=====================================
compiler/GHC/Core/Opt/Simplify/Utils.hs
=====================================
@@ -214,7 +214,7 @@ data SimplCont
 
 type StaticEnv = SimplEnv       -- Just the static part is relevant
 
-data FromWhat = FromLet | FromBeta OutType
+data FromWhat = FromLet | FromBeta Levity
 
 -- See Note [DupFlag invariants]
 data DupFlag = NoDup       -- Unsimplified, might be big


=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -126,7 +126,7 @@ module GHC.Core.Type (
 
         -- *** Levity and boxity
         sORTKind_maybe, typeTypeOrConstraint,
-        typeLevity_maybe, tyConIsTYPEorCONSTRAINT,
+        typeLevity, typeLevity_maybe, tyConIsTYPEorCONSTRAINT,
         isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
         isLiftedRuntimeRep, isUnliftedRuntimeRep, runtimeRepLevity_maybe,
         isBoxedRuntimeRep,
@@ -1417,7 +1417,7 @@ funResultTy ty
   | FunTy { ft_res = res } <- coreFullView ty = res
   | otherwise                                 = pprPanic "funResultTy" (ppr ty)
 
-funArgTy :: Type -> Type
+funArgTy :: HasDebugCallStack => Type -> Type
 -- ^ Extract the function argument type and panic if that is not possible
 funArgTy ty
   | FunTy { ft_arg = arg } <- coreFullView ty = arg
@@ -1471,8 +1471,9 @@ piResultTys ty orig_args@(arg:args)
   | FunTy { ft_res = res } <- ty
   = piResultTys res args
 
-  | ForAllTy (Bndr tv _) res <- ty
-  = go (extendTCvSubst init_subst tv arg) res args
+  | ForAllTy (Bndr tcv _) res <- ty
+  = -- Both type and coercion variables
+    go (extendTCvSubst init_subst tcv arg) res args
 
   | Just ty' <- coreView ty
   = piResultTys ty' orig_args
@@ -2291,6 +2292,11 @@ buildSynTyCon name binders res_kind roles rhs
 typeLevity_maybe :: HasDebugCallStack => Type -> Maybe Levity
 typeLevity_maybe ty = runtimeRepLevity_maybe (getRuntimeRep ty)
 
+typeLevity :: HasDebugCallStack => Type -> Levity
+typeLevity ty = case typeLevity_maybe ty of
+                   Just lev -> lev
+                   Nothing  -> pprPanic "typeLevity" (ppr ty)
+
 -- | Is the given type definitely unlifted?
 -- See "Type#type_classification" for what an unlifted type is.
 --
@@ -2647,18 +2653,20 @@ typeKind (AppTy fun arg)
     go fun             args = piResultTys (typeKind fun) args
 
 typeKind ty@(ForAllTy {})
-  = case occCheckExpand tvs body_kind of
-      -- We must make sure tv does not occur in kind
-      -- As it is already out of scope!
+  = assertPpr (not (null tcvs)) (ppr ty) $
+       -- If tcvs is empty somehow we'll get an infinite loop!
+    case occCheckExpand tcvs body_kind of
+      -- We must make sure tvs do not occur in kind,
+      -- as they would be out of scope!
       -- See Note [Phantom type variables in kinds]
       Nothing -> pprPanic "typeKind"
-                  (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
+                  (ppr ty $$ ppr tcvs $$ ppr body <+> dcolon <+> ppr body_kind)
 
-      Just k' | all isTyVar tvs -> k'                     -- Rule (FORALL1)
-              | otherwise       -> lifted_kind_from_body  -- Rule (FORALL2)
+      Just k' | all isTyVar tcvs -> k'                     -- Rule (FORALL1)
+              | otherwise        -> lifted_kind_from_body  -- Rule (FORALL2)
   where
-    (tvs, body) = splitForAllTyVars ty
-    body_kind   = typeKind body
+    (tcvs, body) = splitForAllTyCoVars ty  -- Important: splits both TyVar and CoVar binders
+    body_kind    = typeKind body
 
     lifted_kind_from_body  -- Implements (FORALL2)
       = case sORTKind_maybe body_kind of


=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -11,7 +11,7 @@ module GHC.Core.Utils (
         -- * Constructing expressions
         mkCast, mkCastMCo, mkPiMCo,
         mkTick, mkTicks, mkTickNoHNF, tickHNFArgs,
-        bindNonRec, needsCaseBinding,
+        bindNonRec, needsCaseBinding, needsCaseBindingL,
         mkAltExpr, mkDefaultCase, mkSingleAltCase,
 
         -- * Taking expressions apart
@@ -513,14 +513,21 @@ bindNonRec bndr rhs body
     case_bind = mkDefaultCase rhs bndr body
     let_bind  = Let (NonRec bndr rhs) body
 
--- | Tests whether we have to use a @case@ rather than @let@ binding for this
--- expression as per the invariants of 'CoreExpr': see "GHC.Core#let_can_float_invariant"
-needsCaseBinding :: Type -> CoreExpr -> Bool
-needsCaseBinding ty rhs
-  = mightBeUnliftedType ty && not (exprOkForSpeculation rhs)
-        -- Make a case expression instead of a let
-        -- These can arise either from the desugarer,
-        -- or from beta reductions: (\x.e) (x +# y)
+-- | `needsCaseBinding` tests whether we have to use a @case@ rather than @let@
+-- binding for this expression as per the invariants of 'CoreExpr': see
+-- "GHC.Core#let_can_float_invariant"
+-- (needsCaseBinding ty rhs) requires that `ty` has a well-defined levity, else
+-- `typeLevity ty` will fail; but that should be the case because
+-- `needsCaseBinding` is only called once typechecking is complete
+needsCaseBinding :: HasDebugCallStack => Type -> CoreExpr -> Bool
+needsCaseBinding ty rhs = needsCaseBindingL (typeLevity ty) rhs
+
+needsCaseBindingL :: Levity -> CoreExpr -> Bool
+-- True <=> make a case expression instead of a let
+-- These can arise either from the desugarer,
+-- or from beta reductions: (\x.e) (x +# y)
+needsCaseBindingL Lifted   _rhs = False
+needsCaseBindingL Unlifted rhs = not (exprOkForSpeculation rhs)
 
 mkAltExpr :: AltCon     -- ^ Case alternative constructor
           -> [CoreBndr] -- ^ Things bound by the pattern match



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c4078f2fbc4b2655e66d8e1e256e9f18c5102c5f
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/20240118/84ef4e48/attachment-0001.html>


More information about the ghc-commits mailing list