[Git][ghc/ghc][wip/T24335] Fix four bug in handling of (forall cv. body_ty)
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sun Jan 14 22:27:46 UTC 2024
Simon Peyton Jones pushed to branch wip/T24335 at Glasgow Haskell Compiler / GHC
Commits:
e3875235 by Simon Peyton Jones at 2024-01-14T22:26:59+00: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
=====================================
@@ -995,6 +995,9 @@ lintCoreExpr (Case scrut var alt_ty alts)
lintCoreExpr (Type ty)
= failWithL (text "Type found as expression" <+> ppr ty)
+-- ToDo: is (Coercion co) OK in a term in places other
+-- than as the argument of an App?
+-- It is certainly needed for coercible_sel in ghc-prim:GHC.Types
lintCoreExpr (Coercion co)
= do { co' <- addLoc (InCo co) $
lintCoercion co
@@ -1438,6 +1441,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 +1451,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 +1523,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 +1534,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 +3663,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,41 @@ 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
+
; 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,7 +1861,7 @@ 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
+ 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.
=====================================
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
@@ -516,11 +516,14 @@ bindNonRec 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 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/e387523514661c9062aecbfa94d1640f30a3a39a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e387523514661c9062aecbfa94d1640f30a3a39a
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/20240114/9de19dab/attachment-0001.html>
More information about the ghc-commits
mailing list