+
+
+%************************************************************************
+%* *
+ 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)
+
+
+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
+fromACo (IdCo {}) = panic "fromACo"
+
+-- | 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}
+type NormalCo = Coercion
+ -- Invariants:
+ -- * For trans coercions (co1 `trans` co2)
+ -- co1 is not a trans, and neither co1 nor co2 is identity
+ -- * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
+
+type NormalNonIdCo = NormalCo -- Extra invariant: not the identity
+
+optCoercion :: Coercion -> NormalCo
+optCoercion co = opt_co False co
+
+opt_co :: Bool -- True <=> return (sym co)
+ -> Coercion
+ -> NormalCo
+opt_co = opt_co'
+-- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
+-- co1 `seq`
+-- pprTrace "opt_co done }" (ppr co1)
+-- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1)
+-- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
+-- co1
+-- where
+-- co1 = opt_co' sym co
+-- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
+-- (s,t) = coercionKind co
+-- (s1,t1) | sym = (t,s)
+-- | otherwise = (s,t)
+-- (s2,t2) = coercionKind co1
+
+opt_co' sym (AppTy ty1 ty2) = mkAppTy (opt_co sym ty1) (opt_co sym ty2)
+opt_co' sym (FunTy ty1 ty2) = FunTy (opt_co sym ty1) (opt_co sym ty2)
+opt_co' sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co sym) tys))
+opt_co' sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co sym ty))
+
+opt_co' sym co@(TyVarTy tv)
+ | not (isCoVar tv) = co -- Identity; does not mention a CoVar
+ | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..
+ | not sym = co
+ | otherwise = mkSymCoercion co
+ where
+ (ty1,ty2) = coVarKind tv
+
+opt_co' sym (ForAllTy tv cor)
+ | isCoVar tv = mkCoPredTy (opt_co sym co1) (opt_co sym co2) (opt_co sym cor)
+ | otherwise = ForAllTy tv (opt_co sym cor)
+ where
+ (co1,co2) = coVarKind tv
+
+opt_co' sym (TyConApp tc cos)
+ | isCoercionTyCon tc
+ = foldl mkAppTy opt_co_tc
+ (map (opt_co sym) (drop arity cos))
+ | otherwise
+ = TyConApp tc (map (opt_co sym) cos)
+ where
+ arity = tyConArity tc
+ opt_co_tc :: NormalCo
+ opt_co_tc = opt_co_tc_app sym tc (take arity cos)
+
+--------
+opt_co_tc_app :: Bool -> TyCon -> [Type] -> NormalCo
+-- Used for CoercionTyCons only
+opt_co_tc_app sym tc cos
+ | tc `hasKey` symCoercionTyConKey
+ = opt_co (not sym) co1
+
+ | tc `hasKey` transCoercionTyConKey
+ = if sym then opt_trans opt_co2 opt_co1
+ else opt_trans opt_co1 opt_co2
+
+ | tc `hasKey` leftCoercionTyConKey
+ , Just (co1, _) <- splitAppTy_maybe opt_co1
+ = co1
+
+ | tc `hasKey` rightCoercionTyConKey
+ , Just (_, co2) <- splitAppTy_maybe opt_co1
+ = co2
+
+ | tc `hasKey` csel1CoercionTyConKey
+ , Just (s1,_,_) <- splitCoPredTy_maybe opt_co1
+ = s1
+
+ | tc `hasKey` csel2CoercionTyConKey
+ , Just (_,s2,_) <- splitCoPredTy_maybe opt_co1
+ = s2
+
+ | tc `hasKey` cselRCoercionTyConKey
+ , Just (_,_,r) <- splitCoPredTy_maybe opt_co1
+ = r
+
+ | tc `hasKey` instCoercionTyConKey
+ , Just (tv, co'') <- splitForAllTy_maybe opt_co1
+ , let ty = co2
+ = substTyWith [tv] [ty] co''
+
+ | otherwise -- Do not push sym inside top-level axioms
+ -- e.g. if g is a top-level axiom
+ -- g a : F a ~ a
+ -- Then (sym (g ty)) /= g (sym ty) !!
+ = if sym then mkSymCoercion the_co
+ else the_co
+ where
+ the_co = TyConApp tc cos
+ (co1 : cos1) = cos
+ (co2 : _) = cos1
+ opt_co1 = opt_co sym co1
+ opt_co2 = opt_co sym co2
+
+-------------
+opt_trans :: NormalCo -> NormalCo -> NormalCo
+opt_trans co1 co2
+ | isIdNormCo co1 = co2
+ | otherwise = opt_trans1 co1 co2
+
+opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo
+-- First arg is not the identity
+opt_trans1 co1 co2
+ | isIdNormCo co2 = co1
+ | otherwise = opt_trans2 co1 co2
+
+opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo
+-- Neither arg is the identity
+opt_trans2 (TyConApp tc [co1a,co1b]) co2
+ | tc `hasKey` transCoercionTyConKey
+ = opt_trans1 co1a (opt_trans2 co1b co2)
+
+opt_trans2 co1 co2
+ | Just co <- opt_trans_rule co1 co2
+ = co
+
+opt_trans2 co1 (TyConApp tc [co2a,co2b])
+ | tc `hasKey` transCoercionTyConKey
+ , Just co1_2a <- opt_trans_rule co1 co2a
+ = if isIdNormCo co1_2a
+ then co2b
+ else opt_trans2 co1_2a co2b
+
+opt_trans2 co1 co2
+ = mkTransCoercion co1 co2
+
+------
+opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
+opt_trans_rule (TyConApp tc [co1]) co2
+ | tc `hasKey` symCoercionTyConKey
+ , co1 `coreEqType` co2
+ , (_,ty2) <- coercionKind co2
+ = Just ty2
+
+opt_trans_rule co1 (TyConApp tc [co2])
+ | tc `hasKey` symCoercionTyConKey
+ , co1 `coreEqType` co2
+ , (ty1,_) <- coercionKind co1
+ = Just ty1
+
+opt_trans_rule (TyConApp tc1 [co1,ty1]) (TyConApp tc2 [co2,ty2])
+ | tc1 `hasKey` instCoercionTyConKey
+ , tc1 == tc2
+ , ty1 `coreEqType` ty2
+ = Just (mkInstCoercion (opt_trans2 co1 co2) ty1)
+
+opt_trans_rule (TyConApp tc1 cos1) (TyConApp tc2 cos2)
+ | not (isCoercionTyCon tc1) ||
+ getUnique tc1 `elem` [ leftCoercionTyConKey, rightCoercionTyConKey
+ , csel1CoercionTyConKey, csel2CoercionTyConKey
+ , cselRCoercionTyConKey ] --Yuk!
+ , tc1 == tc2 -- Works for left,right, and csel* family
+ -- BUT NOT equality axioms
+ -- E.g. (g Int) `trans` (g Bool)
+ -- /= g (Int . Bool)
+ = Just (TyConApp tc1 (zipWith opt_trans cos1 cos2))
+
+opt_trans_rule co1 co2
+ | Just (co1a, co1b) <- splitAppTy_maybe co1
+ , Just (co2a, co2b) <- splitAppTy_maybe co2
+ = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
+
+ | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
+ , Just (s2,t2,r2) <- splitCoPredTy_maybe co1
+ = Just (mkCoPredTy (opt_trans s1 s2)
+ (opt_trans t1 t2)
+ (opt_trans r1 r2))
+
+ | Just (tv1,r1) <- splitForAllTy_maybe co1
+ , Just (tv2,r2) <- splitForAllTy_maybe co2
+ , not (isCoVar tv1) -- Both have same kind
+ , let r2' = substTyWith [tv2] [TyVarTy tv1] r2
+ = Just (ForAllTy tv1 (opt_trans2 r1 r2'))
+
+opt_trans_rule _ _ = Nothing
+
+
+-------------
+isIdNormCo :: NormalCo -> Bool
+-- Cheap identity test: look for coercions with no coercion variables at all
+-- So it'll return False for (sym g `trans` g)
+isIdNormCo ty = go ty
+ where
+ go (TyVarTy tv) = not (isCoVar tv)
+ go (AppTy t1 t2) = go t1 && go t2
+ go (FunTy t1 t2) = go t1 && go t2
+ go (ForAllTy tv ty) = go (tyVarKind tv) && go ty
+ go (TyConApp tc tys) = not (isCoercionTyCon tc) && all go tys
+ go (PredTy (IParam _ ty)) = go ty
+ go (PredTy (ClassP _ tys)) = all go tys
+ go (PredTy (EqPred t1 t2)) = go t1 && go t2
+\end{code}