+
+ 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}