X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=7df5b8e38fb82d77f1689165bdc8a70631827695;hp=b49b35612d5d937f3b29883204c37963b630d14c;hb=c8c2f6bb7d79a2a6aeaa3233363fdf0bbbfad205;hpb=d436c70d43fb905c63220040168295e473f4b90a diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index b49b356..7df5b8e 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -3,544 +3,673 @@ % \begin{code} -{-# OPTIONS -fno-warn-incomplete-patterns #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and fix --- any warnings in the module. See --- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings --- for details - --- | Module for type coercions, as used in System FC. See 'CoreSyn.Expr' for +-- | Module for (a) type kinds and (b) type coercions, +-- as used in System FC. See 'CoreSyn.Expr' for -- more on System FC and how coercions fit into it. -- --- Coercions are represented as types, and their kinds tell what types the --- coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so: --- --- > typeKind (symCoercion type) :: TyConApp CoercionTyCon{...} [type, type] module Coercion ( -- * Main data type - Coercion, - - mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind, - coercionKind, coercionKinds, coercionKindPredTy, isIdentityCoercion, - - -- ** Equality predicates - isEqPred, mkEqPred, getEqPredTys, isEqPredTy, - - -- ** Coercion transformations - mkCoercion, - mkSymCoercion, mkTransCoercion, - mkLeftCoercion, mkRightCoercion, mkRightCoercions, - mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion, - mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion, - mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, - + Coercion(..), Var, CoVar, + + -- ** Deconstructing Kinds + kindFunResult, kindAppResult, synTyConResKind, + splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe, + + -- ** Predicates on Kinds + isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, + isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, + isSuperKind, isCoercionKind, + mkArrowKind, mkArrowKinds, + + isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind, + isSubKindCon, + + mkCoType, coVarKind, coVarKind_maybe, + coercionType, coercionKind, coercionKinds, isReflCo, + + -- ** Constructing coercions + mkReflCo, mkCoVarCo, + mkAxInstCo, mkPiCo, mkPiCos, + mkSymCo, mkTransCo, mkNthCo, + mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo, + mkForAllCo, mkUnsafeCo, + mkNewTypeCo, mkFamInstCo, + mkPredCo, + + -- ** Decomposition + splitCoPredTy_maybe, splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo, - - unsafeCoercionTyCon, symCoercionTyCon, - transCoercionTyCon, leftCoercionTyCon, - rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn - + getCoVar_maybe, + + splitTyConAppCo_maybe, + splitAppCo_maybe, + splitForAllCo_maybe, + + -- ** Coercion variables + mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique, + + -- ** Free variables + tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize, + + -- ** Substitution + CvSubstEnv, emptyCvSubstEnv, + CvSubst(..), emptyCvSubst, Coercion.lookupTyVar, lookupCoVar, + isEmptyCvSubst, zapCvSubstEnv, getCvInScope, + substCo, substCos, substCoVar, substCoVars, + substCoWithTy, substCoWithTys, + cvTvSubst, tvCvSubst, zipOpenCvSubst, + substTy, extendTvSubst, + substTyVarBndr, substCoVarBndr, + + -- ** Lifting + liftCoMatch, liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, + -- ** Comparison - coreEqCoercion, + coreEqCoercion, coreEqCoercion2, - -- * CoercionI - CoercionI(..), - isIdentityCoI, - mkSymCoI, mkTransCoI, - mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI, - mkForAllTyCoI, - fromCoI, fromACo, - mkClassPPredCoI, mkIParamPredCoI, mkEqPredCoI + -- ** Forcing evaluation of coercions + seqCo, + + -- * Pretty-printing + pprCo, pprParendCo, pprCoAxiom, + -- * Other + applyCo, coVarPred + ) where #include "HsVersions.h" +import Unify ( MatchEnv(..), ruleMatchTyX, matchList ) import TypeRep -import Type +import qualified Type +import Type hiding( substTy, substTyVarBndr, extendTvSubst ) +import Kind +import Class ( classTyCon ) import TyCon -import Class import Var -import Name -import PrelNames +import VarEnv +import VarSet +import UniqFM ( minusUFM ) +import Maybes ( orElse ) +import Name ( Name, NamedThing(..), nameUnique ) +import OccName ( isSymOcc ) import Util import BasicTypes import Outputable +import Unique +import Pair +import TysPrim ( eqPredPrimTyCon ) +import PrelNames ( funTyConKey ) +import Control.Applicative +import Data.Traversable (traverse, sequenceA) +import Control.Arrow (second) import FastString --- | A 'Coercion' represents a 'Type' something should be coerced to. -type Coercion = Type +import qualified Data.Data as Data hiding ( TyCon ) +\end{code} --- | A 'CoercionKind' is always of form @ty1 ~ ty2@ and indicates the --- types that a 'Coercion' will work on. -type CoercionKind = Kind +%************************************************************************ +%* * + Coercions +%* * +%************************************************************************ ------------------------------- +\begin{code} +-- | A 'Coercion' is concrete evidence of the equality/convertibility +-- of two types. + +data Coercion + -- These ones mirror the shape of types + = Refl Type -- See Note [Refl invariant] + -- Invariant: applications of (Refl T) to a bunch of identity coercions + -- always show up as Refl. + -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)). + + -- Applications of (Refl T) to some coercions, at least one of + -- which is NOT the identity, show up as TyConAppCo. + -- (They may not be fully saturated however.) + -- ConAppCo coercions (like all coercions other than Refl) + -- are NEVER the identity. + + -- These ones simply lift the correspondingly-named + -- Type constructors into Coercions + | TyConAppCo TyCon [Coercion] -- lift TyConApp + -- The TyCon is never a synonym; + -- we expand synonyms eagerly + + | AppCo Coercion Coercion -- lift AppTy + + -- See Note [Forall coercions] + | ForAllCo TyVar Coercion -- forall a. g + + -- These are special + | CoVarCo CoVar + | AxiomInstCo CoAxiom [Coercion] -- The coercion arguments always *precisely* + -- saturate arity of CoAxiom. + -- See [Coercion axioms applied to coercions] + | UnsafeCo Type Type + | SymCo Coercion + | TransCo Coercion Coercion + + -- These are destructors + | NthCo Int Coercion -- Zero-indexed + | InstCo Coercion Type + deriving (Data.Data, Data.Typeable) +\end{code} --- | This breaks a 'Coercion' with 'CoercionKind' @T A B C ~ T D E F@ into --- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence: --- --- > decomposeCo 3 c = [right (left (left c)), right (left c), right c] -decomposeCo :: Arity -> Coercion -> [Coercion] -decomposeCo n co - = go n co [] - where - go 0 _ cos = cos - go n co cos = go (n-1) (mkLeftCoercion co) - (mkRightCoercion co : cos) +Note [Refl invariant] +~~~~~~~~~~~~~~~~~~~~~ +Coercions have the following invariant + Refl is always lifted as far as possible. ------------------------------- +You might think that a consequencs is: + Every identity coercions has Refl at the root -------------------------------------------------------- --- and some coercion kind stuff +But that's not quite true because of coercion variables. Consider + g where g :: Int~Int + Left h where h :: Maybe Int ~ Maybe Int +etc. So the consequence is only true of coercions that +have no coercion variables. --- | Tests whether a type is just a type equality predicate -isEqPredTy :: Type -> Bool -isEqPredTy (PredTy pred) = isEqPred pred -isEqPredTy _ = False - --- | Creates a type equality predicate -mkEqPred :: (Type, Type) -> PredType -mkEqPred (ty1, ty2) = EqPred ty1 ty2 - --- | Splits apart a type equality predicate, if the supplied 'PredType' is one. --- Panics otherwise -getEqPredTys :: PredType -> (Type,Type) -getEqPredTys (EqPred ty1 ty2) = (ty1, ty2) -getEqPredTys other = pprPanic "getEqPredTys" (ppr other) - --- | Makes a 'CoercionKind' from two types: the types whose equality is proven by the relevant 'Coercion' -mkCoKind :: Type -> Type -> CoercionKind -mkCoKind ty1 ty2 = PredTy (EqPred ty1 ty2) - --- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself -mkReflCoKind :: Type -> CoercionKind -mkReflCoKind ty = mkCoKind ty ty - --- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'. --- Panics if the argument is not a valid 'CoercionKind' -splitCoercionKind :: CoercionKind -> (Type, Type) -splitCoercionKind co | Just co' <- kindView co = splitCoercionKind co' -splitCoercionKind (PredTy (EqPred ty1 ty2)) = (ty1, ty2) - --- | Take a 'CoercionKind' apart into the two types it relates, if possible. See also 'splitCoercionKind' -splitCoercionKind_maybe :: Kind -> Maybe (Type, Type) -splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe co' -splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2) -splitCoercionKind_maybe _ = Nothing +Note [Coercion axioms applied to coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The reason coercion axioms can be applied to coercions and not just +types is to allow for better optimization. There are some cases where +we need to be able to "push transitivity inside" an axiom in order to +expose further opportunities for optimization. --- | If it is the case that --- --- > c :: (t1 ~ t2) --- --- i.e. the kind of @c@ is a 'CoercionKind' relating @t1@ and @t2@, then @coercionKind c = (t1, t2)@. --- See also 'coercionKindPredTy' -coercionKind :: Coercion -> (Type, Type) -coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a) - | otherwise = (ty, ty) -coercionKind (AppTy ty1 ty2) - = let (t1, t2) = coercionKind ty1 - (s1, s2) = coercionKind ty2 in - (mkAppTy t1 s1, mkAppTy t2 s2) -coercionKind (TyConApp tc args) - | Just (ar, rule) <- isCoercionTyCon_maybe tc - -- CoercionTyCons carry their kinding rule, so we use it here - = ASSERT( length args >= ar ) -- Always saturated - let (ty1,ty2) = rule (take ar args) -- Apply the rule to the right number of args - (tys1, tys2) = coercionKinds (drop ar args) - in (mkAppTys ty1 tys1, mkAppTys ty2 tys2) +For example, suppose we have - | otherwise - = let (lArgs, rArgs) = coercionKinds args in - (TyConApp tc lArgs, TyConApp tc rArgs) -coercionKind (FunTy ty1 ty2) - = let (t1, t2) = coercionKind ty1 - (s1, s2) = coercionKind ty2 in - (mkFunTy t1 s1, mkFunTy t2 s2) -coercionKind (ForAllTy tv ty) - = let (ty1, ty2) = coercionKind ty in - (ForAllTy tv ty1, ForAllTy tv ty2) -coercionKind (PredTy (EqPred c1 c2)) - = let k1 = coercionKindPredTy c1 - k2 = coercionKindPredTy c2 in - (k1,k2) -coercionKind (PredTy (ClassP cl args)) - = let (lArgs, rArgs) = coercionKinds args in - (PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs)) -coercionKind (PredTy (IParam name ty)) - = let (ty1, ty2) = coercionKind ty in - (PredTy (IParam name ty1), PredTy (IParam name ty2)) - --- | Recover the 'CoercionKind' corresponding to a particular 'Coerceion'. See also 'coercionKind' --- and 'mkCoKind' -coercionKindPredTy :: Coercion -> CoercionKind -coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2 + C a : t[a] ~ F a + g : b ~ c --- | Apply 'coercionKind' to multiple 'Coercion's -coercionKinds :: [Coercion] -> ([Type], [Type]) -coercionKinds tys = unzip $ map coercionKind tys - -------------------------------------- -isIdentityCoercion :: Coercion -> Bool -isIdentityCoercion co - = case coercionKind co of - (t1,t2) -> t1 `coreEqType` t2 - -------------------------------------- --- Coercion kind and type mk's --- (make saturated TyConApp CoercionTyCon{...} args) - --- | Make a coercion from the specified coercion 'TyCon' and the 'Type' arguments to --- that coercion. Try to use the @mk*Coercion@ family of functions instead of using this function --- if possible -mkCoercion :: TyCon -> [Type] -> Coercion -mkCoercion coCon args = ASSERT( tyConArity coCon == length args ) - TyConApp coCon args - --- | Apply a 'Coercion' to another 'Coercion', which is presumably a --- 'Coercion' constructor of some kind -mkAppCoercion :: Coercion -> Coercion -> Coercion -mkAppCoercion co1 co2 = mkAppTy co1 co2 +and we want to optimize --- | Applies multiple 'Coercion's to another 'Coercion', from left to right. --- See also 'mkAppCoercion' -mkAppsCoercion :: Coercion -> [Coercion] -> Coercion -mkAppsCoercion co1 tys = foldl mkAppTy co1 tys + sym (C b) ; t[g] ; C c --- | Apply a type constructor to a list of coercions. -mkTyConCoercion :: TyCon -> [Coercion] -> Coercion -mkTyConCoercion con cos = mkTyConApp con cos +which has the kind --- | Make a function 'Coercion' between two other 'Coercion's -mkFunCoercion :: Coercion -> Coercion -> Coercion -mkFunCoercion co1 co2 = mkFunTy co1 co2 + F b ~ F c --- | Make a 'Coercion' which binds a variable within an inner 'Coercion' -mkForAllCoercion :: Var -> Coercion -> Coercion --- note that a TyVar should be used here, not a CoVar (nor a TcTyVar) -mkForAllCoercion tv co = ASSERT ( isTyVar tv ) mkForAllTy tv co +(stopping through t[b] and t[c] along the way). +We'd like to optimize this to just F g -- but how? The key is +that we need to allow axioms to be instantiated by *coercions*, +not just by types. Then we can (in certain cases) push +transitivity inside the axiom instantiations, and then react +opposite-polarity instantiations of the same axiom. In this +case, e.g., we match t[g] against the LHS of (C c)'s kind, to +obtain the substitution a |-> g (note this operation is sort +of the dual of lifting!) and hence end up with -------------------------------- + C g : t[b] ~ F c -mkSymCoercion :: Coercion -> Coercion --- ^ Create a symmetric version of the given 'Coercion' that asserts equality --- between the same types but in the other "direction", so a kind of @t1 ~ t2@ --- becomes the kind @t2 ~ t1@. --- --- This function attempts to simplify the generated 'Coercion' by removing --- redundant applications of @sym@. This is done by pushing this new @sym@ --- down into the 'Coercion' and exploiting the fact that @sym (sym co) = co@. -mkSymCoercion co - | Just co' <- coreView co = mkSymCoercion co' - -mkSymCoercion (ForAllTy tv ty) = ForAllTy tv (mkSymCoercion ty) -mkSymCoercion (AppTy co1 co2) = AppTy (mkSymCoercion co1) (mkSymCoercion co2) -mkSymCoercion (FunTy co1 co2) = FunTy (mkSymCoercion co1) (mkSymCoercion co2) - -mkSymCoercion (TyConApp tc cos) - | not (isCoercionTyCon tc) = mkTyConApp tc (map mkSymCoercion cos) - -mkSymCoercion (TyConApp tc [co]) - | tc `hasKey` symCoercionTyConKey = co -- sym (sym co) --> co - | tc `hasKey` leftCoercionTyConKey = mkLeftCoercion (mkSymCoercion co) - | tc `hasKey` rightCoercionTyConKey = mkRightCoercion (mkSymCoercion co) - -mkSymCoercion (TyConApp tc [co1,co2]) - | tc `hasKey` transCoercionTyConKey - -- sym (co1 `trans` co2) --> (sym co2) `trans (sym co2) - -- Note reversal of arguments! - = mkTransCoercion (mkSymCoercion co2) (mkSymCoercion co1) - - | tc `hasKey` instCoercionTyConKey - -- sym (co @ ty) --> (sym co) @ ty - -- Note: sym is not applied to 'ty' - = mkInstCoercion (mkSymCoercion co1) co2 - -mkSymCoercion (TyConApp tc cos) -- Other coercion tycons, such as those - = mkCoercion symCoercionTyCon [TyConApp tc cos] -- arising from newtypes - -mkSymCoercion (TyVarTy tv) - | isCoVar tv = mkCoercion symCoercionTyCon [TyVarTy tv] - | otherwise = TyVarTy tv -- Reflexive +which indeed has the same kind as t[g] ; C c. -------------------------------- --- ToDo: we should be cleverer about transitivity - -mkTransCoercion :: Coercion -> Coercion -> Coercion --- ^ Create a new 'Coercion' by exploiting transitivity on the two given 'Coercion's. --- --- This function attempts to simplify the generated 'Coercion' by exploiting the fact that --- @sym g `trans` g = id@. -mkTransCoercion g1 g2 -- sym g `trans` g = id - | (t1,_) <- coercionKind g1 - , (_,t2) <- coercionKind g2 - , t1 `coreEqType` t2 - = t1 +Now we have - | otherwise - = mkCoercion transCoercionTyCon [g1, g2] + sym (C b) ; C g +which can be optimized to F g. -------------------------------- --- Smart constructors for left and right -mkLeftCoercion :: Coercion -> Coercion --- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of --- the "functions" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then: --- --- > mkLeftCoercion c :: f ~ g -mkLeftCoercion co - | Just (co', _) <- splitAppCoercion_maybe co = co' - | otherwise = mkCoercion leftCoercionTyCon [co] - -mkRightCoercion :: Coercion -> Coercion --- ^ From an application 'Coercion' build a 'Coercion' that asserts the equality of --- the "arguments" on either side of the type equality. So if @c@ has kind @f x ~ g y@ then: --- --- > mkLeftCoercion c :: x ~ y -mkRightCoercion co - | Just (_, co2) <- splitAppCoercion_maybe co = co2 - | otherwise = mkCoercion rightCoercionTyCon [co] - -mkRightCoercions :: Int -> Coercion -> [Coercion] --- ^ As 'mkRightCoercion', but finds the 'Coercion's available on the right side of @n@ --- nested application 'Coercion's, manufacturing new left or right cooercions as necessary --- if suffficiently many are not directly available. -mkRightCoercions n co - = go n co [] - where - go n co acc - | n > 0 - = case splitAppCoercion_maybe co of - Just (co1,co2) -> go (n-1) co1 (co2:acc) - Nothing -> go (n-1) (mkCoercion leftCoercionTyCon [co]) (mkCoercion rightCoercionTyCon [co]:acc) - | otherwise - = acc - - -mkInstCoercion :: Coercion -> Type -> Coercion --- ^ Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs --- the resulting beta-reduction, otherwise it creates a suspended instantiation. -mkInstCoercion co ty - | Just (tv,co') <- splitForAllTy_maybe co - = substTyWith [tv] [ty] co' -- (forall a.co) @ ty --> co[ty/a] - | otherwise - = mkCoercion instCoercionTyCon [co, ty] - -mkInstsCoercion :: Coercion -> [Type] -> Coercion --- ^ As 'mkInstCoercion', but instantiates the coercion with a number of type arguments, left-to-right -mkInstsCoercion co tys = foldl mkInstCoercion co tys - -{- -splitSymCoercion_maybe :: Coercion -> Maybe Coercion -splitSymCoercion_maybe (TyConApp tc [co]) = - if tc `hasKey` symCoercionTyConKey - then Just co - else Nothing -splitSymCoercion_maybe co = Nothing --} - -splitAppCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion) --- ^ Splits a coercion application, being careful *not* to split @left c@ etc. --- This is because those are really syntactic constructs, not applications -splitAppCoercion_maybe co | Just co' <- coreView co = splitAppCoercion_maybe co' -splitAppCoercion_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2) -splitAppCoercion_maybe (AppTy ty1 ty2) = Just (ty1, ty2) -splitAppCoercion_maybe (TyConApp tc tys) - | not (isCoercionTyCon tc) - = case snocView tys of - Just (tys', ty') -> Just (TyConApp tc tys', ty') - Nothing -> Nothing -splitAppCoercion_maybe _ = Nothing - -{- -splitTransCoercion_maybe :: Coercion -> Maybe (Coercion, Coercion) -splitTransCoercion_maybe (TyConApp tc [ty1, ty2]) - = if tc `hasKey` transCoercionTyConKey then - Just (ty1, ty2) - else - Nothing -splitTransCoercion_maybe other = Nothing - -splitInstCoercion_maybe :: Coercion -> Maybe (Coercion, Type) -splitInstCoercion_maybe (TyConApp tc [ty1, ty2]) - = if tc `hasKey` instCoercionTyConKey then - Just (ty1, ty2) - else - Nothing -splitInstCoercion_maybe other = Nothing - -splitLeftCoercion_maybe :: Coercion -> Maybe Coercion -splitLeftCoercion_maybe (TyConApp tc [co]) - = if tc `hasKey` leftCoercionTyConKey then - Just co - else - Nothing -splitLeftCoercion_maybe other = Nothing - -splitRightCoercion_maybe :: Coercion -> Maybe Coercion -splitRightCoercion_maybe (TyConApp tc [co]) - = if tc `hasKey` rightCoercionTyConKey then - Just co - else - Nothing -splitRightCoercion_maybe other = Nothing --} - --- | Manufacture a coercion from this air. Needless to say, this is not usually safe, --- but it is used when we know we are dealing with bottom, which is one case in which --- it is safe. This is also used implement the @unsafeCoerce#@ primitive. -mkUnsafeCoercion :: Type -> Type -> Coercion -mkUnsafeCoercion ty1 ty2 - = mkCoercion unsafeCoercionTyCon [ty1, ty2] +Note [Forall coercions] +~~~~~~~~~~~~~~~~~~~~~~~ +Constructing coercions between forall-types can be a bit tricky. +Currently, the situation is as follows: + ForAllCo TyVar Coercion --- See note [Newtype coercions] in TyCon +represents a coercion between polymorphic types, with the rule --- | Create a coercion suitable for the given 'TyCon'. The 'Name' should be that of a --- new coercion 'TyCon', the 'TyVar's the arguments expected by the @newtype@ and the --- type the appropriate right hand side of the @newtype@, with the free variables --- a subset of those 'TyVar's. -mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon -mkNewTypeCoercion name tycon tvs rhs_ty - = mkCoercionTyCon name co_con_arity rule - where - co_con_arity = length tvs + v : k g : t1 ~ t2 + ---------------------------------------------- + ForAllCo v g : (all v:k . t1) ~ (all v:k . t2) - rule args = ASSERT( co_con_arity == length args ) - (TyConApp tycon args, substTyWith tvs args rhs_ty) +Note that it's only necessary to coerce between polymorphic types +where the type variables have identical kinds, because equality on +kinds is trivial. --- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type --- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is --- the coercion tycon built here, @F@ the family tycon and @R@ the (derived) --- representation tycon. -mkFamInstCoercion :: Name -- ^ Unique name for the coercion tycon - -> [TyVar] -- ^ Type parameters of the coercion (@tvs@) - -> TyCon -- ^ Family tycon (@F@) - -> [Type] -- ^ Type instance (@ts@) - -> TyCon -- ^ Representation tycon (@R@) - -> TyCon -- ^ Coercion tycon (@Co@) -mkFamInstCoercion name tvs family instTys rep_tycon - = mkCoercionTyCon name coArity rule - where - coArity = length tvs - rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs], - TyConApp family instTys, -- sigma (F ts) - TyConApp rep_tycon args) -- ~ R tys - --------------------------------------- --- Coercion Type Constructors... - --- Example. The coercion ((sym c) (sym d) (sym e)) --- will be represented by (TyConApp sym [c, sym d, sym e]) --- If sym c :: p1=q1 --- sym d :: p2=q2 --- sym e :: p3=q3 --- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3) - --- | Coercion type constructors: avoid using these directly and instead use the @mk*Coercion@ and @split*Coercion@ family --- of functions if possible. -symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon :: TyCon --- Each coercion TyCon is built with the special CoercionTyCon record and --- carries its own kinding rule. Such CoercionTyCons must be fully applied --- by any TyConApp in which they are applied, however they may also be over --- applied (see example above) and the kinding function must deal with this. -symCoercionTyCon = - mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf - where - flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1) - where - (ty1, ty2) = coercionKind co +Note [Predicate coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + g :: a~b +How can we coerce between types + ([c]~a) => [a] -> c +and + ([c]~b) => [b] -> c +where the equality predicate *itself* differs? + +Answer: we simply treat (~) as an ordinary type constructor, so these +types really look like + + ((~) [c] a) -> [a] -> c + ((~) [c] b) -> [b] -> c -transCoercionTyCon = - mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf +So the coercion between the two is obviously + + ((~) [c] g) -> [g] -> c + +Another way to see this to say that we simply collapse predicates to +their representation type (see Type.coreView and Type.predTypeRep). + +This collapse is done by mkPredCo; there is no PredCo constructor +in Coercion. This is important because we need Nth to work on +predicates too: + Nth 1 ((~) [c] g) = g +See Simplify.simplCoercionF, which generates such selections. + +%************************************************************************ +%* * +\subsection{Coercion variables} +%* * +%************************************************************************ + +\begin{code} +coVarName :: CoVar -> Name +coVarName = varName + +setCoVarUnique :: CoVar -> Unique -> CoVar +setCoVarUnique = setVarUnique + +setCoVarName :: CoVar -> Name -> CoVar +setCoVarName = setVarName + +isCoVar :: Var -> Bool +isCoVar v = isCoVarType (varType v) + +isCoVarType :: Type -> Bool +isCoVarType = isEqPredTy +\end{code} + + +\begin{code} +tyCoVarsOfCo :: Coercion -> VarSet +-- Extracts type and coercion variables from a coercion +tyCoVarsOfCo (Refl ty) = tyVarsOfType ty +tyCoVarsOfCo (TyConAppCo _ cos) = tyCoVarsOfCos cos +tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2 +tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv +tyCoVarsOfCo (CoVarCo v) = unitVarSet v +tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos +tyCoVarsOfCo (UnsafeCo ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 +tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co +tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2 +tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co +tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty + +tyCoVarsOfCos :: [Coercion] -> VarSet +tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos + +coVarsOfCo :: Coercion -> VarSet +-- Extract *coerction* variables only. Tiresome to repeat the code, but easy. +coVarsOfCo (Refl _) = emptyVarSet +coVarsOfCo (TyConAppCo _ cos) = coVarsOfCos cos +coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 +coVarsOfCo (ForAllCo _ co) = coVarsOfCo co +coVarsOfCo (CoVarCo v) = unitVarSet v +coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos +coVarsOfCo (UnsafeCo _ _) = emptyVarSet +coVarsOfCo (SymCo co) = coVarsOfCo co +coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 +coVarsOfCo (NthCo _ co) = coVarsOfCo co +coVarsOfCo (InstCo co _) = coVarsOfCo co + +coVarsOfCos :: [Coercion] -> VarSet +coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos + +coercionSize :: Coercion -> Int +coercionSize (Refl ty) = typeSize ty +coercionSize (TyConAppCo _ cos) = 1 + sum (map coercionSize cos) +coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2 +coercionSize (ForAllCo _ co) = 1 + coercionSize co +coercionSize (CoVarCo _) = 1 +coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos) +coercionSize (UnsafeCo ty1 ty2) = typeSize ty1 + typeSize ty2 +coercionSize (SymCo co) = 1 + coercionSize co +coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2 +coercionSize (NthCo _ co) = 1 + coercionSize co +coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty +\end{code} + +%************************************************************************ +%* * + Pretty-printing coercions +%* * +%************************************************************************ + +@pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@ +function is defined to use this. @pprParendCo@ is the same, except it +puts parens around the type, except for the atomic cases. +@pprParendCo@ works just by setting the initial context precedence +very high. + +\begin{code} +instance Outputable Coercion where + ppr = pprCo + +pprCo, pprParendCo :: Coercion -> SDoc +pprCo co = ppr_co TopPrec co +pprParendCo co = ppr_co TyConPrec co + +ppr_co :: Prec -> Coercion -> SDoc +ppr_co _ (Refl ty) = angles (ppr ty) + +ppr_co p co@(TyConAppCo tc cos) + | tc `hasKey` funTyConKey = ppr_fun_co p co + | otherwise = pprTcApp p ppr_co tc cos + +ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $ + pprCo co1 <+> ppr_co TyConPrec co2 + +ppr_co p co@(ForAllCo {}) = ppr_forall_co p co + +ppr_co _ (CoVarCo cv) + | isSymOcc (getOccName cv) = parens (ppr cv) + | otherwise = ppr cv + +ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos + + +ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $ + ppr_co FunPrec co1 + <+> ptext (sLit ";") + <+> ppr_co FunPrec co2 +ppr_co p (InstCo co ty) = maybeParen p TyConPrec $ + pprParendCo co <> ptext (sLit "@") <> pprType ty + +ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) [pprParendType ty1, pprParendType ty2] +ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co] +ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co] + + +angles :: SDoc -> SDoc +angles p = char '<' <> p <> char '>' + +ppr_fun_co :: Prec -> Coercion -> SDoc +ppr_fun_co p co = pprArrowChain p (split co) where - composeCoercionKindsOf (co1:co2:rest) - = ASSERT( null rest ) - WARN( not (r1 `coreEqType` a2), - text "Strange! Type mismatch in trans coercion, probably a bug" - $$ - ppr r1 <+> text "=/=" <+> ppr a2) - (a1, r2) - where - (a1, r1) = coercionKind co1 - (a2, r2) = coercionKind co2 - -leftCoercionTyCon = - mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf + split (TyConAppCo f [arg,res]) + | f `hasKey` funTyConKey + = ppr_co FunPrec arg : split res + split co = [ppr_co TopPrec co] + +ppr_forall_co :: Prec -> Coercion -> SDoc +ppr_forall_co p ty + = maybeParen p FunPrec $ + sep [pprForAll tvs, ppr_co TopPrec rho] where - leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2) - where - (ty1,ty2) = fst (splitCoercionKindOf co) + (tvs, rho) = split1 [] ty + split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty + split1 tvs ty = (reverse tvs, ty) +\end{code} -rightCoercionTyCon = - mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf - where - rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2) - where - (ty1,ty2) = snd (splitCoercionKindOf co) +\begin{code} +pprCoAxiom :: CoAxiom -> SDoc +pprCoAxiom ax + = sep [ ptext (sLit "axiom") <+> ppr ax <+> ppr (co_ax_tvs ax) + , nest 2 (dcolon <+> pprEqPred (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ] +\end{code} + +%************************************************************************ +%* * + Functions over Kinds +%* * +%************************************************************************ -splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type)) --- Helper for left and right. Finds coercion kind of its input and --- returns the left and right projections of the coercion... +\begin{code} +-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into +-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence: -- --- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) -splitCoercionKindOf co - | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co) - , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1 - , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2 - = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2)) -splitCoercionKindOf co - = pprPanic "Coercion.splitCoercionKindOf" - (ppr co $$ ppr (coercionKindPredTy co)) - -instCoercionTyCon - = mkCoercionTyCon instCoercionTyConName 2 instCoercionKind +-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c] +decomposeCo :: Arity -> Coercion -> [Coercion] +decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ] + +-- | Attempts to obtain the type variable underlying a 'Coercion' +getCoVar_maybe :: Coercion -> Maybe CoVar +getCoVar_maybe (CoVarCo cv) = Just cv +getCoVar_maybe _ = Nothing + +-- | Attempts to tease a coercion apart into a type constructor and the application +-- of a number of coercion arguments to that constructor +splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion]) +splitTyConAppCo_maybe (Refl ty) = (fmap . second . map) Refl (splitTyConApp_maybe ty) +splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos) +splitTyConAppCo_maybe _ = Nothing + +splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion) +-- ^ Attempt to take a coercion application apart. +splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2) +splitAppCo_maybe (TyConAppCo tc cos) + | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc + , Just (cos', co') <- snocView cos + = Just (mkTyConAppCo tc cos', co') -- Never create unsaturated type family apps! + -- Use mkTyConAppCo to preserve the invariant + -- that identity coercions are always represented by Refl +splitAppCo_maybe (Refl ty) + | Just (ty1, ty2) <- splitAppTy_maybe ty + = Just (Refl ty1, Refl ty2) +splitAppCo_maybe _ = Nothing + +splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion) +splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co) +splitForAllCo_maybe _ = Nothing + +------------------------------------------------------- +-- and some coercion kind stuff + +coVarPred :: CoVar -> PredType +coVarPred cv + = ASSERT( isCoVar cv ) + case splitPredTy_maybe (varType cv) of + Just pred -> pred + other -> pprPanic "coVarPred" (ppr cv $$ ppr other) + +coVarKind :: CoVar -> (Type,Type) +-- c :: t1 ~ t2 +coVarKind cv = case coVarKind_maybe cv of + Just ts -> ts + Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv)) + +coVarKind_maybe :: CoVar -> Maybe (Type,Type) +coVarKind_maybe cv = splitEqPredTy_maybe (varType cv) + +-- | Makes a coercion type from two types: the types whose equality +-- is proven by the relevant 'Coercion' +mkCoType :: Type -> Type -> Type +mkCoType ty1 ty2 = PredTy (EqPred ty1 ty2) + +splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type) +splitCoPredTy_maybe ty + | Just (cv,r) <- splitForAllTy_maybe ty + , isCoVar cv + , Just (s,t) <- coVarKind_maybe cv + = Just (s,t,r) + | otherwise + = Nothing + +isReflCo :: Coercion -> Bool +isReflCo (Refl {}) = True +isReflCo _ = False + +isReflCo_maybe :: Coercion -> Maybe Type +isReflCo_maybe (Refl ty) = Just ty +isReflCo_maybe _ = Nothing +\end{code} + +%************************************************************************ +%* * + Building coercions +%* * +%************************************************************************ + +\begin{code} +mkCoVarCo :: CoVar -> Coercion +mkCoVarCo cv + | ty1 `eqType` ty2 = Refl ty1 + | otherwise = CoVarCo cv where - instantiateCo t s = - let Just (tv, ty) = splitForAllTy_maybe t in - substTyWith [tv] [s] ty + (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv - instCoercionKind (co1:ty:rest) = ASSERT( null rest ) - (instantiateCo t1 ty, instantiateCo t2 ty) - where (t1, t2) = coercionKind co1 +mkReflCo :: Type -> Coercion +mkReflCo = Refl -unsafeCoercionTyCon - = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind +mkAxInstCo :: CoAxiom -> [Type] -> Coercion +mkAxInstCo ax tys + | arity == n_tys = AxiomInstCo ax rtys + | otherwise = ASSERT( arity < n_tys ) + foldl AppCo (AxiomInstCo ax (take arity rtys)) + (drop arity rtys) where - unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) - --------------------------------------- --- ...and their names + n_tys = length tys + arity = coAxiomArity ax + rtys = map Refl tys + +-- | Apply a 'Coercion' to another 'Coercion'. +mkAppCo :: Coercion -> Coercion -> Coercion +mkAppCo (Refl ty1) (Refl ty2) = Refl (mkAppTy ty1 ty2) +mkAppCo (Refl (TyConApp tc tys)) co = TyConAppCo tc (map Refl tys ++ [co]) +mkAppCo (TyConAppCo tc cos) co = TyConAppCo tc (cos ++ [co]) +mkAppCo co1 co2 = AppCo co1 co2 +-- Note, mkAppCo is careful to maintain invariants regarding +-- where Refl constructors appear; see the comments in the definition +-- of Coercion and the Note [Refl invariant] in types/TypeRep.lhs. -mkCoConName :: FastString -> Unique -> TyCon -> Name -mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ) - key (ATyCon coCon) BuiltInSyntax +-- | Applies multiple 'Coercion's to another 'Coercion', from left to right. +-- See also 'mkAppCo' +mkAppCos :: Coercion -> [Coercion] -> Coercion +mkAppCos co1 tys = foldl mkAppCo co1 tys -transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: Name +-- | Apply a type constructor to a list of coercions. +mkTyConAppCo :: TyCon -> [Coercion] -> Coercion +mkTyConAppCo tc cos + -- Expand type synonyms + | Just (tv_co_prs, rhs_ty, leftover_cos) <- tcExpandTyCon_maybe tc cos + = mkAppCos (liftCoSubst (mkTopCvSubst tv_co_prs) rhs_ty) leftover_cos -transCoercionTyConName = mkCoConName (fsLit "trans") transCoercionTyConKey transCoercionTyCon -symCoercionTyConName = mkCoConName (fsLit "sym") symCoercionTyConKey symCoercionTyCon -leftCoercionTyConName = mkCoConName (fsLit "left") leftCoercionTyConKey leftCoercionTyCon -rightCoercionTyConName = mkCoConName (fsLit "right") rightCoercionTyConKey rightCoercionTyCon -instCoercionTyConName = mkCoConName (fsLit "inst") instCoercionTyConKey instCoercionTyCon -unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon + | Just tys <- traverse isReflCo_maybe cos + = Refl (mkTyConApp tc tys) -- See Note [Refl invariant] + | otherwise = TyConAppCo tc cos +-- | Make a function 'Coercion' between two other 'Coercion's +mkFunCo :: Coercion -> Coercion -> Coercion +mkFunCo co1 co2 = mkTyConAppCo funTyCon [co1, co2] + +-- | Make a 'Coercion' which binds a variable within an inner 'Coercion' +mkForAllCo :: Var -> Coercion -> Coercion +-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar) +mkForAllCo tv (Refl ty) = ASSERT( isTyVar tv ) Refl (mkForAllTy tv ty) +mkForAllCo tv co = ASSERT ( isTyVar tv ) ForAllCo tv co + +mkPredCo :: Pred Coercion -> Coercion +-- See Note [Predicate coercions] +mkPredCo (EqPred co1 co2) = mkTyConAppCo eqPredPrimTyCon [co1,co2] +mkPredCo (ClassP cls cos) = mkTyConAppCo (classTyCon cls) cos +mkPredCo (IParam _ co) = co + +------------------------------- -instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI) +-- | Create a symmetric version of the given 'Coercion' that asserts +-- equality between the same types but in the other "direction", so +-- a kind of @t1 ~ t2@ becomes the kind @t2 ~ t1@. +mkSymCo :: Coercion -> Coercion + +-- Do a few simple optimizations, but don't bother pushing occurrences +-- of symmetry to the leaves; the optimizer will take care of that. +mkSymCo co@(Refl {}) = co +mkSymCo (UnsafeCo ty1 ty2) = UnsafeCo ty2 ty1 +mkSymCo (SymCo co) = co +mkSymCo co = SymCo co + +-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively. +mkTransCo :: Coercion -> Coercion -> Coercion +mkTransCo (Refl _) co = co +mkTransCo co (Refl _) = co +mkTransCo co1 co2 = TransCo co1 co2 + +mkNthCo :: Int -> Coercion -> Coercion +mkNthCo n (Refl ty) = Refl (getNth n ty) +mkNthCo n co = NthCo n co + +-- | Instantiates a 'Coercion' with a 'Type' argument. If possible, it immediately performs +-- the resulting beta-reduction, otherwise it creates a suspended instantiation. +mkInstCo :: Coercion -> Type -> Coercion +mkInstCo (ForAllCo tv co) ty = substCoWithTy tv ty co +mkInstCo co ty = InstCo co ty + +-- | Manufacture a coercion from thin air. Needless to say, this is +-- not usually safe, but it is used when we know we are dealing with +-- bottom, which is one case in which it is safe. This is also used +-- to implement the @unsafeCoerce#@ primitive. Optimise by pushing +-- down through type constructors. +mkUnsafeCo :: Type -> Type -> Coercion +mkUnsafeCo ty1 ty2 | ty1 `eqType` ty2 = Refl ty1 +mkUnsafeCo (TyConApp tc1 tys1) (TyConApp tc2 tys2) + | tc1 == tc2 + = mkTyConAppCo tc1 (zipWith mkUnsafeCo tys1 tys2) + +mkUnsafeCo (FunTy a1 r1) (FunTy a2 r2) + = mkFunCo (mkUnsafeCo a1 a2) (mkUnsafeCo r1 r2) + +mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2 + +-- See note [Newtype coercions] in TyCon + +-- | Create a coercion constructor (axiom) suitable for the given +-- newtype 'TyCon'. The 'Name' should be that of a new coercion +-- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and +-- the type the appropriate right hand side of the @newtype@, with +-- the free variables a subset of those 'TyVar's. +mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom +mkNewTypeCo name tycon tvs rhs_ty + = CoAxiom { co_ax_unique = nameUnique name + , co_ax_name = name + , co_ax_tvs = tvs + , co_ax_lhs = mkTyConApp tycon (mkTyVarTys tvs) + , co_ax_rhs = rhs_ty } + +-- | Create a coercion identifying a @data@, @newtype@ or @type@ representation type +-- and its family instance. It has the form @Co tvs :: F ts ~ R tvs@, where @Co@ is +-- the coercion constructor built here, @F@ the family tycon and @R@ the (derived) +-- representation tycon. +mkFamInstCo :: Name -- ^ Unique name for the coercion tycon + -> [TyVar] -- ^ Type parameters of the coercion (@tvs@) + -> TyCon -- ^ Family tycon (@F@) + -> [Type] -- ^ Type instance (@ts@) + -> TyCon -- ^ Representation tycon (@R@) + -> CoAxiom -- ^ Coercion constructor (@Co@) +mkFamInstCo name tvs family inst_tys rep_tycon + = CoAxiom { co_ax_unique = nameUnique name + , co_ax_name = name + , co_ax_tvs = tvs + , co_ax_lhs = mkTyConApp family inst_tys + , co_ax_rhs = mkTyConApp rep_tycon (mkTyVarTys tvs) } + +mkPiCos :: [Var] -> Coercion -> Coercion +mkPiCos vs co = foldr mkPiCo co vs + +mkPiCo :: Var -> Coercion -> Coercion +mkPiCo v co | isTyVar v = mkForAllCo v co + | otherwise = mkFunCo (mkReflCo (varType v)) co +\end{code} + +%************************************************************************ +%* * + Newtypes +%* * +%************************************************************************ + +\begin{code} +instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion) -- ^ If @co :: T ts ~ rep_ty@ then: -- -- > instNewTyCon_maybe T ts = Just (rep_ty, co) instNewTyCon_maybe tc tys - | Just (tvs, ty, mb_co_tc) <- unwrapNewTyCon_maybe tc + | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc = ASSERT( tys `lengthIs` tyConArity tc ) - Just (substTyWith tvs tys ty, - case mb_co_tc of - Nothing -> IdCo - Just co_tc -> ACo (mkTyConApp co_tc tys)) + Just (substTyWith tvs tys ty, mkAxInstCo co_tc tys) | otherwise = Nothing @@ -557,113 +686,425 @@ splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion) splitNewTypeRepCo_maybe ty | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty' splitNewTypeRepCo_maybe (TyConApp tc tys) - | Just (ty', coi) <- instNewTyCon_maybe tc tys - = case coi of - ACo co -> Just (ty', co) - IdCo -> panic "splitNewTypeRepCo_maybe" + | Just (ty', co) <- instNewTyCon_maybe tc tys + = case co of + Refl _ -> panic "splitNewTypeRepCo_maybe" -- This case handled by coreView + _ -> Just (ty', co) splitNewTypeRepCo_maybe _ = Nothing -- | Determines syntactic equality of coercions coreEqCoercion :: Coercion -> Coercion -> Bool -coreEqCoercion = coreEqType +coreEqCoercion co1 co2 = coreEqCoercion2 rn_env co1 co2 + where rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2)) + +coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool +coreEqCoercion2 env (Refl ty1) (Refl ty2) = eqTypeX env ty1 ty2 +coreEqCoercion2 env (TyConAppCo tc1 cos1) (TyConAppCo tc2 cos2) + = tc1 == tc2 && all2 (coreEqCoercion2 env) cos1 cos2 + +coreEqCoercion2 env (AppCo co11 co12) (AppCo co21 co22) + = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22 + +coreEqCoercion2 env (ForAllCo v1 co1) (ForAllCo v2 co2) + = coreEqCoercion2 (rnBndr2 env v1 v2) co1 co2 + +coreEqCoercion2 env (CoVarCo cv1) (CoVarCo cv2) + = rnOccL env cv1 == rnOccR env cv2 + +coreEqCoercion2 env (AxiomInstCo con1 cos1) (AxiomInstCo con2 cos2) + = con1 == con2 + && all2 (coreEqCoercion2 env) cos1 cos2 + +coreEqCoercion2 env (UnsafeCo ty11 ty12) (UnsafeCo ty21 ty22) + = eqTypeX env ty11 ty21 && eqTypeX env ty12 ty22 + +coreEqCoercion2 env (SymCo co1) (SymCo co2) + = coreEqCoercion2 env co1 co2 + +coreEqCoercion2 env (TransCo co11 co12) (TransCo co21 co22) + = coreEqCoercion2 env co11 co21 && coreEqCoercion2 env co12 co22 + +coreEqCoercion2 env (NthCo d1 co1) (NthCo d2 co2) + = d1 == d2 && coreEqCoercion2 env co1 co2 + +coreEqCoercion2 env (InstCo co1 ty1) (InstCo co2 ty2) + = coreEqCoercion2 env co1 co2 && eqTypeX env ty1 ty2 + +coreEqCoercion2 _ _ _ = False \end{code} +%************************************************************************ +%* * + Substitution of coercions +%* * +%************************************************************************ + +\begin{code} +-- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when +-- doing a \"lifting\" substitution) +type CvSubstEnv = VarEnv Coercion + +emptyCvSubstEnv :: CvSubstEnv +emptyCvSubstEnv = emptyVarEnv + +data CvSubst + = CvSubst InScopeSet -- The in-scope type variables + TvSubstEnv -- Substitution of types + CvSubstEnv -- Substitution of coercions + +instance Outputable CvSubst where + ppr (CvSubst ins tenv cenv) + = brackets $ sep[ ptext (sLit "CvSubst"), + nest 2 (ptext (sLit "In scope:") <+> ppr ins), + nest 2 (ptext (sLit "Type env:") <+> ppr tenv), + nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ] + +emptyCvSubst :: CvSubst +emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv + +isEmptyCvSubst :: CvSubst -> Bool +isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv + +getCvInScope :: CvSubst -> InScopeSet +getCvInScope (CvSubst in_scope _ _) = in_scope + +zapCvSubstEnv :: CvSubst -> CvSubst +zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv + +cvTvSubst :: CvSubst -> TvSubst +cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs --------------------------------------- --- CoercionI smart constructors --- lifted smart constructors of ordinary coercions +tvCvSubst :: TvSubst -> CvSubst +tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv + +extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst +extendTvSubst (CvSubst in_scope tenv cenv) tv ty + = CvSubst in_scope (extendVarEnv tenv tv ty) cenv + +substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar) +substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var + = ASSERT( isCoVar old_var ) + (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var) + where + -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t) + -- In that case, mkCoVarCo will return a ReflCoercion, and + -- we want to substitute that (not new_var) for old_var + new_co = mkCoVarCo new_var + no_change = new_var == old_var && not (isReflCo new_co) + + new_cenv | no_change = delVarEnv cenv old_var + | otherwise = extendVarEnv cenv old_var new_co + + new_var = uniqAway in_scope subst_old_var + subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var)) + -- It's important to do the substitution for coercions, + -- because only they can have free type variables + +substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar) +substTyVarBndr (CvSubst in_scope tenv cenv) old_var + = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of + (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var) + +zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst +zipOpenCvSubst vs cos + | debugIsOn && (length vs /= length cos) + = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst + | otherwise + = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos) + +mkTopCvSubst :: [(Var,Coercion)] -> CvSubst +mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs) + +substCoWithTy :: TyVar -> Type -> Coercion -> Coercion +substCoWithTy tv ty = substCoWithTys [tv] [ty] + +substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion +substCoWithTys tvs tys co + | debugIsOn && (length tvs /= length tys) + = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co + | otherwise + = ASSERT( length tvs == length tys ) + substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co + where + in_scope = mkInScopeSet (tyVarsOfTypes tys) + +-- | Substitute within a 'Coercion' +substCo :: CvSubst -> Coercion -> Coercion +substCo subst co | isEmptyCvSubst subst = co + | otherwise = subst_co subst co + +-- | Substitute within several 'Coercion's +substCos :: CvSubst -> [Coercion] -> [Coercion] +substCos subst cos | isEmptyCvSubst subst = cos + | otherwise = map (substCo subst) cos + +substTy :: CvSubst -> Type -> Type +substTy subst = Type.substTy (cvTvSubst subst) + +subst_co :: CvSubst -> Coercion -> Coercion +subst_co subst co + = go co + where + go_ty :: Type -> Type + go_ty = Coercion.substTy subst + + go :: Coercion -> Coercion + go (Refl ty) = Refl $! go_ty ty + go (TyConAppCo tc cos) = let args = map go cos + in args `seqList` TyConAppCo tc args + go (AppCo co1 co2) = mkAppCo (go co1) $! go co2 + go (ForAllCo tv co) = case substTyVarBndr subst tv of + (subst', tv') -> + ForAllCo tv' $! subst_co subst' co + go (CoVarCo cv) = substCoVar subst cv + go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos + go (UnsafeCo ty1 ty2) = (UnsafeCo $! go_ty ty1) $! go_ty ty2 + go (SymCo co) = mkSymCo (go co) + go (TransCo co1 co2) = mkTransCo (go co1) (go co2) + go (NthCo d co) = mkNthCo d (go co) + go (InstCo co ty) = mkInstCo (go co) $! go_ty ty + +substCoVar :: CvSubst -> CoVar -> Coercion +substCoVar (CvSubst in_scope _ cenv) cv + | Just co <- lookupVarEnv cenv cv = co + | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1 + | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv ) + ASSERT( isCoVar cv ) CoVarCo cv + +substCoVars :: CvSubst -> [CoVar] -> [Coercion] +substCoVars subst cvs = map (substCoVar subst) cvs + +lookupTyVar :: CvSubst -> TyVar -> Maybe Type +lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv + +lookupCoVar :: CvSubst -> Var -> Maybe Coercion +lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v +\end{code} + +%************************************************************************ +%* * + "Lifting" substitution + [(TyVar,Coercion)] -> Type -> Coercion +%* * +%************************************************************************ \begin{code} --- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it --- can represent either one of: +liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion +liftCoSubstWith tvs cos = liftCoSubst (zipOpenCvSubst tvs cos) + +-- | The \"lifting\" operation which substitutes coercions for type +-- variables in a type to produce a coercion. -- --- 1. A proper 'Coercion' +-- For the inverse operation, see 'liftCoMatch' +liftCoSubst :: CvSubst -> Type -> Coercion +-- The CvSubst maps TyVar -> Type (mainly for cloning foralls) +-- TyVar -> Coercion (this is the payload) +-- The unusual thing is that the *coercion* substitution maps +-- some *type* variables. That's the whole point of this function! +liftCoSubst subst ty | isEmptyCvSubst subst = Refl ty + | otherwise = ty_co_subst subst ty + +ty_co_subst :: CvSubst -> Type -> Coercion +ty_co_subst subst ty + = go ty + where + go (TyVarTy tv) = liftCoSubstTyVar subst tv `orElse` Refl (TyVarTy tv) + go (AppTy ty1 ty2) = mkAppCo (go ty1) (go ty2) + go (TyConApp tc tys) = mkTyConAppCo tc (map go tys) + go (FunTy ty1 ty2) = mkFunCo (go ty1) (go ty2) + go (ForAllTy v ty) = mkForAllCo v' $! (ty_co_subst subst' ty) + where + (subst', v') = liftCoSubstTyVarBndr subst v + go (PredTy p) = mkPredCo (go <$> p) + +liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion +liftCoSubstTyVar subst@(CvSubst _ tenv cenv) tv + = case (lookupVarEnv tenv tv, lookupVarEnv cenv tv) of + (Nothing, Nothing) -> Nothing + (Just ty, Nothing) -> Just (Refl ty) + (Nothing, Just co) -> Just co + (Just {}, Just {}) -> pprPanic "ty_co_subst" (ppr tv $$ ppr subst) + +liftCoSubstTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar) +liftCoSubstTyVarBndr (CvSubst in_scope tenv cenv) old_var + = (CvSubst (in_scope `extendInScopeSet` new_var) + new_tenv + (delVarEnv cenv old_var) -- See Note [Lifting substitutions] + , new_var) + where + new_tenv | no_change = delVarEnv tenv old_var + | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) + + no_change = new_var == old_var + new_var = uniqAway in_scope old_var +\end{code} + +Note [Lifting substitutions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider liftCoSubstWith [a] [co] (a, forall a. a) +Then we want to substitute for the free 'a', but obviously not for +the bound 'a'. hence the (delVarEnv cent old_var) in liftCoSubstTyVarBndr. + +This also why we need a full CvSubst when doing lifting substitutions. + +\begin{code} +-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if +-- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@. +-- That is, it matches a type against a coercion of the same +-- "shape", and returns a lifting substitution which could have been +-- used to produce the given coercion from the given type. +liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst +liftCoMatch tmpls ty co + = case ty_co_match menv (emptyVarEnv, emptyVarEnv) ty co of + Just (tv_env, cv_env) -> Just (CvSubst in_scope tv_env cv_env) + Nothing -> Nothing + where + menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope } + in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co) + -- Like tcMatchTy, assume all the interesting variables + -- in ty are in tmpls + +type TyCoSubstEnv = (TvSubstEnv, CvSubstEnv) + -- Used locally inside ty_co_match only + +-- | 'ty_co_match' does all the actual work for 'liftCoMatch'. +ty_co_match :: MatchEnv -> TyCoSubstEnv -> Type -> Coercion -> Maybe TyCoSubstEnv +ty_co_match menv subst ty co | Just ty' <- coreView ty = ty_co_match menv subst ty' co + + -- Deal with the Refl case by delegating to type matching +ty_co_match menv (tenv, cenv) ty co + | Just ty' <- isReflCo_maybe co + = case ruleMatchTyX ty_menv tenv ty ty' of + Just tenv' -> Just (tenv', cenv) + Nothing -> Nothing + where + ty_menv = menv { me_tmpls = me_tmpls menv `minusUFM` cenv } + -- Remove from the template set any variables already bound to non-refl coercions + + -- Match a type variable against a non-refl coercion +ty_co_match menv subst@(tenv, cenv) (TyVarTy tv1) co + | Just {} <- lookupVarEnv tenv tv1' -- tv1' is already bound to (Refl ty) + = Nothing -- The coercion 'co' is not Refl + + | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1 + = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co + then Just subst + else Nothing -- no match since tv1 matches two different coercions + + | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var + = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co)) + then Nothing -- occurs check failed + else return (tenv, extendVarEnv cenv tv1' co) + -- BAY: I don't think we need to do any kind matching here yet + -- (compare 'match'), but we probably will when moving to SHE. + + | otherwise -- tv1 is not a template ty var, so the only thing it + -- can match is a reflexivity coercion for itself. + -- But that case is dealt with already + = Nothing + + where + rn_env = me_env menv + tv1' = rnOccL rn_env tv1 + +ty_co_match menv subst (AppTy ty1 ty2) co + | Just (co1, co2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy + = do { subst' <- ty_co_match menv subst ty1 co1 + ; ty_co_match menv subst' ty2 co2 } + +ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos) + | tc1 == tc2 = ty_co_matches menv subst tys cos + +ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos) + | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos + +ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co) + = ty_co_match menv' subst ty co + where + menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 } + +ty_co_match _ _ _ _ = Nothing + +ty_co_matches :: MatchEnv -> TyCoSubstEnv -> [Type] -> [Coercion] -> Maybe TyCoSubstEnv +ty_co_matches menv = matchList (ty_co_match menv) +\end{code} + +%************************************************************************ +%* * + Sequencing on coercions +%* * +%************************************************************************ + +\begin{code} +seqCo :: Coercion -> () +seqCo (Refl ty) = seqType ty +seqCo (TyConAppCo tc cos) = tc `seq` seqCos cos +seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2 +seqCo (ForAllCo tv co) = tv `seq` seqCo co +seqCo (CoVarCo cv) = cv `seq` () +seqCo (AxiomInstCo con cos) = con `seq` seqCos cos +seqCo (UnsafeCo ty1 ty2) = seqType ty1 `seq` seqType ty2 +seqCo (SymCo co) = seqCo co +seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2 +seqCo (NthCo _ co) = seqCo co +seqCo (InstCo co ty) = seqCo co `seq` seqType ty + +seqCos :: [Coercion] -> () +seqCos [] = () +seqCos (co:cos) = seqCo co `seq` seqCos cos +\end{code} + + +%************************************************************************ +%* * + The kind of a type, and of a coercion +%* * +%************************************************************************ + +\begin{code} +coercionType :: Coercion -> Type +coercionType co = case coercionKind co of + Pair ty1 ty2 -> mkCoType ty1 ty2 + +------------------ +-- | If it is the case that -- --- 2. The identity coercion -data CoercionI = IdCo | ACo Coercion - -instance Outputable CoercionI where - ppr IdCo = ptext (sLit "IdCo") - ppr (ACo co) = ppr co - -isIdentityCoI :: CoercionI -> Bool -isIdentityCoI IdCo = True -isIdentityCoI _ = False - --- | Tests whether all the given 'CoercionI's represent the identity coercion -allIdCoIs :: [CoercionI] -> Bool -allIdCoIs = all isIdentityCoI - --- | For each 'CoercionI' in the input list, return either the 'Coercion' it --- contains or the corresponding 'Type' from the other list -zipCoArgs :: [CoercionI] -> [Type] -> [Coercion] -zipCoArgs cois tys = zipWith fromCoI cois tys - --- | Return either the 'Coercion' contained within the 'CoercionI' or the given --- 'Type' if the 'CoercionI' is the identity 'Coercion' -fromCoI :: CoercionI -> Type -> Type -fromCoI IdCo ty = ty -- Identity coercion represented -fromCoI (ACo co) _ = co -- by the type itself - --- | Smart constructor for @sym@ on 'CoercionI', see also 'mkSymCoercion' -mkSymCoI :: CoercionI -> CoercionI -mkSymCoI IdCo = IdCo -mkSymCoI (ACo co) = ACo $ mkCoercion symCoercionTyCon [co] - -- the smart constructor - -- is too smart with tyvars - --- | Smart constructor for @trans@ on 'CoercionI', see also 'mkTransCoercion' -mkTransCoI :: CoercionI -> CoercionI -> CoercionI -mkTransCoI IdCo aco = aco -mkTransCoI aco IdCo = aco -mkTransCoI (ACo co1) (ACo co2) = ACo $ mkTransCoercion co1 co2 - --- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion' -mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI -mkTyConAppCoI tyCon tys cois - | allIdCoIs cois = IdCo - | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys)) - --- | Smart constructor for honest-to-god 'Coercion' application on 'CoercionI', see also 'mkAppCoercion' -mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI -mkAppTyCoI _ IdCo _ IdCo = IdCo -mkAppTyCoI ty1 coi1 ty2 coi2 = - ACo $ AppTy (fromCoI coi1 ty1) (fromCoI coi2 ty2) - --- | Smart constructor for function-'Coercion's on 'CoercionI', see also 'mkFunCoercion' -mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI -mkFunTyCoI _ IdCo _ IdCo = IdCo -mkFunTyCoI ty1 coi1 ty2 coi2 = - ACo $ FunTy (fromCoI coi1 ty1) (fromCoI coi2 ty2) - --- | Smart constructor for quantified 'Coercion's on 'CoercionI', see also 'mkForAllCoercion' -mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI -mkForAllTyCoI _ IdCo = IdCo -mkForAllTyCoI tv (ACo co) = ACo $ ForAllTy tv co - --- | Extract a 'Coercion' from a 'CoercionI' if it represents one. If it is the identity coercion, --- panic -fromACo :: CoercionI -> Coercion -fromACo (ACo co) = co - --- | Smart constructor for class 'Coercion's on 'CoercionI'. Satisfies: +-- > c :: (t1 ~ t2) -- --- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois)) -mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI -mkClassPPredCoI cls tys cois - | allIdCoIs cois = IdCo - | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys) - --- | Smart constructor for implicit parameter 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' -mkIParamPredCoI :: (IPName Name) -> CoercionI -> CoercionI -mkIParamPredCoI _ IdCo = IdCo -mkIParamPredCoI ipn (ACo co) = ACo $ PredTy $ IParam ipn co - --- | Smart constructor for type equality 'Coercion's on 'CoercionI'. Similar to 'mkClassPPredCoI' -mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI -mkEqPredCoI _ IdCo _ IdCo = IdCo -mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2 -mkEqPredCoI _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2) +-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@. +coercionKind :: Coercion -> Pair Type +coercionKind (Refl ty) = Pair ty ty +coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos) +coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2 +coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co +coercionKind (CoVarCo cv) = ASSERT( isCoVar cv ) toPair $ coVarKind cv +coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos + in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax)) + (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax)) +coercionKind (UnsafeCo ty1 ty2) = Pair ty1 ty2 +coercionKind (SymCo co) = swap $ coercionKind co +coercionKind (TransCo co1 co2) = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2) +coercionKind (NthCo d co) = getNth d <$> coercionKind co +coercionKind co@(InstCo aco ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind aco + = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks + | otherwise = pprPanic "coercionKind" (ppr co) + +-- | Apply 'coercionKind' to multiple 'Coercion's +coercionKinds :: [Coercion] -> Pair [Type] +coercionKinds tys = sequenceA $ map coercionKind tys + +getNth :: Int -> Type -> Type +getNth n ty | Just (_, tys) <- splitTyConApp_maybe ty + = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n +getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty) \end{code} + +\begin{code} +applyCo :: Type -> Coercion -> Type +-- Gives the type of (e co) where e :: (a~b) => ty +applyCo ty co | Just ty' <- coreView ty = applyCo ty' co +applyCo (FunTy _ ty) _ = ty +applyCo _ _ = panic "applyCo" +\end{code} \ No newline at end of file