diff options
Diffstat (limited to 'compiler/GHC/Core/Reduction.hs')
| -rw-r--r-- | compiler/GHC/Core/Reduction.hs | 493 |
1 files changed, 275 insertions, 218 deletions
diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs index a4f1df4f70..bfa2b09523 100644 --- a/compiler/GHC/Core/Reduction.hs +++ b/compiler/GHC/Core/Reduction.hs @@ -7,18 +7,21 @@ module GHC.Core.Reduction -- * Reductions Reduction(..), ReductionN, ReductionR, HetReduction(..), Reductions(..), - mkReduction, mkReductions, mkHetReduction, coercionRedn, - reductionOriginalType, - downgradeRedn, mkSubRedn, + mkReduction, mkReductions, mkHetReduction, mkDehydrateCoercionRedn, + mkHydrateReductionDCoercion, + mkSubRedn, mkTransRedn, mkCoherenceRightRedn, mkCoherenceRightMRedn, mkCastRedn1, mkCastRedn2, mkReflRedn, mkGReflRightRedn, mkGReflRightMRedn, mkGReflLeftRedn, mkGReflLeftMRedn, mkAppRedn, mkAppRedns, mkFunRedn, mkForAllRedn, mkHomoForAllRedn, mkTyConAppRedn, mkClassPredRedn, + mkTyConAppRedn_MightBeSynonym, mkProofIrrelRedn, mkReflCoRedn, - homogeniseHetRedn, + homogeniseHetRedn, homogeniseRedn, unzipRedns, + mkReflRedns, + mkReflDCos, -- * Rewriting type arguments ArgsReductions(..), @@ -28,15 +31,14 @@ module GHC.Core.Reduction import GHC.Prelude -import GHC.Core.Class ( Class(classTyCon) ) +import GHC.Core.Class ( Class(..) ) import GHC.Core.Coercion import GHC.Core.Predicate ( mkClassPred ) -import GHC.Core.TyCon ( TyCon ) +import GHC.Core.TyCon import GHC.Core.Type import GHC.Data.Pair ( Pair(Pair) ) import GHC.Data.List.Infinite ( Infinite (..) ) -import qualified GHC.Data.List.Infinite as Inf import GHC.Types.Var ( VarBndr(..), setTyVarKind ) import GHC.Types.Var.Env ( mkInScopeSet ) @@ -46,6 +48,8 @@ import GHC.Utils.Misc ( HasDebugCallStack, equalLength ) import GHC.Utils.Outputable import GHC.Utils.Panic ( assertPpr ) +import Data.List ( zipWith4 ) + {- %************************************************************************ %* * @@ -55,170 +59,119 @@ import GHC.Utils.Panic ( assertPpr ) Note [The Reduction type] ~~~~~~~~~~~~~~~~~~~~~~~~~ -Many functions in the type-checker rewrite a type, using Given type equalitie -or type-family reductions, and return a Reduction, which is just a pair of the -coercion and the RHS type of the coercion: - data Reduction = Reduction Coercion !Type +Many functions in the type-checker rewrite a type, using Given type equalities +or type-family reductions, and return a Reduction: + + data Reduction = Reduction DCoercion !Type + +When we rewrite ty at role r, producing Reduction dco xi, we guarantee that +dco :: ty ~r xi, up to zonking. + +In particular, if ty is fully zonked, we can call followDCo, and we should have + + followDCo r ty dco ~ xi (up to zonking) -The order of the arguments to the constructor serves as a reminder -of what the Type is. In - Reduction co ty -`ty` appears to the right of `co`, reminding us that we must have: - co :: unrewritten_ty ~ ty +The order of the arguments to the constructor serves as a reminder: + + ty ~rewrite~> Reduction dco xi + +the rewritten type appears on the right, reminding us that we must have: + + dco :: ty ~r xi Example functions that use this datatype: + GHC.Core.FamInstEnv.topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction GHC.Tc.Solver.Rewrite.rewrite :: CtEvidence -> TcType -> TcS Reduction Having Reduction as a data type, with a strict Type field, rather than using -a pair (Coercion,Type) gives several advantages (see #20161) +a tuple (with all fields lazy), gives several advantages (see #20161) * The strictness in Type improved performance in rewriting of type families (around 2.5% improvement in T9872), * Compared to the situation before, it gives improved consistency around orientation of rewritings, as a Reduction is always left-to-right (the coercion's RHS type is always the type stored in the 'Reduction'). No more 'mkSymCo's needed to convert between left-to-right and right-to-left. - -One could imagine storing the LHS type of the coercion in the Reduction as well, -but in fact `reductionOriginalType` is very seldom used, so it's not worth it. -} -- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@. --- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@ --- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined --- by the context. That is, the LHS type of the coercion is the original type --- @ty_in@, while its RHS type is the rewritten type @ty_out@. +-- The 'Reduction' includes: +-- +-- - a directed coercion @dco@, +-- - the rewritten type @ty_out@ -- --- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction', --- which separately stores the kind coercion. +-- such that @dco :: ty_in ~ ty_out@, where the role @r@ of the coercion +-- is determined by the context. -- -- See Note [The Reduction type]. data Reduction = Reduction - { reductionCoercion :: Coercion - , reductionReducedType :: !Type + { reductionDCoercion :: DCoercion + , reductionReducedType :: !Type } --- N.B. the 'Coercion' field must be lazy: see for instance GHC.Tc.Solver.Rewrite.rewrite_tyvar2 --- which returns an error in the 'Coercion' field when dealing with a Derived constraint --- (which is OK as this Coercion gets ignored later). --- We might want to revisit the strictness once Deriveds are removed. +-- NB: the DCoercion field is left lazy, as we might not have any need +-- to look at it. --- | Stores a heterogeneous reduction. --- --- The stored kind coercion must relate the kinds of the --- stored reduction. That is, in @HetReduction (Reduction co xi) kco@, --- we must have: --- --- > co :: ty ~ xi --- > kco :: typeKind ty ~ typeKind xi -data HetReduction = - HetReduction - Reduction - MCoercionN - -- N.B. strictness annotations don't seem to make a difference here - --- | Create a heterogeneous reduction. --- --- Pre-condition: the provided kind coercion (second argument) --- relates the kinds of the stored reduction. --- That is, if the coercion stored in the 'Reduction' is of the form --- --- > co :: ty ~ xi --- --- Then the kind coercion supplied must be of the form: --- --- > kco :: typeKind ty ~ typeKind xi -mkHetReduction :: Reduction -- ^ heterogeneous reduction - -> MCoercionN -- ^ kind coercion - -> HetReduction -mkHetReduction redn mco = HetReduction redn mco -{-# INLINE mkHetReduction #-} +-- | A 'Reduction' in which the 'Coercion' has 'Nominal' role. +type ReductionN = Reduction --- | Homogenise a heterogeneous reduction. --- --- Given @HetReduction (Reduction co xi) kco@, with --- --- > co :: ty ~ xi --- > kco :: typeKind(ty) ~ typeKind(xi) --- --- this returns the homogeneous reduction: --- --- > hco :: ty ~ ( xi |> sym kco ) -homogeniseHetRedn :: Role -> HetReduction -> Reduction -homogeniseHetRedn role (HetReduction redn kco) - = mkCoherenceRightMRedn role redn (mkSymMCo kco) -{-# INLINE homogeniseHetRedn #-} +-- | A 'Reduction' in which the 'Coercion' has 'Representational' role. +type ReductionR = Reduction --- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type. --- --- Pre-condition: the RHS type of the coercion matches the provided type --- (perhaps up to zonking). +-- | Create a 'Reduction' from a pair of a 'DCoercion' and a 'Type. -- --- Use 'coercionRedn' when you only have the coercion. -mkReduction :: Coercion -> Type -> Reduction -mkReduction co ty = Reduction co ty +-- Use 'mkDehydrateCoercionRedn' when you only have a 'Coercion'. +mkReduction :: DCoercion -> Type -> Reduction +mkReduction co rty = Reduction co rty {-# INLINE mkReduction #-} instance Outputable Reduction where ppr redn = braces $ vcat - [ text "reductionOriginalType:" <+> ppr (reductionOriginalType redn) - , text " reductionReducedType:" <+> ppr (reductionReducedType redn) - , text " reductionCoercion:" <+> ppr (reductionCoercion redn) + [ text " reductionReducedType:" <+> ppr (reductionReducedType redn) + , text " reductionDCoercion:" <+> ppr (reductionDCoercion redn) ] --- | A 'Reduction' in which the 'Coercion' has 'Nominal' role. -type ReductionN = Reduction +-- | Turn a 'Coercion' into a 'Reduction' by dehydrating. +-- +-- Prefer using 'mkReduction' wherever possible to avoid doing these indirections. +mkDehydrateCoercionRedn :: Coercion -> Reduction +mkDehydrateCoercionRedn co = + Reduction (mkDehydrateCo co) (coercionRKind co) +{-# INLINE mkDehydrateCoercionRedn #-} --- | A 'Reduction' in which the 'Coercion' has 'Representational' role. -type ReductionR = Reduction +-- | Hydrate the 'DCoercion' stored inside a 'Reduction' into a full-fledged 'Coercion'. +mkHydrateReductionDCoercion :: HasDebugCallStack + => Role + -> Type -- ^ LHS type (must not contain metavariables) + -> Reduction + -> Coercion +mkHydrateReductionDCoercion r lty (Reduction dco rty) = mkHydrateDCo r lty dco rty +{-# INLINE mkHydrateReductionDCoercion #-} --- | Get the original, unreduced type corresponding to a 'Reduction'. --- --- This is obtained by computing the LHS kind of the stored coercion, --- which may be slow. -reductionOriginalType :: Reduction -> Type -reductionOriginalType = coercionLKind . reductionCoercion -{-# INLINE reductionOriginalType #-} - --- | Turn a 'Coercion' into a 'Reduction' --- by inspecting the RHS type of the coercion. --- --- Prefer using 'mkReduction' when you already know --- the RHS type of the coercion, to avoid computing it anew. -coercionRedn :: Coercion -> Reduction -coercionRedn co = Reduction co (coercionRKind co) -{-# INLINE coercionRedn #-} - --- | Downgrade the role of the coercion stored in the 'Reduction'. -downgradeRedn :: Role -- ^ desired role - -> Role -- ^ current role - -> Reduction - -> Reduction -downgradeRedn new_role old_role redn@(Reduction co _) - = redn { reductionCoercion = downgradeRole new_role old_role co } -{-# INLINE downgradeRedn #-} - --- | Downgrade the role of the coercion stored in the 'Reduction', +-- | Downgrade the role of the directed coercion stored in the 'Reduction', -- from 'Nominal' to 'Representational'. -mkSubRedn :: Reduction -> Reduction -mkSubRedn redn@(Reduction co _) = redn { reductionCoercion = mkSubCo co } +mkSubRedn :: HasDebugCallStack => Type -> Reduction -> Reduction +mkSubRedn lhs redn@(Reduction dco rhs) + = redn { reductionDCoercion = mkSubDCo lhs dco rhs } {-# INLINE mkSubRedn #-} --- | Compose a reduction with a coercion on the left. +-- | Compose two reductions. -- --- Pre-condition: the provided coercion's RHS type must match the LHS type --- of the coercion that is stored in the reduction. -mkTransRedn :: Coercion -> Reduction -> Reduction -mkTransRedn co1 redn@(Reduction co2 _) - = redn { reductionCoercion = co1 `mkTransCo` co2 } +-- Assumes that forming a composite is valid, i.e. the RHS type of +-- the first directed coercion equals, up to zonking, +-- the LHS type of the second directed coercion. +mkTransRedn :: Reduction -> Reduction -> Reduction +mkTransRedn (Reduction dco1 _) (Reduction dco2 ty2) + = Reduction (dco1 `mkTransDCo` dco2) ty2 {-# INLINE mkTransRedn #-} -- | The reflexive reduction. -mkReflRedn :: Role -> Type -> Reduction -mkReflRedn r ty = mkReduction (mkReflCo r ty) ty +mkReflRedn :: Type -> Reduction +mkReflRedn ty = mkReduction mkReflDCo ty +{-# INLINE mkReflRedn #-} -- | Create a 'Reduction' from a kind cast, in which -- the casted type is the rewritten type. @@ -226,10 +179,10 @@ mkReflRedn r ty = mkReduction (mkReflCo r ty) ty -- Given @ty :: k1@, @mco :: k1 ~ k2@, -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ -- at the given 'Role'. -mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction -mkGReflRightRedn role ty co +mkGReflRightRedn :: Type -> CoercionN -> Reduction +mkGReflRightRedn ty co = mkReduction - (mkGReflRightCo role ty co) + (mkGReflRightDCo co) (mkCastTy ty co) {-# INLINE mkGReflRightRedn #-} @@ -239,11 +192,13 @@ mkGReflRightRedn role ty co -- Given @ty :: k1@, @mco :: k1 ~ k2@, -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ -- at the given 'Role'. -mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction -mkGReflRightMRedn role ty mco +mkGReflRightMRedn :: Type -> MCoercionN -> Reduction +mkGReflRightMRedn ty MRefl + = mkReflRedn ty +mkGReflRightMRedn ty (MCo kco) = mkReduction - (mkGReflRightMCo role ty mco) - (mkCastTyMCo ty mco) + (mkGReflRightDCo kco) + (mkCastTy ty kco) {-# INLINE mkGReflRightMRedn #-} -- | Create a 'Reduction' from a kind cast, in which @@ -252,10 +207,10 @@ mkGReflRightMRedn role ty mco -- Given @ty :: k1@, @mco :: k1 ~ k2@, -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ -- at the given 'Role'. -mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction -mkGReflLeftRedn role ty co +mkGReflLeftRedn :: Type -> CoercionN -> Reduction +mkGReflLeftRedn ty co = mkReduction - (mkGReflLeftCo role ty co) + (mkGReflLeftDCo co) ty {-# INLINE mkGReflLeftRedn #-} @@ -265,10 +220,12 @@ mkGReflLeftRedn role ty co -- Given @ty :: k1@, @mco :: k1 ~ k2@, -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ -- at the given 'Role'. -mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction -mkGReflLeftMRedn role ty mco +mkGReflLeftMRedn :: Type -> MCoercionN -> Reduction +mkGReflLeftMRedn ty MRefl + = mkReflRedn ty +mkGReflLeftMRedn ty (MCo kco) = mkReduction - (mkGReflLeftMCo role ty mco) + (mkGReflLeftDCo kco) ty {-# INLINE mkGReflLeftMRedn #-} @@ -278,10 +235,10 @@ mkGReflLeftMRedn role ty mco -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@ -- of the given 'Role' (which must match the role of the coercion stored -- in the 'Reduction' argument). -mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction -mkCoherenceRightRedn r (Reduction co1 ty2) kco +mkCoherenceRightRedn :: Reduction -> CoercionN -> Reduction +mkCoherenceRightRedn (Reduction co1 ty2) kco = mkReduction - (mkCoherenceRightCo r ty2 kco co1) + (mkCoherenceRightDCo kco co1) (mkCastTy ty2 kco) {-# INLINE mkCoherenceRightRedn #-} @@ -291,11 +248,12 @@ mkCoherenceRightRedn r (Reduction co1 ty2) kco -- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@ -- of the given 'Role' (which must match the role of the coercion stored -- in the 'Reduction' argument). -mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction -mkCoherenceRightMRedn r (Reduction co1 ty2) kco +mkCoherenceRightMRedn :: Reduction -> MCoercionN -> Reduction +mkCoherenceRightMRedn redn MRefl = redn +mkCoherenceRightMRedn (Reduction co1 ty2) (MCo kco) = mkReduction - (mkCoherenceRightMCo r ty2 kco co1) - (mkCastTyMCo ty2 kco) + (mkCoherenceRightDCo kco co1) + (mkCastTy ty2 kco) {-# INLINE mkCoherenceRightMRedn #-} -- | Apply a cast to a 'Reduction', casting both the original and the reduced type. @@ -307,16 +265,14 @@ mkCoherenceRightMRedn r (Reduction co1 ty2) kco -- -- Pre-condition: the 'Type' passed in is the same as the LHS type -- of the coercion stored in the 'Reduction'. -mkCastRedn1 :: Role - -> Type -- ^ original type - -> CoercionN -- ^ coercion to cast with - -> Reduction -- ^ rewritten type, with rewriting coercion +mkCastRedn1 :: CoercionN -- ^ coercion to cast with + -> Reduction -- ^ rewritten type, with rewriting coercion -> Reduction -mkCastRedn1 r ty cast_co (Reduction co xi) +mkCastRedn1 cast_co (Reduction dco xi) -- co :: ty ~r ty' -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co) = mkReduction - (castCoercionKind1 co r ty xi cast_co) + (castDCoercionKind1 dco cast_co) (mkCastTy xi cast_co) {-# INLINE mkCastRedn1 #-} @@ -327,15 +283,13 @@ mkCastRedn1 r ty cast_co (Reduction co xi) -- -- Pre-condition: the 'Type' passed in is the same as the LHS type -- of the coercion stored in the 'Reduction'. -mkCastRedn2 :: Role - -> Type -- ^ original type - -> CoercionN -- ^ coercion to cast with on the left +mkCastRedn2 :: CoercionN -- ^ coercion to cast with on the left -> Reduction -- ^ rewritten type, with rewriting coercion -> CoercionN -- ^ coercion to cast with on the right -> Reduction -mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co' +mkCastRedn2 cast_co (Reduction nco nty) cast_co' = mkReduction - (castCoercionKind2 nco r ty nty cast_co cast_co') + (castDCoercionKind2 nco cast_co cast_co') (mkCastTy nty cast_co') {-# INLINE mkCastRedn2 #-} @@ -343,26 +297,31 @@ mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co' -- -- Combines 'mkAppCo' and 'mkAppTy`. mkAppRedn :: Reduction -> Reduction -> Reduction -mkAppRedn (Reduction co1 ty1) (Reduction co2 ty2) - = mkReduction (mkAppCo co1 co2) (mkAppTy ty1 ty2) +mkAppRedn (Reduction co1 rty1) (Reduction co2 rty2) + = mkReduction + (mkAppDCo co1 co2) + (mkAppTy rty1 rty2) {-# INLINE mkAppRedn #-} -- | Create a function 'Reduction'. -- -- Combines 'mkFunCo' and 'mkFunTy'. -mkFunRedn :: Role - -> FunTyFlag +mkFunRedn :: FunTyFlag -> ReductionN -- ^ multiplicity reduction + -> DCoercionN -- ^ argument 'RuntimeRep' coercion + -> DCoercionN -- ^ result 'RuntimeRep' coercion -> Reduction -- ^ argument reduction -> Reduction -- ^ result reduction -> Reduction -mkFunRedn r af - (Reduction w_co w_ty) - (Reduction arg_co arg_ty) - (Reduction res_co res_ty) +mkFunRedn af + (Reduction w_co w_rty) + arg_repco + res_repco + (Reduction arg_co arg_rty) + (Reduction res_co res_rty) = mkReduction - (mkFunCo r af w_co arg_co res_co) - (mkFunTy af w_ty arg_ty res_ty) + (mkFunDCo af w_co arg_repco res_repco arg_co res_co) + (mkFunTy af w_rty arg_rty res_rty) {-# INLINE mkFunRedn #-} -- | Create a 'Reduction' associated to a Π type, @@ -374,48 +333,44 @@ mkForAllRedn :: ForAllTyFlag -> ReductionN -- ^ kind reduction -> Reduction -- ^ body reduction -> Reduction -mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty) +mkForAllRedn vis tv1 (Reduction h rki) (Reduction co rty) = mkReduction - (mkForAllCo tv1 h co) - (mkForAllTy (Bndr tv2 vis) ty) + (mkForAllDCo tv1 h co) + (mkForAllTy (Bndr tv2 vis) rty) where - tv2 = setTyVarKind tv1 ki' + tv2 = setTyVarKind tv1 rki {-# INLINE mkForAllRedn #-} -- | Create a 'Reduction' of a quantified type from a -- 'Reduction' of the body. -- -- Combines 'mkHomoForAllCos' and 'mkForAllTys'. -mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction -mkHomoForAllRedn bndrs (Reduction co ty) +mkHomoForAllRedn :: [TyVarBinder] -> Type -> Reduction -> Reduction +mkHomoForAllRedn bndrs ty1 (Reduction co ty2) = mkReduction - (mkHomoForAllCos (binderVars bndrs) co) - (mkForAllTys bndrs ty) + (mkHomoForAllDCos (binderVars bndrs) (typeTypeOrConstraint ty1) co) + (mkForAllTys bndrs ty2) {-# INLINE mkHomoForAllRedn #-} -- | Create a 'Reduction' from a coercion between coercions. -- -- Combines 'mkProofIrrelCo' and 'mkCoercionTy'. -mkProofIrrelRedn :: Role -- ^ role of the created coercion, "r" - -> CoercionN -- ^ co :: phi1 ~N phi2 - -> Coercion -- ^ g1 :: phi1 - -> Coercion -- ^ g2 :: phi2 - -> Reduction -- ^ res_co :: g1 ~r g2 -mkProofIrrelRedn role co g1 g2 +mkProofIrrelRedn :: Coercion -- ^ lhs_co + -> DCoercionN -- ^ dco :: lhs_co ~ rhs_co + -> Coercion -- ^ rhs_co + -> Reduction +mkProofIrrelRedn _g1 co g2 = mkReduction - (mkProofIrrelCo role co g1 g2) - (mkCoercionTy g2) + (mkProofIrrelDCo co rhs_co) + rhs_co + where + rhs_co = mkCoercionTy g2 {-# INLINE mkProofIrrelRedn #-} --- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion', +-- | Create a reflexive 'Reduction' whose LHS and RHS is the given 'Coercion', -- with the specified 'Role'. -mkReflCoRedn :: Role -> Coercion -> Reduction -mkReflCoRedn role co - = mkReduction - (mkReflCo role co_ty) - co_ty - where - co_ty = mkCoercionTy co +mkReflCoRedn :: Coercion -> Reduction +mkReflCoRedn co = mkReduction mkReflDCo (mkCoercionTy co) {-# INLINE mkReflCoRedn #-} -- | A collection of 'Reduction's where the coercions and the types are stored separately. @@ -425,36 +380,72 @@ mkReflCoRedn role co -- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn', -- which expect separate types and coercions. -- --- Invariant: the two stored lists are of the same length, --- and the RHS type of each coercion is the corresponding type. -data Reductions = Reductions [Coercion] [Type] +-- Invariant: given @Reductions lhs_tys dcos rhs_tys@, and an ambient role @r@, +-- we can obtain the @rhs_tys@ by following the directed coercions starting from the repsective +-- @lhs_tys@. Equivalently, @zipWith (followDCo r) lhs_tys dcos@ is equal (up to zonking) to @rhs_tys@. +data Reductions = Reductions [DCoercion] [Type] + +instance Outputable Reductions where + ppr (Reductions dcos rtys) = parens (text "Reductions" <+> ppr dcos <+> ppr rtys) -- | Create 'Reductions' from individual lists of coercions and types. -- -- The lists should be of the same length, and the RHS type of each coercion -- should match the specified type in the other list. -mkReductions :: [Coercion] -> [Type] -> Reductions -mkReductions cos tys = Reductions cos tys +mkReductions :: [DCoercion] -> [Type] -> Reductions +mkReductions cos tys2 = Reductions cos tys2 {-# INLINE mkReductions #-} +mkReflRedns :: [Type] -> Reductions +mkReflRedns tys = mkReductions (mkReflDCos tys) tys +{-# INLINE mkReflRedns #-} + +mkReflDCos :: [Type] -> [DCoercion] +mkReflDCos tys = replicate (length tys) mkReflDCo +{-# INLINE mkReflDCos #-} + -- | Combines 'mkAppCos' and 'mkAppTys'. mkAppRedns :: Reduction -> Reductions -> Reduction -mkAppRedns (Reduction co ty) (Reductions cos tys) - = mkReduction (mkAppCos co cos) (mkAppTys ty tys) +mkAppRedns (Reduction co ty2) (Reductions cos tys2) + = mkReduction (mkAppDCos co cos) (mkAppTys ty2 tys2) {-# INLINE mkAppRedns #-} -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`. -mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction -mkTyConAppRedn role tc (Reductions cos tys) - = mkReduction (mkTyConAppCo role tc cos) (mkTyConApp tc tys) +-- +-- Use this when you know the 'TyCon' is not a type synonym. If it might be, +-- use 'mkTyConAppRedn_MightBeSynonym'. +mkTyConAppRedn :: TyCon -> Reductions -> Reduction +mkTyConAppRedn tc (Reductions cos tys2) + = mkReduction (mkTyConAppDCo cos) (mkTyConApp tc tys2) {-# INLINE mkTyConAppRedn #-} +-- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`. +-- +-- Use 'mkTyConAppRedn' if the 'TyCon' is definitely not a type synonym. +mkTyConAppRedn_MightBeSynonym :: Role -> TyCon -> [Type] -> Reductions -> Reduction +mkTyConAppRedn_MightBeSynonym role tc tys1 redns@(Reductions dcos tys2) + -- 'mkTyConAppCo' handles synomyms by using substitution lifting. + -- We don't have that for directed coercions, so we use hydrate/dehydrate + -- so that we can call 'liftCoSubst'. + -- In the future, it might be desirable to implement substitution lifting + -- for directed coercions to avoid this (and a similar issue in simplifyArgsWorker). + | ExpandsSyn tv_dco_prs rhs_ty leftover_dcos <- expandSynTyCon_maybe tc dcos + , let tv_co_prs = zipWith4 hydrate (tyConRoleListX role tc) tys1 tv_dco_prs tys2 + = mkReduction + (mkAppDCos (mkDehydrateCo $ liftCoSubst role (mkLiftingContext tv_co_prs) rhs_ty) leftover_dcos) + (mkTyConApp tc tys2) + | otherwise = mkTyConAppRedn tc redns + where + hydrate r l (tv,dco) t = (tv, mkHydrateDCo r l dco t) + {-# INLINE hydrate #-} +{-# INLINE mkTyConAppRedn_MightBeSynonym #-} + -- | Reduce the arguments of a 'Class' 'TyCon'. mkClassPredRedn :: Class -> Reductions -> Reduction -mkClassPredRedn cls (Reductions cos tys) +mkClassPredRedn cls (Reductions cos tys2) = mkReduction - (mkTyConAppCo Nominal (classTyCon cls) cos) - (mkClassPred cls tys) + (mkTyConAppDCo cos) + (mkClassPred cls tys2) {-# INLINE mkClassPredRedn #-} -- | Obtain 'Reductions' from a list of 'Reduction's by unzipping. @@ -471,7 +462,7 @@ unzipRedns = foldr accRedn (Reductions [] []) -- -- unzipRedns <$> zipWithM f tys roles -- --- - GHC.Tc.Solver.Monad.breakTyEqCycle_maybe, with two calls of the form: +-- - GHC.Tc.Solver.Monad.breakTyVarCycle_maybe, with two calls of the form: -- -- unzipRedns <$> mapM f tys -- @@ -479,6 +470,67 @@ unzipRedns = foldr accRedn (Reductions [] []) -- but the above locations aren't performance critical, so it was deemed -- to not be worth it. +-- | Stores a heterogeneous reduction. +-- +-- The stored kind coercion must relate the kinds of the +-- stored reduction. That is, in @HetReduction (Reduction co xi) kco@, +-- we must have: +-- +-- > co :: ty ~ xi +-- > kco :: typeKind ty ~ typeKind xi +data HetReduction = + HetReduction + Reduction + MCoercionN + -- N.B. strictness annotations don't seem to make a difference here + +-- | Create a heterogeneous reduction. +-- +-- Pre-condition: the provided kind coercion (second argument) +-- relates the kinds of the stored reduction. +-- That is, if the coercion stored in the 'Reduction' is of the form +-- +-- > co :: ty ~ xi +-- +-- Then the kind coercion supplied must be of the form: +-- +-- > kco :: typeKind ty ~ typeKind xi +mkHetReduction :: Reduction -- ^ heterogeneous reduction + -> MCoercionN -- ^ kind coercion + -> HetReduction +mkHetReduction redn mco = HetReduction redn mco +{-# INLINE mkHetReduction #-} + +-- | Homogenise a heterogeneous reduction. +-- +-- Given @HetReduction (Reduction co xi) kco@, with +-- +-- > co :: ty ~ xi +-- > kco :: typeKind(ty) ~ typeKind(xi) +-- +-- this returns the homogeneous reduction: +-- +-- > hco :: ty ~ ( xi |> sym kco ) +homogeniseHetRedn :: HetReduction -> Reduction +homogeniseHetRedn (HetReduction redn kco) + = mkCoherenceRightMRedn redn (mkSymMCo kco) +{-# INLINE homogeniseHetRedn #-} + +-- | Homogenise a reduction. +-- +-- Given @redn = Reduction co xi@ and kind coercion @kco@, with +-- +-- > co :: ty ~ xi +-- > kco :: typeKind(ty) ~ typeKind(xi) +-- +-- this returns the homogeneous reduction: +-- +-- > hco :: ty ~ ( xi |> sym kco ) +homogeniseRedn :: Reduction -> MCoercionN -> Reduction +homogeniseRedn redn mco + = mkCoherenceRightMRedn redn (mkSymMCo mco) +{-# INLINE homogeniseRedn #-} + {- %************************************************************************ %* * @@ -779,6 +831,9 @@ data ArgsReductions = -- The strictness annotations and UNPACK pragma here are crucial -- to getting good performance in simplifyArgsWorker's tight loop. +instance Outputable ArgsReductions where + ppr (ArgsReductions redns kco) = parens (text "ArgsReductions" <+> ppr redns <+> ppr kco) + -- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv. -- See Note [simplifyArgsWorker] {-# INLINE simplifyArgsWorker #-} @@ -791,6 +846,7 @@ simplifyArgsWorker :: HasDebugCallStack -- list of binders can be shorter or longer than the list of args -> TyCoVarSet -- free vars of the args -> Infinite Role-- list of roles, r + -> [Type] -- original type arguments ty_i -> [Reduction] -- rewritten type arguments, arg_i -- each comes with the coercion used to rewrite it, -- arg_co_i :: ty_i ~ arg_i @@ -804,10 +860,10 @@ simplifyArgsWorker :: HasDebugCallStack -- function is all about. That is, (f xi_1 ... xi_n), where xi_i are the returned arguments, -- *is* well kinded. simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs - orig_roles orig_simplified_args + orig_roles tys redns = go orig_lc orig_ki_binders orig_inner_ki - orig_roles orig_simplified_args + orig_roles (zip tys redns) where orig_lc = emptyLiftingContext $ mkInScopeSet orig_fvs @@ -815,7 +871,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs -> [PiTyBinder] -- Unsubsted binders of function's kind -> Kind -- Unsubsted result kind of function (not a Pi-type) -> Infinite Role -- Roles at which to rewrite these ... - -> [Reduction] -- rewritten arguments, with their rewriting coercions + -> [(Type, Reduction)] -- rewritten arguments, with their rewriting coercions -> ArgsReductions go !lc binders inner_ki _ [] -- The !lc makes the function strict in the lifting context @@ -828,7 +884,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs kind_co | noFreeVarsOfType final_kind = MRefl | otherwise = MCo $ liftCoSubst Nominal lc final_kind - go lc (binder:binders) inner_ki (Inf role roles) (arg_redn:arg_redns) + go lc (binder:binders) inner_ki (Inf role roles) ((orig_ty,arg_redn):arg_redns) = -- We rewrite an argument ty with arg_redn = Reduction arg_co arg -- By Note [Rewriting] in GHC.Tc.Solver.Rewrite invariant (F2), -- typeKind(ty) = typeKind(arg). @@ -841,10 +897,11 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs -- significantly in optimized builds; see #18502 let !kind_co = liftCoSubst Nominal lc (piTyBinderType binder) !(Reduction casted_co casted_xi) - = mkCoherenceRightRedn role arg_redn kind_co + = mkCoherenceRightRedn arg_redn kind_co -- now, extend the lifting context with the new binding !new_lc | Just tv <- namedPiTyBinder_maybe binder - = extendLiftingContextAndInScope lc tv casted_co + = extendLiftingContextAndInScope lc tv + $ mkHydrateDCo role orig_ty casted_co casted_xi | otherwise = lc !(ArgsReductions (Reductions cos xis) final_kind_co) @@ -854,14 +911,14 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs final_kind_co -- See Note [Last case in simplifyArgsWorker] - go lc [] inner_ki roles arg_redns + go lc [] inner_ki roles arg_tys_and_redns = let co1 = liftCoSubst Nominal lc inner_ki + (orig_tys, arg_redns) = unzip arg_tys_and_redns co1_kind = coercionKind co1 - unrewritten_tys = map reductionOriginalType arg_redns - (arg_cos, res_co) = decomposePiCos co1 co1_kind unrewritten_tys - casted_args = assertPpr (equalLength arg_redns arg_cos) + (arg_cos, res_co) = decomposePiCos co1 co1_kind orig_tys + casted_redns = assertPpr (equalLength arg_redns arg_cos) (ppr arg_redns $$ ppr arg_cos) - $ zipWith3 mkCoherenceRightRedn (Inf.toList roles) arg_redns arg_cos + $ zipWith mkCoherenceRightRedn arg_redns arg_cos -- In general decomposePiCos can return fewer cos than tys, -- but not here; because we're well typed, there will be enough -- binders. Note that decomposePiCos does substitutions, so even @@ -873,6 +930,6 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs (bndrs, new_inner) = splitPiTys rewritten_kind ArgsReductions redns_out res_co_out - = go zapped_lc bndrs new_inner roles casted_args + = go zapped_lc bndrs new_inner roles (zip orig_tys casted_redns) in ArgsReductions redns_out (res_co `mkTransMCoR` res_co_out) |