-    , mkKindCo, mkSelCo

-    , mkAppCo, mkTyConAppCo

-    , mkInstCo, mkLRCo

-    ( mkLRCo, mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkSelCo

-    go_tys !_   []       = return []

-    go_tys !env (ty:tys) = (:) <$> go_ty env ty <*> go_tys env tys

-    go_ty !env (TyVarTy tv)    = tyvar env tv

-    go_ty !env (AppTy t1 t2)   = mkAppTy <$> go_ty env t1 <*> go_ty env t2

-    go_ty !_   ty@(LitTy {})   = return ty

-    go_ty !env (CastTy ty co)  = mkCastTy <$> go_ty env ty <*> go_co env co

-    go_ty !env (CoercionTy co) = CoercionTy <$> go_co env co

-    go_ty !env ty@(FunTy _ w arg res)

-    go_ty !env ty@(TyConApp tc tys)

-    go_ty !env (ForAllTy (Bndr tv vis) inner)

-    go_cos !_   []       = return []

-    go_cos !env (co:cos) = (:) <$> go_co env co <*> go_cos env cos

-    go_mco !_   MRefl    = return MRefl

-    go_mco !env (MCo co) = MCo <$> (go_co env co)

-    go_co !env (Refl ty)                  = Refl <$> go_ty env ty

-    go_co !env (GRefl r ty mco)           = mkGReflCo r <$> go_ty env ty <*> go_mco env mco

-    go_co !env (AppCo c1 c2)              = mkAppCo <$> go_co env c1 <*> go_co env c2

-    go_co !env (FunCo r afl afr cw c1 c2) = mkFunCo2 r afl afr <$> go_co env cw

-    go_co !env (CoVarCo cv)               = covar env cv

-    go_co !env (HoleCo hole)              = cohole env hole

-    go_co !env (UnivCo { uco_prov = p, uco_role = r

-                       , uco_lty = t1, uco_rty = t2, uco_deps = deps })

-                                          = mkUnivCo <$> pure p

-                                                     <*> go_cos env deps

-                                                     <*> pure r

-                                                     <*> go_ty env t1 <*> go_ty env t2

-    go_co !env (SymCo co)                 = mkSymCo <$> go_co env co

-    go_co !env (TransCo c1 c2)            = mkTransCo <$> go_co env c1 <*> go_co env c2

-    go_co !env (AxiomCo r cos)            = mkAxiomCo r <$> go_cos env cos

-    go_co !env (SelCo i co)               = SelCo i <$> go_co env co

-    go_co !env (LRCo lr co)               = mkLRCo lr <$> go_co env co

-    go_co !env (InstCo co arg)            = mkInstCo <$> go_co env co <*> go_co env arg

-    go_co !env (KindCo co)                = mkKindCo <$> go_co env co

-    go_co !env (SubCo co)                 = mkSubCo <$> go_co env co

-    go_co !env co@(TyConAppCo r tc cos)   = do { cos' <- go_cos env cos

-    go_co !env (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR

-                         , fco_kind = kind_co, fco_body = co })

-import {-# SOURCE #-} GHC.Core.Coercion ( mkCoercionType, coVarTypesRole )

-import Data.Functor.Identity ( Identity (..) )

-

-substTyCoMapper :: TyCoMapper Subst Identity

-       (subst', tcv') = substVarBndrUnchecked subst tcv

-   tcapp_ty :: Subst -> Type -> TyCon -> [Type] -> Identity Type

-   tcapp_co :: Subst -> Coercion -> Role -> TyCon -> [Coercion] -> Identity Coercion

-    run :: forall a. (Subst -> a -> Identity a) -> Subst -> a -> a

-    run ms subst x = runIdentity (ms subst x)

-

-{-

-subst_ty :: Subst -> Type -> Type

--- subst_ty is the main workhorse for type substitution

---

--- Note that the in_scope set is poked only if we hit a forall

--- so it may often never be fully computed

-subst_ty subst ty

-   = go ty

-  where

-    go (TyVarTy tv)      = substTyVar subst tv

-    go (AppTy fun arg)   = (mkAppTy $! (go fun)) $! (go arg)

-                -- The mkAppTy smart constructor is important

-                -- we might be replacing (a Int), represented with App

-                -- by [Int], represented with TyConApp

-    go ty@(TyConApp tc []) = tc `seq` ty  -- avoid allocation in this common case

-    go (TyConApp tc tys) = (mkTyConApp $! tc) $! strictMap go tys

-                               -- NB: mkTyConApp, not TyConApp.

-                               -- mkTyConApp has optimizations.

-                               -- See Note [Using synonyms to compress types]

-                               -- in GHC.Core.Type

-    go ty@(FunTy { ft_mult = mult, ft_arg = arg, ft_res = res })

-      = let !mult' = go mult

-            !arg' = go arg

-            !res' = go res

-        in ty { ft_mult = mult', ft_arg = arg', ft_res = res' }

-    go (ForAllTy (Bndr tv vis) ty)

-      = (ForAllTy $! ((Bndr $! tv') vis)) $! (subst_ty subst' ty)

-      where

-        !(subst',tv') = substVarBndrUnchecked subst tv

-                        -- Unchecked because subst_ty is used from substTyUnchecked

-    go (LitTy n)         = LitTy $! n

-    go (CastTy ty co)    = (mkCastTy $! (go ty)) $! (subst_co subst co)

-    go (CoercionTy co)   = CoercionTy $! (subst_co subst co)

--}

-{-

-subst_co :: HasDebugCallStack => Subst -> Coercion -> Coercion

-subst_co subst co

-  = go co

-  where

-    go_ty :: Type -> Type

-    go_ty = subst_ty subst

-

-    go_mco :: MCoercion -> MCoercion

-    go_mco MRefl    = MRefl

-    go_mco (MCo co) = MCo (go co)

-

-    go :: Coercion -> Coercion

-    go (Refl ty)             = mkNomReflCo $! (go_ty ty)

-    go (GRefl r ty mco)      = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)

-    go (TyConAppCo r tc args)= mkTyConAppCo r tc $! go_cos args

-    go (AxiomCo con cos)     = mkAxiomCo con $! go_cos cos

-    go (AppCo co arg)        = (mkAppCo $! go co) $! go arg

-    go (ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR

-                 , fco_kind = kind_co, fco_body = co })

-      = ((mkForAllCo $! tcv') visL visR

-           $! go_mco kind_co)

-           $! subst_co subst' co

-      where

-        !(subst', tcv') = substVarBndrUnchecked subst tcv

-                          -- Unchecked because used from substTyUnchecked

-    go (FunCo r afl afr w co1 co2)   = ((mkFunCo2 r afl afr $! go w) $! go co1) $! go co2

-    go (CoVarCo cv)          = substCoVar subst cv

-    go (HoleCo h)            = substCoHole subst h

-    go (UnivCo { uco_prov = p, uco_role = r

-               , uco_lty = t1, uco_rty = t2, uco_deps = deps })

-                             = ((((mkUnivCo $! p) $! go_cos deps) $! r) $!

-                                  (go_ty t1)) $! (go_ty t2)

-    go (SymCo co)            = mkSymCo $! (go co)

-    go (TransCo co1 co2)     = (mkTransCo $! (go co1)) $! (go co2)

-    go (SelCo d co)          = mkSelCo d $! (go co)

-    go (LRCo lr co)          = mkLRCo lr $! (go co)

-    go (InstCo co arg)       = (mkInstCo $! (go co)) $! go arg

-    go (KindCo co)           = mkKindCo $! (go co)

-    go (SubCo co)            = mkSubCo $! (go co)

-

-    go_cos cos = let cos' = map go cos

-                 in cos' `seqList` cos'

--}

-

-import GHC.Data.FastString

-import Data.Functor.Identity

-      (exp_ty, _, _, _) -> \subst ty -> runIdentity (exp_ty subst ty)

-expandTypeSynonymMapper :: TyCoMapper Subst Identity