diff options
Diffstat (limited to 'compiler/GHC/Core/Coercion/Opt.hs')
| -rw-r--r-- | compiler/GHC/Core/Coercion/Opt.hs | 802 |
1 files changed, 583 insertions, 219 deletions
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs index 98506c444e..8df3dc31e5 100644 --- a/compiler/GHC/Core/Coercion/Opt.hs +++ b/compiler/GHC/Core/Coercion/Opt.hs @@ -1,10 +1,15 @@ -- (c) The University of Glasgow 2006 {-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} module GHC.Core.Coercion.Opt ( optCoercion , OptCoercionOpts (..) + , OptDCoMethod (..) ) where @@ -21,6 +26,7 @@ import GHC.Core.TyCon import GHC.Core.Coercion.Axiom import GHC.Core.Unify +import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Types.Unique.Set @@ -35,6 +41,7 @@ import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Control.Monad ( zipWithM ) +import qualified Data.Kind ( Type ) {- %************************************************************************ @@ -123,31 +130,40 @@ So we substitute the coercion variable c for the coercion -- | Coercion optimisation options newtype OptCoercionOpts = OptCoercionOpts - { optCoercionEnabled :: Bool -- ^ Enable coercion optimisation (reduce its size) + { optCoercionOpts :: Maybe OptDCoMethod + -- ^ @Nothing@: no coercion optimisation. + -- ^ @Just opt@: do full coercion optimisation, with @opt@ specifying + -- how to deal with directed coercions. } +data OptDCoMethod + = HydrateDCos + -- ^ Turn directed coercions back into fully-fledged coercions in the + -- coercion optimiser, so that they can be fully optimised. + | OptDCos + -- ^ Optimise directed coercions with the (currently limited) + -- forms of optimisation avaiable for directed coercions. + { skipDCoOpt :: !Bool + -- ^ Whether to skip optimisation of directed coercions entirely + -- when possible. + } + +data OptCoParams = + OptCoParams { optDCoMethod :: !OptDCoMethod } + optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo -- ^ optCoercion applies a substitution to a coercion, -- *and* optimises it to reduce its size -optCoercion opts env co - | optCoercionEnabled opts - = optCoercion' env co -{- - = pprTrace "optCoercion {" (text "Co:" <+> ppr co) $ - let result = optCoercion' env co in - pprTrace "optCoercion }" (vcat [ text "Co:" <+> ppr co - , text "Optco:" <+> ppr result ]) $ - result --} - - | otherwise - = substCo env co - - -optCoercion' :: Subst -> Coercion -> NormalCo -optCoercion' env co +optCoercion (OptCoercionOpts opts) env co + | Just dco_method <- opts = optCoercion' + (OptCoParams { optDCoMethod = dco_method }) env + $ co + | otherwise = substCo env $ co + +optCoercion' :: OptCoParams -> Subst -> Coercion -> NormalCo +optCoercion' opts env co | debugIsOn - = let out_co = opt_co1 lc False co + = let out_co = opt_co1 opts lc False co (Pair in_ty1 in_ty2, in_role) = coercionKindRole co (Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co in @@ -167,7 +183,7 @@ optCoercion' env co , text "subst:" <+> ppr env ])) out_co - | otherwise = opt_co1 lc False co + | otherwise = opt_co1 opts lc False co where lc = mkSubstLiftingContext env ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv) @@ -179,7 +195,10 @@ type NormalCo = Coercion -- * For trans coercions (co1 `trans` co2) -- co1 is not a trans, and neither co1 nor co2 is identity +type NormalDCo = DCoercion + type NormalNonIdCo = NormalCo -- Extra invariant: not the identity +type NormalNonIdDCo = NormalDCo -- Extra invariant: not the identity -- | Do we apply a @sym@ to the result? type SymFlag = Bool @@ -189,65 +208,71 @@ type ReprFlag = Bool -- | Optimize a coercion, making no assumptions. All coercions in -- the lifting context are already optimized (and sym'd if nec'y) -opt_co1 :: LiftingContext +opt_co1 :: OptCoParams + -> LiftingContext -> SymFlag -> Coercion -> NormalCo -opt_co1 env sym co = opt_co2 env sym (coercionRole co) co +opt_co1 opts env sym co = opt_co2 opts env sym (coercionRole co) co -- See Note [Optimising coercion optimisation] -- | Optimize a coercion, knowing the coercion's role. No other assumptions. -opt_co2 :: LiftingContext +opt_co2 :: OptCoParams + -> LiftingContext -> SymFlag -> Role -- ^ The role of the input coercion -> Coercion -> NormalCo -opt_co2 env sym Phantom co = opt_phantom env sym co -opt_co2 env sym r co = opt_co3 env sym Nothing r co +opt_co2 opts env sym Phantom co = opt_phantom opts env sym co +opt_co2 opts env sym r co = opt_co3 opts env sym Nothing r co -- See Note [Optimising coercion optimisation] -- | Optimize a coercion, knowing the coercion's non-Phantom role. -opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo -opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co -opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co +opt_co3 :: OptCoParams -> LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo +opt_co3 opts env sym (Just Phantom) _ co = opt_phantom opts env sym co +opt_co3 opts env sym (Just Representational) r co = opt_co4 opts env sym True r co -- if mrole is Just Nominal, that can't be a downgrade, so we can ignore -opt_co3 env sym _ r co = opt_co4_wrap env sym False r co +opt_co3 opts env sym _ r co = opt_co4 opts env sym False r co + +-- | Utility function for debugging coercion optimisation: uncomment +-- the logging functions in the body of this function, and the coercion +-- optimiser will produce a log of what it is doing. +wrap :: (Outputable in_co, Outputable out_co) => String -> Optimiser in_co out_co -> Optimiser in_co out_co +wrap _str opt_thing opts env sym rep r co + = {- pprTrace (_str ++ " wrap {") + ( vcat [ text "Sym:" <+> ppr sym + , text "Rep:" <+> ppr rep + , text "Role:" <+> ppr r + , text "Co:" <+> ppr co + , text "LC:" <+> ppr env + , text "Subst:" <+> ppr (lcTCvSubst env)]) $ + --assert (r == coercionRole co) + pprTrace (_str ++ " wrap }") (ppr co $$ text "---" $$ ppr result) $ -} + result + where result = opt_thing opts env sym rep r co -- See Note [Optimising coercion optimisation] -- | Optimize a non-phantom coercion. -opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag - -> Role -> Coercion -> NormalCo +opt_co4_wrap :: String -> OptCoParams -> LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo -- Precondition: In every call (opt_co4 lc sym rep role co) -- we should have role = coercionRole co -opt_co4_wrap = opt_co4 - -{- -opt_co4_wrap env sym rep r co - = pprTrace "opt_co4_wrap {" - ( vcat [ text "Sym:" <+> ppr sym - , text "Rep:" <+> ppr rep - , text "Role:" <+> ppr r - , text "Co:" <+> ppr co ]) $ - assert (r == coercionRole co ) $ - let result = opt_co4 env sym rep r co in - pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $ - result --} +opt_co4_wrap str opts env sym rep r co = wrap ("opt_co4 " ++ str) opt_co4 opts env sym rep r co -opt_co4 env _ rep r (Refl ty) +opt_co4 :: OptCoParams -> LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo +opt_co4 _ env _ rep r (Refl ty) = assertPpr (r == Nominal) (text "Expected role:" <+> ppr r $$ text "Found role:" <+> ppr Nominal $$ text "Type:" <+> ppr ty) $ liftCoSubst (chooseRole rep r) env ty -opt_co4 env _ rep r (GRefl _r ty MRefl) +opt_co4 _ env _ rep r (GRefl _r ty MRefl) = assertPpr (r == _r) (text "Expected role:" <+> ppr r $$ text "Found role:" <+> ppr _r $$ text "Type:" <+> ppr ty) $ liftCoSubst (chooseRole rep r) env ty -opt_co4 env sym rep r (GRefl _r ty (MCo co)) +opt_co4 opts env sym rep r (GRefl _r ty (MCo co)) = assertPpr (r == _r) (text "Expected role:" <+> ppr r $$ text "Found role:" <+> ppr _r $$ @@ -258,58 +283,58 @@ opt_co4 env sym rep r (GRefl _r ty (MCo co)) where r' = chooseRole rep r ty' = substTy (lcSubstLeft env) ty - co' = opt_co4 env False False Nominal co + co' = opt_co4 opts env False False Nominal co -opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co +opt_co4 opts env sym rep r (SymCo co) = opt_co4_wrap "SymCo" opts env (not sym) rep r co -- surprisingly, we don't have to do anything to the env here. This is -- because any "lifting" substitutions in the env are tied to ForAllCos, -- which treat their left and right sides differently. We don't want to -- exchange them. -opt_co4 env sym rep r g@(TyConAppCo _r tc cos) +opt_co4 opts env sym rep r g@(TyConAppCo _r tc cos) = assert (r == _r) $ case (rep, r) of (True, Nominal) -> mkTyConAppCo Representational tc - (zipWith3 (opt_co3 env sym) + (zipWith3 (opt_co3 opts env sym) (map Just (tyConRoleListRepresentational tc)) (repeat Nominal) cos) (False, Nominal) -> - mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos) + mkTyConAppCo Nominal tc (map (opt_co4_wrap "TyConAppCo (False, Nominal)" opts env sym False Nominal) cos) (_, Representational) -> -- must use opt_co2 here, because some roles may be P -- See Note [Optimising coercion optimisation] - mkTyConAppCo r tc (zipWith (opt_co2 env sym) + mkTyConAppCo r tc (zipWith (opt_co2 opts env sym) (tyConRoleListRepresentational tc) -- the current roles cos) (_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g) -opt_co4 env sym rep r (AppCo co1 co2) - = mkAppCo (opt_co4_wrap env sym rep r co1) - (opt_co4_wrap env sym False Nominal co2) +opt_co4 opts env sym rep r (AppCo co1 co2) + = mkAppCo (opt_co4_wrap "AppCo co1" opts env sym rep r co1) + (opt_co4_wrap "AppCo co2" opts env sym False Nominal co2) -opt_co4 env sym rep r (ForAllCo tv k_co co) - = case optForAllCoBndr env sym tv k_co of +opt_co4 opts env sym rep r (ForAllCo tv k_co co) + = case optForAllCoBndr opts env sym tv k_co of (env', tv', k_co') -> mkForAllCo tv' k_co' $ - opt_co4_wrap env' sym rep r co + opt_co4_wrap "ForAllCo" opts env' sym rep r co -- Use the "mk" functions to check for nested Refls -opt_co4 env sym rep r (FunCo _r afl afr cow co1 co2) +opt_co4 opts env sym rep r (FunCo _r afl afr cow co1 co2) = assert (r == _r) $ mkFunCo2 r' afl' afr' cow' co1' co2' where - co1' = opt_co4_wrap env sym rep r co1 - co2' = opt_co4_wrap env sym rep r co2 - cow' = opt_co1 env sym cow + co1' = opt_co4_wrap "FunCo co1" opts env sym rep r co1 + co2' = opt_co4_wrap "FunCo co2" opts env sym rep r co2 + cow' = opt_co1 opts env sym cow !r' | rep = Representational | otherwise = r !(afl', afr') | sym = (afr,afl) | otherwise = (afl,afr) -opt_co4 env sym rep r (CoVarCo cv) +opt_co4 opts env sym rep r (CoVarCo cv) | Just co <- lookupCoVar (lcSubst env) cv - = opt_co4_wrap (zapLiftingContext env) sym rep r co + = opt_co4_wrap "CoVarCo" opts (zapLiftingContext env) sym rep r co | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl] = mkReflCo (chooseRole rep r) ty1 @@ -330,10 +355,10 @@ opt_co4 env sym rep r (CoVarCo cv) cv -- cv1 might have a substituted kind! -opt_co4 _ _ _ _ (HoleCo h) +opt_co4 _ _ _ _ _ (HoleCo h) = pprPanic "opt_univ fell into a hole" (ppr h) -opt_co4 env sym rep r (AxiomInstCo con ind cos) +opt_co4 opts env sym rep r (AxiomInstCo con ind cos) -- Do *not* push sym inside top-level axioms -- e.g. if g is a top-level axiom -- g a : f a ~ a @@ -343,43 +368,64 @@ opt_co4 env sym rep r (AxiomInstCo con ind cos) wrapSym sym $ -- some sub-cos might be P: use opt_co2 -- See Note [Optimising coercion optimisation] - AxiomInstCo con ind (zipWith (opt_co2 env False) + AxiomInstCo con ind (zipWith (opt_co2 opts env False) (coAxBranchRoles (coAxiomNthBranch con ind)) cos) -- Note that the_co does *not* have sym pushed into it -opt_co4 env sym rep r (UnivCo prov _r t1 t2) - = assert (r == _r ) - opt_univ env sym prov (chooseRole rep r) t1 t2 +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) + OptDCos { skipDCoOpt = do_skip } + | do_skip && isEmptyVarEnv _lift_co_env + -> let res = substCo (lcSubst env) (HydrateDCo r lhs_ty dco rhs_ty) + in assert (r == _r) $ + wrapSym sym $ + wrapRole rep r $ + res + | otherwise + -> assert (r == _r) $ + wrapSym sym $ + (\ (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 + r' = chooseRole rep r + +opt_co4 opts env sym rep r (UnivCo prov _r t1 t2) + = assert (r == _r) $ + opt_univ Co opts env sym prov (chooseRole rep r) t1 t2 -opt_co4 env sym rep r (TransCo co1 co2) +opt_co4 opts env sym rep r (TransCo co1 co2) -- sym (g `o` h) = sym h `o` sym g - | sym = opt_trans in_scope co2' co1' - | otherwise = opt_trans in_scope co1' co2' + | sym = opt_trans opts in_scope co2' co1' + | otherwise = opt_trans opts in_scope co1' co2' + where - co1' = opt_co4_wrap env sym rep r co1 - co2' = opt_co4_wrap env sym rep r co2 + co1' = opt_co4_wrap "TransCo co1" opts env sym rep r co1 + co2' = opt_co4_wrap "TransCo co2" opts env sym rep r co2 in_scope = lcInScopeSet env -opt_co4 env _sym rep r (SelCo n co) +opt_co4 _ env _sym rep r (SelCo n co) | Just (ty, _co_role) <- isReflCo_maybe co = liftCoSubst (chooseRole rep r) env (getNthFromType n ty) -- NB: it is /not/ true that r = _co_role -- Rather, r = coercionRole (SelCo n co) -opt_co4 env sym rep r (SelCo (SelTyCon n r1) (TyConAppCo _ _ cos)) +opt_co4 opts env sym rep r (SelCo (SelTyCon n r1) (TyConAppCo _ _ cos)) = assert (r == r1 ) - opt_co4_wrap env sym rep r (cos `getNth` n) + opt_co4_wrap "SelTyCon" opts env sym rep r (cos `getNth` n) -- see the definition of GHC.Builtin.Types.Prim.funTyCon -opt_co4 env sym rep r (SelCo (SelFun fs) (FunCo _r2 _afl _afr w co1 co2)) - = opt_co4_wrap env sym rep r (getNthFun fs w co1 co2) +opt_co4 opts env sym rep r (SelCo (SelFun fs) (FunCo _r2 _afl _afr w co1 co2)) + = opt_co4_wrap "SelFun" opts env sym rep r (getNthFun fs w co1 co2) -opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo _ eta _)) +opt_co4 opts env sym rep _ (SelCo SelForAll (ForAllCo _ eta _)) -- works for both tyvar and covar - = opt_co4_wrap env sym rep Nominal eta + = opt_co4_wrap "SelForAll" opts env sym rep Nominal eta -opt_co4 env sym rep r (SelCo n co) +opt_co4 opts env sym rep r (SelCo n co) | Just nth_co <- case (co', n) of (TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n) (FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2) @@ -387,71 +433,73 @@ opt_co4 env sym rep r (SelCo n co) _ -> Nothing = if rep && (r == Nominal) -- keep propagating the SubCo - then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co + then opt_co4_wrap "NthCo" opts (zapLiftingContext env) False True Nominal nth_co else nth_co | otherwise = wrapRole rep r $ SelCo n co' where - co' = opt_co1 env sym co + co' = opt_co1 opts env sym co -opt_co4 env sym rep r (LRCo lr co) +opt_co4 opts env sym rep r (LRCo lr co) | Just pr_co <- splitAppCo_maybe co = assert (r == Nominal ) - opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co) + opt_co4_wrap "LrCO AppCo" opts env sym rep Nominal (pick_lr lr pr_co) | Just pr_co <- splitAppCo_maybe co' = assert (r == Nominal) $ if rep - then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co) + then opt_co4_wrap "LrCo AppCo'" opts (zapLiftingContext env) False True Nominal (pick_lr lr pr_co) else pick_lr lr pr_co | otherwise = wrapRole rep Nominal $ LRCo lr co' where - co' = opt_co4_wrap env sym False Nominal co + co' = opt_co4_wrap "LrCo co'" opts env sym False Nominal co pick_lr CLeft (l, _) = l pick_lr CRight (_, r) = r -- See Note [Optimising InstCo] -opt_co4 env sym rep r (InstCo co1 arg) +opt_co4 opts env sym rep r (InstCo co1 arg) -- forall over type... | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1 - = opt_co4_wrap (extendLiftingContext env tv - (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg)) - -- mkSymCo kind_co :: k1 ~ k2 - -- sym_arg :: (t1 :: k1) ~ (t2 :: k2) - -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1) - sym rep r co_body + = opt_co4_wrap "InstCo ForAllTy" opts + (extendLiftingContext env tv + (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg)) + -- mkSymCo kind_co :: k1 ~ k2 + -- sym_arg :: (t1 :: k1) ~ (t2 :: k2) + -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1) + sym rep r co_body -- forall over coercion... | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1 , CoercionTy h1 <- t1 , CoercionTy h2 <- t2 - = let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2 - in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body + = let new_co = mk_new_co cv (opt_co4_wrap "InstCo kind_co" opts env sym False Nominal kind_co) h1 h2 + in opt_co4_wrap "InstCo ForAllCo" opts (extendLiftingContext env cv new_co) sym rep r co_body -- See if it is a forall after optimization -- If so, do an inefficient one-variable substitution, then re-optimize -- forall over type... | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1' - = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv' - (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg')) - False False r' co_body' + = opt_co4_wrap "InstCo ForAllTy 2" opts + (extendLiftingContext (zapLiftingContext env) tv' + (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg')) + False False r' co_body' -- forall over coercion... | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1' , CoercionTy h1' <- t1' , CoercionTy h2' <- t2' = let new_co = mk_new_co cv' kind_co' h1' h2' - in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co) + in opt_co4_wrap "InstCo ForAllCo 2" opts (extendLiftingContext (zapLiftingContext env) cv' new_co) False False r' co_body' | otherwise = InstCo co1' arg' where - co1' = opt_co4_wrap env sym rep r co1 + co1' = opt_co4_wrap "InstCo recur co1" opts env sym rep r co1 r' = chooseRole rep r - arg' = opt_co4_wrap env sym False Nominal arg + arg' = opt_co4_wrap "InstCo recur arg" opts env sym False Nominal arg sym_arg = wrapSym sym arg' -- Performance note: don't be alarmed by the two calls to coercionKind @@ -479,25 +527,28 @@ opt_co4 env sym rep r (InstCo co1 arg) in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1 (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2)) -opt_co4 env sym _rep r (KindCo co) +opt_co4 opts env sym _rep r (KindCo co) = assert (r == Nominal) $ let kco' = promoteCoercion co in case kco' of - KindCo co' -> promoteCoercion (opt_co1 env sym co') - _ -> opt_co4_wrap env sym False Nominal kco' + KindCo co' -> promoteCoercion (opt_co1 opts env sym co') + _ -> opt_co4_wrap "KindCo" opts env sym False Nominal kco' -- This might be able to be optimized more to do the promotion -- and substitution/optimization at the same time -opt_co4 env sym _ r (SubCo co) - = assert (r == Representational) $ - opt_co4_wrap env sym True Nominal co +opt_co4 opts env sym _ _r (SubCo co) + = assert (_r == Representational) $ + let res = opt_co4_wrap "SubCo" opts env sym True Nominal co + in case coercionRole res of + Nominal -> SubCo res + _ -> res -- This could perhaps be optimized more. -opt_co4 env sym rep r (AxiomRuleCo co cs) +opt_co4 opts env sym rep r (AxiomRuleCo co cs) = assert (r == coaxrRole co) $ wrapRole rep r $ wrapSym sym $ - AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs) + AxiomRuleCo co (zipWith (opt_co2 opts env False) (coaxrAsmpRoles co) cs) {- Note [Optimise CoVarCo to Refl] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -511,9 +562,9 @@ in GHC.Core.Coercion. ------------- -- | Optimize a phantom coercion. The input coercion may not necessarily -- be a phantom, but the output sure will be. -opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo -opt_phantom env sym co - = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2 +opt_phantom :: OptCoParams -> LiftingContext -> SymFlag -> Coercion -> NormalCo +opt_phantom opts env sym co + = opt_univ Co opts env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2 where Pair ty1 ty2 = coercionKind co @@ -548,17 +599,41 @@ See #19509. -} -opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role - -> Type -> Type -> Coercion -opt_univ env sym (PhantomProv h) _r ty1 ty2 - | sym = mkPhantomCo h' ty2' ty1' - | otherwise = mkPhantomCo h' ty1' ty2' +type OptRes :: Data.Kind.Type -> Data.Kind.Type +type family OptRes co_or_dco where + OptRes Coercion = Coercion + OptRes DCoercion = ( Type, DCoercion ) + +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 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 +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' = opt_co4 env sym False Nominal h + h' = wrap "opt_univ PhantomProv" (opt_co_or_dco co_or_dco ty1) opts env sym False Nominal h ty1' = substTy (lcSubstLeft env) ty1 ty2' = substTy (lcSubstRight env) ty2 -opt_univ env sym prov role oty1 oty2 + 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) + +opt_univ co_or_dco opts env sym prov role oty1 oty2 | Just (tc1, tys1) <- splitTyConApp_maybe oty1 , Just (tc2, tys2) <- splitTyConApp_maybe oty2 , tc1 == tc2 @@ -567,10 +642,19 @@ opt_univ 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 - arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2 - arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos - in - mkTyConAppCo role tc1 arg_cos' + 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') -- can't optimize the AppTy case because we can't build the kind coercions. @@ -579,13 +663,16 @@ opt_univ env sym prov role oty1 oty2 -- NB: prov isn't interesting here either = let k1 = tyVarKind tv1 k2 = tyVarKind tv2 - eta = mkUnivCo prov' Nominal k1 k2 + eta = case co_or_dco of + Co -> mk_univ Nominal k1 k2 + DCo -> snd $ mk_univ Nominal k1 k2 + tv1' = mk_castTy (TyVarTy tv1) k1 eta k2 -- eta gets opt'ed soon, but not yet. - ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2 + ty2' = substTyWith [tv2] [tv1'] ty2 - (env', tv1', eta') = optForAllCoBndr env sym tv1 eta + (env', tv1'', eta') = opt_forall tv1 eta in - mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2') + mk_forall tv1'' eta' (opt_univ co_or_dco opts env' sym prov' role ty1 ty2') | Just (cv1, ty1) <- splitForAllCoVar_maybe oty1 , Just (cv2, ty2) <- splitForAllCoVar_maybe oty2 @@ -593,17 +680,22 @@ opt_univ env sym prov role oty1 oty2 = let k1 = varType cv1 k2 = varType cv2 r' = coVarRole cv1 - eta = mkUnivCo prov' Nominal k1 k2 - eta_d = downgradeRole r' Nominal eta + eta = case co_or_dco of + Co -> mk_univ Nominal k1 k2 + DCo -> snd $ mk_univ Nominal k1 k2 + eta_d = downgradeRole r' Nominal $ + case co_or_dco of + Co -> eta + DCo -> mkHydrateDCo Nominal k1 eta k2 -- eta gets opt'ed soon, but not yet. n_co = (mkSymCo $ mkSelCo (SelTyCon 2 r') eta_d) `mkTransCo` (mkCoVarCo cv1) `mkTransCo` (mkSelCo (SelTyCon 3 r') eta_d) ty2' = substTyWithCoVars [cv2] [n_co] ty2 - (env', cv1', eta') = optForAllCoBndr env sym cv1 eta + (env', cv1', eta') = opt_forall cv1 eta in - mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2') + mk_forall cv1' eta' (opt_univ co_or_dco opts env' sym prov' role ty1 ty2') | otherwise = let ty1 = substTyUnchecked (lcSubstLeft env) oty1 @@ -611,87 +703,122 @@ opt_univ env sym prov role oty1 oty2 (a, b) | sym = (ty2, ty1) | otherwise = (ty1, ty2) in - mkUnivCo prov' role a b + 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 prov' = case prov of #if __GLASGOW_HASKELL__ < 901 -- This alt is redundant with the first match of the FunDef - PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco + PhantomProv kco -> PhantomProv + $ wrap "univ_co phantom" (opt_co_or_dco co_or_dco oty1) + opts env sym False Nominal kco #endif - ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco - PluginProv _ -> prov - CorePrepProv _ -> prov + ProofIrrelProv kco -> ProofIrrelProv + $ wrap "univ_co proof_irrel" (opt_co_or_dco co_or_dco oty1) + opts env sym False Nominal kco + PluginProv str -> PluginProv str + CorePrepProv homo -> CorePrepProv homo ------------- -opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo] -opt_transList is = zipWithEqual "opt_transList" (opt_trans is) +opt_transList :: HasDebugCallStack => OptCoParams -> InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo] +opt_transList opts is = zipWithEqual "opt_transList" (opt_trans opts is) -- The input lists must have identical length. -opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo -opt_trans is co1 co2 +opt_trans :: OptCoParams -> InScopeSet -> NormalCo -> NormalCo -> NormalCo +opt_trans opts is co1 co2 | isReflCo co1 = co2 -- optimize when co1 is a Refl Co - | otherwise = opt_trans1 is co1 co2 + | otherwise = opt_trans1 opts is co1 co2 -opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo +opt_trans1 :: OptCoParams -> InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo -- First arg is not the identity -opt_trans1 is co1 co2 +opt_trans1 opts is co1 co2 | isReflCo co2 = co1 -- optimize when co2 is a Refl Co - | otherwise = opt_trans2 is co1 co2 + | otherwise = opt_trans2 opts is co1 co2 -opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo +opt_trans2 :: OptCoParams -> InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo -- Neither arg is the identity -opt_trans2 is (TransCo co1a co1b) co2 +opt_trans2 opts is (TransCo co1a co1b) co2 -- Don't know whether the sub-coercions are the identity - = opt_trans is co1a (opt_trans is co1b co2) + = opt_trans opts is co1a (opt_trans opts is co1b co2) -opt_trans2 is co1 co2 - | Just co <- opt_trans_rule is co1 co2 +opt_trans2 opts is co1 co2 + | Just co <- opt_trans_rule opts is co1 co2 = co -opt_trans2 is co1 (TransCo co2a co2b) - | Just co1_2a <- opt_trans_rule is co1 co2a +opt_trans2 opts is co1 (TransCo co2a co2b) + | Just co1_2a <- opt_trans_rule opts is co1 co2a = if isReflCo co1_2a then co2b - else opt_trans1 is co1_2a co2b + else opt_trans1 opts is co1_2a co2b -opt_trans2 _ co1 co2 +opt_trans2 _ _ co1 co2 = mkTransCo co1 co2 ------ + -- Optimize coercions with a top-level use of transitivity. -opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo +opt_trans_rule :: OptCoParams -> InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo + +-- Handle a composition of two directed coercions. +opt_trans_rule opts is (HydrateDCo r lty1 dco1 _) (HydrateDCo _ lty2 dco2 rhs2) + = ( \ dco -> mkHydrateDCo r lty1 dco rhs2 ) + <$> opt_trans_rule_dco opts is r lty1 dco1 lty2 dco2 -opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2)) +opt_trans_rule opts is (SymCo (HydrateDCo r lty1 dco1 rhs1)) (SymCo (HydrateDCo _ lty2 dco2 _)) + = ( \ dco -> mkSymCo $ mkHydrateDCo r lty2 dco rhs1 ) + <$> opt_trans_rule_dco opts is r lty2 dco2 lty1 dco1 + +-- When composing a Coercion with a DCoercion, we could imagine hydrating the DCoercion +-- a single step (e.g. using 'hydrateOneLayerDCo') to expose cancellation opportunities. +-- We don't do that for now. + +opt_trans_rule opts is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2)) = assert (r1 == r2) $ fireTransRule "GRefl" in_co1 in_co2 $ - mkGReflRightCo r1 t1 (opt_trans is co1 co2) + mkGReflRightCo r1 t1 (opt_trans opts is co1 co2) -- Push transitivity through matching destructors -opt_trans_rule is in_co1@(SelCo d1 co1) in_co2@(SelCo d2 co2) +opt_trans_rule opts is in_co1@(SelCo d1 co1) in_co2@(SelCo d2 co2) | d1 == d2 , coercionRole co1 == coercionRole co2 , co1 `compatible_co` co2 = fireTransRule "PushNth" in_co1 in_co2 $ - mkSelCo d1 (opt_trans is co1 co2) + mkSelCo d1 (opt_trans opts is co1 co2) -opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2) +opt_trans_rule opts is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2) | d1 == d2 , co1 `compatible_co` co2 = fireTransRule "PushLR" in_co1 in_co2 $ - mkLRCo d1 (opt_trans is co1 co2) + mkLRCo d1 (opt_trans opts is co1 co2) -- Push transitivity inside instantiation -opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2) +opt_trans_rule opts is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2) | ty1 `eqCoercion` ty2 , co1 `compatible_co` co2 = fireTransRule "TrPushInst" in_co1 in_co2 $ - mkInstCo (opt_trans is co1 co2) ty1 + mkInstCo (opt_trans opts is co1 co2) ty1 -opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1) - in_co2@(UnivCo p2 r2 _tyl2 tyr2) +opt_trans_rule opts is in_co1@(UnivCo p1 r1 tyl1 _tyr1) + in_co2@(UnivCo p2 r2 _tyl2 tyr2) | Just prov' <- opt_trans_prov p1 p2 = assert (r1 == r2) $ fireTransRule "UnivCo" in_co1 in_co2 $ @@ -699,54 +826,56 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1) where -- if the provenances are different, opt'ing will be very confusing opt_trans_prov (PhantomProv kco1) (PhantomProv kco2) - = Just $ PhantomProv $ opt_trans is kco1 kco2 + = Just $ PhantomProv $ opt_trans opts is kco1 kco2 opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2) - = Just $ ProofIrrelProv $ opt_trans is kco1 kco2 - opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1 + = Just $ ProofIrrelProv $ opt_trans opts is kco1 kco2 + opt_trans_prov (PluginProv str1) (PluginProv str2) + | str1 == str2 + = Just p1 opt_trans_prov _ _ = Nothing -- Push transitivity down through matching top-level constructors. -opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2) +opt_trans_rule opts is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2) | tc1 == tc2 = assert (r1 == r2) $ fireTransRule "PushTyConApp" in_co1 in_co2 $ - mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2) + mkTyConAppCo r1 tc1 (opt_transList opts is cos1 cos2) -opt_trans_rule is in_co1@(FunCo r1 afl1 afr1 w1 co1a co1b) - in_co2@(FunCo r2 afl2 afr2 w2 co2a co2b) +opt_trans_rule opts is in_co1@(FunCo r1 afl1 afr1 w1 co1a co1b) + in_co2@(FunCo r2 afl2 afr2 w2 co2a co2b) = assert (r1 == r2) $ -- Just like the TyConAppCo/TyConAppCo case assert (afr1 == afl2) $ fireTransRule "PushFun" in_co1 in_co2 $ - mkFunCo2 r1 afl1 afr2 (opt_trans is w1 w2) - (opt_trans is co1a co2a) - (opt_trans is co1b co2b) + mkFunCo2 r1 afl1 afr2 (opt_trans opts is w1 w2) + (opt_trans opts is co1a co2a) + (opt_trans opts is co1b co2b) -opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b) +opt_trans_rule opts is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b) -- Must call opt_trans_rule_app; see Note [EtaAppCo] - = opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b] + = opt_trans_rule_app opts is in_co1 in_co2 co1a [co1b] co2a [co2b] -- Eta rules -opt_trans_rule is co1@(TyConAppCo r tc cos1) co2 +opt_trans_rule opts is co1@(TyConAppCo r tc cos1) co2 | Just cos2 <- etaTyConAppCo_maybe tc co2 = fireTransRule "EtaCompL" co1 co2 $ - mkTyConAppCo r tc (opt_transList is cos1 cos2) + mkTyConAppCo r tc (opt_transList opts is cos1 cos2) -opt_trans_rule is co1 co2@(TyConAppCo r tc cos2) +opt_trans_rule opts is co1 co2@(TyConAppCo r tc cos2) | Just cos1 <- etaTyConAppCo_maybe tc co1 = fireTransRule "EtaCompR" co1 co2 $ - mkTyConAppCo r tc (opt_transList is cos1 cos2) + mkTyConAppCo r tc (opt_transList opts is cos1 cos2) -opt_trans_rule is co1@(AppCo co1a co1b) co2 +opt_trans_rule opts is co1@(AppCo co1a co1b) co2 | Just (co2a,co2b) <- etaAppCo_maybe co2 - = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b] + = opt_trans_rule_app opts is co1 co2 co1a [co1b] co2a [co2b] -opt_trans_rule is co1 co2@(AppCo co2a co2b) +opt_trans_rule opts is co1 co2@(AppCo co2a co2b) | Just (co1a,co1b) <- etaAppCo_maybe co1 - = opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b] + = opt_trans_rule_app opts is co1 co2 co1a [co1b] co2a [co2b] -- Push transitivity inside forall -- forall over types. -opt_trans_rule is co1 co2 +opt_trans_rule opts is co1 co2 | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1 , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2 = push_trans tv1 eta1 r1 tv2 eta2 r2 @@ -763,14 +892,14 @@ opt_trans_rule is co1 co2 -- Wanted: -- /\tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1]) = fireTransRule "EtaAllTy_ty" co1 co2 $ - mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2') + mkForAllCo tv1 (opt_trans opts is eta1 eta2) (opt_trans opts is' r1 r2') where is' = is `extendInScopeSet` tv1 r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 -- Push transitivity inside forall -- forall over coercions. -opt_trans_rule is co1 co2 +opt_trans_rule opts is co1 co2 | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1 , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2 = push_trans cv1 eta1 r1 cv2 eta2 r2 @@ -789,7 +918,7 @@ opt_trans_rule is co1 co2 -- n2 = nth 3 eta1 -- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2]) = fireTransRule "EtaAllTy_co" co1 co2 $ - mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2') + mkForAllCo cv1 (opt_trans opts is eta1 eta2) (opt_trans opts is' r1 r2') where is' = is `extendInScopeSet` cv1 role = coVarRole cv1 @@ -801,7 +930,7 @@ opt_trans_rule is co1 co2 r2 -- Push transitivity inside axioms -opt_trans_rule is co1 co2 +opt_trans_rule opts is co1 co2 -- See Note [Push transitivity inside axioms] and -- Note [Push transitivity inside newtype axioms only] @@ -810,34 +939,34 @@ opt_trans_rule is co1 co2 , isNewTyCon (coAxiomTyCon con) , True <- sym , Just cos2 <- matchAxiom sym con ind co2 - , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1) + , let newAxInst = AxiomInstCo con ind (opt_transList opts is (map mkSymCo cos2) cos1) = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst - -- TrPushAxR + -- TrPushAxR (AxSuckR) | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe , isNewTyCon (coAxiomTyCon con) , False <- sym , Just cos2 <- matchAxiom sym con ind co2 - , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2) + , let newAxInst = AxiomInstCo con ind (opt_transList opts is cos1 cos2) = fireTransRule "TrPushAxR" co1 co2 newAxInst - -- TrPushSymAxL + -- TrPushSymAxL (SymAxSuckL) | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe , isNewTyCon (coAxiomTyCon con) , True <- sym , Just cos1 <- matchAxiom (not sym) con ind co1 - , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1)) + , let newAxInst = AxiomInstCo con ind (opt_transList opts is cos2 (map mkSymCo cos1)) = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst - -- TrPushAxL + -- TrPushAxL (AxSuckL) | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe , isNewTyCon (coAxiomTyCon con) , False <- sym , Just cos1 <- matchAxiom (not sym) con ind co1 - , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2) + , let newAxInst = AxiomInstCo con ind (opt_transList opts is cos1 cos2) = fireTransRule "TrPushAxL" co1 co2 newAxInst - -- TrPushAxSym/TrPushSymAx + -- TrPushAxSym/TrPushSymAx (AxSym/SymAx) | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe , con1 == con2 @@ -851,16 +980,16 @@ opt_trans_rule is co1 co2 , all (`elemVarSet` pivot_tvs) qtvs = fireTransRule "TrPushAxSym" co1 co2 $ if sym2 - -- TrPushAxSym - then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs - -- TrPushSymAx - else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs + -- TrPushAxSym (AxSym) + then liftCoSubstWith role qtvs (opt_transList opts is cos1 (map mkSymCo cos2)) lhs + -- TrPushSymAx (SymAx) + else liftCoSubstWith role qtvs (opt_transList opts is (map mkSymCo cos1) cos2) rhs where co1_is_axiom_maybe = isAxiom_maybe co1 co2_is_axiom_maybe = isAxiom_maybe co2 role = coercionRole co1 -- should be the same as coercionRole co2! -opt_trans_rule _ co1 co2 -- Identity rule +opt_trans_rule _ _ co1 co2 -- Identity rule | let ty1 = coercionLKind co1 r = coercionRole co1 ty2 = coercionRKind co2 @@ -868,10 +997,11 @@ opt_trans_rule _ co1 co2 -- Identity rule = fireTransRule "RedTypeDirRefl" co1 co2 $ mkReflCo r ty2 -opt_trans_rule _ _ _ = Nothing +opt_trans_rule _ _ _ _ = Nothing -- See Note [EtaAppCo] -opt_trans_rule_app :: InScopeSet +opt_trans_rule_app :: OptCoParams + -> InScopeSet -> Coercion -- original left-hand coercion (printing only) -> Coercion -- original right-hand coercion (printing only) -> Coercion -- left-hand coercion "function" @@ -879,14 +1009,14 @@ opt_trans_rule_app :: InScopeSet -> Coercion -- right-hand coercion "function" -> [Coercion] -- right-hand coercion "args" -> Maybe Coercion -opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs +opt_trans_rule_app opts is orig_co1 orig_co2 co1a co1bs co2a co2bs | AppCo co1aa co1ab <- co1a , Just (co2aa, co2ab) <- etaAppCo_maybe co2a - = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs) + = opt_trans_rule_app opts is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs) | AppCo co2aa co2ab <- co2a , Just (co1aa, co1ab) <- etaAppCo_maybe co1a - = opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs) + = opt_trans_rule_app opts is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs) | otherwise = assert (co1bs `equalLength` co2bs) $ @@ -907,12 +1037,224 @@ opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs co2bs'' = zipWith mkTransCo co2bs' co2bs in - mkAppCos (opt_trans is co1a co2a') - (zipWith (opt_trans is) co1bs co2bs'') + mkAppCos (opt_trans opts is co1a co2a') + (zipWith (opt_trans opts is) co1bs co2bs'') fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion fireTransRule _rule _co1 _co2 res - = Just res + = -- pprTrace _rule + -- (vcat [ text "co1:" <+> ppr _co1 + -- , text "co2:" <+> ppr _co2 + -- , text "res:" <+> ppr res ]) $ + Just res + +------ +-- Optimize directed coercions + +-- 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 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) + 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 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 + +opt_dco2 :: OptCoParams + -> LiftingContext + -> Role -- ^ The role of the input coercion + -> Type + -> DCoercion -> (Type, NormalDCo) +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 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 + + ReflDCo + -> lifted_dco + GReflRightDCo kco + | isGReflCo kco || isGReflCo kco' + -> lifted_dco + | otherwise + -> (l_ty', mkGReflRightDCo kco') + where + kco' = opt_co4 opts env False False Nominal kco + GReflLeftDCo kco + | isGReflCo kco || isGReflCo kco' + -> lifted_dco + | otherwise + -> (l_ty', mkGReflLeftDCo 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) = + 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) + + | otherwise + -> pprPanic "opt_dco4: TyConAppDCo where ty is not a TyConApp" $ + vcat [ text "dco =" <+> ppr dco + , text "l_ty =" <+> ppr l_ty ] + + 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) + | otherwise + -> pprPanic "opt_dco4: AppDCo where ty is not an AppTy" $ + vcat [ text "dco =" <+> ppr dco + , text "l_ty =" <+> ppr l_ty ] + + 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 + (env', dco_tcv', k_dco') -> + -- SLD TODO: can this be simplified? I made too many mistakes writing this... + let body_ty' = substTyWithInScope (lcInScopeSet env') [ty_tv] [mkTyVarTy dco_tcv'] body_ty + (body_ty'', body_dco') = opt_dco4_wrap "ForAllDCo" opts env' rep r body_ty' body_dco + forall_ty = mkForAllTy (Bndr dco_tcv' af) body_ty'' + forall_dco = mkForAllDCo dco_tcv' k_dco' body_dco' + forall_ty' = followDCo r forall_ty forall_dco + in (forall_ty, wrapRole_dco rep r forall_ty forall_dco forall_ty') + | otherwise + -> 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') + + AxiomInstDCo {} + -> (l_ty', rep_dco) + StepsDCo {} + -> (l_ty', rep_dco) + + 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 + + -- 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 + in + (l_ty', opt_trans_dco opts (lcInScopeSet env) r' l_ty' dco1' mid_ty' dco2') + + 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') + + where + lifted_dco = let lifted_co = liftCoSubst r' env l_ty + in ( coercionLKind lifted_co, mkDehydrateCo lifted_co ) + 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) + +--------------------------------------------------------- +-- Transitivity for directed coercions. + +opt_trans_dco :: OptCoParams -> InScopeSet -> Role -> Type -> NormalDCo -> Type -> NormalDCo -> NormalDCo +opt_trans_dco opts is r l_ty dco1 mid_ty dco2 + | isReflDCo dco1 = dco2 + -- optimize when dco1 is a Refl DCo + | otherwise = opt_trans1_dco opts is r l_ty dco1 mid_ty dco2 + +opt_trans1_dco :: OptCoParams -> InScopeSet -> Role -> Type -> NormalNonIdDCo -> Type -> NormalDCo -> NormalDCo +-- First arg is not the identity +opt_trans1_dco opts is r l_ty dco1 mid_ty dco2 + | isReflDCo dco2 = dco1 + -- optimize when co2 is a Refl Co + | otherwise = opt_trans2_dco opts is r l_ty dco1 mid_ty dco2 + +opt_trans2_dco :: OptCoParams -> InScopeSet -> Role -> Type -> NormalNonIdDCo -> Type -> NormalNonIdDCo -> NormalDCo +-- Neither arg is the identity +opt_trans2_dco opts is r l_ty (TransDCo dco1a dco1b) mid_ty dco2 + -- Don't know whether the sub-coercions are the identity + = let inner_ty = followDCo r l_ty dco1a + in opt_trans_dco opts is r l_ty dco1a inner_ty + (opt_trans_dco opts is r inner_ty dco1b mid_ty dco2) + + +opt_trans2_dco opts is r l_ty dco1 mid_ty dco2 + | Just co <- opt_trans_rule_dco opts is r l_ty dco1 mid_ty dco2 + = co + +opt_trans2_dco opts is r l_ty dco1 mid_ty (TransDCo dco2a dco2b) + | Just dco1_2a <- opt_trans_rule_dco opts is r l_ty dco1 mid_ty dco2a + = if isReflDCo dco1_2a + then dco2b + else + let inner_ty = followDCo r mid_ty dco1_2a + in opt_trans1_dco opts is r mid_ty dco1_2a inner_ty dco2b + +opt_trans2_dco _ _ _ _ dco1 _ dco2 + = mkTransDCo dco1 dco2 + +opt_trans_rule_dco :: OptCoParams -> InScopeSet -> Role -> Type -> NormalNonIdDCo -> Type -> NormalNonIdDCo -> Maybe NormalDCo + +-- Handle undirected coercions. +opt_trans_rule_dco opts is _ _ (DehydrateCo co1) _ (DehydrateCo co2) + = DehydrateCo <$> opt_trans_rule opts is co1 co2 + +opt_trans_rule_dco _ _ r l_ty dco1 mid_ty dco2 + | let r_ty = followDCo r mid_ty dco2 + , l_ty `eqType` r_ty + = fireTransRule_dco "RedTypeDirRefl" dco1 dco2 $ + mkReflDCo + +opt_trans_rule_dco _ _ _ _ _ _ _ = Nothing + +fireTransRule_dco :: String -> DCoercion -> DCoercion -> DCoercion -> Maybe DCoercion +fireTransRule_dco _rule _dco1 _dco2 res + = --pprTrace _rule + -- (vcat [ text "dco1:" <+> ppr _dco1 + -- , text "dco2:" <+> ppr _dco2 + -- , text "res:" <+> ppr res ]) $ + Just res {- Note [Push transitivity inside axioms] @@ -1092,12 +1434,21 @@ wrapSym sym co | sym = mkSymCo co | otherwise = co -- | Conditionally set a role to be representational -wrapRole :: ReprFlag +wrapRole :: HasDebugCallStack + => ReprFlag -> Role -- ^ current role -> Coercion -> Coercion wrapRole False _ = id wrapRole True current = downgradeRole Representational current +wrapRole_dco :: HasDebugCallStack + => ReprFlag + -> Role -- ^ current role + -> Type -> DCoercion -> Type + -> DCoercion +wrapRole_dco False _ _ dco _ = dco +wrapRole_dco True current l_ty dco r_ty = downgradeDCoToRepresentational current l_ty dco r_ty + -- | If we require a representational role, return that. Otherwise, -- return the "default" role provided. chooseRole :: ReprFlag @@ -1112,6 +1463,7 @@ isAxiom_maybe (SymCo co) | Just (sym, con, ind, cos) <- isAxiom_maybe co = Just (not sym, con, ind, cos) isAxiom_maybe (AxiomInstCo con ind cos) + | isNewTyCon (coAxiomTyCon con) -- Adam Gundry's special sauce = Just (False, con, ind, cos) isAxiom_maybe _ = Nothing @@ -1294,7 +1646,19 @@ and these two imply -} -optForAllCoBndr :: LiftingContext -> Bool +optForAllCoBndr :: OptCoParams + -> LiftingContext -> Bool -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion) -optForAllCoBndr env sym - = substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env +optForAllCoBndr opts env sym + = substForAllCoBndrUsingLC sym + (substTyUnchecked (lcSubstLeft env)) + (opt_co4_wrap "optForAllCoBndr" opts env sym False Nominal) env + +optForAllDCoBndr :: OptCoParams + -> LiftingContext -> Bool + -> TyCoVar -> DCoercion -> (LiftingContext, TyCoVar, DCoercion) +optForAllDCoBndr opts env sym tv + = substForAllDCoBndrUsingLC sym + (substTyUnchecked (lcSubstLeft env)) + (snd . opt_dco4_wrap "optForAllDCoBndr" opts env False Nominal (tyVarKind tv)) env + tv |