+Note [Lifting substitutions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider liftCoSubstWith [a] [co] (a, forall a. a)
+Then we want to substitute for the free 'a', but obviously not for
+the bound 'a'. hence the (delVarEnv cent old_var) in liftCoSubstTyVarBndr.
+
+This also why we need a full CvSubst when doing lifting substitutions.
+
+\begin{code}
+-- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if
+-- @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@.
+-- That is, it matches a type against a coercion of the same
+-- "shape", and returns a lifting substitution which could have been
+-- used to produce the given coercion from the given type.
+liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
+liftCoMatch tmpls ty co
+ = case ty_co_match menv (emptyVarEnv, emptyVarEnv) ty co of
+ Just (tv_env, cv_env) -> Just (CvSubst in_scope tv_env cv_env)
+ Nothing -> Nothing
+ where
+ menv = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
+ in_scope = mkInScopeSet (tmpls `unionVarSet` tyCoVarsOfCo co)
+ -- Like tcMatchTy, assume all the interesting variables
+ -- in ty are in tmpls
+
+type TyCoSubstEnv = (TvSubstEnv, CvSubstEnv)
+ -- Used locally inside ty_co_match only
+
+-- | 'ty_co_match' does all the actual work for 'liftCoMatch'.
+ty_co_match :: MatchEnv -> TyCoSubstEnv -> Type -> Coercion -> Maybe TyCoSubstEnv
+ty_co_match menv subst ty co | Just ty' <- coreView ty = ty_co_match menv subst ty' co
+
+ -- Deal with the Refl case by delegating to type matching
+ty_co_match menv (tenv, cenv) ty co
+ | Just ty' <- isReflCo_maybe co
+ = case ruleMatchTyX ty_menv tenv ty ty' of
+ Just tenv' -> Just (tenv', cenv)
+ Nothing -> Nothing
+ where
+ ty_menv = menv { me_tmpls = me_tmpls menv `minusUFM` cenv }
+ -- Remove from the template set any variables already bound to non-refl coercions
+
+ -- Match a type variable against a non-refl coercion
+ty_co_match menv subst@(tenv, cenv) (TyVarTy tv1) co
+ | Just {} <- lookupVarEnv tenv tv1' -- tv1' is already bound to (Refl ty)
+ = Nothing -- The coercion 'co' is not Refl
+
+ | Just co1' <- lookupVarEnv cenv tv1' -- tv1' is already bound to co1
+ = if coreEqCoercion2 (nukeRnEnvL rn_env) co1' co
+ then Just subst
+ else Nothing -- no match since tv1 matches two different coercions
+
+ | tv1' `elemVarSet` me_tmpls menv -- tv1' is a template var
+ = if any (inRnEnvR rn_env) (varSetElems (tyCoVarsOfCo co))
+ then Nothing -- occurs check failed
+ else return (tenv, extendVarEnv cenv tv1' co)
+ -- BAY: I don't think we need to do any kind matching here yet
+ -- (compare 'match'), but we probably will when moving to SHE.
+
+ | otherwise -- tv1 is not a template ty var, so the only thing it
+ -- can match is a reflexivity coercion for itself.
+ -- But that case is dealt with already
+ = Nothing
+
+ where
+ rn_env = me_env menv
+ tv1' = rnOccL rn_env tv1
+
+ty_co_match menv subst (AppTy ty1 ty2) co
+ | Just (co1, co2) <- splitAppCo_maybe co -- c.f. Unify.match on AppTy
+ = do { subst' <- ty_co_match menv subst ty1 co1
+ ; ty_co_match menv subst' ty2 co2 }
+
+ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo tc2 cos)
+ | tc1 == tc2 = ty_co_matches menv subst tys cos
+
+ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo tc cos)
+ | tc == funTyCon = ty_co_matches menv subst [ty1,ty2] cos
+
+ty_co_match menv subst (ForAllTy tv1 ty) (ForAllCo tv2 co)
+ = ty_co_match menv' subst ty co
+ where
+ menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
+
+ty_co_match _ _ _ _ = Nothing
+
+ty_co_matches :: MatchEnv -> TyCoSubstEnv -> [Type] -> [Coercion] -> Maybe TyCoSubstEnv
+ty_co_matches menv = matchList (ty_co_match menv)
+\end{code}
+
+%************************************************************************
+%* *
+ Sequencing on coercions
+%* *
+%************************************************************************
+
+\begin{code}
+seqCo :: Coercion -> ()
+seqCo (Refl ty) = seqType ty
+seqCo (TyConAppCo tc cos) = tc `seq` seqCos cos
+seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
+seqCo (ForAllCo tv co) = tv `seq` seqCo co
+seqCo (CoVarCo cv) = cv `seq` ()
+seqCo (AxiomInstCo con cos) = con `seq` seqCos cos
+seqCo (UnsafeCo ty1 ty2) = seqType ty1 `seq` seqType ty2
+seqCo (SymCo co) = seqCo co
+seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
+seqCo (NthCo _ co) = seqCo co
+seqCo (InstCo co ty) = seqCo co `seq` seqType ty
+
+seqCos :: [Coercion] -> ()
+seqCos [] = ()
+seqCos (co:cos) = seqCo co `seq` seqCos cos
+\end{code}
+
+
+%************************************************************************
+%* *
+ The kind of a type, and of a coercion
+%* *
+%************************************************************************
+
+\begin{code}
+coercionType :: Coercion -> Type
+coercionType co = case coercionKind co of
+ Pair ty1 ty2 -> mkCoType ty1 ty2
+
+------------------
+-- | If it is the case that
+--
+-- > c :: (t1 ~ t2)
+--
+-- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@.
+coercionKind :: Coercion -> Pair Type
+coercionKind (Refl ty) = Pair ty ty
+coercionKind (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map coercionKind cos)
+coercionKind (AppCo co1 co2) = mkAppTy <$> coercionKind co1 <*> coercionKind co2
+coercionKind (ForAllCo tv co) = mkForAllTy tv <$> coercionKind co
+coercionKind (CoVarCo cv) = ASSERT( isCoVar cv ) toPair $ coVarKind cv
+coercionKind (AxiomInstCo ax cos) = let Pair tys1 tys2 = coercionKinds cos
+ in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax))
+ (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax))
+coercionKind (UnsafeCo ty1 ty2) = Pair ty1 ty2
+coercionKind (SymCo co) = swap $ coercionKind co
+coercionKind (TransCo co1 co2) = Pair (pFst $ coercionKind co1) (pSnd $ coercionKind co2)
+coercionKind (NthCo d co) = getNth d <$> coercionKind co
+coercionKind co@(InstCo aco ty) | Just ks <- splitForAllTy_maybe `traverse` coercionKind aco
+ = (\(tv, body) -> substTyWith [tv] [ty] body) <$> ks
+ | otherwise = pprPanic "coercionKind" (ppr co)
+
+-- | Apply 'coercionKind' to multiple 'Coercion's
+coercionKinds :: [Coercion] -> Pair [Type]
+coercionKinds tys = sequenceA $ map coercionKind tys
+
+getNth :: Int -> Type -> Type
+getNth n ty | Just (_, tys) <- splitTyConApp_maybe ty
+ = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n
+getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty)
+\end{code}
+
+\begin{code}
+applyCo :: Type -> Coercion -> Type
+-- Gives the type of (e co) where e :: (a~b) => ty
+applyCo ty co | Just ty' <- coreView ty = applyCo ty' co
+applyCo (FunTy _ ty) _ = ty
+applyCo _ _ = panic "applyCo"
+\end{code}
\ No newline at end of file