[Git][ghc/ghc][wip/amg/dcoercion-optimisation] WIP: experiment with DCoercion optimisation
Adam Gundry (@adamgundry)
gitlab at gitlab.haskell.org
Wed May 24 06:46:49 UTC 2023
Adam Gundry pushed to branch wip/amg/dcoercion-optimisation at Glasgow Haskell Compiler / GHC
Commits:
fdf40c60 by Adam Gundry at 2023-05-24T07:46:27+01:00
WIP: experiment with DCoercion optimisation
- - - - -
1 changed file:
- compiler/GHC/Core/Coercion/Opt.hs
Changes:
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -5,6 +5,7 @@
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wwarn #-} -- AMG TODO
module GHC.Core.Coercion.Opt
( optCoercion
@@ -374,6 +375,7 @@ opt_co4 opts env sym rep r (AxiomInstCo con ind cos)
-- Note that the_co does *not* have sym pushed into it
opt_co4 opts env@(LC _ _lift_co_env) sym rep r (HydrateDCo _r lhs_ty dco rhs_ty)
+{-
= case optDCoMethod opts of
HydrateDCos ->
opt_co4 opts env sym rep r (hydrateOneLayerDCo r lhs_ty dco)
@@ -384,10 +386,13 @@ opt_co4 opts env@(LC _ _lift_co_env) sym rep r (HydrateDCo _r lhs_ty dco rhs_ty)
wrapSym sym $
wrapRole rep r $
res
+
| otherwise
- -> assert (r == _r) $
+-}
+-- -> assert (r == _r) $
+ = assert (r == _r) $
wrapSym sym $
- (\ (lhs', dco') -> mkHydrateDCo r' lhs' dco' rhs') $
+-- (\ (lhs', dco') -> mkHydrateDCo r' lhs' dco' rhs') $
opt_dco4_wrap "HydrateDCo" opts env rep r lhs_ty dco
where
rhs' = substTyUnchecked (lcSubstRight env) rhs_ty
@@ -607,31 +612,29 @@ type family OptRes co_or_dco where
type Optimiser in_co out_co =
OptCoParams -> LiftingContext -> SymFlag -> ReprFlag -> Role -> in_co -> out_co
-opt_co_or_dco :: CoOrDCo co_or_dco -> Type -> Optimiser co_or_dco co_or_dco
+opt_co_or_dco :: CoOrDCo co_or_dco -> Type -> Optimiser co_or_dco Coercion
opt_co_or_dco Co _ = opt_co4
opt_co_or_dco DCo l_ty = \ opts lc sym repr r dco ->
assert (sym == False) $
- snd $
opt_dco4 opts lc repr r l_ty dco
opt_univ :: forall co_or_dco
. Outputable co_or_dco
=> CoOrDCo co_or_dco
-> OptCoParams
- -> LiftingContext -> SymFlag -> UnivCoProvenance co_or_dco -> Role
- -> Type -> Type -> OptRes co_or_dco
+ -> LiftingContext -> SymFlag -> UnivCoProvenance Coercion -> Role
+ -> Type -> Type -> Coercion
opt_univ co_or_dco opts env sym (PhantomProv h) _r ty1 ty2
| sym = mk_phantom h' ty2' ty1'
| otherwise = mk_phantom h' ty1' ty2'
where
- h' = wrap "opt_univ PhantomProv" (opt_co_or_dco co_or_dco ty1) opts env sym False Nominal h
+ h' = wrap "opt_univ PhantomProv" (opt_co_or_dco Co ty1) opts env sym False Nominal h
ty1' = substTy (lcSubstLeft env) ty1
ty2' = substTy (lcSubstRight env) ty2
- mk_phantom :: co_or_dco -> Type -> Type -> OptRes co_or_dco
- mk_phantom = case co_or_dco of
- Co -> mkPhantomCo
- DCo -> \ h t1 t2 -> (t1, mkUnivDCo (PhantomProv h) t2)
+ mk_phantom :: Coercion -> Type -> Type -> Coercion
+ mk_phantom = mkPhantomCo
+
opt_univ co_or_dco opts env sym prov role oty1 oty2
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
@@ -642,19 +645,10 @@ opt_univ co_or_dco opts env sym prov role oty1 oty2
-- NB: prov must not be the two interesting ones (ProofIrrel & Phantom);
-- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps
= let roles = tyConRoleListX role tc1
- in case co_or_dco of
- Co ->
- let
- arg_cos = zipWith3 mk_univ roles tys1 tys2
- arg_cos' = zipWith (opt_co4 opts env sym False) roles arg_cos
- in
- mkTyConAppCo role tc1 arg_cos'
- DCo ->
- let
- arg_cos = zipWith3 (\ r x y -> snd $ mk_univ r x y) roles tys1 tys2
- (arg_lhs', arg_dcos') = unzip $ zipWith3 (opt_dco4 opts env False) roles tys1 arg_cos
- in
- (mkTyConApp tc1 arg_lhs', mkTyConAppDCo arg_dcos')
+ arg_cos = zipWith3 mk_univ roles tys1 tys2
+ arg_cos' = zipWith (opt_co4 opts env sym False) roles arg_cos
+ in
+ mkTyConAppCo role tc1 arg_cos'
-- can't optimize the AppTy case because we can't build the kind coercions.
@@ -663,9 +657,7 @@ opt_univ co_or_dco opts env sym prov role oty1 oty2
-- NB: prov isn't interesting here either
= let k1 = tyVarKind tv1
k2 = tyVarKind tv2
- eta = case co_or_dco of
- Co -> mk_univ Nominal k1 k2
- DCo -> snd $ mk_univ Nominal k1 k2
+ eta = mk_univ Nominal k1 k2
tv1' = mk_castTy (TyVarTy tv1) k1 eta k2
-- eta gets opt'ed soon, but not yet.
ty2' = substTyWith [tv2] [tv1'] ty2
@@ -680,13 +672,9 @@ opt_univ co_or_dco opts env sym prov role oty1 oty2
= let k1 = varType cv1
k2 = varType cv2
r' = coVarRole cv1
- eta = case co_or_dco of
- Co -> mk_univ Nominal k1 k2
- DCo -> snd $ mk_univ Nominal k1 k2
+ eta = mk_univ Nominal k1 k2
eta_d = downgradeRole r' Nominal $
- case co_or_dco of
- Co -> eta
- DCo -> mkHydrateDCo Nominal k1 eta k2
+ eta
-- eta gets opt'ed soon, but not yet.
n_co = (mkSymCo $ mkSelCo (SelTyCon 2 r') eta_d) `mkTransCo`
(mkCoVarCo cv1) `mkTransCo`
@@ -706,32 +694,24 @@ opt_univ co_or_dco opts env sym prov role oty1 oty2
mk_univ role a b
where
- mk_castTy :: Type -> Type -> co_or_dco -> Type -> Type
- mk_castTy = case co_or_dco of
- Co -> \ ty _ co _ -> CastTy ty co
- DCo -> \ ty l dco r -> CastTy ty (mkHydrateDCo Nominal l dco r)
- mk_univ :: Role -> Type -> Type -> OptRes co_or_dco
- mk_univ = case co_or_dco of
- Co -> mkUnivCo prov'
- DCo -> \ _ l_ty r_ty -> (l_ty, mkUnivDCo prov' r_ty)
- mk_forall :: TyCoVar -> co_or_dco -> OptRes co_or_dco -> OptRes co_or_dco
- mk_forall cv eta = case co_or_dco of
- Co -> mkForAllCo cv eta
- DCo -> \ (_,body) -> (mkTyVarTy cv, mkForAllDCo cv eta body)
- opt_forall :: TyCoVar -> co_or_dco -> (LiftingContext,TyCoVar,co_or_dco)
- opt_forall tv co = case co_or_dco of
- Co -> optForAllCoBndr opts env sym tv co
- DCo -> optForAllDCoBndr opts env sym tv co
- prov' :: UnivCoProvenance co_or_dco
+ mk_castTy :: Type -> Type -> Coercion -> Type -> Type
+ mk_castTy = \ ty _ co _ -> CastTy ty co
+ mk_univ :: Role -> Type -> Type -> Coercion
+ mk_univ = mkUnivCo prov'
+ mk_forall :: TyCoVar -> Coercion -> Coercion -> Coercion
+ mk_forall cv eta = mkForAllCo cv eta
+ opt_forall :: TyCoVar -> Coercion -> (LiftingContext,TyCoVar,Coercion)
+ opt_forall tv co = optForAllCoBndr opts env sym tv co
+ prov' :: UnivCoProvenance KindCoercion
prov' = case prov of
#if __GLASGOW_HASKELL__ < 901
-- This alt is redundant with the first match of the FunDef
PhantomProv kco -> PhantomProv
- $ wrap "univ_co phantom" (opt_co_or_dco co_or_dco oty1)
+ $ wrap "univ_co phantom" (opt_co_or_dco Co oty1)
opts env sym False Nominal kco
#endif
ProofIrrelProv kco -> ProofIrrelProv
- $ wrap "univ_co proof_irrel" (opt_co_or_dco co_or_dco oty1)
+ $ wrap "univ_co proof_irrel" (opt_co_or_dco Co oty1)
opts env sym False Nominal kco
PluginProv str -> PluginProv str
CorePrepProv homo -> CorePrepProv homo
@@ -1054,14 +1034,14 @@ fireTransRule _rule _co1 _co2 res
-- N.B.: The reason we return (Type, DCoercion) and not just DCoercion is that we
-- sometimes need the substituted LHS type (see opt_trans_dco).
-opt_phantom_dco :: OptCoParams -> LiftingContext -> Role -> Type -> DCoercion -> (Type, NormalDCo)
+opt_phantom_dco :: OptCoParams -> LiftingContext -> Role -> Type -> DCoercion -> NormalCo
opt_phantom_dco opts env r l_ty dco = opt_univ DCo opts env False (PhantomProv kco) Phantom l_ty r_ty
where
- kco = DehydrateCo (mkKindCo $ mkHydrateDCo r l_ty dco r_ty)
+ kco = mkKindCo $ mkHydrateDCo r l_ty dco r_ty
r_ty = followDCo r l_ty dco
-- A naive attempt at removing this entirely causes issues in test "type_in_type_hole_fits".
-opt_dco4_wrap :: String -> OptCoParams -> LiftingContext -> ReprFlag -> Role -> Type -> DCoercion -> (Type, NormalDCo)
+opt_dco4_wrap :: String -> OptCoParams -> LiftingContext -> ReprFlag -> Role -> Type -> DCoercion -> NormalCo
opt_dco4_wrap str opts lc rep r l_ty dco = wrap ("opt_dco4 " ++ str) go opts lc False rep r dco
where
go opts lc _sym repr r dco = opt_dco4 opts lc repr r l_ty dco
@@ -1070,59 +1050,104 @@ opt_dco2 :: OptCoParams
-> LiftingContext
-> Role -- ^ The role of the input coercion
-> Type
- -> DCoercion -> (Type, NormalDCo)
+ -> DCoercion -> NormalCo
opt_dco2 opts env Phantom ty dco = opt_phantom_dco opts env Phantom ty dco
opt_dco2 opts env r ty dco = opt_dco3 opts env Nothing r ty dco
-opt_dco3 :: OptCoParams -> LiftingContext -> Maybe Role -> Role -> Type -> DCoercion -> (Type, NormalDCo)
+opt_dco3 :: OptCoParams -> LiftingContext -> Maybe Role -> Role -> Type -> DCoercion -> NormalCo
opt_dco3 opts env (Just Phantom) r ty dco = opt_phantom_dco opts env r ty dco
opt_dco3 opts env (Just Representational) r ty dco = opt_dco4_wrap "opt_dco3 R" opts env True r ty dco
opt_dco3 opts env _ r ty dco = opt_dco4_wrap "opt_dco3 _" opts env False r ty dco
-opt_dco4 :: OptCoParams -> LiftingContext -> ReprFlag -> Role -> Type -> DCoercion -> (Type, NormalDCo)
-opt_dco4 opts env rep r l_ty dco = case dco of
+{-
+
+My plan for DCoercion optimisation is this: try to get rid of DCoercions as much
+as possible, because Coercions are easier to optimise. In particular, they may
+disappear to nothing at all, and unblock subsequent coercion
+optimisations. There is only really one case in which DCoercions are better,
+which is where we have a long transitive chain of type family reduction steps.
+
+-}
+
+opt_dco4 :: OptCoParams -> LiftingContext -> ReprFlag -> Role -> Type -> DCoercion -> NormalCo
+opt_dco4 opts env@(LC _ lift_co_env) rep r l_ty dco = case dco of
+ TransDCo dco1 dco2
+ -> case opt_dco4 opts env rep r l_ty dco1 of
+ HydrateDCo r' l_ty' dco1' r_ty
+ | isEmptyVarEnv lift_co_env ->
+ let dco2' = substDCo (lcSubst env) dco2
+ in HydrateDCo r' l_ty' (dco1' `mkTransDCo` dco2') (followDCo r' r_ty dco2')
+ co1@(AxiomInstCo coax br cos)
+ | not (isNewTyCon (coAxiomTyCon coax))
+ , isEmptyVarEnv lift_co_env ->
+ let dco2' = substDCo (lcSubst env) dco2
+ Pair l_ty' r_ty = coercionKind co1
+ dco1' = mkDehydrateCo co1 -- TODO: inline; use assumption cos are refls?
+ in HydrateDCo r l_ty' (dco1' `mkTransDCo` dco2') (followDCo r r_ty dco2')
+ -- TODO: AxiomRuleCo?
+ co1 -> opt_trans opts (lcInScopeSet env) co1 (opt_dco4 opts env rep r (coercionRKind co1) dco2)
+ _ -> opt_co4 opts env False rep r (hydrateOneLayerDCo r l_ty dco)
+
+
+_opt_dco4 :: OptCoParams -> LiftingContext -> ReprFlag -> Role -> Type -> DCoercion -> NormalCo
+_opt_dco4 opts env rep r l_ty dco = case dco of
ReflDCo
- -> lifted_dco
+ -> lifted_co
GReflRightDCo kco
| isGReflCo kco || isGReflCo kco'
- -> lifted_dco
+ -> lifted_co
| otherwise
- -> (l_ty', mkGReflRightDCo kco')
+ -> mkGReflRightCo r l_ty' kco'
where
kco' = opt_co4 opts env False False Nominal kco
GReflLeftDCo kco
| isGReflCo kco || isGReflCo kco'
- -> lifted_dco
+ -> lifted_co
| otherwise
- -> (l_ty', mkGReflLeftDCo kco')
+ -> mkGReflLeftCo r l_ty' kco'
where
kco' = opt_co4 opts env False False Nominal kco
TyConAppDCo dcos
| Just (tc, l_tys) <- splitTyConApp_maybe l_ty
-> let
- (arg_ltys, arg_dcos) =
+ arg_cos =
case (rep, r) of
(True, Nominal) ->
- unzip $
zipWith3
(\ mb_r' -> opt_dco3 opts env mb_r' Nominal)
(map Just (tyConRoleListRepresentational tc))
l_tys
dcos
(False, Nominal) ->
- unzip $
zipWith (opt_dco4 opts env False Nominal) l_tys dcos
(_, Representational) ->
- unzip $
zipWith3
(opt_dco2 opts env)
(tyConRoleListRepresentational tc)
l_tys
dcos
(_, Phantom) -> pprPanic "opt_dco4 sees a phantom!" (ppr dco)
- in (mkTyConApp tc arg_ltys, mkTyConAppDCo arg_dcos)
+ in mkTyConAppCo r tc arg_cos
+
+-- AMG TODO: experimenting with changing dco opt to return a Coercion.
+--
+-- Key question: do we want to push Hydrate up or down?
+-- If we have TyConApp for a non-family, it will never reduce, so might want to be a Coercion?
+-- But then perhaps that is included in a larger context which wants a DCoercion?
+--
+-- Idea: we only benefit from DCoercion when we have a long chain of
+-- Steps/AxiomInstDCo. For coercion optimisation purposes, a Coercion is
+-- better. Thus dcoercion optimisation produces Coercions. Then in
+-- opt_trans_rule we need to handle the cases intelligently.
+--
+-- Idea: look out for
+-- Hydrate ty1 dco ; Sym (Hydrate ty2 dco)
+-- and handle it by converting to coercions and optimising their transitive composition?
+
+-- Sym (Hydrate ty dco1) ; Hydrate ty dco2
+-- should be easy as we can follow common prefix of both dco1 and dco2
| otherwise
-> pprPanic "opt_dco4: TyConAppDCo where ty is not a TyConApp" $
@@ -1132,14 +1157,17 @@ opt_dco4 opts env rep r l_ty dco = case dco of
AppDCo dco1 dco2
| Just (l_ty1, l_ty2) <- splitAppTy_maybe l_ty
, let
- (l_ty1', l_dco1) = opt_dco4 opts env rep r l_ty1 dco1
- (l_ty2', l_dco2) = opt_dco4 opts env False Nominal l_ty2 dco2
- -> (mkAppTy l_ty1' l_ty2', mkAppDCo l_dco1 l_dco2)
+ l_co1 = opt_dco4 opts env rep r l_ty1 dco1
+ l_co2 = opt_dco4 opts env False Nominal l_ty2 dco2
+ -> mkAppCo l_co1 l_co2
| otherwise
-> pprPanic "opt_dco4: AppDCo where ty is not an AppTy" $
vcat [ text "dco =" <+> ppr dco
, text "l_ty =" <+> ppr l_ty ]
+ ForAllDCo{} -- AMG TODO
+ -> rep_dco
+{-
ForAllDCo dco_tcv k_dco body_dco
| ForAllTy (Bndr ty_tv af) body_ty <- coreFullView l_ty
-> case optForAllDCoBndr opts env False dco_tcv k_dco of
@@ -1155,44 +1183,45 @@ opt_dco4 opts env rep r l_ty dco = case dco of
-> pprPanic "opt_dco4: ForAllDCo where ty is not a ForAllTy" $
vcat [ text "dco =" <+> ppr dco
, text "l_ty =" <+> ppr l_ty ]
+-}
CoVarDCo cv
- -> let co' = opt_co4 opts env False rep r (CoVarCo cv)
- in (coercionLKind co', mkDehydrateCo co')
+ -> opt_co4 opts env False rep r (CoVarCo cv)
AxiomInstDCo {}
- -> (l_ty', rep_dco)
+ -> rep_dco
StepsDCo {}
- -> (l_ty', rep_dco)
+ -> rep_dco
+ UnivDCo{} -> rep_dco -- TODO
+{-
UnivDCo prov rhs_ty
-> opt_univ DCo opts env False prov r' l_ty rhs_ty
+-}
TransDCo dco1 dco2 ->
let
- (l_ty', dco1') = opt_dco4 opts env rep r l_ty dco1
+ co1' = opt_dco4 opts env rep r l_ty dco1
-- Follow the original directed coercion,
-- to avoid applying the substitution twice.
- mid_ty = followDCo r l_ty dco1
- (mid_ty', dco2') = opt_dco4 opts env rep r mid_ty dco2
+ Pair l_ty' mid_ty' = coercionKind co1'
+ co2' = opt_dco4 opts env rep r mid_ty' dco2
in
- (l_ty', opt_trans_dco opts (lcInScopeSet env) r' l_ty' dco1' mid_ty' dco2')
+ opt_trans opts (lcInScopeSet env) co1' co2'
SubDCo dco ->
assert (r == Representational) $
opt_dco4_wrap "SubDCo" opts env True Nominal l_ty dco
DehydrateCo co ->
- let co' = opt_co4_wrap "DehydrateCo" opts env False rep r co
- in (coercionLKind co', mkDehydrateCo co')
+ opt_co4_wrap "DehydrateCo" opts env False rep r co
where
- lifted_dco = let lifted_co = liftCoSubst r' env l_ty
- in ( coercionLKind lifted_co, mkDehydrateCo lifted_co )
+ lifted_co = liftCoSubst r' env l_ty
l_ty' = substTyUnchecked (lcSubstLeft env) l_ty
r' = chooseRole rep r
- rep_dco = wrapRole_dco rep r l_ty' dco (followDCo r l_ty' dco)
+ rep_dco = wrapRole rep r $ mkHydrateDCo r l_ty' dco (followDCo r l_ty' dco)
---------------------------------------------------------
-- Transitivity for directed coercions.
@@ -1236,6 +1265,8 @@ opt_trans2_dco _ _ _ _ dco1 _ dco2
opt_trans_rule_dco :: OptCoParams -> InScopeSet -> Role -> Type -> NormalNonIdDCo -> Type -> NormalNonIdDCo -> Maybe NormalDCo
+-- AMG TODO: should be more cases here?
+
-- Handle undirected coercions.
opt_trans_rule_dco opts is _ _ (DehydrateCo co1) _ (DehydrateCo co2)
= DehydrateCo <$> opt_trans_rule opts is co1 co2
@@ -1660,5 +1691,5 @@ optForAllDCoBndr :: OptCoParams
optForAllDCoBndr opts env sym tv
= substForAllDCoBndrUsingLC sym
(substTyUnchecked (lcSubstLeft env))
- (snd . opt_dco4_wrap "optForAllDCoBndr" opts env False Nominal (tyVarKind tv)) env
+ (mkDehydrateCo . opt_dco4_wrap "optForAllDCoBndr" opts env False Nominal (tyVarKind tv)) env
tv
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fdf40c6097ff27b259d8d5b2de5c0c0d29379db0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fdf40c6097ff27b259d8d5b2de5c0c0d29379db0
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/20230524/1334f3f1/attachment-0001.html>
More information about the ghc-commits
mailing list