-%
+T%
% (c) The University of Glasgow 2006
%
-- * Main data type
Coercion,
- mkCoKind, mkReflCoKind, splitCoercionKind_maybe, splitCoercionKind,
- coercionKind, coercionKinds, coercionKindPredTy,
+ mkCoKind, mkReflCoKind, coVarKind,
+ coercionKind, coercionKinds, isIdentityCoercion,
-- ** Equality predicates
isEqPred, mkEqPred, getEqPredTys, isEqPredTy,
mkCoercion,
mkSymCoercion, mkTransCoercion,
mkLeftCoercion, mkRightCoercion, mkRightCoercions,
- mkInstCoercion, mkAppCoercion,
- mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
+ mkInstCoercion, mkAppCoercion, mkTyConCoercion, mkFunCoercion,
+ mkForAllCoercion, mkInstsCoercion, mkUnsafeCoercion,
mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion,
+ mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion,
splitNewTypeRepCo_maybe, instNewTyCon_maybe, decomposeCo,
unsafeCoercionTyCon, symCoercionTyCon,
transCoercionTyCon, leftCoercionTyCon,
rightCoercionTyCon, instCoercionTyCon, -- needed by TysWiredIn
+ csel1CoercionTyCon, csel2CoercionTyCon, cselRCoercionTyCon,
+
+ -- ** Optimisation
+ optCoercion,
-- ** Comparison
coreEqCoercion,
-- * CoercionI
CoercionI(..),
- isIdentityCoercion,
+ isIdentityCoI,
mkSymCoI, mkTransCoI,
mkTyConAppCoI, mkAppTyCoI, mkFunTyCoI,
mkForAllTyCoI,
import Class
import Var
import Name
-import OccName
import PrelNames
import Util
-import Unique
import BasicTypes
import Outputable
import FastString
-------------------------------------------------------
-- and some coercion kind stuff
+coVarKind :: CoVar -> (Type,Type)
+-- c :: t1 ~ t2
+coVarKind cv = splitCoVarKind (tyVarKind cv)
+
+-- | 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)
+
+-- | 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)
+
+-- | (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
+
-- | Tests whether a type is just a type equality predicate
isEqPredTy :: Type -> Bool
isEqPredTy (PredTy pred) = isEqPred pred
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
-
-- | 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)
+coercionKind ty@(TyVarTy a) | isCoVar a = coVarKind a
| otherwise = (ty, ty)
coercionKind (AppTy ty1 ty2)
= let (t1, t2) = coercionKind ty1
= let (t1, t2) = coercionKind ty1
(s1, s2) = coercionKind ty2 in
(mkFunTy t1 s1, mkFunTy t2 s2)
-coercionKind (ForAllTy tv ty)
+
+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)
+
+ | 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))
- = let k1 = coercionKindPredTy c1
+ = 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
+
+
+
coercionKind (PredTy (ClassP cl args))
= let (lArgs, rArgs) = coercionKinds args in
(PredTy (ClassP cl lArgs), PredTy (ClassP cl rArgs))
= 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
-
-- | Apply 'coercionKind' to multiple 'Coercion's
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKinds tys = unzip $ map coercionKind tys
-------------------------------------
--- Coercion kind and type mk's
--- (make saturated TyConApp CoercionTyCon{...} args)
+isIdentityCoercion :: Coercion -> Bool
+isIdentityCoercion co
+ = case coercionKind co of
+ (t1,t2) -> t1 `coreEqType` t2
+\end{code}
+%************************************************************************
+%* *
+ Building coercions
+%* *
+%************************************************************************
+
+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 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
+-- | 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
+mkAppCoercion co1 co2 = mkAppTy co1 co2
-- | 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
+mkAppsCoercion co1 tys = foldl mkAppTy co1 tys
+
+-- | Apply a type constructor to a list of coercions.
+mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
+mkTyConCoercion con cos = mkTyConApp con cos
+
+-- | Make a function 'Coercion' between two other 'Coercion's
+mkFunCoercion :: Coercion -> Coercion -> Coercion
+mkFunCoercion co1 co2 = mkFunTy co1 co2
-- | 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
--- | Make a function 'Coercion' between two other 'Coercion's
-mkFunCoercion :: Coercion -> Coercion -> Coercion
-mkFunCoercion co1 co2 = mkFunTy co1 co2
-
-------------------------------
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@.
+-- ^ 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@.
+-- 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'
= acc
+mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion :: Coercion -> Coercion
+mkCsel1Coercion co = mkCoercion csel1CoercionTyCon [co]
+mkCsel2Coercion co = mkCoercion csel2CoercionTyCon [co]
+mkCselRCoercion co = mkCoercion cselRCoercionTyCon [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.
rule args = (substTyWith tvs args $ -- with sigma = [tys/tvs],
TyConApp family instTys, -- sigma (F ts)
TyConApp rep_tycon args) -- ~ R tys
+\end{code}
---------------------------------------
--- 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
+
+%************************************************************************
+%* *
+ 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)
+
+\begin{code}
+-- | Coercion type constructors: avoid using these directly and instead use
+-- the @mk*Coercion@ and @split*Coercion@ family of functions if possible.
+--
-- 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
where
composeCoercionKindsOf (co1:co2:rest)
= ASSERT( null rest )
- WARN( not (r1 `coreEqType` a2),
+ WARN( not (r1 `coreEqType` a2),
text "Strange! Type mismatch in trans coercion, probably a bug"
$$
- ppr r1 <+> text "=/=" <+> ppr a2)
+ _err_stuff )
(a1, r2)
where
(a1, r1) = coercionKind co1
(a2, r2) = coercionKind co2
-leftCoercionTyCon =
- mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf
- where
- leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
- where
- (ty1,ty2) = fst (splitCoercionKindOf co)
+ _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 ]
-rightCoercionTyCon =
- mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf
- where
- rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)
- where
- (ty1,ty2) = snd (splitCoercionKindOf co)
+---------------------------------------------------
+leftCoercionTyCon = mkCoercionTyCon leftCoercionTyConName 1 (fst . decompLR)
+rightCoercionTyCon = mkCoercionTyCon rightCoercionTyConName 1 (snd . decompLR)
-splitCoercionKindOf :: Type -> ((Type,Type), (Type,Type))
+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))
-splitCoercionKindOf co
- | Just (ty1, ty2) <- splitCoercionKind_maybe (coercionKindPredTy co)
+decompLR (co : rest)
+ | (ty1, ty2) <- coercionKind 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))
+ = 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
where
(instantiateCo t1 ty, instantiateCo t2 ty)
where (t1, t2) = coercionKind co1
+---------------------------------------------------
unsafeCoercionTyCon
= mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind
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
+
--------------------------------------
--- ...and their names
+-- 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
-
-transCoercionTyConName, symCoercionTyConName, leftCoercionTyConName, rightCoercionTyConName, instCoercionTyConName, unsafeCoercionTyConName :: 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
-unsafeCoercionTyConName = mkCoConName (fsLit "CoUnsafe") unsafeCoercionTyConKey unsafeCoercionTyCon
+\end{code}
+%************************************************************************
+%* *
+ Newtypes
+%* *
+%************************************************************************
+\begin{code}
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
-- ^ If @co :: T ts ~ rep_ty@ then:
--
\end{code}
+%************************************************************************
+%* *
+ CoercionI and its constructors
+%* *
+%************************************************************************
+
--------------------------------------
-- CoercionI smart constructors
-- lifted smart constructors of ordinary coercions
ppr IdCo = ptext (sLit "IdCo")
ppr (ACo co) = ppr co
-isIdentityCoercion :: CoercionI -> Bool
-isIdentityCoercion IdCo = True
-isIdentityCoercion _ = False
+isIdentityCoI :: CoercionI -> Bool
+isIdentityCoI IdCo = True
+isIdentityCoI _ = False
-- | Tests whether all the given 'CoercionI's represent the identity coercion
-allIdCos :: [CoercionI] -> Bool
-allIdCos = all isIdentityCoercion
+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
-- | Smart constructor for type constructor application on 'CoercionI', see also 'mkAppCoercion'
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
mkTyConAppCoI tyCon tys cois
- | allIdCos cois = IdCo
- | otherwise = ACo (TyConApp tyCon (zipCoArgs cois tys))
+ | 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
-- > mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
mkClassPPredCoI cls tys cois
- | allIdCos cois = IdCo
- | otherwise = ACo $ PredTy $ ClassP cls (zipCoArgs cois tys)
+ | 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
mkEqPredCoI ty1 IdCo _ (ACo co2) = ACo $ PredTy $ EqPred ty1 co2
mkEqPredCoI _ (ACo co1) ty2 coi2 = ACo $ PredTy $ EqPred co1 (fromCoI coi2 ty2)
\end{code}
+
+%************************************************************************
+%* *
+ Optimising coercions
+%* *
+%************************************************************************
+
+\begin{code}
+optCoercion :: Coercion -> Coercion
+optCoercion co
+ = ASSERT2( coercionKind co `eq` coercionKind result,
+ ppr co $$ ppr result $$ ppr (coercionKind co) $$ ppr (coercionKind result) )
+ result
+ 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
+ -- sym (sym co) >-> co
+ -- trans g (sym g) >-> id
+ -- trans (sym g) g >-> id
+ --
+ 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:tys) <- args
+ = goSym ty ty1 tys
+ | tc == transCoercionTyCon, [ty1,ty2] <- args
+ = goTrans ty ty1 ty2
+ | tc == leftCoercionTyCon, [ty1] <- args
+ = goLeft ty ty1
+ | tc == rightCoercionTyCon, [ty1] <- args
+ = goRight ty ty1
+ | tc == instCoercionTyCon, [ty1,ty2] <- args
+ = goInst ty ty1 ty2
+ | 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)
+
+ goSym :: Coercion -> Coercion -> [Coercion] -> ( Coercion, Bool, Bool )
+ --
+ -- pushes the sym constructor inwards, if possible
+ --
+ -- takes original coercion term
+ -- first argument
+ -- rest of arguments
+ goSym ty ty1 tys
+ = case mkSymCoercion ty1 of
+ (TyConApp tc _ ) | tc == symCoercionTyCon
+ -> let (tys',chans',ids) = mapAndUnzip3 go (ty1:tys)
+ in if or chans'
+ then (TyConApp symCoercionTyCon tys', True , and ids)
+ else (ty , False, and ids)
+ ty1' -> let (ty',_ ,id') = go (mkAppsCoercion ty1' tys)
+ in (ty',True,id')
+
+
+ goRight :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
+ --
+ -- reduces the right constructor, if possible
+ --
+ -- takes original coercion term
+ -- argument
+ --
+ goRight ty ty1
+ = case mkRightCoercion ty1 of
+ (TyConApp tc _ ) | tc == rightCoercionTyCon
+ -> let (ty1',chan1,id1) = go ty1
+ in if chan1
+ then (TyConApp rightCoercionTyCon [ty1'], True , id1)
+ else (ty , False, id1)
+ ty1' -> let (ty',_ ,id') = go ty1'
+ in (ty',True,id')
+
+ goLeft :: Coercion -> Coercion -> ( Coercion, Bool, Bool )
+ --
+ -- reduces the left constructor, if possible
+ --
+ -- takes original coercion term
+ -- argument
+ --
+ goLeft ty ty1
+ = case mkLeftCoercion ty1 of
+ (TyConApp tc _ ) | tc == leftCoercionTyCon
+ -> let (ty1',chan1,id1) = go ty1
+ in if chan1
+ then (TyConApp leftCoercionTyCon [ty1'], True , id1)
+ else (ty , False, id1)
+ ty1' -> let (ty',_ ,id') = go ty1'
+ in (ty',True,id')
+
+ goInst :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
+ --
+ -- reduces the inst constructor, if possible
+ --
+ -- takes original coercion term
+ -- coercion argument
+ -- type argument
+ --
+ goInst ty ty1 ty2
+ = case mkInstCoercion ty1 ty2 of
+ (TyConApp tc _ ) | tc == instCoercionTyCon
+ -> let (ty1',chan1,id1) = go ty1
+ in if chan1
+ then (TyConApp instCoercionTyCon [ty1',ty2], True , id1)
+ else (ty , False, id1)
+ ty1' -> let (ty',_ ,id') = go ty1'
+ in (ty',True,id')
+
+ goTrans :: Coercion -> Coercion -> Coercion -> ( Coercion, Bool, Bool )
+ --
+ -- trans id co >-> co
+ -- trans co id >-> co
+ -- trans g (sym g) >-> id
+ -- trans (sym g) g >-> id
+ --
+ goTrans ty ty1 ty2
+ | id1
+ = (ty2', True, id2)
+ | id2
+ = (ty1', True, False)
+ | chan1 || chan2
+ = (TyConApp transCoercionTyCon [ty1',ty2'], True , False)
+ | Just ty' <- mty'
+ = (ty', True, True)
+ | otherwise
+ = (ty, False, False)
+ where (ty1', chan1, id1) = go ty1
+ (ty2', chan2, id2) = go ty2
+ mty' = case mkTransCoercion ty1' ty2'
+ of (TyConApp tc _) | tc == transCoercionTyCon
+ -> Nothing
+ ty' -> Just ty'
+\end{code}