+ppr_co p (UnsafeCo ty1 ty2) = pprPrefixApp p (ptext (sLit "UnsafeCo")) [pprParendType ty1, pprParendType ty2]
+ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo co]
+ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co]
+
+
+angles :: SDoc -> SDoc
+angles p = char '<' <> p <> char '>'
+
+ppr_fun_co :: Prec -> Coercion -> SDoc
+ppr_fun_co p co = pprArrowChain p (split co)
+ where
+ split (TyConAppCo f [arg,res])
+ | f `hasKey` funTyConKey
+ = ppr_co FunPrec arg : split res
+ split co = [ppr_co TopPrec co]
+
+ppr_forall_co :: Prec -> Coercion -> SDoc
+ppr_forall_co p ty
+ = maybeParen p FunPrec $
+ sep [pprForAll tvs, ppr_co TopPrec rho]
+ where
+ (tvs, rho) = split1 [] ty
+ split1 tvs (ForAllCo tv ty) = split1 (tv:tvs) ty
+ split1 tvs ty = (reverse tvs, ty)
+\end{code}
+
+\begin{code}
+pprCoAxiom :: CoAxiom -> SDoc
+pprCoAxiom ax
+ = sep [ ptext (sLit "axiom") <+> ppr ax <+> ppr (co_ax_tvs ax)
+ , nest 2 (dcolon <+> pprEqPred (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
+\end{code}
+
+%************************************************************************
+%* *
+ Functions over Kinds
+%* *
+%************************************************************************
+
+\begin{code}
+-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
+-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
+--
+-- > decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]
+decomposeCo :: Arity -> Coercion -> [Coercion]
+decomposeCo arity co = [mkNthCo n co | n <- [0..(arity-1)] ]
+
+-- | Attempts to obtain the type variable underlying a 'Coercion'
+getCoVar_maybe :: Coercion -> Maybe CoVar
+getCoVar_maybe (CoVarCo cv) = Just cv
+getCoVar_maybe _ = Nothing
+
+-- | Attempts to tease a coercion apart into a type constructor and the application
+-- of a number of coercion arguments to that constructor
+splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
+splitTyConAppCo_maybe (Refl ty) = (fmap . second . map) Refl (splitTyConApp_maybe ty)
+splitTyConAppCo_maybe (TyConAppCo tc cos) = Just (tc, cos)
+splitTyConAppCo_maybe _ = Nothing
+
+splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
+-- ^ Attempt to take a coercion application apart.
+splitAppCo_maybe (AppCo co1 co2) = Just (co1, co2)
+splitAppCo_maybe (TyConAppCo tc cos)
+ | isDecomposableTyCon tc || cos `lengthExceeds` tyConArity tc
+ , Just (cos', co') <- snocView cos
+ = Just (mkTyConAppCo tc cos', co') -- Never create unsaturated type family apps!
+ -- Use mkTyConAppCo to preserve the invariant
+ -- that identity coercions are always represented by Refl
+splitAppCo_maybe (Refl ty)
+ | Just (ty1, ty2) <- splitAppTy_maybe ty
+ = Just (Refl ty1, Refl ty2)
+splitAppCo_maybe _ = Nothing
+
+splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
+splitForAllCo_maybe (ForAllCo tv co) = Just (tv, co)
+splitForAllCo_maybe _ = Nothing
+
+-------------------------------------------------------
+-- and some coercion kind stuff
+
+coVarPred :: CoVar -> PredType
+coVarPred cv
+ = ASSERT( isCoVar cv )
+ case splitPredTy_maybe (varType cv) of
+ Just pred -> pred
+ other -> pprPanic "coVarPred" (ppr cv $$ ppr other)
+
+coVarKind :: CoVar -> (Type,Type)
+-- c :: t1 ~ t2
+coVarKind cv = case coVarKind_maybe cv of
+ Just ts -> ts
+ Nothing -> pprPanic "coVarKind" (ppr cv $$ ppr (tyVarKind cv))
+
+coVarKind_maybe :: CoVar -> Maybe (Type,Type)
+coVarKind_maybe cv = splitEqPredTy_maybe (varType cv)
+
+-- | Makes a coercion type from two types: the types whose equality
+-- is proven by the relevant 'Coercion'
+mkCoType :: Type -> Type -> Type
+mkCoType ty1 ty2 = PredTy (EqPred ty1 ty2)
+
+splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
+splitCoPredTy_maybe ty
+ | Just (cv,r) <- splitForAllTy_maybe ty
+ , isCoVar cv
+ , Just (s,t) <- coVarKind_maybe cv
+ = Just (s,t,r)