diff options
Diffstat (limited to 'compiler/GHC/Core/TyCo/Rep.hs')
| -rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 310 |
1 files changed, 258 insertions, 52 deletions
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 245a1c507b..11e4b6db79 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE GADTs #-} {-# OPTIONS_HADDOCK not-home #-} @@ -42,6 +43,9 @@ module GHC.Core.TyCo.Rep ( CoercionN, CoercionR, CoercionP, KindCoercion, MCoercion(..), MCoercionR, MCoercionN, + DCoercion(..), DCoercionN, KindDCoercion, + CoOrDCo(..), + -- * Functions over types mkNakedTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, @@ -61,7 +65,7 @@ module GHC.Core.TyCo.Rep ( TyCoFolder(..), foldTyCo, noView, -- * Sizes - typeSize, typesSize, coercionSize, provSize, + typeSize, typesSize, coercionSize, dcoercionSize, provSize, -- * Multiplicities Scaled(..), scaledMult, scaledThing, mapScaledType, Mult @@ -69,7 +73,7 @@ module GHC.Core.TyCo.Rep ( import GHC.Prelude -import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprCo, pprTyLit ) +import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprCo, pprParendCo, pprDCo, pprTyLit ) import {-# SOURCE #-} GHC.Builtin.Types import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstraint ) @@ -882,9 +886,23 @@ data Coercion -- The number coercions should match exactly the expectations -- of the CoAxiomRule (i.e., the rule is fully saturated). - | UnivCo UnivCoProvenance Role Type Type + | UnivCo (UnivCoProvenance Coercion) Role Type Type -- :: _ -> "e" -> _ -> _ -> e + -- | Embed a directed coercion into a coercion, by specifying + -- the LHS type and role of the directed coercion. + -- + -- The RHS type is also cached, as we often already know the RHS, + -- which avoids us computing it anew using 'followDCo'. + -- + -- See Note [Directed coercions] + | HydrateDCo + Role -- ^ `r` + Type -- ^ `lhs`: LHS type of the directed coercion + DCoercion + Type -- ^ Cached RHS type of the directed coercion. + -- Can be computed from `r` and `lhs` using 'followDCo'. + | SymCo Coercion -- :: e -> e | TransCo Coercion Coercion -- :: e -> e -> e @@ -980,7 +998,7 @@ type MCoercionN = MCoercion instance Outputable MCoercion where ppr MRefl = text "MRefl" - ppr (MCo co) = text "MCo" <+> ppr co + ppr (MCo co) = text "MCo" <+> pprParendCo co {- Note [Refl invariant] ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1402,6 +1420,152 @@ A more nuanced treatment might be able to relax this condition somewhat, by checking if t1 and/or t2 use their bound variables in nominal ways. If not, having w be representational is OK. +Note [Directed coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~ +A directed coercion is a compact representation of a coercion, used to avoid +storing a large amount of extra types in coercions in the rewriter. + +Recall that a coercion always contains enough information for us to be +able to retrieve its role and its left and right hand side types. + +Examples: + + Refl ty + coercionRole: Nominal + coercionLKind: ty + coercionRKind: ty + + TyConAppCo r tc cos + coercionRole: r + coercionLKind: mkTyConApp tc (map coercionLKind cos) + coercionRKind: mkTyConApp tc (map coercionRKind cos) + +In practice, this means that when rewriting type family applications, +coercions end up storing large amounts of extra information: + + type family a + b where + Zero + b = b + Succ a + b = Succ (a + b) + +Reducing 5 + 0 gives rise to a coercion of the form + + +[1] <Succ (Succ (Succ (Succ Zero)))> <Zero> + ; (Succ (+[1] <Succ (Succ (Succ Zero))> <Zero> + ; (Succ (+[1] <Succ (Succ Zero)> <Zero> + ; (Succ (+[1] <Succ Zero> <Zero> + ; (Succ (+[1] <Zero> <Zero> + ; (Succ (+[0] <Zero>)))))))))) + +Compare this to the corresponding directed coercion, where we don't store +so many types: + + Steps 1 + ; (TyConApp (Steps 1 + ; (TyConApp (Steps 1 + ; (TyConApp (Steps 1 + ; (TyConApp (Steps 1 + ; (TyConApp (Steps 1)))))))))) + +To achieve this, we sacrifice being able to query what the LHS type of a +directed coercion is. Instead, this information must be provided as an +input. More specifically, when we have: + + dco :: lhs ~r rhs + +We understand that the role `r` and the LHS type `lhs` are **inputs**, +from which we are able to compute the RHS type `rhs`. +(This is what the function followDCo does.) +This allows us to get away with storing less information in a directed +coercion than in an undirected coercion, while still retaining the ability +to run Core Lint on our program. +-} + +type DCoercionN = DCoercion +type KindDCoercion = DCoercionN + +-- | A directed coercion is a more compact representation of a coercion, +-- which is used in the rewriter to avoid producing quadratically large +-- coercions. +-- +-- For a directed coercion @dco :: lhs ~r rhs@, we think of the role @r@ +-- and the LHS type @lhs@ as /inputs/. Only once this context is given +-- are we able to compute the RHS type @rhs@. +-- +-- See Note [Directed coercions]. +data DCoercion + + -- | 'ReflCo' for 'DCoercion'. + = ReflDCo + + -- | 'GReflCo' for 'DCoercion'. + | GReflRightDCo CoercionN + + -- | @GReflLeftDCo mco@ corresponds to @SymCo (GReflCo mco)@. + -- + -- We need this alongside @GReflRightDCo@ because we don't have + -- symmetry for directed coercions. + | GReflLeftDCo CoercionN + -- SLD TODO: remove GReflLeftDCo? We could use @GReflRightDCo (mkSymMCo mco)@. + + -- | 'TyConAppCo' for 'DCoercion'. + -- + -- NB: we use 'TyConAppDCo' for functions too, + -- unlike coercions which have 'TyConAppCo' and 'FunCo'. + | TyConAppDCo [DCoercion] + + -- | 'AppCo' for 'DCoercion'. + | AppDCo DCoercion DCoercionN + + -- | 'ForAllCo' for 'DCoercion'. + | ForAllDCo TyCoVar KindDCoercion DCoercion + + -- | 'CoVarCo' for 'DCoercion'. + | CoVarDCo CoVar + + -- | 'AxiomInstCo' for 'DCoercion', but specialised + -- to open type family coercion axioms. + -- + -- For newtypes and closed type families, we use the more + -- compact 'StepsDCo'. + | AxiomInstDCo (CoAxiom Branched) + + -- | @StepsDCo n@ means: \"take n successive reduction steps\", + -- where a reduction step could be using a closed type family equation + -- or using a newtype axiom. + | StepsDCo !Int + + -- | 'UnivCo' for 'DCoercion'. We only need to store the RHS type, + -- as the LHS type and role will be provided by context. + | UnivDCo + (UnivCoProvenance DCoercion) + Type -- ^ RHS type + + -- | 'TransCo' for 'DCoercion'. + | TransDCo DCoercion DCoercion + + -- | 'SubCo' for 'DCoercion'. + | SubDCo DCoercion + + -- | Embed a coercion inside a directed coercion, e.g. \"forget\" + -- that we can compute its LHS type and role without context. + | DehydrateCo Coercion + + deriving Data.Data + +instance Outputable DCoercion where + ppr = pprDCo + +-- | A convenient GADT for handling 'Coercion' and 'DCoercion' +-- at the same time. +data CoOrDCo co_or_dco where + Co :: CoOrDCo Coercion + DCo :: CoOrDCo DCoercion + +instance Outputable (CoOrDCo co_or_dco) where + ppr Co = text "Co" + ppr DCo = text "DCo" + +{- %************************************************************************ %* * @@ -1425,25 +1589,25 @@ role and kind, which is done in the UnivCo constructor. -- It is reasonable to consider each constructor of 'UnivCoProvenance' -- as a totally independent coercion form; their only commonality is -- that they don't tell you what types they coercion between. (That info --- is in the 'UnivCo' constructor of 'Coercion'. -data UnivCoProvenance - = PhantomProv KindCoercion -- ^ See Note [Phantom coercions]. Only in Phantom - -- roled coercions +-- is in the 'UnivCo' constructor of 'Coercion'). +data UnivCoProvenance kco + = PhantomProv kco -- ^ See Note [Phantom coercions]. Only in Phantom + -- roled coercions - | ProofIrrelProv KindCoercion -- ^ From the fact that any two coercions are - -- considered equivalent. See Note [ProofIrrelProv]. - -- Can be used in Nominal or Representational coercions + | ProofIrrelProv kco -- ^ From the fact that any two coercions are + -- considered equivalent. See Note [ProofIrrelProv]. + -- Can be used in Nominal or Representational coercions | PluginProv String -- ^ From a plugin, which asserts that this coercion -- is sound. The string is for the use of the plugin. - | CorePrepProv -- See Note [Unsafe coercions] in GHC.Core.CoreToStg.Prep + | CorePrepProv -- ^ See Note [Unsafe coercions] in GHC.Core.CoreToStg.Prep Bool -- True <=> the UnivCo must be homogeneously kinded -- False <=> allow hetero-kinded, e.g. Int ~ Int# deriving Data.Data -instance Outputable UnivCoProvenance where +instance Outputable (UnivCoProvenance kco) where ppr (PhantomProv _) = text "(phantom)" ppr (ProofIrrelProv _) = text "(proof irrel.)" ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str)) @@ -1708,14 +1872,17 @@ data TyCoFolder env a } {-# INLINE foldTyCo #-} -- See Note [Specialising foldType] -foldTyCo :: Monoid a => TyCoFolder env a -> env - -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a) +foldTyCo :: forall env a. Monoid a => TyCoFolder env a -> env + -> ( Type -> a, [Type] -> a + , Coercion -> a, [Coercion] -> a + , DCoercion -> a, [DCoercion] -> a + ) foldTyCo (TyCoFolder { tcf_view = view , tcf_tyvar = tyvar , tcf_tycobinder = tycobinder , tcf_covar = covar , tcf_hole = cohole }) env - = (go_ty env, go_tys env, go_co env, go_cos env) + = (go_ty env, go_tys env, go_co env, go_cos env, go_dco env, go_dcos env) where go_ty env ty | Just ty' <- view ty = go_ty env ty' go_ty env (TyVarTy tv) = tyvar env tv @@ -1738,38 +1905,61 @@ foldTyCo (TyCoFolder { tcf_view = view go_cos _ [] = mempty go_cos env (c:cs) = go_co env c `mappend` go_cos env cs - go_co env (Refl ty) = go_ty env ty - go_co env (GRefl _ ty MRefl) = go_ty env ty - go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co - go_co env (TyConAppCo _ _ args) = go_cos env args - go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2 - go_co env (CoVarCo cv) = covar env cv - go_co env (AxiomInstCo _ _ args) = go_cos env args - go_co env (HoleCo hole) = cohole env hole - go_co env (UnivCo p _ t1 t2) = go_prov env p `mappend` go_ty env t1 - `mappend` go_ty env t2 - go_co env (SymCo co) = go_co env co - go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2 - go_co env (AxiomRuleCo _ cos) = go_cos env cos - go_co env (SelCo _ co) = go_co env co - go_co env (LRCo _ co) = go_co env co - go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg - go_co env (KindCo co) = go_co env co - go_co env (SubCo co) = go_co env co - - go_co env (FunCo { fco_mult = cw, fco_arg = c1, fco_res = c2 }) - = go_co env cw `mappend` go_co env c1 `mappend` go_co env c2 - - go_co env (ForAllCo tv kind_co co) - = go_co env kind_co `mappend` go_ty env (varType tv) - `mappend` go_co env' co + go_co env (Refl ty) = go_ty env ty + go_co env (GRefl _ ty MRefl) = go_ty env ty + go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co + go_co env (TyConAppCo _ _ args) = go_cos env args + go_co env (AppCo c1 c2) = go_co env c1 `mappend` go_co env c2 + go_co env (FunCo _ _ _ cw c1 c2) = go_co env cw `mappend` + go_co env c1 `mappend` + go_co env c2 + go_co env (CoVarCo cv) = covar env cv + go_co env (AxiomInstCo _ _ args) = go_cos env args + go_co env (HoleCo hole) = cohole env hole + go_co env (HydrateDCo _ t1 dco _t2) = go_ty env t1 `mappend` go_dco env dco + go_co env (UnivCo p _ t1 t2) = go_prov go_co env p + `mappend` go_ty env t1 + `mappend` go_ty env t2 + go_co env (SymCo co) = go_co env co + go_co env (TransCo co1 co2) = go_co env co1 `mappend` go_co env co2 + go_co env (AxiomRuleCo _ cos) = go_cos env cos + go_co env (SelCo _ co) = go_co env co + go_co env (LRCo _ co) = go_co env co + go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg + go_co env (KindCo co) = go_co env co + go_co env (SubCo co) = go_co env co + go_co env (ForAllCo tv kind_co co) = go_co env kind_co + `mappend` go_ty env (varType tv) + `mappend` go_co env' co + where + !env' = tycobinder env tv Inferred + + go_dcos _ [] = mempty + go_dcos env (c:cs) = go_dco env c `mappend` go_dcos env cs + + go_dco _ ReflDCo = mempty + go_dco env (GReflRightDCo co) = go_co env co + go_dco env (GReflLeftDCo co) = go_co env co + go_dco env (TyConAppDCo args) = go_dcos env args + go_dco env (AppDCo c1 c2) = go_dco env c1 `mappend` go_dco env c2 + go_dco env (CoVarDCo cv) = covar env cv + go_dco _ AxiomInstDCo{} = mempty + go_dco _ StepsDCo{} = mempty + go_dco env (TransDCo co1 co2) = go_dco env co1 `mappend` go_dco env co2 + go_dco env (SubDCo dco) = go_dco env dco + go_dco env (DehydrateCo co) = go_co env co + go_dco env (ForAllDCo tv kind_dco co) = go_dco env kind_dco + `mappend` go_ty env (varType tv) + `mappend` go_dco env' co where - env' = tycobinder env tv Inferred + !env' = tycobinder env tv Inferred + go_dco env (UnivDCo prov t2) = go_prov go_dco env prov `mappend` go_ty env t2 - go_prov env (PhantomProv co) = go_co env co - go_prov env (ProofIrrelProv co) = go_co env co - go_prov _ (PluginProv _) = mempty - go_prov _ (CorePrepProv _) = mempty + go_prov :: (env ->co -> a) -> env -> UnivCoProvenance co -> a + go_prov do_fold env (PhantomProv co) = do_fold env co + go_prov do_fold env (ProofIrrelProv co) = do_fold env co + go_prov _ _ (PluginProv _) = mempty + go_prov _ _ (CorePrepProv _) = mempty -- | A view function that looks through nothing. noView :: Type -> Maybe Type @@ -1821,7 +2011,8 @@ coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2 coercionSize (CoVarCo _) = 1 coercionSize (HoleCo _) = 1 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args) -coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2 +coercionSize (HydrateDCo _ t1 dco t2) = 1 + typeSize t1 + dcoercionSize dco + typeSize t2 +coercionSize (UnivCo p _ t1 t2) = 1 + provSize coercionSize p + typeSize t1 + typeSize t2 coercionSize (SymCo co) = 1 + coercionSize co coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2 coercionSize (SelCo _ co) = 1 + coercionSize co @@ -1831,11 +2022,26 @@ coercionSize (KindCo co) = 1 + coercionSize co coercionSize (SubCo co) = 1 + coercionSize co coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs) -provSize :: UnivCoProvenance -> Int -provSize (PhantomProv co) = 1 + coercionSize co -provSize (ProofIrrelProv co) = 1 + coercionSize co -provSize (PluginProv _) = 1 -provSize (CorePrepProv _) = 1 +dcoercionSize :: DCoercion -> Int +dcoercionSize ReflDCo = 1 +dcoercionSize (GReflRightDCo co) = 1 + coercionSize co +dcoercionSize (GReflLeftDCo co) = 1 + coercionSize co +dcoercionSize (TyConAppDCo args) = 1 + sum (map dcoercionSize args) +dcoercionSize (AppDCo co arg) = dcoercionSize co + dcoercionSize arg +dcoercionSize (ForAllDCo _ h co) = 1 + dcoercionSize co + dcoercionSize h +dcoercionSize (CoVarDCo _) = 1 +dcoercionSize AxiomInstDCo{} = 1 +dcoercionSize StepsDCo{} = 1 +dcoercionSize (TransDCo co1 co2) = 1 + dcoercionSize co1 + dcoercionSize co2 +dcoercionSize (SubDCo co) = 1 + dcoercionSize co +dcoercionSize (DehydrateCo co) = 1 + coercionSize co +dcoercionSize (UnivDCo prov rhs) = 1 + provSize dcoercionSize prov + typeSize rhs + +provSize :: (co -> Int) -> UnivCoProvenance co -> Int +provSize co_size (PhantomProv co) = 1 + co_size co +provSize co_size (ProofIrrelProv co) = 1 + co_size co +provSize _ (PluginProv _) = 1 +provSize _ (CorePrepProv _) = 1 {- ************************************************************************ |