X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypes%2FCoercion.lhs;h=7df5b8e38fb82d77f1689165bdc8a70631827695;hp=83a5af341cacc4c33acb5a8a390b2852b47ee2b8;hb=c8c2f6bb7d79a2a6aeaa3233363fdf0bbbfad205;hpb=bcadca676448e38427b910bad5d7063f948a99c8 diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 83a5af3..7df5b8e 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -1,618 +1,659 @@ -T% +% % (c) The University of Glasgow 2006 % \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, coVarKind, - coercionKind, coercionKinds, 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, - mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, - + 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 - csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon, - - -- ** Optimisation - optCoercion, - + 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. -coVarKind :: CoVar -> (Type,Type) --- c :: t1 ~ t2 -coVarKind cv = splitCoVarKind (tyVarKind cv) +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. --- | Take a 'CoercionKind' apart into the two types it relates: see also 'mkCoKind'. --- Panics if the argument is not a valid 'CoercionKind' -splitCoVarKind :: Kind -> (Type, Type) -splitCoVarKind co | Just co' <- kindView co = splitCoVarKind co' -splitCoVarKind (PredTy (EqPred ty1 ty2)) = (ty1, ty2) +For example, suppose we have --- | 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) + C a : t[a] ~ F a + g : b ~ c --- | (mkCoPredTy s t r) produces the type: (s~t) => r -mkCoPredTy :: Type -> Type -> Type -> Type -mkCoPredTy s t r = ForAllTy (mkWildCoVar (mkCoKind s t)) r +and we want to optimize --- | Tests whether a type is just a type equality predicate -isEqPredTy :: Type -> Bool -isEqPredTy (PredTy pred) = isEqPred pred -isEqPredTy _ = False + sym (C b) ; t[g] ; C c --- | Creates a type equality predicate -mkEqPred :: (Type, Type) -> PredType -mkEqPred (ty1, ty2) = EqPred ty1 ty2 +which has the kind --- | 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) + F b ~ F c --- | Create a reflexive 'CoercionKind' that asserts that a type can be coerced to itself -mkReflCoKind :: Type -> CoercionKind -mkReflCoKind ty = mkCoKind ty ty +(stopping through t[b] and t[c] along the way). --- | 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)@. -coercionKind :: Coercion -> (Type, Type) -coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind 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) +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 - | 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) - | isCoVar tv --- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2 --- ---------------------------------------------- --- c1~c2 => c3 :: (s1~t1) => r1 ~ (s2~t2) => r2 --- or --- forall (_:c1~c2) - = let (c1,c2) = coVarKind tv - (s1,s2) = coercionKind c1 - (t1,t2) = coercionKind c2 - (r1,r2) = coercionKind ty - in - (mkCoPredTy s1 t1 r1, mkCoPredTy s2 t2 r2) + C g : t[b] ~ F c - | otherwise --- c1 :: s1~s2 c2 :: t1~t2 c3 :: r1~r2 --- ---------------------------------------------- --- forall a:k. c :: forall a:k. t1 ~ forall a:k. t2 - = let (ty1, ty2) = coercionKind ty in - (ForAllTy tv ty1, ForAllTy tv ty2) - -coercionKind (PredTy (EqPred c1 c2)) - = pprTrace "coercionKind" (pprEqPred (c1,c2)) $ - let k1 = coercionKindPredTy c1 - k2 = coercionKindPredTy c2 in - (k1,k2) - -- These should not show up in coercions at all - -- becuase they are in the form of for-alls - where - coercionKindPredTy c = let (t1, t2) = coercionKind c in mkCoKind t1 t2 +which indeed has the same kind as t[g] ; C c. +Now we have + sym (C b) ; C g -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)) +which can be optimized to F g. --- | 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 -\end{code} + +Note [Forall coercions] +~~~~~~~~~~~~~~~~~~~~~~~ +Constructing coercions between forall-types can be a bit tricky. +Currently, the situation is as follows: + + ForAllCo TyVar Coercion + +represents a coercion between polymorphic types, with the rule + + v : k g : t1 ~ t2 + ---------------------------------------------- + ForAllCo v g : (all v:k . t1) ~ (all v:k . t2) + +Note that it's only necessary to coerce between polymorphic types +where the type variables have identical kinds, because equality on +kinds is trivial. + +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 + +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. %************************************************************************ %* * - Building coercions +\subsection{Coercion variables} %* * %************************************************************************ -Coercion kind and type mk's (make saturated TyConApp CoercionTyCon{...} args) - \begin{code} --- | 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 +coVarName :: CoVar -> Name +coVarName = varName --- | 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 +setCoVarUnique :: CoVar -> Unique -> CoVar +setCoVarUnique = setVarUnique --- | Apply a type constructor to a list of coercions. -mkTyConCoercion :: TyCon -> [Coercion] -> Coercion -mkTyConCoercion con cos = mkTyConApp con cos +setCoVarName :: CoVar -> Name -> CoVar +setCoVarName = setVarName --- | Make a function 'Coercion' between two other 'Coercion's -mkFunCoercion :: Coercion -> Coercion -> Coercion -mkFunCoercion co1 co2 = mkFunTy co1 co2 +isCoVar :: Var -> Bool +isCoVar v = isCoVarType (varType v) --- | 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 +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} -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 +%************************************************************************ +%* * + Pretty-printing coercions +%* * +%************************************************************************ -------------------------------- --- 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 +@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. - | otherwise - = mkCoercion transCoercionTyCon [g1, g2] +\begin{code} +instance Outputable Coercion where + ppr = pprCo +pprCo, pprParendCo :: Coercion -> SDoc +pprCo co = ppr_co TopPrec co +pprParendCo co = ppr_co TyConPrec co -------------------------------- --- Smart constructors for left and right +ppr_co :: Prec -> Coercion -> SDoc +ppr_co _ (Refl ty) = angles (ppr ty) -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 +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 -mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion -mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co] -mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co] -mkCselRCoercion co = mkCoercion cselRCoercionTyCon [co] +ppr_co p co@(ForAllCo {}) = ppr_forall_co p co -------------------------------- -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] +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 --- See note [Newtype coercions] in TyCon --- | 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 +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 - rule args = ASSERT( co_con_arity == length args ) - (TyConApp tycon args, substTyWith tvs args rhs_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] --- | 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 + +angles :: SDoc -> SDoc +angles p = char '<' <> p <> char '>' + +ppr_fun_co :: Prec -> Coercion -> SDoc +ppr_fun_co p co = pprArrowChain p (split co) 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 + 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 + (tvs, rho) = split1 [] ty + split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty + split1 tvs ty = (reverse tvs, ty) \end{code} +\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} %************************************************************************ %* * - Coercion Type Constructors + Functions over Kinds %* * %************************************************************************ -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) - \begin{code} --- | Coercion type constructors: avoid using these directly and instead use --- the @mk*Coercion@ and @split*Coercion@ family of functions if possible. +-- | 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: -- --- 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, transCoercionTyCon, leftCoercionTyCon, - rightCoercionTyCon, instCoercionTyCon, unsafeCoercionTyCon, - csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon :: TyCon - -symCoercionTyCon = - mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf - where - flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1) - where - (ty1, ty2) = coercionKind co +-- > 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 -transCoercionTyCon = - mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf - where - composeCoercionKindsOf (co1:co2:rest) - = ASSERT( null rest ) - WARN( not (r1 `coreEqType` a2), - text "Strange! Type mismatch in trans coercion, probably a bug" - $$ - _err_stuff ) - (a1, r2) - where - (a1, r1) = coercionKind co1 - (a2, r2) = coercionKind co2 - - _err_stuff = vcat [ text "co1:" <+> ppr co1 - , text "co1 kind left:" <+> ppr a1 - , text "co1 kind right:" <+> ppr r1 - , text "co2:" <+> ppr co2 - , text "co2 kind left:" <+> ppr a2 - , text "co2 kind right:" <+> ppr r2 ] - ---------------------------------------------------- -leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 (fst . decompLR) -rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR) - -decompLR :: [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... --- --- if c :: t1 s1 ~ t2 s2 then splitCoercionKindOf c = ((t1, t2), (s1, s2)) -decompLR (co : rest) - | (ty1, ty2) <- coercionKind co - , Just (ty_fun1, ty_arg1) <- splitAppTy_maybe ty1 - , Just (ty_fun2, ty_arg2) <- splitAppTy_maybe ty2 - = ASSERT( null rest) - ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2)) -decompLR cos - = pprPanic "Coercion.decompLR" - (ppr cos $$ vcat (map (pprEqPred .coercionKind) cos)) - ---------------------------------------------------- -instCoercionTyCon - = mkCoercionTyCon instCoercionTyConName 2 instCoercionKind +------------------------------------------------------- +-- 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) - ---------------------------------------------------- --- The csel* family --- If co :: (s1~t1 => r1) ~ (s2~t2 => r2) --- Then csel1 co :: s1 ~ s2 --- csel2 co :: t1 ~ t2 --- cselR co :: r1 ~ r2 - -csel1CoercionTyCon = mkCoercionTyCon csel1CoercionTyConName 1 (fstOf3 . decompCsel) -csel2CoercionTyCon = mkCoercionTyCon csel2CoercionTyConName 1 (sndOf3 . decompCsel) -cselRCoercionTyCon = mkCoercionTyCon cselRCoercionTyConName 1 (thirdOf3 . decompCsel) - -decompCsel :: [Coercion] -> ((Type,Type), (Type,Type), (Type,Type)) -decompCsel (co : rest) - | (ty1,ty2) <- coercionKind co - , Just (cv1, r1) <- splitForAllTy_maybe ty1 - , Just (cv2, r2) <- splitForAllTy_maybe ty2 - , (s1,t1) <- ASSERT( isCoVar cv1) coVarKind cv1 - , (s2,t2) <- ASSERT( isCoVar cv1) coVarKind cv2 - = ASSERT( null rest ) - ((s1,s2), (t1,t2), (r1,r2)) -decompCsel other = pprPanic "decompCsel" (ppr other) - -fstOf3 :: (a,b,c) -> a -sndOf3 :: (a,b,c) -> b -thirdOf3 :: (a,b,c) -> c -fstOf3 (a,_,_) = a -sndOf3 (_,b,_) = b -thirdOf3 (_,_,c) = c - --------------------------------------- --- Their Names - -transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, - rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName, - csel1CoercionTyConName, csel2CoercionTyConName, cselRCoercionTyConName :: Name - -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 -csel1CoercionTyConName = mkCoConName (fsLit "csel1") csel1CoercionTyConKey csel1CoercionTyCon -csel2CoercionTyConName = mkCoConName (fsLit "csel2") csel2CoercionTyConKey csel2CoercionTyCon -cselRCoercionTyConName = mkCoConName (fsLit "cselR") cselRCoercionTyConKey cselRCoercionTyCon -unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon - -mkCoConName :: FastString -> Unique -> TyCon -> Name -mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ) - key (ATyCon coCon) BuiltInSyntax -\end{code} + 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. +-- | 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 + +-- | 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 + + | 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 + +------------------------------- + +-- | 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} %************************************************************************ %* * @@ -621,17 +662,14 @@ mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkTcOccFS occ) %************************************************************************ \begin{code} -instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI) +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 @@ -648,223 +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 -\end{code} +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} %************************************************************************ %* * - CoercionI and its constructors -%* * + Substitution of coercions +%* * %************************************************************************ --------------------------------------- --- CoercionI smart constructors --- lifted smart constructors of ordinary coercions - \begin{code} --- | 'CoercionI' represents a /lifted/ ordinary 'Coercion', in that it --- can represent either one of: --- --- 1. A proper 'Coercion' --- --- 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: --- --- > 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) +-- | 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 + +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} %************************************************************************ -%* * - Optimising coercions +%* * + "Lifting" substitution + [(TyVar,Coercion)] -> Type -> Coercion %* * %************************************************************************ \begin{code} -optCoercion :: Coercion -> Coercion -optCoercion co - = ASSERT2( coercionKind co `eq` coercionKind result, - ppr co $$ ppr result $$ ppr (coercionKind co) $$ ppr (coercionKind result) ) - result +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. +-- +-- 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 - (s1,t1) `eq` (s2,t2) = s1 `coreEqType` s2 && t1 `coreEqType` t2 - - (result,_,_) = go co - -- optimized, changed?, identity? - go :: Coercion -> ( Coercion, Bool, Bool ) - -- traverse coercion term bottom up and return - -- - -- 1) equivalent coercion, in optimized form - -- - -- 2) whether the output coercion differs from - -- the input coercion - -- - -- 3) whether the coercion is an identity coercion - -- - -- Performs the following optimizations: - -- - -- sym id >-> id - -- trans id co >-> co - -- trans co id >-> co - -- - go ty@(TyVarTy a) | isCoVar a = let (ty1,ty2) = coercionKind ty - in (ty, False, ty1 `coreEqType` ty2) - | otherwise = (ty, False, True) - go ty@(AppTy ty1 ty2) - = let (ty1', chan1, id1) = go ty1 - (ty2', chan2, id2) = go ty2 - in if chan1 || chan2 - then (AppTy ty1' ty2', True, id1 && id2) - else (ty , False, id1 && id2) - go ty@(TyConApp tc args) - | tc == symCoercionTyCon, [ty1] <- args - = case go ty1 of - (ty1', _ , True) -> (ty1', True, True) - (ty1', True, _ ) -> (TyConApp tc [ty1'], True, False) - (_ , _ , _ ) -> (ty, False, False) - | tc == transCoercionTyCon, [ty1,ty2] <- args - = let (ty1', chan1, id1) = go ty1 - (ty2', chan2, id2) = go ty2 - in if id1 - then (ty2', True, id2) - else if id2 - then (ty1', True, False) - else if chan1 || chan2 - then (TyConApp tc [ty1',ty2'], True , False) - else (ty , False, False) - | tc == leftCoercionTyCon, [ty1] <- args - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (TyConApp tc [ty1'], True , id1) - else (ty , False, id1) - | tc == rightCoercionTyCon, [ty1] <- args - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (TyConApp tc [ty1'], True , id1) - else (ty , False, id1) - | not (isCoercionTyCon tc) - = let (args', chans, ids) = mapAndUnzip3 go args - in if or chans - then (TyConApp tc args', True , and ids) - else (ty , False, and ids) - | otherwise - = (ty, False, False) - go ty@(FunTy ty1 ty2) - = let (ty1',chan1,id1) = go ty1 - (ty2',chan2,id2) = go ty2 - in if chan1 || chan2 - then (FunTy ty1' ty2', True , id1 && id2) - else (ty , False, id1 && id2) - go ty@(ForAllTy tv ty1) - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (ForAllTy tv ty1', True , id1) - else (ty , False, id1) - go ty@(PredTy (EqPred ty1 ty2)) - = let (ty1', chan1, id1) = go ty1 - (ty2', chan2, id2) = go ty2 - in if chan1 || chan2 - then (PredTy (EqPred ty1' ty2'), True , id1 && id2) - else (ty , False, id1 && id2) - go ty@(PredTy (ClassP cl args)) - = let (args', chans, ids) = mapAndUnzip3 go args - in if or chans - then (PredTy (ClassP cl args'), True , and ids) - else (ty , False, and ids) - go ty@(PredTy (IParam name ty1)) - = let (ty1', chan1, id1) = go ty1 - in if chan1 - then (PredTy (IParam name ty1'), True , id1) - else (ty , False, id1) + 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 +-- +-- > c :: (t1 ~ t2) +-- +-- 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