+\begin{code}
+-- | A 'Coercion' is concrete evidence of the equality/convertibility
+-- of two types.
+
+data Coercion
+ -- These ones mirror the shape of types
+ = Refl Type -- See Note [Refl invariant]
+ -- Invariant: applications of (Refl T) to a bunch of identity coercions
+ -- always show up as Refl.
+ -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
+
+ -- Applications of (Refl T) to some coercions, at least one of
+ -- which is NOT the identity, show up as TyConAppCo.
+ -- (They may not be fully saturated however.)
+ -- ConAppCo coercions (like all coercions other than Refl)
+ -- are NEVER the identity.
+
+ -- These ones simply lift the correspondingly-named
+ -- Type constructors into Coercions
+ | TyConAppCo TyCon [Coercion] -- lift TyConApp
+ -- The TyCon is never a synonym;
+ -- we expand synonyms eagerly
+
+ | AppCo Coercion Coercion -- lift AppTy
+
+ -- See Note [Forall coercions]
+ | ForAllCo TyVar Coercion -- forall a. g
+
+ -- These are special
+ | CoVarCo CoVar
+ | AxiomInstCo CoAxiom [Coercion] -- The coercion arguments always *precisely*
+ -- saturate arity of CoAxiom.
+ -- See [Coercion axioms applied to coercions]
+ | UnsafeCo Type Type
+ | SymCo Coercion
+ | TransCo Coercion Coercion
+
+ -- These are destructors
+ | NthCo Int Coercion -- Zero-indexed
+ | InstCo Coercion Type
+ deriving (Data.Data, Data.Typeable)
+\end{code}
+
+Note [Refl invariant]
+~~~~~~~~~~~~~~~~~~~~~
+Coercions have the following invariant
+ Refl is always lifted as far as possible.
+
+You might think that a consequencs is:
+ Every identity coercions has Refl at the root
+
+But that's not quite true because of coercion variables. Consider
+ g where g :: Int~Int
+ Left h where h :: Maybe Int ~ Maybe Int
+etc. So the consequence is only true of coercions that
+have no coercion variables.
+
+Note [Coercion axioms applied to coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The reason coercion axioms can be applied to coercions and not just
+types is to allow for better optimization. There are some cases where
+we need to be able to "push transitivity inside" an axiom in order to
+expose further opportunities for optimization.
+
+For example, suppose we have
+
+ C a : t[a] ~ F a
+ g : b ~ c
+
+and we want to optimize
+
+ sym (C b) ; t[g] ; C c
+
+which has the kind
+
+ F b ~ F c
+
+(stopping through t[b] and t[c] along the way).
+
+We'd like to optimize this to just F g -- but how? The key is
+that we need to allow axioms to be instantiated by *coercions*,
+not just by types. Then we can (in certain cases) push
+transitivity inside the axiom instantiations, and then react
+opposite-polarity instantiations of the same axiom. In this
+case, e.g., we match t[g] against the LHS of (C c)'s kind, to
+obtain the substitution a |-> g (note this operation is sort
+of the dual of lifting!) and hence end up with
+
+ C g : t[b] ~ F c
+
+which indeed has the same kind as t[g] ; C c.
+
+Now we have
+
+ sym (C b) ; C g
+
+which can be optimized to F g.
+
+
+Note [Forall coercions]
+~~~~~~~~~~~~~~~~~~~~~~~
+Constructing coercions between forall-types can be a bit tricky.
+Currently, the situation is as follows:
+
+ ForAllCo TyVar Coercion
+
+represents a coercion between polymorphic types, with the rule
+
+ v : k g : t1 ~ t2
+ ----------------------------------------------
+ ForAllCo v g : (all v:k . t1) ~ (all v:k . t2)
+
+Note that it's only necessary to coerce between polymorphic types
+where the type variables have identical kinds, because equality on
+kinds is trivial.
+
+Note [Predicate coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+ g :: a~b
+How can we coerce between types
+ ([c]~a) => [a] -> c
+and
+ ([c]~b) => [b] -> c
+where the equality predicate *itself* differs?
+
+Answer: we simply treat (~) as an ordinary type constructor, so these
+types really look like
+
+ ((~) [c] a) -> [a] -> c
+ ((~) [c] b) -> [b] -> c
+
+So the coercion between the two is obviously
+
+ ((~) [c] g) -> [g] -> c
+
+Another way to see this to say that we simply collapse predicates to
+their representation type (see Type.coreView and Type.predTypeRep).
+
+This collapse is done by mkPredCo; there is no PredCo constructor
+in Coercion. This is important because we need Nth to work on
+predicates too:
+ Nth 1 ((~) [c] g) = g
+See Simplify.simplCoercionF, which generates such selections.
+
+%************************************************************************
+%* *
+\subsection{Coercion variables}
+%* *
+%************************************************************************
+
+\begin{code}
+coVarName :: CoVar -> Name
+coVarName = varName
+
+setCoVarUnique :: CoVar -> Unique -> CoVar
+setCoVarUnique = setVarUnique
+
+setCoVarName :: CoVar -> Name -> CoVar
+setCoVarName = setVarName
+
+isCoVar :: Var -> Bool
+isCoVar v = isCoVarType (varType v)
+
+isCoVarType :: Type -> Bool
+isCoVarType = isEqPredTy
+\end{code}
+
+
+\begin{code}
+tyCoVarsOfCo :: Coercion -> VarSet
+-- Extracts type and coercion variables from a coercion
+tyCoVarsOfCo (Refl ty) = tyVarsOfType ty
+tyCoVarsOfCo (TyConAppCo _ cos) = tyCoVarsOfCos cos
+tyCoVarsOfCo (AppCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
+tyCoVarsOfCo (ForAllCo tv co) = tyCoVarsOfCo co `delVarSet` tv
+tyCoVarsOfCo (CoVarCo v) = unitVarSet v
+tyCoVarsOfCo (AxiomInstCo _ cos) = tyCoVarsOfCos cos
+tyCoVarsOfCo (UnsafeCo ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+tyCoVarsOfCo (SymCo co) = tyCoVarsOfCo co
+tyCoVarsOfCo (TransCo co1 co2) = tyCoVarsOfCo co1 `unionVarSet` tyCoVarsOfCo co2
+tyCoVarsOfCo (NthCo _ co) = tyCoVarsOfCo co
+tyCoVarsOfCo (InstCo co ty) = tyCoVarsOfCo co `unionVarSet` tyVarsOfType ty
+
+tyCoVarsOfCos :: [Coercion] -> VarSet
+tyCoVarsOfCos cos = foldr (unionVarSet . tyCoVarsOfCo) emptyVarSet cos
+
+coVarsOfCo :: Coercion -> VarSet
+-- Extract *coerction* variables only. Tiresome to repeat the code, but easy.
+coVarsOfCo (Refl _) = emptyVarSet
+coVarsOfCo (TyConAppCo _ cos) = coVarsOfCos cos
+coVarsOfCo (AppCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
+coVarsOfCo (ForAllCo _ co) = coVarsOfCo co
+coVarsOfCo (CoVarCo v) = unitVarSet v
+coVarsOfCo (AxiomInstCo _ cos) = coVarsOfCos cos
+coVarsOfCo (UnsafeCo _ _) = emptyVarSet
+coVarsOfCo (SymCo co) = coVarsOfCo co
+coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
+coVarsOfCo (NthCo _ co) = coVarsOfCo co
+coVarsOfCo (InstCo co _) = coVarsOfCo co
+
+coVarsOfCos :: [Coercion] -> VarSet
+coVarsOfCos cos = foldr (unionVarSet . coVarsOfCo) emptyVarSet cos
+
+coercionSize :: Coercion -> Int
+coercionSize (Refl ty) = typeSize ty
+coercionSize (TyConAppCo _ cos) = 1 + sum (map coercionSize cos)
+coercionSize (AppCo co1 co2) = coercionSize co1 + coercionSize co2
+coercionSize (ForAllCo _ co) = 1 + coercionSize co
+coercionSize (CoVarCo _) = 1
+coercionSize (AxiomInstCo _ cos) = 1 + sum (map coercionSize cos)
+coercionSize (UnsafeCo ty1 ty2) = typeSize ty1 + typeSize ty2
+coercionSize (SymCo co) = 1 + coercionSize co
+coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
+coercionSize (NthCo _ co) = 1 + coercionSize co
+coercionSize (InstCo co ty) = 1 + coercionSize co + typeSize ty
+\end{code}
+
+%************************************************************************
+%* *
+ Pretty-printing coercions
+%* *
+%************************************************************************
+
+@pprCo@ is the standard @Coercion@ printer; the overloaded @ppr@
+function is defined to use this. @pprParendCo@ is the same, except it
+puts parens around the type, except for the atomic cases.
+@pprParendCo@ works just by setting the initial context precedence
+very high.
+
+\begin{code}
+instance Outputable Coercion where
+ ppr = pprCo
+
+pprCo, pprParendCo :: Coercion -> SDoc
+pprCo co = ppr_co TopPrec co
+pprParendCo co = ppr_co TyConPrec co
+
+ppr_co :: Prec -> Coercion -> SDoc
+ppr_co _ (Refl ty) = angles (ppr ty)
+
+ppr_co p co@(TyConAppCo tc cos)
+ | tc `hasKey` funTyConKey = ppr_fun_co p co
+ | otherwise = pprTcApp p ppr_co tc cos
+
+ppr_co p (AppCo co1 co2) = maybeParen p TyConPrec $
+ pprCo co1 <+> ppr_co TyConPrec co2
+
+ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
+
+ppr_co _ (CoVarCo cv)
+ | isSymOcc (getOccName cv) = parens (ppr cv)
+ | otherwise = ppr cv
+
+ppr_co p (AxiomInstCo con cos) = pprTypeNameApp p ppr_co (getName con) cos
+
+
+ppr_co p (TransCo co1 co2) = maybeParen p FunPrec $
+ ppr_co FunPrec co1
+ <+> ptext (sLit ";")
+ <+> ppr_co FunPrec co2
+ppr_co p (InstCo co ty) = maybeParen p TyConPrec $
+ pprParendCo co <> ptext (sLit "@") <> pprType ty
+
+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]