Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC Commits: 6ef18f2a by Adam Gundry at 2025-11-27T08:59:21+00:00 Remove unused MOutCoercion - - - - - 7bee0604 by Adam Gundry at 2025-11-27T09:00:27+00:00 Handle ZCoercion in getCastedVar - - - - - dd8c18da by Adam Gundry at 2025-11-27T09:14:19+00:00 Handle ZCoercion in pushCoercionIntoLambda - - - - - cd9d5fb7 by Adam Gundry at 2025-11-27T09:23:59+00:00 Simplify reflexivity handling in simplCast - - - - - 6 changed files: - compiler/GHC/Core.hs - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/SimpleOpt.hs - compiler/GHC/HsToCore/Binds.hs Changes: ===================================== compiler/GHC/Core.hs ===================================== @@ -18,8 +18,7 @@ module GHC.Core ( InCastCoercion, OutId, OutBind, OutExpr, OutAlt, OutArg, OutType, OutKind, OutBndr, OutVar, OutCoercion, OutCoercionR, OutTyVar, OutCoVar, - OutTyCoVar, MOutCoercion, - OutCastCoercion, + OutTyCoVar, OutCastCoercion, -- ** 'Expr' construction mkLet, mkLets, mkLetNonRec, mkLetRec, mkLams, @@ -1133,7 +1132,6 @@ type OutBind = CoreBind type OutExpr = CoreExpr type OutAlt = CoreAlt type OutArg = CoreArg -type MOutCoercion = MCoercion type OutCastCoercion = CastCoercion ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -65,6 +65,7 @@ module GHC.Core.Coercion ( mkFunResCastCo, mkFunCastCoNoFTF, applyForAllTy, + decomposeFunCastCo, -- ** Decomposition instNewTyCon_maybe, @@ -459,6 +460,14 @@ decomposeFunCo co Pair s1t1 s2t2 = coercionKind co all_ok = isFunTy s1t1 && isFunTy s2t2 + +decomposeFunCastCo :: HasDebugCallStack => CastCoercion -> (CastCoercion, CastCoercion) +decomposeFunCastCo (CCoercion co) = let (_, arg_co, res_co) = decomposeFunCo co + in (CCoercion arg_co, CCoercion res_co) +decomposeFunCastCo ReflCastCo = (ReflCastCo, ReflCastCo) +decomposeFunCastCo (ZCoercion tyR cos) = (ZCoercion (funArgTy tyR) cos, ZCoercion (funResultTy tyR) cos) + + {- Note [Pushing a coercion into a pi-type] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have this: ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -3010,18 +3010,18 @@ pushCoValArg co Pair tyL tyR = coercionKind co pushCoercionIntoLambda - :: HasDebugCallStack => Subst -> InVar -> InExpr -> OutCastCoercion -> Maybe (OutVar, OutExpr) + :: HasDebugCallStack => Subst -> InVar -> InExpr -> Type -> OutCastCoercion -> Maybe (OutVar, OutExpr) -- This implements the Push rule from the paper on coercions -- (\x. e) |> co -- ===> -- (\x'. e |> co') -pushCoercionIntoLambda subst x e cco +pushCoercionIntoLambda subst x e ty co | 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 + , let s1s2 = castCoercionLKind ty co + , let t1t2 = castCoercionRKind ty co + , Just (_, _, s1, _) <- splitFunTy_maybe s1s2 , Just (_, w1, t1,_t2) <- splitFunTy_maybe t1t2 - , (_, co1, co2) <- decomposeFunCo co + , (co1, co2) <- decomposeFunCastCo co , typeHasFixedRuntimeRep t1 -- We can't push the coercion into the lambda if it would create -- a representation-polymorphic binder. @@ -3033,12 +3033,12 @@ pushCoercionIntoLambda subst x e cco subst' = extendIdSubst (setInScope subst in_scope') x - (mkCast (Var x') (mkSymCo co1)) + (mkCastCo (Var x') (mkSymCastCo s1 co1)) -- We substitute x' for x, except we need to preserve types. -- The types are as follows: -- x :: s1, x' :: t1, co1 :: s1 ~# t1, -- so we extend the substitution with x |-> (x' |> sym co1). - in Just (x', substExpr subst' e `mkCast` co2) + in Just (x', substExpr subst' e `mkCastCo` co2) | otherwise = Nothing ===================================== compiler/GHC/Core/Opt/Simplify/Iteration.hs ===================================== @@ -1691,20 +1691,18 @@ simplCast :: SimplEnv -> InExpr -> InCastCoercion -> SimplCont simplCast env body co0 cont0 = do { (tyL, co1) <- {-#SCC "simplCast-simplCoercion" #-} simplCastCoercion env (exprType body) co0 ; cont1 <- {-#SCC "simplCast-addCoerce" #-} - if isReflCastCo co1 - then return cont0 -- See Note [Optimising reflexivity] - else addCoerce tyL co1 True cont0 + addCoerceMaybeRefl 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. - -- 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 - + -- If simplifying revealed an obviously reflexive coercion, omit it. + -- See Note [Optimising reflexivity]. + addCoerceMaybeRefl :: OutType -> OutCastCoercion -> Bool -> SimplCont -> SimplM SimplCont + addCoerceMaybeRefl tyL co opt cont + | isReflCastCo co = return cont + | otherwise = addCoerce tyL co opt cont + + -- Here the coercion is known not to satisfy isReflCastCo. -- 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] @@ -1715,7 +1713,7 @@ simplCast env body co0 cont0 addCoerce tyL co co_is_opt (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail }) | Just (arg_ty', res_ty, m_co') <- pushCastCoTyArg tyL co arg_ty = {-#SCC "addCoerce-pushCoTyArg" #-} - do { tail' <- addCoerceM res_ty m_co' co_is_opt tail + do { tail' <- addCoerceMaybeRefl res_ty m_co' co_is_opt tail ; return (ApplyToTy { sc_arg_ty = arg_ty' , sc_cont = tail' , sc_hole_ty = tyL }) } @@ -1729,11 +1727,11 @@ simplCast env body co0 cont0 , sc_dup = dup, sc_cont = tail , sc_hole_ty = fun_ty }) | not co_is_opt -- pushCoValArg duplicates the coercion, so optimise first - = addCoerce tyL (optOutCoercion (zapSubstEnv env) tyL co co_is_opt) True cont + = addCoerceMaybeRefl tyL (optOutCoercion (zapSubstEnv env) tyL co co_is_opt) True cont | Just (_, m_co1, res_ty, m_co2) <- pushCastCoValArg tyL co = {-#SCC "addCoerce-pushCoValArg" #-} - do { tail' <- addCoerceM res_ty m_co2 co_is_opt tail + do { tail' <- addCoerceMaybeRefl res_ty m_co2 co_is_opt tail ; if isReflCastCo m_co1 then return (cont { sc_cont = tail' , sc_hole_ty = tyL }) ; @@ -1753,10 +1751,7 @@ simplCast env body co0 cont0 , sc_hole_ty = tyL }) } } 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_hole_ty = tyL, sc_opt = co_is_opt, sc_cont = cont }) + = 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 ===================================== compiler/GHC/Core/SimpleOpt.hs ===================================== @@ -213,11 +213,11 @@ simpleOptPgm opts this_mod binds rules = ---------------------- type SimpleClo = (SimpleOptEnv, InExpr) -data SimpleContItem = ApplyToArg SimpleClo | CastIt OutCastCoercion +data SimpleContItem = ApplyToArg SimpleClo | CastIt OutType OutCastCoercion instance Outputable SimpleContItem where ppr (ApplyToArg (_, arg)) = text "ARG" <+> ppr arg - ppr (CastIt co) = text "CAST" <+> ppr co + ppr (CastIt _ co) = text "CAST" <+> ppr co data SimpleOptEnv = SOE { soe_opts :: {-# UNPACK #-} !SimpleOpts @@ -392,10 +392,10 @@ simple_app env e0@(Lam {}) as0@(_:_) = wrapLet mb_pr $ do_beta env'' body as where (env', b') = subst_opt_bndr env b - do_beta env e@(Lam b body) as@(CastIt co:rest) + do_beta env e@(Lam b body) as@(CastIt ty co:rest) -- See Note [Desugaring unlifted newtypes] | isNonCoVarId b - , Just (b', body') <- pushCoercionIntoLambda (soe_subst env) b body co + , Just (b', body') <- pushCoercionIntoLambda (soe_subst env) b body ty co = do_beta (soeZapSubst env) (Lam b' body') rest -- soeZapSubst: pushCoercionIntoLambda applies the substitution | otherwise @@ -461,10 +461,10 @@ add_cast env tyL co1 as = as | otherwise = case as of - CastIt co2:rest -> CastIt (co1' `mkTransCastCo` co2):rest - _ -> CastIt co1':as + CastIt _ co2:rest -> CastIt ty (co1' `mkTransCastCo` co2):rest + _ -> CastIt ty co1':as where - (_, co1') = optCastCoercion (so_co_opts (soe_opts env)) (soe_subst env) tyL co1 + (ty, 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 co + CastIt _ co -> mk_cast out_fun co {- Note [Desugaring unlifted newtypes] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1675,7 +1675,7 @@ exprIsLambda_maybe ise@(ISE in_scope_set _) (Cast casted_e co) -- this implies that x is not in scope in gamma (makes this code simpler) , not (isTyVar x) && not (isCoVar x) , assert (not $ x `elemVarSet` tyCoVarsOfCastCo co) True - , Just (x',e') <- pushCoercionIntoLambda (mkEmptySubst in_scope_set) x e co + , Just (x',e') <- pushCoercionIntoLambda (mkEmptySubst in_scope_set) x e (exprType casted_e) co , let res = Just (x',e',ts) = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)]) res ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -1166,9 +1166,9 @@ getRenamings orig_bndrs binds rule_bndrs go [] = init_renamings go (bind : binds) | NonRec b rhs <- bind - , Just (v, mco) <- getCastedVar rhs + , Just (v, co) <- getCastedVar rhs , Just e <- lookupVarEnv renamings b - = extendVarEnv renamings v (mkCastMCo e (mkSymMCo mco)) + = extendVarEnv renamings v (mkCastCo e co) | otherwise = renamings where @@ -1186,9 +1186,9 @@ pickSpecBinds is_local known_bndrs (bind:binds) keep_me rhs = isEmptyVarSet (exprSomeFreeVars bad_var rhs) bad_var v = is_local v && not (v `elemVarSet` known_bndrs) -getCastedVar :: CoreExpr -> Maybe (Var, MCoercionR) -getCastedVar (Var v) = Just (v, MRefl) -getCastedVar (Cast (Var v) (CCoercion co)) = Just (v, MCo co) -- TODO what about ZCoercion case? +getCastedVar :: CoreExpr -> Maybe (Var, CastCoercion) +getCastedVar (Var v) = Just (v, ReflCastCo) +getCastedVar (Cast (Var v) co) = Just (v, mkSymCastCo (varType v) co) getCastedVar _ = Nothing specFunInlinePrag :: Id -> InlinePragma View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/bbf23b1297daa21fcffd76566bf02d5... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/bbf23b1297daa21fcffd76566bf02d5... You're receiving this email because of your account on gitlab.haskell.org.