module GHC.Core.Reduction ( -- * Reductions Reduction(..), ReductionN, ReductionR, HetReduction(..), Reductions(..), mkReduction, mkReductions, mkHetReduction, coercionRedn, reductionOriginalType, downgradeRedn, mkSubRedn, mkTransRedn, mkCoherenceRightRedn, mkCoherenceRightMRedn, mkCastRedn1, mkCastRedn2, mkReflRedn, mkGReflRightRedn, mkGReflRightMRedn, mkGReflLeftRedn, mkGReflLeftMRedn, mkAppRedn, mkAppRedns, mkFunRedn, mkForAllRedn, mkHomoForAllRedn, mkTyConAppRedn, mkClassPredRedn, mkProofIrrelRedn, mkReflCoRedn, homogeniseHetRedn, unzipRedns, -- * Rewriting type arguments ArgsReductions(..), simplifyArgsWorker ) where import GHC.Prelude import GHC.Core.Class ( Class(classTyCon) ) import GHC.Core.Coercion import GHC.Core.Predicate ( mkClassPred ) import GHC.Core.TyCon ( 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 ) import GHC.Types.Var.Set ( TyCoVarSet ) import GHC.Utils.Misc ( HasDebugCallStack, equalLength ) import GHC.Utils.Outputable import GHC.Utils.Panic ( assertPpr ) {- %************************************************************************ %* * Reductions %* * %************************************************************************ 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 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 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) * 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@. -- -- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction', -- which separately stores the kind coercion. -- -- See Note [The Reduction type]. data Reduction = Reduction { Reduction -> Coercion reductionCoercion :: Coercion , Reduction -> Type 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. -- | 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 :: Reduction -> MCoercionN -> HetReduction mkHetReduction Reduction redn MCoercionN mco = Reduction -> MCoercionN -> HetReduction HetReduction Reduction redn MCoercionN 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 :: Role -> HetReduction -> Reduction homogeniseHetRedn :: Role -> HetReduction -> Reduction homogeniseHetRedn Role role (HetReduction Reduction redn MCoercionN kco) = Role -> Reduction -> MCoercionN -> Reduction mkCoherenceRightMRedn Role role Reduction redn (MCoercionN -> MCoercionN mkSymMCo MCoercionN kco) {-# INLINE homogeniseHetRedn #-} -- | 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). -- -- Use 'coercionRedn' when you only have the coercion. mkReduction :: Coercion -> Type -> Reduction mkReduction :: Coercion -> Type -> Reduction mkReduction Coercion co Type ty = Coercion -> Type -> Reduction Reduction Coercion co Type ty {-# INLINE mkReduction #-} instance Outputable Reduction where ppr :: Reduction -> SDoc ppr Reduction redn = SDoc -> SDoc forall doc. IsLine doc => doc -> doc braces (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ String -> SDoc forall doc. IsLine doc => String -> doc text String "reductionOriginalType:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Reduction -> Type reductionOriginalType Reduction redn) , String -> SDoc forall doc. IsLine doc => String -> doc text String " reductionReducedType:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Type -> SDoc forall a. Outputable a => a -> SDoc ppr (Reduction -> Type reductionReducedType Reduction redn) , String -> SDoc forall doc. IsLine doc => String -> doc text String " reductionCoercion:" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Coercion -> SDoc forall a. Outputable a => a -> SDoc ppr (Reduction -> Coercion reductionCoercion Reduction redn) ] -- | A 'Reduction' in which the 'Coercion' has 'Nominal' role. type ReductionN = Reduction -- | A 'Reduction' in which the 'Coercion' has 'Representational' role. type ReductionR = Reduction -- | 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 :: Reduction -> Type reductionOriginalType = Coercion -> Type coercionLKind (Coercion -> Type) -> (Reduction -> Coercion) -> Reduction -> Type forall b c a. (b -> c) -> (a -> b) -> a -> c . Reduction -> Coercion 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 :: Coercion -> Reduction coercionRedn Coercion co = Coercion -> Type -> Reduction Reduction Coercion co (Coercion -> Type coercionRKind Coercion co) {-# INLINE coercionRedn #-} -- | Downgrade the role of the coercion stored in the 'Reduction'. downgradeRedn :: Role -- ^ desired role -> Role -- ^ current role -> Reduction -> Reduction downgradeRedn :: Role -> Role -> Reduction -> Reduction downgradeRedn Role new_role Role old_role redn :: Reduction redn@(Reduction Coercion co Type _) = Reduction redn { reductionCoercion = downgradeRole new_role old_role co } {-# INLINE downgradeRedn #-} -- | Downgrade the role of the coercion stored in the 'Reduction', -- from 'Nominal' to 'Representational'. mkSubRedn :: Reduction -> Reduction mkSubRedn :: Reduction -> Reduction mkSubRedn redn :: Reduction redn@(Reduction Coercion co Type _) = Reduction redn { reductionCoercion = mkSubCo co } {-# INLINE mkSubRedn #-} -- | Compose a reduction with a coercion on the left. -- -- 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 :: Coercion -> Reduction -> Reduction mkTransRedn Coercion co1 redn :: Reduction redn@(Reduction Coercion co2 Type _) = Reduction redn { reductionCoercion = co1 `mkTransCo` co2 } {-# INLINE mkTransRedn #-} -- | The reflexive reduction. mkReflRedn :: Role -> Type -> Reduction mkReflRedn :: Role -> Type -> Reduction mkReflRedn Role r Type ty = Coercion -> Type -> Reduction mkReduction (Role -> Type -> Coercion mkReflCo Role r Type ty) Type ty -- | Create a 'Reduction' from a kind cast, in which -- the casted type is the rewritten type. -- -- 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 -> Type -> Coercion -> Reduction mkGReflRightRedn Role role Type ty Coercion co = Coercion -> Type -> Reduction mkReduction (Role -> Type -> Coercion -> Coercion mkGReflRightCo Role role Type ty Coercion co) (Type -> Coercion -> Type mkCastTy Type ty Coercion co) {-# INLINE mkGReflRightRedn #-} -- | Create a 'Reduction' from a kind cast, in which -- the casted type is the rewritten type. -- -- 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 -> Type -> MCoercionN -> Reduction mkGReflRightMRedn Role role Type ty MCoercionN mco = Coercion -> Type -> Reduction mkReduction (Role -> Type -> MCoercionN -> Coercion mkGReflRightMCo Role role Type ty MCoercionN mco) (Type -> MCoercionN -> Type mkCastTyMCo Type ty MCoercionN mco) {-# INLINE mkGReflRightMRedn #-} -- | Create a 'Reduction' from a kind cast, in which -- the casted type is the original (non-rewritten) type. -- -- 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 -> Type -> Coercion -> Reduction mkGReflLeftRedn Role role Type ty Coercion co = Coercion -> Type -> Reduction mkReduction (Role -> Type -> Coercion -> Coercion mkGReflLeftCo Role role Type ty Coercion co) Type ty {-# INLINE mkGReflLeftRedn #-} -- | Create a 'Reduction' from a kind cast, in which -- the casted type is the original (non-rewritten) type. -- -- 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 -> Type -> MCoercionN -> Reduction mkGReflLeftMRedn Role role Type ty MCoercionN mco = Coercion -> Type -> Reduction mkReduction (Role -> Type -> MCoercionN -> Coercion mkGReflLeftMCo Role role Type ty MCoercionN mco) Type ty {-# INLINE mkGReflLeftMRedn #-} -- | Apply a cast to the result of a 'Reduction'. -- -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@ -- 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 :: Role -> Reduction -> Coercion -> Reduction mkCoherenceRightRedn Role r (Reduction Coercion co1 Type ty2) Coercion kco = Coercion -> Type -> Reduction mkReduction (Role -> Type -> Coercion -> Coercion -> Coercion mkCoherenceRightCo Role r Type ty2 Coercion kco Coercion co1) (Type -> Coercion -> Type mkCastTy Type ty2 Coercion kco) {-# INLINE mkCoherenceRightRedn #-} -- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'. -- -- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@ -- 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 :: Role -> Reduction -> MCoercionN -> Reduction mkCoherenceRightMRedn Role r (Reduction Coercion co1 Type ty2) MCoercionN kco = Coercion -> Type -> Reduction mkReduction (Role -> Type -> MCoercionN -> Coercion -> Coercion mkCoherenceRightMCo Role r Type ty2 MCoercionN kco Coercion co1) (Type -> MCoercionN -> Type mkCastTyMCo Type ty2 MCoercionN kco) {-# INLINE mkCoherenceRightMRedn #-} -- | Apply a cast to a 'Reduction', casting both the original and the reduced type. -- -- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns -- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@ -- of the given 'Role' (which must match the role of the coercion stored -- in the 'Reduction' argument). -- -- 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 -> Reduction mkCastRedn1 :: Role -> Type -> Coercion -> Reduction -> Reduction mkCastRedn1 Role r Type ty Coercion cast_co (Reduction Coercion co Type xi) -- co :: ty ~r ty' -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co) = Coercion -> Type -> Reduction mkReduction (Coercion -> Role -> Type -> Type -> Coercion -> Coercion castCoercionKind1 Coercion co Role r Type ty Type xi Coercion cast_co) (Type -> Coercion -> Type mkCastTy Type xi Coercion cast_co) {-# INLINE mkCastRedn1 #-} -- | Apply casts on both sides of a 'Reduction' (of the given 'Role'). -- -- Use 'mkCastRedn1' when you want to cast both the original and reduced types -- in a 'Reduction' using the same coercion. -- -- 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 -> Reduction -- ^ rewritten type, with rewriting coercion -> CoercionN -- ^ coercion to cast with on the right -> Reduction mkCastRedn2 :: Role -> Type -> Coercion -> Reduction -> Coercion -> Reduction mkCastRedn2 Role r Type ty Coercion cast_co (Reduction Coercion nco Type nty) Coercion cast_co' = Coercion -> Type -> Reduction mkReduction (Coercion -> Role -> Type -> Type -> Coercion -> Coercion -> Coercion castCoercionKind2 Coercion nco Role r Type ty Type nty Coercion cast_co Coercion cast_co') (Type -> Coercion -> Type mkCastTy Type nty Coercion cast_co') {-# INLINE mkCastRedn2 #-} -- | Apply one 'Reduction' to another. -- -- Combines 'mkAppCo' and 'mkAppTy`. mkAppRedn :: Reduction -> Reduction -> Reduction mkAppRedn :: Reduction -> Reduction -> Reduction mkAppRedn (Reduction Coercion co1 Type ty1) (Reduction Coercion co2 Type ty2) = Coercion -> Type -> Reduction mkReduction (Coercion -> Coercion -> Coercion mkAppCo Coercion co1 Coercion co2) (Type -> Type -> Type mkAppTy Type ty1 Type ty2) {-# INLINE mkAppRedn #-} -- | Create a function 'Reduction'. -- -- Combines 'mkFunCo' and 'mkFunTy'. mkFunRedn :: Role -> FunTyFlag -> ReductionN -- ^ multiplicity reduction -> Reduction -- ^ argument reduction -> Reduction -- ^ result reduction -> Reduction mkFunRedn :: Role -> FunTyFlag -> Reduction -> Reduction -> Reduction -> Reduction mkFunRedn Role r FunTyFlag af (Reduction Coercion w_co Type w_ty) (Reduction Coercion arg_co Type arg_ty) (Reduction Coercion res_co Type res_ty) = Coercion -> Type -> Reduction mkReduction (Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion mkFunCo Role r FunTyFlag af Coercion w_co Coercion arg_co Coercion res_co) (HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type FunTyFlag -> Type -> Type -> Type -> Type mkFunTy FunTyFlag af Type w_ty Type arg_ty Type res_ty) {-# INLINE mkFunRedn #-} -- | Create a 'Reduction' associated to a Π type, -- from a kind 'Reduction' and a body 'Reduction'. -- -- Combines 'mkForAllCo' and 'mkForAllTy'. mkForAllRedn :: ForAllTyFlag -> TyVar -> ReductionN -- ^ kind reduction -> Reduction -- ^ body reduction -> Reduction mkForAllRedn :: ForAllTyFlag -> TyVar -> Reduction -> Reduction -> Reduction mkForAllRedn ForAllTyFlag vis TyVar tv1 (Reduction Coercion h Type ki') (Reduction Coercion co Type ty) = Coercion -> Type -> Reduction mkReduction (HasDebugCallStack => TyVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion TyVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion mkForAllCo TyVar tv1 ForAllTyFlag vis ForAllTyFlag vis Coercion h Coercion co) (ForAllTyBinder -> Type -> Type mkForAllTy (TyVar -> ForAllTyFlag -> ForAllTyBinder forall var argf. var -> argf -> VarBndr var argf Bndr TyVar tv2 ForAllTyFlag vis) Type ty) where tv2 :: TyVar tv2 = TyVar -> Type -> TyVar setTyVarKind TyVar tv1 Type ki' {-# INLINE mkForAllRedn #-} -- | Create a 'Reduction' of a quantified type from a -- 'Reduction' of the body. -- -- Combines 'mkHomoForAllCos' and 'mkForAllTys'. mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction mkHomoForAllRedn :: [ForAllTyBinder] -> Reduction -> Reduction mkHomoForAllRedn [ForAllTyBinder] bndrs (Reduction Coercion co Type ty) = Coercion -> Type -> Reduction mkReduction ([ForAllTyBinder] -> Coercion -> Coercion mkHomoForAllCos [ForAllTyBinder] bndrs Coercion co) ([ForAllTyBinder] -> Type -> Type mkForAllTys [ForAllTyBinder] bndrs Type ty) {-# 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 -> Coercion -> Coercion -> Coercion -> Reduction mkProofIrrelRedn Role role Coercion co Coercion g1 Coercion g2 = Coercion -> Type -> Reduction mkReduction (Role -> Coercion -> Coercion -> Coercion -> Coercion mkProofIrrelCo Role role Coercion co Coercion g1 Coercion g2) (Coercion -> Type mkCoercionTy Coercion g2) {-# INLINE mkProofIrrelRedn #-} -- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion', -- with the specified 'Role'. mkReflCoRedn :: Role -> Coercion -> Reduction mkReflCoRedn :: Role -> Coercion -> Reduction mkReflCoRedn Role role Coercion co = Coercion -> Type -> Reduction mkReduction (Role -> Type -> Coercion mkReflCo Role role Type co_ty) Type co_ty where co_ty :: Type co_ty = Coercion -> Type mkCoercionTy Coercion co {-# INLINE mkReflCoRedn #-} -- | A collection of 'Reduction's where the coercions and the types are stored separately. -- -- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's. -- -- 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] -- | 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 :: [Coercion] -> [Type] -> Reductions mkReductions [Coercion] cos [Type] tys = [Coercion] -> [Type] -> Reductions Reductions [Coercion] cos [Type] tys {-# INLINE mkReductions #-} -- | Combines 'mkAppCos' and 'mkAppTys'. mkAppRedns :: Reduction -> Reductions -> Reduction mkAppRedns :: Reduction -> Reductions -> Reduction mkAppRedns (Reduction Coercion co Type ty) (Reductions [Coercion] cos [Type] tys) = Coercion -> Type -> Reduction mkReduction (Coercion -> [Coercion] -> Coercion mkAppCos Coercion co [Coercion] cos) (Type -> [Type] -> Type mkAppTys Type ty [Type] tys) {-# INLINE mkAppRedns #-} -- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`. mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction mkTyConAppRedn Role role TyCon tc (Reductions [Coercion] cos [Type] tys) = Coercion -> Type -> Reduction mkReduction (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role role TyCon tc [Coercion] cos) (TyCon -> [Type] -> Type mkTyConApp TyCon tc [Type] tys) {-# INLINE mkTyConAppRedn #-} -- | Reduce the arguments of a 'Class' 'TyCon'. mkClassPredRedn :: Class -> Reductions -> Reduction mkClassPredRedn :: Class -> Reductions -> Reduction mkClassPredRedn Class cls (Reductions [Coercion] cos [Type] tys) = Coercion -> Type -> Reduction mkReduction (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Role -> TyCon -> [Coercion] -> Coercion mkTyConAppCo Role Nominal (Class -> TyCon classTyCon Class cls) [Coercion] cos) (Class -> [Type] -> Type mkClassPred Class cls [Type] tys) {-# INLINE mkClassPredRedn #-} -- | Obtain 'Reductions' from a list of 'Reduction's by unzipping. unzipRedns :: [Reduction] -> Reductions unzipRedns :: [Reduction] -> Reductions unzipRedns = (Reduction -> Reductions -> Reductions) -> Reductions -> [Reduction] -> Reductions forall a b. (a -> b -> b) -> b -> [a] -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr Reduction -> Reductions -> Reductions accRedn ([Coercion] -> [Type] -> Reductions Reductions [] []) where accRedn :: Reduction -> Reductions -> Reductions accRedn :: Reduction -> Reductions -> Reductions accRedn (Reduction Coercion co Type xi) (Reductions [Coercion] cos [Type] xis) = [Coercion] -> [Type] -> Reductions Reductions (Coercion coCoercion -> [Coercion] -> [Coercion] forall a. a -> [a] -> [a] :[Coercion] cos) (Type xiType -> [Type] -> [Type] forall a. a -> [a] -> [a] :[Type] xis) {-# INLINE unzipRedns #-} -- NB: this function is currently used in two locations: -- -- - GHC.Tc.Gen.Foreign.normaliseFfiType', with one call of the form: -- -- unzipRedns <$> zipWithM f tys roles -- -- - GHC.Tc.Solver.Monad.breakTyEqCycle_maybe, with two calls of the form: -- -- unzipRedns <$> mapM f tys -- -- It is possible to write 'mapAndUnzipM' functions to handle these cases, -- but the above locations aren't performance critical, so it was deemed -- to not be worth it. {- %************************************************************************ %* * Simplifying types %* * %************************************************************************ The function below morally belongs in GHC.Tc.Solver.Rewrite, but it is used also in FamInstEnv, and so lives here. Note [simplifyArgsWorker] ~~~~~~~~~~~~~~~~~~~~~~~~~ Invariant (F2) of Note [Rewriting] in GHC.Tc.Solver.Rewrite says that rewriting is homogeneous. This causes some trouble when rewriting a function applied to a telescope of arguments, perhaps with dependency. For example, suppose type family F :: forall (j :: Type) (k :: Type). Maybe j -> Either j k -> Bool -> [k] and we wish to rewrite the args of (with kind applications explicit) F @a @b (Just @a c) (Right @a @b d) False where all variables are skolems and a :: Type b :: Type c :: a d :: b [G] aco :: a ~ fa [G] bco :: b ~ fb [G] cco :: c ~ fc [G] dco :: d ~ fd The first step is to rewrite all the arguments. This is done before calling simplifyArgsWorker. We start from a b Just @a c Right @a @b d False and get left-to-right reductions whose coercions are as follows: co1 :: a ~ fa co2 :: b ~ fb co3 :: (Just @a c) ~ (Just @fa (fc |> aco) |> co6) co4 :: (Right @a @b d) ~ (Right @fa @fb (fd |> bco) |> co7) co5 :: False ~ False where co6 = Maybe (sym aco) :: Maybe fa ~ Maybe a co7 = Either (sym aco) (sym bco) :: Either fa fb ~ Either a b We now process the rewritten args in left-to-right order. The first two args need no further processing. But now consider the third argument. Let f3 = the rewritten result, Just fa (fc |> aco) |> co6. This f3 rewritten argument has kind (Maybe a), due to homogeneity of rewriting (F2). And yet, when we build the application (F @fa @fb ...), we need this argument to have kind (Maybe fa), not (Maybe a). We must cast this argument. The coercion to use is determined by the kind of F: we see in F's kind that the third argument has kind Maybe j. Critically, we also know that the argument corresponding to j (in our example, a) rewrote with a coercion co1. We can thus know the coercion needed for the 3rd argument is (Maybe co1), thus building (f3 |> Maybe co1) More generally, we must use the Lifting Lemma, as implemented in Coercion.liftCoSubst. As we work left-to-right, any variable that is a dependent parameter (j and k, in our example) gets mapped in a lifting context to the coercion that is output from rewriting the corresponding argument (co1 and co2, in our example). Then, after rewriting later arguments, we lift the kind of these arguments in the lifting context that we've be building up. This coercion is then used to keep the result of rewriting well-kinded. Working through our example, this is what happens: 1. Extend the (empty) LC with [j |-> co1]. No new casting must be done, because the binder associated with the first argument has a closed type (no variables). 2. Extend the LC with [k |-> co2]. No casting to do. 3. Lifting the kind (Maybe j) with our LC yields co8 :: Maybe a ~ Maybe fa. Use (f3 |> co8) as the argument to F. 4. Lifting the kind (Either j k) with our LC yields co9 :: Either a b ~ Either fa fb. Use (f4 |> co9) as the 4th argument to F, where f4 is the rewritten form of argument 4, written above. 5. We lift Bool with our LC, getting <Bool>; casting has no effect. We're now almost done, but the new application F @fa @fb (f3 |> co8) (f4 |> co9) False has the wrong kind. Its kind is [fb], instead of the original [b]. So we must use our LC one last time to lift the result kind [k], getting res_co :: [fb] ~ [b], and we cast our result. Accordingly, the final result is F @fa @fb (Just @fa (fc |> aco) |> Maybe (sym aco) |> sym (Maybe (sym aco))) (Right @fa @fb (fd |> bco) |> Either (sym aco) (sym bco) |> sym (Either (sym aco) (sym bco))) False |> [sym bco] The res_co (in this case, [sym bco]) is the third component of the tuple returned by simplifyArgsWorker. Note [Last case in simplifyArgsWorker] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In writing simplifyArgsWorker's `go`, we know here that args cannot be empty, because that case is first. We've run out of binders. But perhaps inner_ki is a tyvar that has been instantiated with a Π-type. Here is an example. a :: forall (k :: Type). k -> k Proxy :: forall j. j -> Type type family Star axStar :: Star ~ Type type family NoWay :: Bool axNoWay :: NoWay ~ False bo :: Type [G] bc :: bo ~ Bool (in inert set) co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star) co = forall (j :: sym axStar). (<j> -> sym axStar) We are rewriting: a (forall (j :: Star). (j |> axStar) -> Star) -- 1 (Proxy |> co) -- 2 (bo |> sym axStar) -- 3 (NoWay |> sym bc) -- 4 :: Star First, we rewrite all the arguments (before simplifyArgsWorker), like so: co1 :: (forall (j :: Star). (j |> axStar) -> Star) ~ (forall j. j -> Type) -- 1 co2 :: (Proxy |> co) ~ (Proxy |> co) -- 2 co3 :: (bo |> sym axStar) ~ (Bool |> sym axStar) -- 3 co4 :: (NoWay |> sym bc) ~ (False |> sym bc) -- 4 Then we do the process described in Note [simplifyArgsWorker]. 1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we don't use it. But we do build a lifting context [k -> co1] (where co1 is a result of rewriting an argument, written above). 2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> co1). This is not a dependent argument, so we don't extend the lifting context. Now we need to deal with argument (3). The way we normally proceed is to lift the kind of the binder, to see whether it's dependent. But here, the remainder of the kind of `a` that we're left with after processing two arguments is just `k`. The way forward is look up k in the lifting context, getting co1. If we're at all well-typed, co1 will be a coercion between Π-types, with at least one binder. So, let's decompose co1 with decomposePiCos. This decomposition needs arguments to use to instantiate any kind parameters. Look at the type of co1. If we just decomposed it, we would end up with coercions whose types include j, which is out of scope here. Accordingly, decomposePiCos takes a list of types whose kinds are the *unrewritten* types in the decomposed coercion. (See comments on decomposePiCos.) Because the rewritten types have unrewritten kinds (because rewriting is homogeneous), passing the list of rewritten types to decomposePiCos just won't do: later arguments' kinds won't be as expected. So we need to get the *unrewritten* types to pass to decomposePiCos. We can do this easily enough by taking the kind of the argument coercions, passed in originally. (Alternative 1: We could re-engineer decomposePiCos to deal with this situation. But that function is already gnarly, and other call sites of decomposePiCos would suffer from the change, even though they are much more common than this one.) (Alternative 2: We could avoid calling decomposePiCos entirely, integrating its behavior into simplifyArgsWorker. This would work, I think, but then all of the complication of decomposePiCos would end up layered on top of all the complication here. Please, no.) (Alternative 3: We could pass the unrewritten arguments into simplifyArgsWorker so that we don't have to recreate them. But that would complicate the interface of this function to handle a very dark, dark corner case. Better to keep our demons to ourselves here instead of exposing them to callers. This decision is easily reversed if there is ever any performance trouble due to the call of coercionKind.) So we now call decomposePiCos co1 (Pair (forall (j :: Star). (j |> axStar) -> Star) (forall j. j -> Type)) [bo |> sym axStar, NoWay |> sym bc] to get co5 :: Star ~ Type co6 :: (j |> axStar) ~ (j |> co5), substituted to (bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5) == bo ~ bo res_co :: Type ~ Star We then use these casts on (the rewritten) (3) and (4) to get (Bool |> sym axStar |> co5 :: Type) -- (C3) (False |> sym bc |> co6 :: bo) -- (C4) We can simplify to Bool -- (C3) (False |> sym bc :: bo) -- (C4) Of course, we still must do the processing in Note [simplifyArgsWorker] to finish the job. We thus want to recur. Our new function kind is the left-hand type of co1 (gotten, recall, by lifting the variable k that was the return kind of the original function). Why the left-hand type (as opposed to the right-hand type)? Because we have casted all the arguments according to decomposePiCos, which gets us from the right-hand type to the left-hand one. We thus recur with that new function kind, zapping our lifting context, because we have essentially applied it. This recursive call returns ([Bool, False], [...], Refl). The Bool and False are the correct arguments we wish to return. But we must be careful about the result coercion: our new, rewritten application will have kind Type, but we want to make sure that the result coercion casts this back to Star. (Why? Because we started with an application of kind Star, and rewriting is homogeneous.) So, we have to twiddle the result coercion appropriately. Let's check whether this is well-typed. We know a :: forall (k :: Type). k -> k a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type a (forall j. j -> Type) Proxy :: forall j. j -> Type a (forall j. j -> Type) Proxy Bool :: Bool -> Type a (forall j. j -> Type) Proxy Bool False :: Type a (forall j. j -> Type) Proxy Bool False |> res_co :: Star as desired. Whew. Historical note: I (Richard E) once thought that the final part of the kind had to be a variable k (as in the example above). But it might not be: it could be an application of a variable. Here is the example: let f :: forall (a :: Type) (b :: a -> Type). b (Any @a) k :: Type x :: k rewrite (f @Type @((->) k) x) After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)` is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded. -} -- | Stores 'Reductions' as well as a kind coercion. -- -- Used when rewriting arguments to a type function @f@. -- -- Invariant: -- when the stored reductions are of the form -- co_i :: ty_i ~ xi_i, -- the kind coercion is of the form -- kco :: typeKind (f ty_1 ... ty_n) ~ typeKind (f xi_1 ... xi_n) -- -- The type function @f@ depends on context. data ArgsReductions = ArgsReductions {-# UNPACK #-} !Reductions !MCoercionN -- The strictness annotations and UNPACK pragma here are crucial -- to getting good performance in simplifyArgsWorker's tight loop. -- This is shared between the rewriter and the normaliser in GHC.Core.FamInstEnv. -- See Note [simplifyArgsWorker] {-# INLINE simplifyArgsWorker #-} -- NB. INLINE yields a ~1% decrease in allocations in T9872d compared to INLINEABLE -- This function is only called in two locations, so the amount of code duplication -- should be rather reasonable despite the size of the function. simplifyArgsWorker :: HasDebugCallStack => [PiTyBinder] -> Kind -- the binders & result kind (not a Π-type) of the function applied to the args -- 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 -> [Reduction] -- rewritten type arguments, arg_i -- each comes with the coercion used to rewrite it, -- arg_co_i :: ty_i ~ arg_i -> ArgsReductions -- Returns ArgsReductions (Reductions cos xis) res_co, where co_i :: ty_i ~ xi_i, -- and res_co :: kind (f ty_1 ... ty_n) ~ kind (f xi_1 ... xi_n), where f is the function -- that we are applying. -- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in), -- then (f ty_1 ... ty_n) is well kinded. Note that (f arg_1 ... arg_n) might *not* be well-kinded. -- Massaging the arg_i in order to make the function application well-kinded is what this -- function is all about. That is, (f xi_1 ... xi_n), where xi_i are the returned arguments, -- *is* well kinded. simplifyArgsWorker :: HasDebugCallStack => [PiTyBinder] -> Type -> TyCoVarSet -> Infinite Role -> [Reduction] -> ArgsReductions simplifyArgsWorker [PiTyBinder] orig_ki_binders Type orig_inner_ki TyCoVarSet orig_fvs Infinite Role orig_roles [Reduction] orig_simplified_args = LiftingContext -> [PiTyBinder] -> Type -> Infinite Role -> [Reduction] -> ArgsReductions go LiftingContext orig_lc [PiTyBinder] orig_ki_binders Type orig_inner_ki Infinite Role orig_roles [Reduction] orig_simplified_args where orig_lc :: LiftingContext orig_lc = InScopeSet -> LiftingContext emptyLiftingContext (InScopeSet -> LiftingContext) -> InScopeSet -> LiftingContext forall a b. (a -> b) -> a -> b $ TyCoVarSet -> InScopeSet mkInScopeSet TyCoVarSet orig_fvs go :: LiftingContext -- mapping from tyvars to rewriting coercions -> [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 -> ArgsReductions go :: LiftingContext -> [PiTyBinder] -> Type -> Infinite Role -> [Reduction] -> ArgsReductions go !LiftingContext lc [PiTyBinder] binders Type inner_ki Infinite Role _ [] -- The !lc makes the function strict in the lifting context -- which means GHC can unbox that pair. A modest win. = Reductions -> MCoercionN -> ArgsReductions ArgsReductions ([Coercion] -> [Type] -> Reductions mkReductions [] []) MCoercionN kind_co where final_kind :: Type final_kind = [PiTyBinder] -> Type -> Type HasDebugCallStack => [PiTyBinder] -> Type -> Type mkPiTys [PiTyBinder] binders Type inner_ki kind_co :: MCoercionN kind_co | Type -> Bool noFreeVarsOfType Type final_kind = MCoercionN MRefl | Bool otherwise = Coercion -> MCoercionN MCo (Coercion -> MCoercionN) -> Coercion -> MCoercionN forall a b. (a -> b) -> a -> b $ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion Role -> LiftingContext -> Type -> Coercion liftCoSubst Role Nominal LiftingContext lc Type final_kind go LiftingContext lc (PiTyBinder binder:[PiTyBinder] binders) Type inner_ki (Inf Role role Infinite Role roles) (Reduction arg_redn:[Reduction] 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). -- However, it is possible that arg will be used as an argument to a function -- whose kind is different, if earlier arguments have been rewritten. -- We thus need to compose the reduction with a kind coercion to ensure -- well-kindedness (see the call to mkCoherenceRightRedn below). -- -- The bangs here have been observed to improve performance -- significantly in optimized builds; see #18502 let !kind_co :: Coercion kind_co = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion Role -> LiftingContext -> Type -> Coercion liftCoSubst Role Nominal LiftingContext lc (PiTyBinder -> Type piTyBinderType PiTyBinder binder) !(Reduction Coercion casted_co Type casted_xi) = Role -> Reduction -> Coercion -> Reduction mkCoherenceRightRedn Role role Reduction arg_redn Coercion kind_co -- now, extend the lifting context with the new binding !new_lc :: LiftingContext new_lc | Just TyVar tv <- PiTyBinder -> Maybe TyVar namedPiTyBinder_maybe PiTyBinder binder = LiftingContext -> TyVar -> Coercion -> LiftingContext extendLiftingContextAndInScope LiftingContext lc TyVar tv Coercion casted_co | Bool otherwise = LiftingContext lc !(ArgsReductions (Reductions [Coercion] cos [Type] xis) MCoercionN final_kind_co) = LiftingContext -> [PiTyBinder] -> Type -> Infinite Role -> [Reduction] -> ArgsReductions go LiftingContext new_lc [PiTyBinder] binders Type inner_ki Infinite Role roles [Reduction] arg_redns in Reductions -> MCoercionN -> ArgsReductions ArgsReductions ([Coercion] -> [Type] -> Reductions Reductions (Coercion casted_coCoercion -> [Coercion] -> [Coercion] forall a. a -> [a] -> [a] :[Coercion] cos) (Type casted_xiType -> [Type] -> [Type] forall a. a -> [a] -> [a] :[Type] xis)) MCoercionN final_kind_co -- See Note [Last case in simplifyArgsWorker] go LiftingContext lc [] Type inner_ki Infinite Role roles [Reduction] arg_redns = let co1 :: Coercion co1 = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion Role -> LiftingContext -> Type -> Coercion liftCoSubst Role Nominal LiftingContext lc Type inner_ki co1_kind :: Pair Type co1_kind = Coercion -> Pair Type coercionKind Coercion co1 unrewritten_tys :: [Type] unrewritten_tys = (Reduction -> Type) -> [Reduction] -> [Type] forall a b. (a -> b) -> [a] -> [b] map Reduction -> Type reductionOriginalType [Reduction] arg_redns ([Coercion] arg_cos, Coercion res_co) = HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion) Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion) decomposePiCos Coercion co1 Pair Type co1_kind [Type] unrewritten_tys casted_args :: [Reduction] casted_args = Bool -> SDoc -> [Reduction] -> [Reduction] forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr ([Reduction] -> [Coercion] -> Bool forall a b. [a] -> [b] -> Bool equalLength [Reduction] arg_redns [Coercion] arg_cos) ([Reduction] -> SDoc forall a. Outputable a => a -> SDoc ppr [Reduction] arg_redns SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ [Coercion] -> SDoc forall a. Outputable a => a -> SDoc ppr [Coercion] arg_cos) ([Reduction] -> [Reduction]) -> [Reduction] -> [Reduction] forall a b. (a -> b) -> a -> b $ (Role -> Reduction -> Coercion -> Reduction) -> [Role] -> [Reduction] -> [Coercion] -> [Reduction] forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d] zipWith3 Role -> Reduction -> Coercion -> Reduction mkCoherenceRightRedn (Infinite Role -> [Role] forall a. Infinite a -> [a] Inf.toList Infinite Role roles) [Reduction] arg_redns [Coercion] 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 -- if the original substitution results in something ending with -- ... -> k, that k will be substituted to perhaps reveal more -- binders. zapped_lc :: LiftingContext zapped_lc = LiftingContext -> LiftingContext zapLiftingContext LiftingContext lc Pair Type rewritten_kind Type _ = Pair Type co1_kind ([PiTyBinder] bndrs, Type new_inner) = Type -> ([PiTyBinder], Type) splitPiTys Type rewritten_kind ArgsReductions Reductions redns_out MCoercionN res_co_out = LiftingContext -> [PiTyBinder] -> Type -> Infinite Role -> [Reduction] -> ArgsReductions go LiftingContext zapped_lc [PiTyBinder] bndrs Type new_inner Infinite Role roles [Reduction] casted_args in Reductions -> MCoercionN -> ArgsReductions ArgsReductions Reductions redns_out (Coercion res_co Coercion -> MCoercionN -> MCoercionN `mkTransMCoR` MCoercionN res_co_out)