Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC Commits: d0fbc978 by Adam Gundry at 2025-11-25T11:51:29+00:00 WIP: avoid castCoToCo in the optimizer - - - - - 87cbeb6f by Adam Gundry at 2025-11-25T11:51:29+00:00 WIP: use CastCoercion in rule matcher - - - - - 12 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/Map/Type.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Opt/OccurAnal.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/Opt/Simplify/Utils.hs - compiler/GHC/Core/Opt/SpecConstr.hs - compiler/GHC/Core/Rules.hs - compiler/GHC/Core/SimpleOpt.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/Utils.hs Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -57,6 +57,13 @@ module GHC.Core.Coercion ( castCoToCo, mkTransCastCo, mkTransCastCoCo, mkTransCoCastCo, mkSymCastCo, + mkPiCastCos, + isReflCastCo, + checkReflexiveCastCo, + coToCastCo, + mkForAllCastCo, + mkFunResCastCo, + mkFunCastCoNoFTF, -- ** Decomposition instNewTyCon_maybe, @@ -83,7 +90,7 @@ module GHC.Core.Coercion ( coToMCo, kindCoToMKindCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo, - mkFunResMCo, mkPiMCos, + mkFunResMCo, isReflMCo, checkReflexiveMCo, -- ** Coercion variables @@ -390,13 +397,10 @@ mkCastTyMCo :: Type -> MCoercion -> Type mkCastTyMCo ty MRefl = ty mkCastTyMCo ty (MCo co) = ty `mkCastTy` co -mkPiMCos :: [Var] -> MCoercion -> MCoercion -mkPiMCos _ MRefl = MRefl -mkPiMCos vs (MCo co) = MCo (mkPiCos Representational vs co) - -mkFunResMCo :: Id -> MCoercionR -> MCoercionR -mkFunResMCo _ MRefl = MRefl -mkFunResMCo arg_id (MCo co) = MCo (mkFunResCo Representational arg_id co) +mkFunResMCo :: Id -> CastCoercion -> CastCoercion +mkFunResMCo _ ReflCastCo = ReflCastCo +mkFunResMCo arg_id (CCoercion co) = CCoercion (mkFunResCo Representational arg_id co) +mkFunResMCo arg_id (ZCoercion ty cos) = ZCoercion (mkFunctionType (idMult arg_id) (varType arg_id) ty) cos -- TODO check type mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion mkGReflLeftMCo r ty MRefl = mkReflCo r ty @@ -843,6 +847,17 @@ mkFunCoNoFTF r w arg_co res_co Pair argl_ty argr_ty = coercionKind arg_co Pair resl_ty resr_ty = coercionKind res_co +-- AMG TODO: more cases here, or maybe better to have a FunCo constructor of CastCoercion? +mkFunCastCoNoFTF :: HasDebugCallStack => Role -> Mult -> Type -> CastCoercion -> Type -> CastCoercion -> CastCoercion +mkFunCastCoNoFTF _ mult _ (ZCoercion arg_ty arg_cos) _ (ZCoercion res_ty res_cos) = ZCoercion (mkFunctionType mult arg_ty res_ty) (arg_cos `unionVarSet` res_cos) +mkFunCastCoNoFTF _ mult _ (ZCoercion arg_ty arg_cos) res_ty res_co = ZCoercion (mkFunctionType mult arg_ty (castCoercionRKind res_ty res_co)) (arg_cos `unionVarSet` coVarsOfCastCo res_co) +mkFunCastCoNoFTF _ mult arg_ty arg_co _ (ZCoercion res_ty res_cos) = ZCoercion (mkFunctionType mult (castCoercionRKind arg_ty arg_co) res_ty) (res_cos `unionVarSet` coVarsOfCastCo arg_co) +mkFunCastCoNoFTF r mult _ (CCoercion arg_co) _ (CCoercion res_co) = CCoercion (mkFunCoNoFTF r (multToCo mult) arg_co res_co) +mkFunCastCoNoFTF _ _ _ ReflCastCo _ ReflCastCo = ReflCastCo +mkFunCastCoNoFTF r mult _ (CCoercion arg_co) res_ty ReflCastCo = CCoercion (mkFunCoNoFTF r (multToCo mult) arg_co (mkReflCo r res_ty)) +mkFunCastCoNoFTF r mult arg_ty ReflCastCo _ (CCoercion res_co) = CCoercion (mkFunCoNoFTF r (multToCo mult) (mkReflCo r arg_ty) res_co) + + -- | Build a function 'Coercion' from two other 'Coercion's. That is, -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@ -- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@. @@ -969,6 +984,13 @@ mkForAllCo v visL visR kind_co co | otherwise = mk_forall_co v visL visR kind_co co +mkForAllCastCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag + -> CastCoercion -> CastCoercion +mkForAllCastCo v visL visR cco = case cco of + CCoercion co -> CCoercion (mkForAllCo v visL visR MRefl co) + ZCoercion ty cos -> ZCoercion (mkTyCoForAllTy v visL ty) cos + ReflCastCo -> ReflCastCo + -- mkForAllVisCos [tv{vis}] constructs a cast -- forall tv. res ~R# forall tv{vis} res`. -- See Note [Required foralls in Core] in GHC.Core.TyCo.Rep @@ -1774,6 +1796,9 @@ castCoercionKind g h1 h2 mkPiCos :: Role -> [Var] -> Coercion -> Coercion mkPiCos r vs co = foldr (mkPiCo r) co vs +mkPiCastCos :: Role -> [Var] -> CastCoercion -> CastCoercion +mkPiCastCos r vs co = foldr (mkPiCastCo r) co vs + -- | Make a forall 'Coercion', where both types related by the coercion -- are quantified over the same variable. mkPiCo :: Role -> Var -> Coercion -> Coercion @@ -1787,6 +1812,16 @@ mkPiCo r v co | isTyVar v = mkHomoForAllCo v co mkFunResCo r v co | otherwise = mkFunResCo r v co +mkPiCastCo :: Role -> Var -> CastCoercion -> CastCoercion +mkPiCastCo _ _ ReflCastCo = ReflCastCo +mkPiCastCo r v (CCoercion co) = CCoercion (mkPiCo r v co) +mkPiCastCo _ v (ZCoercion ty cos) + | isTyVar v = ZCoercion (mkForAllTy (Bndr v vis) ty) cos + | otherwise = ZCoercion (mkFunctionType (idMult v) (varType v) ty) cos + where + vis = coreTyLamForAllTyFlag + + mkFunResCo :: Role -> Id -> Coercion -> Coercion -- Given res_co :: res1 ~ res2, -- mkFunResCo r m arg res_co :: (arg -> res1) ~r (arg -> res2) @@ -1797,6 +1832,13 @@ mkFunResCo role id res_co arg_co = mkReflCo role (varType id) mult = multToCo (idMult id) +mkFunResCastCo :: Role -> Id -> CastCoercion -> CastCoercion +mkFunResCastCo role id res_cco = case res_cco of + CCoercion res_co -> CCoercion (mkFunResCo role id res_co) + ZCoercion ty cos -> ZCoercion (mkFunctionType (idMult id) (varType id) ty) cos + ReflCastCo -> ReflCastCo + + -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2 -- The first coercion might be lifted or unlifted; thus the ~? above -- Lifted and unlifted equalities take different numbers of arguments, @@ -2882,7 +2924,7 @@ See Note [Zapped casts] in GHC.Core.TyCo.Rep. -- but requires the type to be supplied by the caller because it cannot be -- recovered in the 'ZCoercion' case. castCoercionLKind :: HasDebugCallStack => Type -> CastCoercion -> Type -castCoercionLKind _ (CCoercion co) = coercionLKind co +castCoercionLKind _ (CCoercion co) = coercionLKind co -- TODO: should we use provided lhs_ty instead? Not sure which is cheaper? castCoercionLKind lhs_ty (ZCoercion _ _) = lhs_ty castCoercionLKind lhs_ty ReflCastCo = lhs_ty @@ -2931,9 +2973,27 @@ mkTransCoCastCo co1 (CCoercion co2) = CCoercion (mkTransCo co1 co2) mkTransCoCastCo co1 (ZCoercion ty cos) = ZCoercion ty (shallowCoVarsOfCo co1 `unionVarSet` cos) mkTransCoCastCo co1 ReflCastCo = CCoercion co1 +-- | Quickly check if a 'CastCoercion' is obviously reflexive. +isReflCastCo :: CastCoercion -> Bool +isReflCastCo (CCoercion co) = isReflCo co +isReflCastCo ZCoercion{} = False -- it might be, but we can't tell +isReflCastCo ReflCastCo = True + -- | Slowly checks if the coercion is reflexive. Don't call this in a loop, -- as it walks over the entire coercion. isReflexiveCastCo :: Type -> CastCoercion -> Bool isReflexiveCastCo _ (CCoercion co) = isReflexiveCo co isReflexiveCastCo lhs_ty (ZCoercion rhs_ty _) = lhs_ty `eqType` rhs_ty isReflexiveCastCo _ ReflCastCo = True + +checkReflexiveCastCo :: Type -> CastCoercion -> CastCoercion +checkReflexiveCastCo ty cco + | isReflexiveCastCo ty cco = ReflCastCo + | otherwise = cco + +coToCastCo :: Coercion -> CastCoercion +-- Convert a coercion to a CastCoercion, checking if it is obviously reflexive. +-- It's not clear whether or not isReflexiveCo would be better here +-- See #19815 for a bit of data and discussion on this point +coToCastCo co | isReflCo co = ReflCastCo + | otherwise = CCoercion co ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -4,6 +4,7 @@ module GHC.Core.Coercion.Opt ( optCoercion + , optCastCoercion , OptCoercionOpts (..) ) where @@ -169,6 +170,13 @@ newtype OptCoercionOpts = OptCoercionOpts { optCoercionEnabled :: Bool -- ^ Enable coercion optimisation (reduce its size) } +optCastCoercion :: OptCoercionOpts -> Subst -> Type -> CastCoercion -> CastCoercion +optCastCoercion _ _ _ ReflCastCo = ReflCastCo +optCastCoercion opts env _ (CCoercion co) = CCoercion (optCoercion opts env co) +optCastCoercion _ env tyL (ZCoercion tyR cos) + | tyL `eqTypeIgnoringMultiplicity` tyR = ReflCastCo + | otherwise = ZCoercion (substTy env tyR) (substCoVarSet env cos) + optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo -- ^ optCoercion applies a substitution to a coercion, -- *and* optimises it to reduce its size ===================================== compiler/GHC/Core/Map/Type.hs ===================================== @@ -139,6 +139,7 @@ xtC (D env co) f (CoercionMapX m) -- We should really never care about the contents of a cast coercion. Instead, -- just look up the coercion's RHS type. +-- TODO: do we need this type, or can we just use TypeMap? newtype CastCoercionMap a = CastCoercionMap (CastCoercionMapG a) -- TODO(22292): derive ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -42,7 +42,7 @@ module GHC.Core.Opt.Arity , etaExpandToJoinPoint, etaExpandToJoinPointRule -- ** Coercions and casts - , pushCoArg, pushCoArgs, pushCoValArg, pushCoTyArg + , pushCoArg, pushCoArgs, pushCastCoValArg, pushCastCoTyArg , pushCoercionIntoLambda, pushCoDataCon, collectBindersPushingCo ) where @@ -2195,7 +2195,7 @@ Now, when we push that eta_co inward in etaInfoApp: -} -------------- -data EtaInfo = EI [Var] MCoercionR +data EtaInfo = EI [Var] CastCoercion -- See Note [The EtaInfo mechanism] instance Outputable EtaInfo where @@ -2221,11 +2221,10 @@ etaInfoApp in_scope expr eis go subst (Tick t e) eis = Tick (substTickish subst t) (go subst e eis) - go subst (Cast e cco) (EI bs mco) + go subst (Cast e co) (EI bs mco) = go subst e (EI bs mco') where - co = castCoToCo (exprType e) cco -- TODO: can we avoid this? - mco' = checkReflexiveMCo (Core.substCo subst co `mkTransMCoR` mco) + mco' = checkReflexiveCastCo (exprType (Core.substExpr subst e)) (Core.substCastCo subst co `mkTransCastCo` mco) -- See Note [Check for reflexive casts in eta expansion] go subst (Case e b ty alts) eis @@ -2247,13 +2246,13 @@ etaInfoApp in_scope expr eis -- Beta-reduction if possible, pushing any intervening casts past -- the argument. See Note [The EtaInfo mechanism] go subst (Lam v e) (EI (b:bs) mco) - | Just (arg,mco') <- pushMCoArg mco (varToCoreExpr b) + | Just (arg,mco') <- pushCoArg (exprType (Lam v e)) mco (varToCoreExpr b) = go (Core.extendSubst subst v arg) e (EI bs mco') -- Stop pushing down; just wrap the expression up -- See Note [Check for reflexive casts in eta expansion] go subst e (EI bs mco) = Core.substExprSC subst e - `mkCastMCo` checkReflexiveMCo mco + `mkCastCo` checkReflexiveCastCo (exprType e) mco -- TODO check type `mkVarApps` bs -------------- @@ -2263,14 +2262,12 @@ etaInfoAppTy :: Type -> EtaInfo -> Type etaInfoAppTy ty (EI bs mco) = applyTypeToArgs ty1 (map varToCoreExpr bs) where - ty1 = case mco of - MRefl -> ty - MCo co -> coercionRKind co + ty1 = castCoercionRKind ty mco -------------- etaInfoAbs :: EtaInfo -> CoreExpr -> CoreExpr -- See Note [The EtaInfo mechanism] -etaInfoAbs (EI bs mco) expr = (mkLams bs expr) `mkCastMCo` mkSymMCo mco +etaInfoAbs (EI bs mco) expr = (mkLams bs expr) `mkCastCo` mkSymCastCo (error "AMG TODO: etaInfoAbs") mco -------------- -- | @mkEtaWW n _ fvs ty@ will compute the 'EtaInfo' necessary for eta-expanding @@ -2307,7 +2304,7 @@ mkEtaWW orig_oss ppr_orig_expr in_scope orig_ty go _ [] subst _ ----------- Done! No more expansion needed - = (substInScopeSet subst, EI [] MRefl) + = (substInScopeSet subst, EI [] ReflCastCo) go n oss@(one_shot:oss1) subst ty ----------- Forall types (forall a. ty) @@ -2348,27 +2345,28 @@ mkEtaWW orig_oss ppr_orig_expr in_scope orig_ty -- we'd have had to zap it for the recursive call) , (in_scope, EI bs mco) <- go n oss subst ty' -- mco :: subst(ty') ~ b1_ty -> ... -> bn_ty -> tr - = (in_scope, EI bs (mkTransMCoR co' mco)) + = (in_scope, EI bs (mkTransCoCastCo co' mco)) | otherwise -- We have an expression of arity > 0, -- but its type isn't a function, or a binder -- does not have a fixed runtime representation = warnPprTrace True "mkEtaWW" ((ppr orig_oss <+> ppr orig_ty) $$ ppr_orig_expr) - (substInScopeSet subst, EI [] MRefl) + (substInScopeSet subst, EI [] ReflCastCo) -- This *can* legitimately happen: -- e.g. coerce Int (\x. x) Essentially the programmer is -- playing fast and loose with types (Happy does this a lot). -- So we simply decline to eta-expand. Otherwise we'd end up -- with an explicit lambda having a non-function type -mkEtaForAllMCo :: ForAllTyBinder -> Type -> MCoercion -> MCoercion +mkEtaForAllMCo :: ForAllTyBinder -> Type -> CastCoercion -> CastCoercion mkEtaForAllMCo (Bndr tcv vis) ty mco = case mco of - MRefl | vis == coreTyLamForAllTyFlag -> MRefl - | otherwise -> mk_fco (mkRepReflCo ty) - MCo co -> mk_fco co + ReflCastCo | vis == coreTyLamForAllTyFlag -> ReflCastCo + | otherwise -> mk_fco (mkRepReflCo ty) + CCoercion co -> mk_fco co + ZCoercion _ty2 cos -> ZCoercion ty cos -- TODO: is ty right? where - mk_fco co = MCo (mkForAllCo tcv vis coreTyLamForAllTyFlag MRefl co) + mk_fco co = CCoercion (mkForAllCo tcv vis coreTyLamForAllTyFlag MRefl co) -- coreTyLamForAllTyFlag: See Note [The EtaInfo mechanism], particularly -- the (EtaInfo Invariant). (sym co) wraps a lambda that always has -- a ForAllTyFlag of coreTyLamForAllTyFlag; see Note [Required foralls in Core] @@ -2701,13 +2699,13 @@ same fix. tryEtaReduce :: UnVarSet -> [Var] -> CoreExpr -> SubDemand -> Maybe CoreExpr -- Return an expression equal to (\bndrs. body) tryEtaReduce rec_ids bndrs body eval_sd - = go (reverse bndrs) body (mkRepReflCo (exprType body)) + = go (reverse bndrs) body ReflCastCo where incoming_arity = count isId bndrs -- See Note [Eta reduction makes sense], point (2) go :: [Var] -- Binders, innermost first, types [a3,a2,a1] -> CoreExpr -- Of type tr - -> Coercion -- Of type tr ~ ts + -> CastCoercion -- Of type tr ~ ts -> Maybe CoreExpr -- Of type a1 -> a2 -> a3 -> ts -- See Note [Eta reduction with casted arguments] -- for why we have an accumulating coercion @@ -2717,7 +2715,7 @@ tryEtaReduce rec_ids bndrs body eval_sd -- See Note [Eta reduction with casted function] go bs (Cast e co1) co2 - = go bs e (castCoToCo (exprType e) co1 `mkTransCo` co2) + = go bs e (co1 `mkTransCastCo` co2) go bs (Tick t e) co | tickishFloatable t @@ -2740,7 +2738,7 @@ tryEtaReduce rec_ids bndrs body eval_sd , remaining_bndrs `ltLength` bndrs -- Only reply Just if /something/ has happened , ok_fun fun - , let used_vars = exprFreeVars fun `unionVarSet` tyCoVarsOfCo co + , let used_vars = exprFreeVars fun `unionVarSet` tyCoVarsOfCastCo co reduced_bndrs = mkVarSet (dropList remaining_bndrs bndrs) -- reduced_bndrs are the ones we are eta-reducing away , used_vars `disjointVarSet` reduced_bndrs @@ -2749,7 +2747,7 @@ tryEtaReduce rec_ids bndrs body eval_sd -- See Note [Eta reduction makes sense], intro and point (1) -- NB: don't compute used_vars from exprFreeVars (mkCast fun co) -- because the latter may be ill formed if the guard fails (#21801) - = Just (mkLams (reverse remaining_bndrs) (mkCast fun co)) + = Just (mkLams (reverse remaining_bndrs) (mkCastCo fun co)) go _remaining_bndrs _fun _ = -- pprTrace "tER fail" (ppr _fun $$ ppr _remaining_bndrs) $ Nothing @@ -2797,10 +2795,10 @@ tryEtaReduce rec_ids bndrs body eval_sd --------------- ok_arg :: Var -- Of type bndr_t -> CoreExpr -- Of type arg_t - -> Coercion -- Of kind (t1~t2) + -> CastCoercion -- Of kind (t1~t2) -> Type -- Type (arg_t -> t1) of the function -- to which the argument is supplied - -> Maybe (Coercion -- Of type (arg_t -> t1 ~ bndr_t -> t2) + -> Maybe (CastCoercion -- Of type (arg_t -> t1 ~ bndr_t -> t2) -- (and similarly for tyvars, coercion args) , [CoreTickish]) -- See Note [Eta reduction with casted arguments] @@ -2808,7 +2806,7 @@ tryEtaReduce rec_ids bndrs body eval_sd | Just tv <- getTyVar_maybe arg_ty , bndr == tv = case splitForAllForAllTyBinder_maybe fun_ty of Just (Bndr _ vis, _) -> Just (fco, []) - where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag MRefl co + where !fco = mkForAllCastCo tv vis coreTyLamForAllTyFlag co -- The lambda we are eta-reducing always has visibility -- 'coreTyLamForAllTyFlag' which may or may not match -- the visibility on the inner function (#24014) @@ -2821,13 +2819,13 @@ tryEtaReduce rec_ids bndrs body eval_sd , let mult = idMult bndr , Just (_af, fun_mult, _, _) <- splitFunTy_maybe fun_ty , mult `eqType` fun_mult -- There is no change in multiplicity, otherwise we must abort - = Just (mkFunResCo Representational bndr co, []) + = Just (mkFunResCastCo Representational bndr co, []) ok_arg bndr (Cast e co_arg) co fun_ty | (ticks, Var v) <- stripTicksTop tickishFloatable e - , Just (_, fun_mult, _, _) <- splitFunTy_maybe fun_ty + , Just (_, fun_mult, _, res_ty) <- splitFunTy_maybe fun_ty , bndr == v , fun_mult `eqType` idMult bndr - = Just (mkFunCoNoFTF Representational (multToCo fun_mult) (mkSymCo (castCoToCo (exprType e) co_arg)) co, ticks) + = Just (mkFunCastCoNoFTF Representational fun_mult (castCoercionRKind (exprType e) co_arg) (mkSymCastCo (exprType e) co_arg) res_ty co, ticks) -- TODO check types -- The simplifier combines multiple casts into one, -- so we can have a simple-minded pattern match here ok_arg bndr (Tick t arg) co fun_ty @@ -2873,43 +2871,44 @@ Here we implement the "push rules" from FC papers: by pushing the coercion into the arguments -} -pushCoArgs :: CoercionR -> [CoreArg] -> Maybe ([CoreArg], MCoercion) -pushCoArgs co [] = return ([], MCo co) -pushCoArgs co (arg:args) = do { (arg', m_co1) <- pushCoArg co arg - ; case m_co1 of - MCo co1 -> do { (args', m_co2) <- pushCoArgs co1 args - ; return (arg':args', m_co2) } - MRefl -> return (arg':args, MRefl) } - -pushMCoArg :: MCoercionR -> CoreArg -> Maybe (CoreArg, MCoercion) -pushMCoArg MRefl arg = Just (arg, MRefl) -pushMCoArg (MCo co) arg = pushCoArg co arg - -pushCoArg :: CoercionR -> CoreArg -> Maybe (CoreArg, MCoercion) +pushCoArgs :: Type -> CastCoercion -> [CoreArg] -> Maybe ([CoreArg], CastCoercion) +pushCoArgs _ co [] = return ([], co) +pushCoArgs fun_ty co (arg:args) = do + { (arg', m_co1) <- pushCoArg fun_ty co arg + ; if isReflCastCo m_co1 + then return (arg':args, ReflCastCo) + else do { (args', m_co2) <- pushCoArgs (funResultTy fun_ty) m_co1 args -- TODO check type + ; return (arg':args', m_co2) } + } + +pushCoArg :: Type -> CastCoercion -> CoreArg -> Maybe (CoreArg, CastCoercion) -- We have (fun |> co) arg, and we want to transform it to -- (fun arg) |> co -- This may fail, e.g. if (fun :: N) where N is a newtype -- C.f. simplCast in GHC.Core.Opt.Simplify -- 'co' is always Representational -pushCoArg co arg +pushCoArg fun_ty co arg | Type ty <- arg - = do { (ty', m_co') <- pushCoTyArg co ty + = do { (ty', m_co') <- pushCastCoTyArg co ty ; return (Type ty', m_co') } | otherwise - = do { (arg_mco, m_co') <- pushCoValArg co - ; let arg_mco' = checkReflexiveMCo arg_mco - -- checkReflexiveMCo: see Note [Check for reflexive casts in eta expansion] + = do { (arg_mco, m_co') <- pushCastCoValArg fun_ty co + ; let arg_mco' = checkReflexiveCastCo (funArgTy fun_ty) arg_mco + -- checkReflexiveCastCo: see Note [Check for reflexive casts in eta expansion] -- The coercion is very often (arg_co -> res_co), but without -- the argument coercion actually being ReflCo - ; return (arg `mkCastMCo` arg_mco', m_co') } + ; return (arg `mkCastCo` arg_mco', m_co') } + +pushCastCoTyArg :: CastCoercion -> Type -> Maybe (Type, CastCoercion) +pushCastCoTyArg (CCoercion co) ty = pushCoTyArg co ty +pushCastCoTyArg ReflCastCo ty = Just (ty, ReflCastCo) +pushCastCoTyArg (ZCoercion _fun_ty _cos) _ty = Nothing -- TODO do better -pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR) +pushCoTyArg :: CoercionR -> Type -> Maybe (Type, CastCoercion) -- We have (fun |> co) @ty -- Push the coercion through to return -- (fun @ty') |> co' -- 'co' is always Representational --- If the returned coercion is Nothing, then it would have been reflexive; --- it's faster not to compute it, though. pushCoTyArg co ty -- The following is inefficient - don't do `eqType` here, the coercion -- optimizer will take care of it. See #14737. @@ -2917,11 +2916,11 @@ pushCoTyArg co ty -- -- = Just (ty, Nothing) | isReflCo co - = Just (ty, MRefl) + = Just (ty, ReflCastCo) | isForAllTy_ty tyL = assertPpr (isForAllTy_ty tyR) (ppr co $$ ppr ty) $ - Just (ty `mkCastTy` co1, MCo co2) + Just (ty `mkCastTy` co1, CCoercion co2) | otherwise = Nothing @@ -2941,6 +2940,18 @@ pushCoTyArg co ty -- co2 :: ty1[ (ty|>co1)/a1 ] ~R ty2[ ty/a2 ] -- Arg of mkInstCo is always nominal, hence Nominal +pushCastCoValArg :: Type -> CastCoercion -> Maybe (CastCoercion, CastCoercion) +pushCastCoValArg _ ReflCastCo = Just (ReflCastCo, ReflCastCo) +pushCastCoValArg _ (CCoercion co) = pushCoValArg co +pushCastCoValArg tyL (ZCoercion tyR cos) + | isFunTy tyL -- TODO: do we need to check this or can we assume it? + , isFunTy tyR + , typeHasFixedRuntimeRep new_arg_ty + = Just (ZCoercion new_arg_ty cos, ZCoercion (funResultTy tyR) cos) + | otherwise = Nothing + where + new_arg_ty = funArgTy tyR + -- | If @pushCoValArg co = Just (co_arg, co_res)@, then -- -- > (\x.body) |> co = (\y. let { x = y |> co_arg } in body) |> co_res) @@ -2952,7 +2963,7 @@ pushCoTyArg co ty -- If the LHS is well-typed, then so is the RHS. In particular, the argument -- @arg |> co_arg@ is guaranteed to have a fixed 'RuntimeRep', in the sense of -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -pushCoValArg :: CoercionR -> Maybe (MCoercionR, MCoercionR) +pushCoValArg :: CoercionR -> Maybe (CastCoercion, CastCoercion) pushCoValArg co -- The following is inefficient - don't do `eqType` here, the coercion -- optimizer will take care of it. See #14737. @@ -2960,7 +2971,7 @@ pushCoValArg co -- -- = Just (mkRepReflCo arg, Nothing) | isReflCo co - = Just (MRefl, MRefl) + = Just (ReflCastCo, ReflCastCo) | isFunTy tyL , (_, co1, co2) <- decomposeFunCo co @@ -2979,8 +2990,8 @@ pushCoValArg co (vcat [ text "co:" <+> ppr co , text "old_arg_ty:" <+> ppr old_arg_ty , text "new_arg_ty:" <+> ppr new_arg_ty ]) $ - Just (coToMCo (mkSymCo co1), coToMCo co2) - -- Critically, coToMCo to checks for ReflCo; the whole coercion may not + Just (coToCastCo (mkSymCo co1), coToCastCo co2) + -- Critically, coToCastCo to checks for ReflCo; the whole coercion may not -- be reflexive, but either of its components might be -- We could use isReflexiveCo, but it's not clear if the benefit -- is worth the cost, and it makes no difference in #18223 @@ -2993,13 +3004,14 @@ pushCoValArg co Pair tyL tyR = coercionKind co pushCoercionIntoLambda - :: HasDebugCallStack => Subst -> InVar -> InExpr -> OutCoercionR -> Maybe (OutVar, OutExpr) + :: HasDebugCallStack => Subst -> InVar -> InExpr -> OutCastCoercion -> Maybe (OutVar, OutExpr) -- This implements the Push rule from the paper on coercions -- (\x. e) |> co -- ===> -- (\x'. e |> co') -pushCoercionIntoLambda subst x e co +pushCoercionIntoLambda subst x e cco | assert (not (isTyVar x) && not (isCoVar x)) True + , CCoercion co <- cco -- AMG TODO: support for other CastCoercions , Pair s1s2 t1t2 <- coercionKind co , Just {} <- splitFunTy_maybe s1s2 , Just (_, w1, t1,_t2) <- splitFunTy_maybe t1t2 @@ -3024,7 +3036,7 @@ pushCoercionIntoLambda subst x e co | otherwise = Nothing -pushCoDataCon :: DataCon -> [CoreExpr] -> MCoercionR +pushCoDataCon :: DataCon -> [CoreExpr] -> CastCoercion -> Maybe (DataCon , [Type] -- Universal type args , [CoreExpr]) -- All other args incl existentials @@ -3034,8 +3046,9 @@ pushCoDataCon :: DataCon -> [CoreExpr] -> MCoercionR -- where co :: (T t1 .. tn) ~ (T s1 .. sn) -- The left-hand one must be a T, because exprIsConApp returned True -- but the right-hand one might not be. (Though it usually will.) -pushCoDataCon dc dc_args MRefl = Just $! (push_dc_refl dc dc_args) -pushCoDataCon dc dc_args (MCo co) = push_dc_gen dc dc_args co (coercionKind co) +pushCoDataCon dc dc_args ReflCastCo = Just $! (push_dc_refl dc dc_args) +pushCoDataCon dc dc_args (CCoercion co) = push_dc_gen dc dc_args co (coercionKind co) +pushCoDataCon _dc _dc_args (ZCoercion _ty _cos) = Nothing -- AMG TODO: pushCoDataCon push_dc_refl :: DataCon -> [CoreExpr] -> (DataCon, [Type], [CoreExpr]) push_dc_refl dc dc_args ===================================== compiler/GHC/Core/Opt/OccurAnal.hs ===================================== @@ -36,11 +36,11 @@ import GHC.Prelude hiding ( head, init, last, tail ) import GHC.Core import GHC.Core.FVs import GHC.Core.Utils ( exprIsTrivial, isDefaultAlt, isExpandableApp, - mkCastMCo, mkTicks ) + mkCastCo, mkTicks ) import GHC.Core.Opt.Arity ( joinRhsArity, isOneShotBndr ) import GHC.Core.Coercion import GHC.Core.Type -import GHC.Core.TyCo.FVs ( tyCoVarsOfMCo, coVarsOfCastCo ) +import GHC.Core.TyCo.FVs ( coVarsOfCastCo ) import GHC.Data.Maybe( orElse ) import GHC.Data.Graph.Directed ( SCC(..), Node(..) @@ -2853,7 +2853,7 @@ data OccEnv -- If x :-> (y, co) is in the env, -- then please replace x by (y |> mco) -- Invariant of course: idType x = exprType (y |> mco) - , occ_bs_env :: !(IdEnv (OutId, MCoercion)) + , occ_bs_env :: !(IdEnv (OutId, CastCoercion)) -- Domain is Global and Local Ids -- Range is just Local Ids , occ_bs_rng :: !VarSet @@ -3455,7 +3455,7 @@ addBndrSwap scrut case_bndr -- Do not add [x :-> x] to occ_bs_env, else lookupBndrSwap will loop = env { occ_bs_env = extendVarEnv swap_env scrut_var (case_bndr', mco) , occ_bs_rng = rng_vars `extendVarSet` case_bndr' - `unionVarSet` tyCoVarsOfMCo mco } + `unionVarSet` tyCoVarsOfCastCo mco } | otherwise = env @@ -3466,7 +3466,7 @@ addBndrSwap scrut case_bndr -- | See bBinderSwaOk. data BinderSwapDecision = NoBinderSwap - | DoBinderSwap OutVar MCoercion + | DoBinderSwap OutVar CastCoercion scrutOkForBinderSwap :: OutExpr -> BinderSwapDecision -- If (scrutOkForBinderSwap e = DoBinderSwap v mco, then @@ -3479,8 +3479,8 @@ scrutOkForBinderSwap :: OutExpr -> BinderSwapDecision scrutOkForBinderSwap e = case e of Tick _ e -> scrutOkForBinderSwap e -- Drop ticks - Var v -> DoBinderSwap v MRefl - Cast (Var v) co -> DoBinderSwap v (MCo (mkSymCo (castCoToCo (idType v) co))) -- TODO: can we do better? + Var v -> DoBinderSwap v ReflCastCo + Cast (Var v) co -> DoBinderSwap v (mkSymCastCo (idType v) co) -- Cast: see Note [Case of cast] _ -> NoBinderSwap @@ -3495,7 +3495,7 @@ lookupBndrSwap env@(OccEnv { occ_bs_env = bs_env }) bndr -- Why do we iterate here? -- See (BS2) in Note [The binder-swap substitution] case lookupBndrSwap env bndr1 of - (fun, fun_id) -> (mkCastMCo fun mco, fun_id) } + (fun, fun_id) -> (mkCastCo fun mco, fun_id) } {- Historical note [Proxy let-bindings] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Core/Opt/Simplify/Iteration.hs ===================================== @@ -19,6 +19,7 @@ import GHC.Core.Opt.Simplify.Monad import GHC.Core.Opt.ConstantFold import GHC.Core.Type hiding ( substCo, substTy, substTyVar, extendTvSubst, extendCvSubst ) import GHC.Core.TyCo.Compare( eqType ) +import GHC.Core.TyCo.Subst ( substCoVarSet ) import GHC.Core.Opt.Simplify.Env import GHC.Core.Opt.Simplify.Inline import GHC.Core.Opt.Simplify.Utils @@ -36,7 +37,7 @@ import GHC.Core.Unfold import GHC.Core.Unfold.Make import GHC.Core.Utils import GHC.Core.Opt.Arity ( ArityType, exprArity, arityTypeBotSigs_maybe - , pushCoTyArg, pushCoValArg, exprIsDeadEnd + , pushCastCoTyArg, pushCastCoValArg, exprIsDeadEnd , typeArity, arityTypeArity, etaExpandAT ) import GHC.Core.SimpleOpt ( exprIsConApp_maybe, joinPointBinding_maybe, joinPointBindings_maybe ) import GHC.Core.FVs ( mkRuleInfo {- exprsFreeIds -} ) @@ -54,6 +55,7 @@ import GHC.Types.Unique ( hasKey ) import GHC.Types.Basic import GHC.Types.Tickish import GHC.Types.Var ( isTyCoVar ) +import GHC.Types.Var.Set import GHC.Builtin.Types.Prim( realWorldStatePrimTy ) import GHC.Builtin.Names( runRWKey, seqHashKey ) @@ -1361,6 +1363,15 @@ simplCoercion env co subst = getTCvSubst env opts = seOptCoercionOpts env +simplCastCoercion :: SimplEnv -> InType -> InCastCoercion -> SimplM (OutType, OutCastCoercion) +simplCastCoercion env _ (CCoercion co) = (\co -> (coercionLKind co, CCoercion co)) <$> simplCoercion env co +simplCastCoercion env tyL (ZCoercion tyR cos) = (,) <$> simplType env tyL <*> (ZCoercion <$> simplType env tyR <*> simplCoVars env cos) +simplCastCoercion env tyL ReflCastCo = (,) <$> simplType env tyL <*> pure ReflCastCo + +simplCoVars :: SimplEnv -> CoVarSet -> SimplM CoVarSet +simplCoVars env covars = pure $ substCoVarSet (getTCvSubst env) covars + + ----------------------------------- -- | Push a TickIt context outwards past applications and cases, as -- long as this is a non-scoping tick, to let case and application @@ -1531,10 +1542,10 @@ rebuild_go env expr cont Stop {} -> return (emptyFloats env, expr) TickIt t cont -> rebuild_go env (mkTick t expr) cont CastIt { sc_co = co, sc_opt = opt, sc_cont = cont } - -> rebuild_go env (mkCast expr co') cont + -> rebuild_go env (mkCastCo expr co') cont -- NB: mkCast implements the (Coercion co |> g) optimisation where - co' = optOutCoercion env co opt + co' = optOutCastCoercion env co opt Select { sc_bndr = bndr, sc_alts = alts, sc_env = se, sc_cont = cont } -> rebuildCase (se `setInScopeFromE` env) expr bndr alts cont @@ -1663,6 +1674,12 @@ on each successive composition -- that's at least quadratic. So: -} +optOutCastCoercion :: SimplEnvIS -> OutCastCoercion -> Bool -> OutCastCoercion +optOutCastCoercion env cco already_optimised = case cco of + ReflCastCo -> ReflCastCo + CCoercion co -> CCoercion (optOutCoercion env co already_optimised) + ZCoercion{} -> cco + optOutCoercion :: SimplEnvIS -> OutCoercion -> Bool -> OutCoercion -- See Note [Avoid re-simplifying coercions] optOutCoercion env co already_optimised @@ -1675,72 +1692,74 @@ optOutCoercion env co already_optimised simplCast :: SimplEnv -> InExpr -> InCastCoercion -> SimplCont -> SimplM (SimplFloats, OutExpr) simplCast env body co0 cont0 - = do { co1 <- {-#SCC "simplCast-simplCoercion" #-} simplCoercion env (castCoToCo (exprType body) co0) -- TODO better way? + = do { (tyL, co1) <- {-#SCC "simplCast-simplCoercion" #-} simplCastCoercion env (exprType body) co0 ; cont1 <- {-#SCC "simplCast-addCoerce" #-} - if isReflCo co1 + if isReflCastCo co1 then return cont0 -- See Note [Optimising reflexivity] - else addCoerce co1 True cont0 + else addCoerce tyL co1 True cont0 -- True <=> co1 is optimised ; {-#SCC "simplCast-simplExprF" #-} simplExprF env body cont1 } where -- If the first parameter is MRefl, then simplifying revealed a -- reflexive coercion. Omit. - addCoerceM :: MOutCoercion -> Bool -> SimplCont -> SimplM SimplCont - addCoerceM MRefl _ cont = return cont - addCoerceM (MCo co) opt cont = addCoerce co opt cont - - addCoerce :: OutCoercion -> Bool -> SimplCont -> SimplM SimplCont - addCoerce co1 _ (CastIt { sc_co = co2, sc_cont = cont }) -- See Note [Optimising reflexivity] - = addCoerce (mkTransCo co1 co2) False cont + -- TODO: probably can simplify this further now? + addCoerceM :: OutType -> OutCastCoercion -> Bool -> SimplCont -> SimplM SimplCont + addCoerceM _ ReflCastCo _ cont = return cont + addCoerceM tyL co opt cont = addCoerce tyL co opt cont + + -- Type tyL is the coercionLKind of the coercion + addCoerce :: OutType -> OutCastCoercion -> Bool -> SimplCont -> SimplM SimplCont + addCoerce tyL co1 _ (CastIt { sc_co = co2, sc_cont = cont }) -- See Note [Optimising reflexivity] + = addCoerce tyL (mkTransCastCo co1 co2) False cont -- False: (mkTransCo co1 co2) is not fully optimised -- See Note [Avoid re-simplifying coercions] - addCoerce co co_is_opt (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail }) - | Just (arg_ty', m_co') <- pushCoTyArg co arg_ty + addCoerce tyL co co_is_opt (ApplyToTy { sc_arg_ty = arg_ty, sc_hole_ty = hole_ty, sc_cont = tail }) + | Just (arg_ty', m_co') <- pushCastCoTyArg co arg_ty = {-#SCC "addCoerce-pushCoTyArg" #-} - do { tail' <- addCoerceM m_co' co_is_opt tail + do { tail' <- addCoerceM hole_ty m_co' co_is_opt tail -- TODO is hole_ty right? ; return (ApplyToTy { sc_arg_ty = arg_ty' , sc_cont = tail' - , sc_hole_ty = coercionLKind co }) } + , sc_hole_ty = tyL }) } -- NB! As the cast goes past, the -- type of the hole changes (#16312) -- (f |> co) e ===> (f (e |> co1)) |> co2 -- where co :: (s1->s2) ~ (t1->t2) -- co1 :: t1 ~ s1 -- co2 :: s2 ~ t2 - addCoerce co co_is_opt cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se + addCoerce tyL co co_is_opt cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se , sc_dup = dup, sc_cont = tail , sc_hole_ty = fun_ty }) | not co_is_opt -- pushCoValArg duplicates the coercion, so optimise first - = addCoerce (optOutCoercion (zapSubstEnv env) co co_is_opt) True cont + = addCoerce tyL (optOutCastCoercion (zapSubstEnv env) co co_is_opt) True cont - | Just (m_co1, m_co2) <- pushCoValArg co + | Just (m_co1, m_co2) <- pushCastCoValArg fun_ty co -- TODO check fun_ty = {-#SCC "addCoerce-pushCoValArg" #-} - do { tail' <- addCoerceM m_co2 co_is_opt tail - ; case m_co1 of { - MRefl -> return (cont { sc_cont = tail' - , sc_hole_ty = coercionLKind co }) ; + do { tail' <- addCoerceM (funResultTy fun_ty) m_co2 co_is_opt tail -- TODO check funResultTy fun_ty + ; if isReflCastCo m_co1 + then return (cont { sc_cont = tail' + , sc_hole_ty = tyL }) ; -- See Note [Avoiding simplifying repeatedly] - MCo co1 -> + else do { (dup', arg_se', arg') <- simplLazyArg env dup fun_ty Nothing arg_se arg -- When we build the ApplyTo we can't mix the OutCoercion -- 'co' with the InExpr 'arg', so we simplify -- to make it all consistent. It's a bit messy. -- But it isn't a common case. -- Example of use: #995 - ; return (ApplyToVal { sc_arg = mkCast arg' co1 + ; return (ApplyToVal { sc_arg = mkCastCo arg' m_co1 , sc_env = arg_se' , sc_dup = dup' , sc_cont = tail' - , sc_hole_ty = coercionLKind co }) } } } + , sc_hole_ty = tyL }) } } - addCoerce co co_is_opt cont - | isReflCo co = return cont -- Having this at the end makes a huge + addCoerce tyL co co_is_opt cont + | isReflCastCo co = return cont -- Having this at the end makes a huge -- difference in T12227, for some reason -- See Note [Optimising reflexivity] - | otherwise = return (CastIt { sc_co = co, sc_opt = co_is_opt, sc_cont = cont }) + | otherwise = return (CastIt { sc_co = co, sc_hole_ty = tyL, sc_opt = co_is_opt, sc_cont = cont }) simplLazyArg :: SimplEnvIS -- ^ Used only for its InScopeSet -> DupFlag @@ -3595,9 +3614,9 @@ addAltUnfoldings env case_bndr bndr_swap con_app -- See Note [Add unfolding for scrutinee] env2 | DoBinderSwap v mco <- bndr_swap = addBinderUnfolding env1 v $ - if isReflMCo mco -- isReflMCo: avoid calling mk_simple_unf + if isReflCastCo mco -- isReflCastCo: avoid calling mk_simple_unf then con_app_unf -- twice in the common case - else mk_simple_unf (mkCastMCo con_app mco) + else mk_simple_unf (mkCastCo con_app mco) | otherwise = env1 @@ -3865,9 +3884,10 @@ mkDupableContWithDmds env _ cont mkDupableContWithDmds _ _ (Stop {}) = panic "mkDupableCont" -- Handled by previous eqn -mkDupableContWithDmds env dmds (CastIt { sc_co = co, sc_opt = opt, sc_cont = cont }) +mkDupableContWithDmds env dmds (CastIt { sc_co = co, sc_hole_ty = ty, sc_opt = opt, sc_cont = cont }) = do { (floats, cont') <- mkDupableContWithDmds env dmds cont - ; return (floats, CastIt { sc_co = optOutCoercion env co opt + ; return (floats, CastIt { sc_co = optOutCastCoercion env co opt + , sc_hole_ty = ty , sc_opt = True, sc_cont = cont' }) } -- optOutCoercion: see Note [Avoid re-simplifying coercions] ===================================== compiler/GHC/Core/Opt/Simplify/Utils.hs ===================================== @@ -52,7 +52,7 @@ import GHC.Core.Opt.Simplify.Inline( smallEnoughToInline ) import GHC.Core.Opt.Stats ( Tick(..) ) import qualified GHC.Core.Subst import GHC.Core.Ppr -import GHC.Core.TyCo.Ppr ( pprParendType ) +import GHC.Core.TyCo.Ppr ( pprParendType, pprCastCo ) import GHC.Core.FVs import GHC.Core.Utils import GHC.Core.Opt.Arity @@ -162,8 +162,9 @@ data SimplCont | CastIt -- (CastIt co K)[e] = K[ e `cast` co ] - { sc_co :: OutCoercion -- The coercion simplified + { sc_co :: OutCastCoercion -- The coercion simplified -- Invariant: never an identity coercion + , sc_hole_ty :: OutType -- LHS kind of sc_co , sc_opt :: Bool -- True <=> sc_co has had optCoercion applied to it -- See Note [Avoid re-simplifying coercions] -- in GHC.Core.Opt.Simplify.Iteration @@ -277,7 +278,7 @@ instance Outputable SimplCont where where pps = [ppr interesting] ++ [ppr eval_sd | eval_sd /= topSubDmd] ppr (CastIt { sc_co = co, sc_cont = cont }) - = (text "CastIt" <+> pprOptCo co) $$ ppr cont + = (text "CastIt" <+> pprCastCo co) $$ ppr cont ppr (TickIt t cont) = (text "TickIt" <+> ppr t) $$ ppr cont ppr (ApplyToTy { sc_arg_ty = ty, sc_cont = cont }) @@ -474,7 +475,7 @@ contResultType (TickIt _ k) = contResultType k contHoleType :: SimplCont -> OutType contHoleType (Stop ty _ _) = ty contHoleType (TickIt _ k) = contHoleType k -contHoleType (CastIt { sc_co = co }) = coercionLKind co +contHoleType (CastIt { sc_hole_ty = ty }) = ty contHoleType (StrictBind { sc_bndr = b, sc_dup = dup, sc_env = se }) = perhapsSubstTy dup se (idType b) contHoleType (StrictArg { sc_fun_ty = ty }) = funArgTy ty @@ -1896,7 +1897,7 @@ rebuildLam env bndrs@(bndr:_) body cont | -- Note [Casts and lambdas] seCastSwizzle env , not (any bad bndrs) - = mkCast (mk_lams bndrs body) (mkPiCos Representational bndrs (castCoToCo (exprType body) co)) + = mkCastCo (mk_lams bndrs body) (mkPiCastCos Representational bndrs co) where co_vars = tyCoVarsOfCastCo co bad bndr = isCoVar bndr && bndr `elemVarSet` co_vars ===================================== compiler/GHC/Core/Opt/SpecConstr.hs ===================================== @@ -1120,7 +1120,7 @@ extendCaseBndrs env scrut case_bndr con alt_bndrs where live_case_bndr = not (isDeadBinder case_bndr) env1 | DoBinderSwap v mco <- scrutOkForBinderSwap scrut - , isReflMCo mco = extendValEnv env v cval + , isReflCastCo mco = extendValEnv env v cval | otherwise = env -- See Note [Add scrutinee to ValueEnv too] env2 | live_case_bndr = extendValEnv env1 case_bndr cval | otherwise = env1 ===================================== compiler/GHC/Core/Rules.hs ===================================== @@ -52,13 +52,14 @@ import GHC.Core.FVs ( exprFreeVars, bindFreeVars , rulesFreeVarsDSet, orphNamesOfExprs ) import GHC.Core.Utils ( exprType, mkTick, mkTicks , stripTicksTopT, stripTicksTopE - , isJoinBind, mkCastMCo ) + , isJoinBind, mkCastCo ) import GHC.Core.Ppr ( pprRules ) import GHC.Core.Unify as Unify ( ruleMatchTyKiX ) import GHC.Core.Type as Type ( Type, extendTvSubst, extendCvSubst , substTy, getTyVar_maybe ) import GHC.Core.TyCo.Ppr( pprParendType ) +import GHC.Core.TyCo.FVs ( tyCoFVsOfCastCoercion ) import GHC.Core.Coercion as Coercion import GHC.Core.Tidy ( tidyRules ) import GHC.Core.Map.Expr ( eqCoreExpr ) @@ -815,7 +816,7 @@ match_exprs :: HasDebugCallStack match_exprs _ subst [] _ = Just subst match_exprs renv subst (e1:es1) (e2:es2) - = do { subst' <- match renv subst e1 e2 MRefl + = do { subst' <- match renv subst e1 e2 ReflCastCo ; match_exprs renv subst' es1 es2 } match_exprs _ _ _ _ = Nothing @@ -1065,7 +1066,7 @@ match :: HasDebugCallStack -> RuleSubst -- Substitution applies to template only -> CoreExpr -- Template -> CoreExpr -- Target - -> MCoercion + -> CastCoercion -> Maybe RuleSubst -- Postcondition (TypeInv): if matching succeeds, then @@ -1102,8 +1103,8 @@ match renv subst (Type ty1) (Type ty2) _mco ------------------------ Coercions --------------------- -- See Note [Coercion arguments] for why this isn't really right -match renv subst (Coercion co1) (Coercion co2) MRefl - = match_co renv subst co1 co2 +match renv subst (Coercion co1) (Coercion co2) ReflCastCo + = match_co renv subst (CCoercion co1) (CCoercion co2) -- TODO should probably have match_cast_co and match_co separately? -- The MCo case corresponds to matching co ~ (co2 |> co3) -- and I have no idea what to do there -- or even if it can occur -- Failing seems the simplest thing to do; it's certainly safe. @@ -1114,23 +1115,23 @@ match renv subst (Coercion co1) (Coercion co2) MRefl -- Note [Cancel reflexive casts] match renv subst e1 (Cast e2 co2) mco - = match renv subst e1 e2 (checkReflexiveMCo (mkTransMCoR (castCoToCo (exprType e2) co2) mco)) + = match renv subst e1 e2 (checkReflexiveCastCo (exprType e2) (mkTransCastCo co2 mco)) -- checkReflexiveMCo: cancel casts if possible -- This is important: see Note [Cancel reflexive casts] match renv subst (Cast e1 co1) e2 mco - = matchTemplateCast renv subst e1 (castCoToCo (exprType e1) co1) e2 mco + = matchTemplateCast renv subst e1 co1 e2 mco ------------------------ Literals --------------------- match _ subst (Lit lit1) (Lit lit2) mco | lit1 == lit2 - = assertPpr (isReflMCo mco) (ppr mco) $ + = assertPpr (isReflCastCo mco) (ppr mco) $ Just subst ------------------------ Variables --------------------- -- The Var case follows closely what happens in GHC.Core.Unify.match match renv subst (Var v1) e2 mco - = match_var renv subst v1 (mkCastMCo e2 mco) + = match_var renv subst v1 (mkCastCo e2 mco) match renv subst e1 (Var v2) mco -- Note [Expanding variables] | not (inRnEnvR rn_env v2) -- Note [Do not expand locally-bound variables] @@ -1148,7 +1149,7 @@ match renv subst e1 (Var v2) mco -- Note [Expanding variables] -- See Note [Matching higher order patterns] match renv@(RV { rv_tmpls = tmpls, rv_lcl = rn_env }) subst e1@App{} e2 - MRefl -- Like the App case we insist on Refl here + ReflCastCo -- Like the App case we insist on Refl here -- See Note [Casts in the target] | (Var f, args) <- collectArgs e1 , let f' = rnOccL rn_env f -- See similar rnOccL in match_var @@ -1308,9 +1309,9 @@ Two wrinkles: -- (e1 e2) ~ (d1 d2) |> co -- See Note [Cancel reflexive casts]: in the Cast equations for 'match' -- we aggressively ensure that if MCo is reflective, it really is MRefl. -match renv subst (App f1 a1) (App f2 a2) MRefl - = do { subst' <- match renv subst f1 f2 MRefl - ; match renv subst' a1 a2 MRefl } +match renv subst (App f1 a1) (App f2 a2) ReflCastCo + = do { subst' <- match renv subst f1 f2 ReflCastCo + ; match renv subst' a1 a2 ReflCastCo } ------------------------ Float lets --------------------- match renv subst e1 (Let bind e2) mco @@ -1336,7 +1337,7 @@ match renv subst e1 (Let bind e2) mco ------------------------ Lambdas --------------------- match renv subst (Lam x1 e1) e2 mco - | let casted_e2 = mkCastMCo e2 mco + | let casted_e2 = mkCastCo e2 mco in_scope = extendInScopeSetSet (rnInScopeSet (rv_lcl renv)) (exprFreeVars casted_e2) in_scope_env = ISE in_scope (rv_unf renv) @@ -1349,7 +1350,7 @@ match renv subst (Lam x1 e1) e2 mco -- See Note [Lambdas in the template] = let renv' = rnMatchBndr2 renv x1 x2 subst' = subst { rs_binds = rs_binds subst . flip (foldr mkTick) ts } - in match renv' subst' e1 e2' MRefl + in match renv' subst' e1 e2' ReflCastCo match renv subst e1 e2@(Lam {}) mco | Just (renv', e2') <- eta_reduce renv e2 -- See Note [Eta reduction in the target] @@ -1400,7 +1401,7 @@ match renv (tv_subst, id_subst, binds) e1 match renv subst (Case e1 x1 ty1 alts1) (Case e2 x2 ty2 alts2) mco = do { subst1 <- match_ty renv subst ty1 ty2 - ; subst2 <- match renv subst1 e1 e2 MRefl + ; subst2 <- match renv subst1 e1 e2 ReflCastCo ; let renv' = rnMatchBndr2 renv x1 x2 ; match_alts renv' subst2 alts1 alts2 mco -- Alts are both sorted } @@ -1503,29 +1504,29 @@ Hence ------------- matchTemplateCast :: RuleMatchEnv -> RuleSubst - -> CoreExpr -> Coercion - -> CoreExpr -> MCoercion + -> CoreExpr -> CastCoercion + -> CoreExpr -> CastCoercion -> Maybe RuleSubst matchTemplateCast renv subst e1 co1 e2 mco | isEmptyVarSet $ fvVarSet $ filterFV (`elemVarSet` rv_tmpls renv) $ -- Check that the coercion does not - tyCoFVsOfCo substed_co -- mention any of the template variables + tyCoFVsOfCastCoercion substed_co -- mention any of the template variables = -- This is the good path -- See Note [Casts in the template] wrinkle (CT0) - match renv subst e1 e2 (checkReflexiveMCo (mkTransMCoL mco (mkSymCo substed_co))) + match renv subst e1 e2 (checkReflexiveCastCo substed_ty (mkTransCastCo mco (mkSymCastCo substed_ty substed_co))) + -- AMG TODO: should be able to make checkReflexiveCastCo cheaper here? | otherwise = -- This is the Deeply Suspicious Path -- See Note [Casts in the template] - do { let co2 = case mco of - MRefl -> mkRepReflCo (exprType e2) - MCo co2 -> co2 + do { let co2 = mco ; subst1 <- match_co renv subst co1 co2 -- If match_co succeeds, then (exprType e1) = (exprType e2) - -- Hence the MRefl in the next line - ; match renv subst1 e1 e2 MRefl } + -- Hence the ReflCastCo in the next line + ; match renv subst1 e1 e2 ReflCastCo } where - substed_co = substCo current_subst co1 + substed_ty = substTy current_subst (exprType e1) + substed_co = substCastCo current_subst co1 current_subst :: Subst current_subst = mkTCvSubst (rnInScopeSet (rv_lcl renv)) @@ -1538,8 +1539,8 @@ matchTemplateCast renv subst e1 co1 e2 mco match_co :: RuleMatchEnv -> RuleSubst - -> Coercion - -> Coercion + -> CastCoercion + -> CastCoercion -> Maybe RuleSubst -- We only match if the template is a coercion variable or Refl: -- see Note [Casts in the template] @@ -1548,7 +1549,7 @@ match_co :: RuleMatchEnv -- But if match_co succeeds, it /is/ guaranteed that -- coercionKind (subst template) = coercionKind target -match_co renv subst co1 co2 +match_co renv subst (CCoercion co1) (CCoercion co2) | Just cv <- getCoVar_maybe co1 = match_var renv subst cv (Coercion co2) @@ -1563,6 +1564,7 @@ match_co renv subst co1 co2 | otherwise = Nothing +match_co _renv _subst _ _ = Nothing -- TODO: support non-CCoercions in rule matcher ------------- rnMatchBndr2 :: RuleMatchEnv -> Var -> Var -> RuleMatchEnv @@ -1575,7 +1577,7 @@ rnMatchBndr2 renv x1 x2 match_alts :: RuleMatchEnv -> RuleSubst -> [CoreAlt] -- Template - -> [CoreAlt] -> MCoercion -- Target + -> [CoreAlt] -> CastCoercion -- Target -> Maybe RuleSubst match_alts _ subst [] [] _ = return subst @@ -2018,7 +2020,7 @@ ruleAppCheck_help env fn args rules mismatches = [i | (rule_arg, (arg,i)) <- rule_args `zip` i_args, not (isJust (match_fn rule_arg arg))] - match_fn rule_arg arg = match renv emptyRuleSubst rule_arg arg MRefl + match_fn rule_arg arg = match renv emptyRuleSubst rule_arg arg ReflCastCo where renv = RV { rv_lcl = mkRnEnv2 in_scope , rv_tmpls = mkVarSet rule_bndrs ===================================== compiler/GHC/Core/SimpleOpt.hs ===================================== @@ -31,8 +31,8 @@ import GHC.Core.Unfold.Make import GHC.Core.Make ( FloatBind(..), mkWildValBinder ) import GHC.Core.Opt.OccurAnal( occurAnalyseExpr, occurAnalysePgm, zapLambdaBndrs ) import GHC.Core.DataCon -import GHC.Core.Coercion.Opt ( optCoercion, OptCoercionOpts (..) ) -import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList +import GHC.Core.Coercion.Opt ( optCoercion, optCastCoercion, OptCoercionOpts (..) ) +import GHC.Core.Type hiding ( extendTvSubst, extendCvSubst, extendTvSubstList , isInScope, substTyVarBndr, cloneTyVarBndr ) import GHC.Core.Predicate( isCoVarType ) import GHC.Core.Coercion hiding ( substCo, substCoVarBndr ) @@ -213,7 +213,7 @@ simpleOptPgm opts this_mod binds rules = ---------------------- type SimpleClo = (SimpleOptEnv, InExpr) -data SimpleContItem = ApplyToArg SimpleClo | CastIt OutCoercion +data SimpleContItem = ApplyToArg SimpleClo | CastIt OutCastCoercion instance Outputable SimpleContItem where ppr (ApplyToArg (_, arg)) = text "ARG" <+> ppr arg @@ -402,7 +402,7 @@ simple_app env e0@(Lam {}) as0@(_:_) = rebuild_app env (simple_opt_expr env e) as do_beta env (Cast e co) as = - do_beta env e (add_cast env (castCoToCo (exprType e) co) as) -- TODO eliminate castCoToCo? + do_beta env e (add_cast env (exprType e) co as) do_beta env body as = simple_app env body as @@ -450,21 +450,21 @@ simple_app env (Let bind body) args expr' = Let bind' (simple_opt_expr env' body) simple_app env (Cast e co) as - = simple_app env e (add_cast env (castCoToCo (exprType e) co) as) -- TODO eliminate castCoToCo? + = simple_app env e (add_cast env (exprType e) co as) simple_app env e as = rebuild_app env (simple_opt_expr env e) as -add_cast :: SimpleOptEnv -> InCoercion -> [SimpleContItem] -> [SimpleContItem] -add_cast env co1 as - | isReflCo co1' +add_cast :: SimpleOptEnv -> InType -> InCastCoercion -> [SimpleContItem] -> [SimpleContItem] +add_cast env tyL co1 as + | isReflCastCo co1' = as | otherwise = case as of - CastIt co2:rest -> CastIt (co1' `mkTransCo` co2):rest + CastIt co2:rest -> CastIt (co1' `mkTransCastCo` co2):rest _ -> CastIt co1':as where - co1' = optCoercion (so_co_opts (soe_opts env)) (soe_subst env) co1 + co1' = optCastCoercion (so_co_opts (soe_opts env)) (soe_subst env) tyL co1 rebuild_app :: HasDebugCallStack => SimpleOptEnv -> OutExpr -> [SimpleContItem] -> OutExpr @@ -473,7 +473,7 @@ rebuild_app env fun args = foldl mk_app fun args in_scope = soeInScope env mk_app out_fun = \case ApplyToArg arg -> App out_fun (simple_opt_clo in_scope arg) - CastIt co -> mk_cast out_fun (CCoercion co) + CastIt co -> mk_cast out_fun co {- Note [Desugaring unlifted newtypes] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1340,7 +1340,7 @@ data-con wrappers, and that cure would be worse than the disease. This Note exists solely to document the problem. -} -data ConCont = CC [CoreExpr] MCoercion +data ConCont = CC [CoreExpr] CastCoercion -- Substitution already applied -- | Returns @Just ([b1..bp], dc, [t1..tk], [x1..xn])@ if the argument @@ -1362,7 +1362,7 @@ exprIsConApp_maybe :: HasDebugCallStack => InScopeEnv -> CoreExpr -> Maybe (InScopeSet, [FloatBind], DataCon, [Type], [CoreExpr]) exprIsConApp_maybe ise@(ISE in_scope id_unf) expr - = go (Left in_scope) [] expr (CC [] MRefl) + = go (Left in_scope) [] expr (CC [] ReflCastCo) where go :: Either InScopeSet Subst -- Left in-scope means "empty substitution" @@ -1375,10 +1375,10 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr go subst floats (Tick t expr) cont | not (tickishIsCode t) = go subst floats expr cont - go subst floats (Cast expr co1) (CC args m_co2) - | Just (args', m_co1') <- pushCoArgs (subst_co subst (castCoToCo (exprType expr) co1)) args + go subst floats (Cast expr co1) (CC args m_co2) -- TODO: is the subst_ty below needed? + | Just (args', m_co1') <- pushCoArgs (subst_ty subst (exprType expr)) (subst_cast_co subst co1) args -- See Note [Push coercions in exprIsConApp_maybe] - = go subst floats expr (CC args' (m_co1' `mkTransMCo` m_co2)) + = go subst floats expr (CC args' (m_co1' `mkTransCastCo` m_co2)) go subst floats (App fun arg) (CC args mco) | let arg_type = exprType arg @@ -1512,8 +1512,11 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr subst_extend_in_scope (Left in_scope) v = Left (in_scope `extendInScopeSet` v) subst_extend_in_scope (Right s) v = Right (s `extendSubstInScope` v) - subst_co (Left {}) co = co - subst_co (Right s) co = GHC.Core.Subst.substCo s co + subst_cast_co (Left {}) co = co + subst_cast_co (Right s) co = substCastCo s co + + subst_ty (Left {}) ty = ty + subst_ty (Right s) ty = substTy s ty subst_expr (Left {}) e = e subst_expr (Right s) e = substExpr s e @@ -1565,7 +1568,7 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr (right, _, _) -> pprPanic "case_bind did not preserve Left" (ppr in_scope $$ ppr arg $$ ppr right) -- See Note [exprIsConApp_maybe on literal strings] -dealWithStringLiteral :: Var -> BS.ByteString -> MCoercion +dealWithStringLiteral :: Var -> BS.ByteString -> CastCoercion -> Maybe (DataCon, [Type], [CoreExpr]) -- This is not possible with user-supplied empty literals, GHC.Core.Make.mkStringExprFS @@ -1666,13 +1669,12 @@ exprIsLambda_maybe ise (Tick t e) = Just (x, e, t:ts) -- Also possible: A casted lambda. Push the coercion inside -exprIsLambda_maybe ise@(ISE in_scope_set _) (Cast casted_e cco) +exprIsLambda_maybe ise@(ISE in_scope_set _) (Cast casted_e co) | Just (x, e,ts) <- exprIsLambda_maybe ise casted_e -- Only do value lambdas. -- this implies that x is not in scope in gamma (makes this code simpler) , not (isTyVar x) && not (isCoVar x) - , let co = castCoToCo (exprType casted_e) cco - , assert (not $ x `elemVarSet` tyCoVarsOfCo co) True + , assert (not $ x `elemVarSet` tyCoVarsOfCastCo co) True , Just (x',e') <- pushCoercionIntoLambda (mkEmptySubst in_scope_set) x e co , let res = Just (x',e',ts) = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)]) ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -21,7 +21,7 @@ module GHC.Core.TyCo.FVs shallowCoVarsOfCo, shallowCoVarsOfCos, shallowCoVarsOfCastCo, tyCoVarsOfCastCoercionDSet, tyCoVarsOfCoDSet, - tyCoFVsOfCo, tyCoFVsOfCos, tyCoFVsOfCoVarSet, + tyCoFVsOfCo, tyCoFVsOfCos, tyCoFVsOfCoVarSet, tyCoFVsOfCastCoercion, tyCoVarsOfCoList, coVarsOfCoDSet, coVarsOfCosDSet, ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -22,7 +22,7 @@ module GHC.Core.Utils ( -- * Properties of expressions exprType, coreAltType, coreAltsType, - mkLamType, mkLamTypes, + mkLamType, mkLamTypes, mkPiMCos, mkFunctionType, exprIsTrivial, getIdFromTrivialExpr, getIdFromTrivialExpr_maybe, trivial_expr_fold, @@ -188,6 +188,12 @@ mkLamType v body_ty mkLamTypes vs ty = foldr mkLamType ty vs +mkPiMCos :: [Var] -> CastCoercion -> CastCoercion +mkPiMCos _ ReflCastCo = ReflCastCo +mkPiMCos vs (CCoercion co) = CCoercion (mkPiCos Representational vs co) +mkPiMCos vs (ZCoercion ty cos) = ZCoercion (mkLamTypes vs ty) cos + + {- Note [Type bindings] ~~~~~~~~~~~~~~~~~~~~ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/58a31cb920f13c461490cdad5f63025... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/58a31cb920f13c461490cdad5f63025... You're receiving this email because of your account on gitlab.haskell.org.