Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC
Commits:
-
07ad307e
by Adam Gundry at 2025-11-26T13:27:55+00:00
-
23014618
by Adam Gundry at 2025-11-26T13:28:34+00:00
-
a2676c3d
by Adam Gundry at 2025-11-26T13:55:32+00:00
-
be7015a8
by Adam Gundry at 2025-11-26T15:20:23+00:00
-
bbf23b12
by Adam Gundry at 2025-11-26T15:28:32+00:00
5 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/SimpleOpt.hs
Changes:
| ... | ... | @@ -64,6 +64,7 @@ module GHC.Core.Coercion ( |
| 64 | 64 | mkForAllCastCo,
|
| 65 | 65 | mkFunResCastCo,
|
| 66 | 66 | mkFunCastCoNoFTF,
|
| 67 | + applyForAllTy,
|
|
| 67 | 68 | |
| 68 | 69 | -- ** Decomposition
|
| 69 | 70 | instNewTyCon_maybe,
|
| ... | ... | @@ -1386,6 +1387,18 @@ mkInstCo co_fun co_arg |
| 1386 | 1387 | substCo subst body_co
|
| 1387 | 1388 | mkInstCo co arg = InstCo co arg
|
| 1388 | 1389 | |
| 1390 | +-- Given @tyR = forall tcv . body_ty@, produces @body_ty[arg/tcv]@
|
|
| 1391 | +-- AMG TODO: surely this must exist somewhere already?
|
|
| 1392 | +applyForAllTy :: Type -> Type -> Type
|
|
| 1393 | +applyForAllTy tyR arg =
|
|
| 1394 | + let (tcv, body_ty) = splitForAllTyCoVar tyR
|
|
| 1395 | + in_scope = mkInScopeSet $
|
|
| 1396 | + tyCoVarsOfType arg `unionVarSet` tyCoVarsOfType body_ty
|
|
| 1397 | + subst = extendTCvSubst (mkEmptySubst in_scope) tcv arg
|
|
| 1398 | + in substTy subst body_ty
|
|
| 1399 | + |
|
| 1400 | + |
|
| 1401 | + |
|
| 1389 | 1402 | -- | Given @ty :: k1@, @co :: k1 ~ k2@,
|
| 1390 | 1403 | -- produces @co' :: ty ~r (ty |> co)@
|
| 1391 | 1404 | mkGReflRightCo :: Role -> Type -> KindCoercion -> Coercion
|
| ... | ... | @@ -170,12 +170,14 @@ newtype OptCoercionOpts = OptCoercionOpts |
| 170 | 170 | { optCoercionEnabled :: Bool -- ^ Enable coercion optimisation (reduce its size)
|
| 171 | 171 | }
|
| 172 | 172 | |
| 173 | -optCastCoercion :: OptCoercionOpts -> Subst -> Type -> CastCoercion -> CastCoercion
|
|
| 174 | -optCastCoercion _ _ _ ReflCastCo = ReflCastCo
|
|
| 175 | -optCastCoercion opts env _ (CCoercion co) = CCoercion (optCoercion opts env co)
|
|
| 173 | +-- AMG TODO: not clear if coercionLKind or substTy is better choice here
|
|
| 174 | +optCastCoercion :: OptCoercionOpts -> Subst -> Type -> CastCoercion -> (Type, CastCoercion)
|
|
| 175 | +optCastCoercion _ env tyL ReflCastCo = (substTy env tyL, ReflCastCo)
|
|
| 176 | +optCastCoercion opts env _ (CCoercion co) = let co' = optCoercion opts env co
|
|
| 177 | + in (coercionLKind co', CCoercion co')
|
|
| 176 | 178 | optCastCoercion _ env tyL (ZCoercion tyR cos)
|
| 177 | - | tyL `eqTypeIgnoringMultiplicity` tyR = ReflCastCo
|
|
| 178 | - | otherwise = ZCoercion (substTy env tyR) (substCoVarSet env cos)
|
|
| 179 | + | tyL `eqTypeIgnoringMultiplicity` tyR = (substTy env tyL, ReflCastCo)
|
|
| 180 | + | otherwise = (substTy env tyL, ZCoercion (substTy env tyR) (substCoVarSet env cos))
|
|
| 179 | 181 | |
| 180 | 182 | optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo
|
| 181 | 183 | -- ^ optCoercion applies a substitution to a coercion,
|
| ... | ... | @@ -56,6 +56,7 @@ import GHC.Core.DataCon |
| 56 | 56 | import GHC.Core.TyCon ( TyCon, tyConArity, isInjectiveTyCon )
|
| 57 | 57 | import GHC.Core.TyCon.RecWalk ( initRecTc, checkRecTc )
|
| 58 | 58 | import GHC.Core.Predicate ( isDictTy, isEvId, isCallStackPredTy, isCallStackTy )
|
| 59 | +import GHC.Core.Make
|
|
| 59 | 60 | import GHC.Core.Multiplicity
|
| 60 | 61 | |
| 61 | 62 | -- We have two sorts of substitution:
|
| ... | ... | @@ -2890,7 +2891,7 @@ pushCoArg :: Type -> CastCoercion -> CoreArg -> Maybe (CoreArg, Type, CastCoerci |
| 2890 | 2891 | -- 'co' is always Representational
|
| 2891 | 2892 | pushCoArg fun_ty co arg
|
| 2892 | 2893 | | Type ty <- arg
|
| 2893 | - = do { (ty', ty, m_co') <- pushCastCoTyArg co ty
|
|
| 2894 | + = do { (ty', ty, m_co') <- pushCastCoTyArg fun_ty co ty
|
|
| 2894 | 2895 | ; return (Type ty', ty, m_co') }
|
| 2895 | 2896 | | otherwise
|
| 2896 | 2897 | = do { (arg_ty, arg_mco, res_ty, m_co') <- pushCastCoValArg fun_ty co
|
| ... | ... | @@ -2900,10 +2901,13 @@ pushCoArg fun_ty co arg |
| 2900 | 2901 | -- the argument coercion actually being ReflCo
|
| 2901 | 2902 | ; return (arg `mkCastCo` arg_mco', res_ty, m_co') }
|
| 2902 | 2903 | |
| 2903 | -pushCastCoTyArg :: CastCoercion -> Type -> Maybe (Type, Type, CastCoercion)
|
|
| 2904 | -pushCastCoTyArg (CCoercion co) ty = pushCoTyArg co ty
|
|
| 2905 | -pushCastCoTyArg ReflCastCo ty = Just (ty, error "TODO: asdasdad", ReflCastCo)
|
|
| 2906 | -pushCastCoTyArg (ZCoercion _fun_ty _cos) _ty = Nothing -- TODO do better
|
|
| 2904 | +pushCastCoTyArg :: Type -> CastCoercion -> Type -> Maybe (Type, Type, CastCoercion)
|
|
| 2905 | +pushCastCoTyArg tyL ReflCastCo arg = Just (arg, applyForAllTy tyL arg, ReflCastCo)
|
|
| 2906 | +pushCastCoTyArg _ (CCoercion co) arg = pushCoTyArg co arg
|
|
| 2907 | +pushCastCoTyArg tyL cco@ZCoercion{} arg = pushCoTyArg co arg
|
|
| 2908 | + where
|
|
| 2909 | + co = castCoToCo tyL cco
|
|
| 2910 | + |
|
| 2907 | 2911 | |
| 2908 | 2912 | pushCoTyArg :: CoercionR -> Type -> Maybe (Type, Type, CastCoercion)
|
| 2909 | 2913 | -- We have (fun |> co) @ty
|
| ... | ... | @@ -2948,10 +2952,11 @@ pushCastCoValArg tyL (ZCoercion tyR cos) |
| 2948 | 2952 | | isFunTy tyL -- TODO: do we need to check this or can we assume it?
|
| 2949 | 2953 | , isFunTy tyR
|
| 2950 | 2954 | , typeHasFixedRuntimeRep new_arg_ty
|
| 2951 | - = Just (funArgTy tyL, ZCoercion new_arg_ty cos, funResultTy tyL, ZCoercion (funResultTy tyR) cos)
|
|
| 2955 | + = Just (old_arg_ty, ZCoercion new_arg_ty cos, funResultTy tyL, ZCoercion (funResultTy tyR) cos)
|
|
| 2952 | 2956 | | otherwise = Nothing
|
| 2953 | 2957 | where
|
| 2954 | - new_arg_ty = funArgTy tyR
|
|
| 2958 | + old_arg_ty = funArgTy tyR
|
|
| 2959 | + new_arg_ty = funArgTy tyL
|
|
| 2955 | 2960 | |
| 2956 | 2961 | -- | If @pushCoValArg co = Just (co_arg, co_res)@, then
|
| 2957 | 2962 | --
|
| ... | ... | @@ -3049,7 +3054,13 @@ pushCoDataCon :: DataCon -> [CoreExpr] -> CastCoercion |
| 3049 | 3054 | -- but the right-hand one might not be. (Though it usually will.)
|
| 3050 | 3055 | pushCoDataCon dc dc_args ReflCastCo = Just $! (push_dc_refl dc dc_args)
|
| 3051 | 3056 | pushCoDataCon dc dc_args (CCoercion co) = push_dc_gen dc dc_args co (coercionKind co)
|
| 3052 | -pushCoDataCon _dc _dc_args (ZCoercion _ty _cos) = Nothing -- AMG TODO: pushCoDataCon
|
|
| 3057 | +pushCoDataCon dc dc_args cco@(ZCoercion to_ty _) =
|
|
| 3058 | + -- Generalising push_data_con to work for a CastCoercion instead of a
|
|
| 3059 | + -- Coercion seems pretty difficult, so instead we fall back on castCoToCo.
|
|
| 3060 | + push_dc_gen dc dc_args (castCoToCo from_ty cco) (Pair from_ty to_ty)
|
|
| 3061 | + where
|
|
| 3062 | + from_ty = exprType (mkCoreConApps dc dc_args) -- TODO: can we calculate from_ty more efficiently?
|
|
| 3063 | + |
|
| 3053 | 3064 | |
| 3054 | 3065 | push_dc_refl :: DataCon -> [CoreExpr] -> (DataCon, [Type], [CoreExpr])
|
| 3055 | 3066 | push_dc_refl dc dc_args
|
| ... | ... | @@ -19,7 +19,6 @@ import GHC.Core.Opt.Simplify.Monad |
| 19 | 19 | import GHC.Core.Opt.ConstantFold
|
| 20 | 20 | import GHC.Core.Type hiding ( substCo, substTy, substTyVar, extendTvSubst, extendCvSubst )
|
| 21 | 21 | import GHC.Core.TyCo.Compare( eqType )
|
| 22 | -import GHC.Core.TyCo.Subst ( substCoVarSet )
|
|
| 23 | 22 | import GHC.Core.Opt.Simplify.Env
|
| 24 | 23 | import GHC.Core.Opt.Simplify.Inline
|
| 25 | 24 | import GHC.Core.Opt.Simplify.Utils
|
| ... | ... | @@ -55,7 +54,6 @@ import GHC.Types.Unique ( hasKey ) |
| 55 | 54 | import GHC.Types.Basic
|
| 56 | 55 | import GHC.Types.Tickish
|
| 57 | 56 | import GHC.Types.Var ( isTyCoVar )
|
| 58 | -import GHC.Types.Var.Set
|
|
| 59 | 57 | import GHC.Builtin.Types.Prim( realWorldStatePrimTy )
|
| 60 | 58 | import GHC.Builtin.Names( runRWKey, seqHashKey )
|
| 61 | 59 | |
| ... | ... | @@ -1364,12 +1362,17 @@ simplCoercion env co |
| 1364 | 1362 | opts = seOptCoercionOpts env
|
| 1365 | 1363 | |
| 1366 | 1364 | simplCastCoercion :: SimplEnv -> InType -> InCastCoercion -> SimplM (OutType, OutCastCoercion)
|
| 1367 | -simplCastCoercion env _ (CCoercion co) = (\co -> (coercionLKind co, CCoercion co)) <$> simplCoercion env co
|
|
| 1368 | -simplCastCoercion env tyL (ZCoercion tyR cos) = (,) <$> simplType env tyL <*> (ZCoercion <$> simplType env tyR <*> simplCoVars env cos)
|
|
| 1369 | -simplCastCoercion env tyL ReflCastCo = (,) <$> simplType env tyL <*> pure ReflCastCo
|
|
| 1370 | - |
|
| 1371 | -simplCoVars :: SimplEnv -> CoVarSet -> SimplM CoVarSet
|
|
| 1372 | -simplCoVars env covars = pure $ substCoVarSet (getTCvSubst env) covars
|
|
| 1365 | +simplCastCoercion env ty co
|
|
| 1366 | + = do { let (opt_ty, opt_co) | reSimplifying env = (substTy env ty, substCastCo subst co)
|
|
| 1367 | + | otherwise = optCastCoercion opts subst ty co
|
|
| 1368 | + -- If (reSimplifying env) is True we have already simplified
|
|
| 1369 | + -- this coercion once, and we don't want do so again; doing
|
|
| 1370 | + -- so repeatedly risks non-linear behaviour
|
|
| 1371 | + -- See Note [Inline depth] in GHC.Core.Opt.Simplify.Env
|
|
| 1372 | + ; seqCastCoercion opt_co `seq` return (opt_ty, opt_co) }
|
|
| 1373 | + where
|
|
| 1374 | + subst = getTCvSubst env
|
|
| 1375 | + opts = seOptCoercionOpts env
|
|
| 1373 | 1376 | |
| 1374 | 1377 | |
| 1375 | 1378 | -----------------------------------
|
| ... | ... | @@ -1678,7 +1681,7 @@ optOutCoercion :: SimplEnvIS -> Type -> OutCastCoercion -> Bool -> OutCastCoerci |
| 1678 | 1681 | -- See Note [Avoid re-simplifying coercions]
|
| 1679 | 1682 | optOutCoercion env ty co already_optimised
|
| 1680 | 1683 | | already_optimised = co -- See Note [Avoid re-simplifying coercions]
|
| 1681 | - | otherwise = optCastCoercion opts empty_subst ty co
|
|
| 1684 | + | otherwise = snd $ optCastCoercion opts empty_subst ty co
|
|
| 1682 | 1685 | where
|
| 1683 | 1686 | empty_subst = mkEmptySubst (seInScope env)
|
| 1684 | 1687 | opts = seOptCoercionOpts env
|
| ... | ... | @@ -1710,7 +1713,7 @@ simplCast env body co0 cont0 |
| 1710 | 1713 | -- See Note [Avoid re-simplifying coercions]
|
| 1711 | 1714 | |
| 1712 | 1715 | addCoerce tyL co co_is_opt (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail })
|
| 1713 | - | Just (arg_ty', res_ty, m_co') <- pushCastCoTyArg co arg_ty
|
|
| 1716 | + | Just (arg_ty', res_ty, m_co') <- pushCastCoTyArg tyL co arg_ty
|
|
| 1714 | 1717 | = {-#SCC "addCoerce-pushCoTyArg" #-}
|
| 1715 | 1718 | do { tail' <- addCoerceM res_ty m_co' co_is_opt tail
|
| 1716 | 1719 | ; return (ApplyToTy { sc_arg_ty = arg_ty'
|
| ... | ... | @@ -464,7 +464,7 @@ add_cast env tyL co1 as |
| 464 | 464 | CastIt co2:rest -> CastIt (co1' `mkTransCastCo` co2):rest
|
| 465 | 465 | _ -> CastIt co1':as
|
| 466 | 466 | where
|
| 467 | - co1' = optCastCoercion (so_co_opts (soe_opts env)) (soe_subst env) tyL co1
|
|
| 467 | + (_, co1') = optCastCoercion (so_co_opts (soe_opts env)) (soe_subst env) tyL co1
|
|
| 468 | 468 | |
| 469 | 469 | rebuild_app :: HasDebugCallStack
|
| 470 | 470 | => SimpleOptEnv -> OutExpr -> [SimpleContItem] -> OutExpr
|