+\begin{code}
+-- | A substitution of 'Coercion's for 'CoVar's (OR 'TyVar's, when
+-- doing a \"lifting\" substitution)
+type CvSubstEnv = VarEnv Coercion
+
+emptyCvSubstEnv :: CvSubstEnv
+emptyCvSubstEnv = emptyVarEnv
+
+data CvSubst
+ = CvSubst InScopeSet -- The in-scope type variables
+ TvSubstEnv -- Substitution of types
+ CvSubstEnv -- Substitution of coercions
+
+instance Outputable CvSubst where
+ ppr (CvSubst ins tenv cenv)
+ = brackets $ sep[ ptext (sLit "CvSubst"),
+ nest 2 (ptext (sLit "In scope:") <+> ppr ins),
+ nest 2 (ptext (sLit "Type env:") <+> ppr tenv),
+ nest 2 (ptext (sLit "Coercion env:") <+> ppr cenv) ]
+
+emptyCvSubst :: CvSubst
+emptyCvSubst = CvSubst emptyInScopeSet emptyVarEnv emptyVarEnv
+
+isEmptyCvSubst :: CvSubst -> Bool
+isEmptyCvSubst (CvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
+
+getCvInScope :: CvSubst -> InScopeSet
+getCvInScope (CvSubst in_scope _ _) = in_scope
+
+zapCvSubstEnv :: CvSubst -> CvSubst
+zapCvSubstEnv (CvSubst in_scope _ _) = CvSubst in_scope emptyVarEnv emptyVarEnv
+
+cvTvSubst :: CvSubst -> TvSubst
+cvTvSubst (CvSubst in_scope tvs _) = TvSubst in_scope tvs
+
+tvCvSubst :: TvSubst -> CvSubst
+tvCvSubst (TvSubst in_scope tenv) = CvSubst in_scope tenv emptyCvSubstEnv
+
+extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
+extendTvSubst (CvSubst in_scope tenv cenv) tv ty
+ = CvSubst in_scope (extendVarEnv tenv tv ty) cenv
+
+substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
+substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var
+ = ASSERT( isCoVar old_var )
+ (CvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
+ where
+ -- When we substitute (co :: t1 ~ t2) we may get the identity (co :: t ~ t)
+ -- In that case, mkCoVarCo will return a ReflCoercion, and
+ -- we want to substitute that (not new_var) for old_var
+ new_co = mkCoVarCo new_var
+ no_change = new_var == old_var && not (isReflCo new_co)
+
+ new_cenv | no_change = delVarEnv cenv old_var
+ | otherwise = extendVarEnv cenv old_var new_co
+
+ new_var = uniqAway in_scope subst_old_var
+ subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var))
+ -- It's important to do the substitution for coercions,
+ -- because only they can have free type variables
+
+substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
+substTyVarBndr (CvSubst in_scope tenv cenv) old_var
+ = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of
+ (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var)
+
+zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
+zipOpenCvSubst vs cos
+ | debugIsOn && (length vs /= length cos)
+ = pprTrace "zipOpenCvSubst" (ppr vs $$ ppr cos) emptyCvSubst
+ | otherwise
+ = CvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv (zipVarEnv vs cos)
+
+mkTopCvSubst :: [(Var,Coercion)] -> CvSubst
+mkTopCvSubst prs = CvSubst emptyInScopeSet emptyTvSubstEnv (mkVarEnv prs)
+
+substCoWithTy :: TyVar -> Type -> Coercion -> Coercion
+substCoWithTy tv ty = substCoWithTys [tv] [ty]
+
+substCoWithTys :: [TyVar] -> [Type] -> Coercion -> Coercion
+substCoWithTys tvs tys co
+ | debugIsOn && (length tvs /= length tys)
+ = pprTrace "substCoWithTys" (ppr tvs $$ ppr tys) co
+ | otherwise
+ = ASSERT( length tvs == length tys )
+ substCo (CvSubst in_scope (zipVarEnv tvs tys) emptyVarEnv) co
+ where
+ in_scope = mkInScopeSet (tyVarsOfTypes tys)
+
+-- | Substitute within a 'Coercion'
+substCo :: CvSubst -> Coercion -> Coercion
+substCo subst co | isEmptyCvSubst subst = co
+ | otherwise = subst_co subst co
+
+-- | Substitute within several 'Coercion's
+substCos :: CvSubst -> [Coercion] -> [Coercion]
+substCos subst cos | isEmptyCvSubst subst = cos
+ | otherwise = map (substCo subst) cos
+
+substTy :: CvSubst -> Type -> Type
+substTy subst = Type.substTy (cvTvSubst subst)
+
+subst_co :: CvSubst -> Coercion -> Coercion
+subst_co subst co
+ = go co
+ where
+ go_ty :: Type -> Type
+ go_ty = Coercion.substTy subst
+
+ go :: Coercion -> Coercion
+ go (Refl ty) = Refl $! go_ty ty
+ go (TyConAppCo tc cos) = let args = map go cos
+ in args `seqList` TyConAppCo tc args
+ go (AppCo co1 co2) = mkAppCo (go co1) $! go co2
+ go (ForAllCo tv co) = case substTyVarBndr subst tv of
+ (subst', tv') ->
+ ForAllCo tv' $! subst_co subst' co
+ go (CoVarCo cv) = substCoVar subst cv
+ go (AxiomInstCo con cos) = AxiomInstCo con $! map go cos
+ go (UnsafeCo ty1 ty2) = (UnsafeCo $! go_ty ty1) $! go_ty ty2
+ go (SymCo co) = mkSymCo (go co)
+ go (TransCo co1 co2) = mkTransCo (go co1) (go co2)
+ go (NthCo d co) = mkNthCo d (go co)
+ go (InstCo co ty) = mkInstCo (go co) $! go_ty ty
+
+substCoVar :: CvSubst -> CoVar -> Coercion
+substCoVar (CvSubst in_scope _ cenv) cv
+ | Just co <- lookupVarEnv cenv cv = co
+ | Just cv1 <- lookupInScope in_scope cv = ASSERT( isCoVar cv1 ) CoVarCo cv1
+ | otherwise = WARN( True, ptext (sLit "substCoVar not in scope") <+> ppr cv )
+ ASSERT( isCoVar cv ) CoVarCo cv
+
+substCoVars :: CvSubst -> [CoVar] -> [Coercion]
+substCoVars subst cvs = map (substCoVar subst) cvs
+
+lookupTyVar :: CvSubst -> TyVar -> Maybe Type
+lookupTyVar (CvSubst _ tenv _) tv = lookupVarEnv tenv tv
+
+lookupCoVar :: CvSubst -> Var -> Maybe Coercion
+lookupCoVar (CvSubst _ _ cenv) v = lookupVarEnv cenv v
+\end{code}
+
+%************************************************************************
+%* *
+ "Lifting" substitution
+ [(TyVar,Coercion)] -> Type -> Coercion
+%* *
+%************************************************************************