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