+
+%************************************************************************
+%* *
+ CoercionI and its constructors
+%* *
+%************************************************************************
+
+--------------------------------------
+-- 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)
+\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
+ --
+ 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)