(Another) minor refactoring of substitutions

No change in functionality here, but greater clarity:

* In FamInstEnv.FlattenEnv, kill off the fi_in_scope field
  We are already maintaining an in-scope set in the fe_subst field,
  so it's silly do to it twice.

  (This isn't strictly connected to the rest of this patch, but
  the nomenclature changes below affect the same code, so I put
  them together.)

* TyCoRep.extendTCVSubst used to take a TyVar or a CoVar and work
  out what to do, but in fact we almost always know which of the
  two we are doing.  So:
    - define extendTvSubst, extendCvSubst
    - and use them

* Similar renamings in TyCoRep:
   - extendTCvSubstList        -->   extendTvSubstList
   - extendTCvSubstBinder      -->   extendTvSubstBinder
   - extendTCvSubstAndInScope  --> extendTvSubstAndInScope

* Add Type.extendTvSubstWithClone, extendCvSubstWithClone

* Similar nomenclature changes in Subst, SimplEnv, Specialise

* Kill off TyCoRep.substTelescope (never used)

22 files changed, 149 insertions, 161 deletions

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 7dfc0b0733..a64e922e21 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -564,8 +564,8 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
     mk_boxer boxers = DCB (\ ty_args src_vars ->
                       do { let (ex_vars, term_vars) = splitAtList ex_tvs src_vars
                                subst1 = zipTvSubst univ_tvs ty_args
-                               subst2 = extendTCvSubstList subst1 ex_tvs
-                                                           (mkTyVarTys ex_vars)
+                               subst2 = extendTvSubstList subst1 ex_tvs
+                                                          (mkTyVarTys ex_vars)
                          ; (rep_ids, binds) <- go subst2 boxers term_vars
                          ; return (ex_vars ++ rep_ids, binds) } )
 
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 6f199ea4f6..1d4d28c151 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1688,7 +1688,7 @@ addInScopeVar var m
 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 extendSubstL tv ty m
   = LintM $ \ env errs ->
-    unLintM m (env { le_subst = Type.extendTCvSubst (le_subst env) tv ty }) errs
+    unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
 
 updateTCvSubst :: TCvSubst -> LintM a -> LintM a
 updateTCvSubst subst' m
diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index 167654e1ea..a31650969e 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -21,7 +21,7 @@ module CoreSubst (
 
         -- ** Operations on substitutions
         emptySubst, mkEmptySubst, mkSubst, mkOpenSubst, substInScope, isEmptySubst,
-        extendIdSubst, extendIdSubstList, extendTCvSubst, extendTCvSubstList,
+        extendIdSubst, extendIdSubstList, extendTCvSubst, extendTvSubstList,
         extendSubst, extendSubstList, extendSubstWithVar, zapSubstEnv,
         addInScopeSet, extendInScope, extendInScopeList, extendInScopeIds,
         isInScope, setInScope,
@@ -50,7 +50,7 @@ import qualified Type
 import qualified Coercion
 
         -- We are defining local versions
-import Type     hiding ( substTy, extendTCvSubst, extendTCvSubstList
+import Type     hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList
                        , isInScope, substTyVarBndr, cloneTyVarBndr )
 import Coercion hiding ( substCo, substCoVarBndr )
 
@@ -215,48 +215,43 @@ extendIdSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope (extendVarEnv id
 extendIdSubstList :: Subst -> [(Id, CoreExpr)] -> Subst
 extendIdSubstList (Subst in_scope ids tvs cvs) prs = Subst in_scope (extendVarEnvList ids prs) tvs cvs
 
--- | Add a substitution for a 'TyVar' to the 'Subst': the 'TyVar' *must*
--- be a real TyVar, and not a CoVar
-extend_tv_subst :: Subst -> TyVar -> Type -> Subst
-extend_tv_subst (Subst in_scope ids tvs cvs) tv ty
+-- | Add a substitution for a 'TyVar' to the 'Subst'
+-- The 'TyVar' *must* be a real TyVar, and not a CoVar
+-- You must ensure that the in-scope set is such that
+-- the "CoreSubst#in_scope_invariant" is true after extending
+-- the substitution like this.
+extendTvSubst :: Subst -> TyVar -> Type -> Subst
+extendTvSubst (Subst in_scope ids tvs cvs) tv ty
   = ASSERT( isTyVar tv )
     Subst in_scope ids (extendVarEnv tvs tv ty) cvs
 
--- | Add a substitution for a 'TyVar' to the 'Subst': you must ensure that the in-scope set is
--- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
-extendTCvSubst :: Subst -> TyVar -> Type -> Subst
-extendTCvSubst subst v r
-  | isTyVar v
-  = extend_tv_subst subst v r
-  | Just co <- isCoercionTy_maybe r
-  = extendCvSubst subst v co
-  | otherwise
-  = pprPanic "CoreSubst.extendTCvSubst" (ppr v <+> text "|->" <+> ppr r)
-
--- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTCvSubst'
-extendTCvSubstList :: Subst -> [(TyVar,Type)] -> Subst
-extendTCvSubstList subst vrs
+-- | Adds multiple 'TyVar' substitutions to the 'Subst': see also 'extendTvSubst'
+extendTvSubstList :: Subst -> [(TyVar,Type)] -> Subst
+extendTvSubstList subst vrs
   = foldl' extend subst vrs
-  where extend subst (v, r) = extendTCvSubst subst v r
+  where
+    extend subst (v, r) = extendTvSubst subst v r
 
 -- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst': you must ensure that the in-scope set is
 -- such that the "CoreSubst#in_scope_invariant" is true after extending the substitution like this
 extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
-extendCvSubst (Subst in_scope ids tvs cvs) v r = Subst in_scope ids tvs (extendVarEnv cvs v r)
+extendCvSubst (Subst in_scope ids tvs cvs) v r
+  = ASSERT( isCoVar v )
+    Subst in_scope ids tvs (extendVarEnv cvs v r)
 
 -- | Add a substitution appropriate to the thing being substituted
 --   (whether an expression, type, or coercion). See also
---   'extendIdSubst', 'extendTCvSubst'
+--   'extendIdSubst', 'extendTvSubst', 'extendCvSubst'
 extendSubst :: Subst -> Var -> CoreArg -> Subst
 extendSubst subst var arg
   = case arg of
-      Type ty     -> ASSERT( isTyVar var ) extend_tv_subst subst var ty
+      Type ty     -> ASSERT( isTyVar var ) extendTvSubst subst var ty
       Coercion co -> ASSERT( isCoVar var ) extendCvSubst subst var co
       _           -> ASSERT( isId    var ) extendIdSubst subst var arg
 
 extendSubstWithVar :: Subst -> Var -> Var -> Subst
 extendSubstWithVar subst v1 v2
-  | isTyVar v1 = ASSERT( isTyVar v2 ) extend_tv_subst subst v1 (mkTyVarTy v2)
+  | isTyVar v1 = ASSERT( isTyVar v2 ) extendTvSubst subst v1 (mkTyVarTy v2)
   | isCoVar v1 = ASSERT( isCoVar v2 ) extendCvSubst subst v1 (mkCoVarCo v2)
   | otherwise  = ASSERT( isId    v2 ) extendIdSubst subst v1 (Var v2)
 
@@ -1050,7 +1045,7 @@ maybe_substitute :: Subst -> InVar -> OutExpr -> Maybe Subst
 maybe_substitute subst b r
   | Type ty <- r        -- let a::* = TYPE ty in <body>
   = ASSERT( isTyVar b )
-    Just (extendTCvSubst subst b ty)
+    Just (extendTvSubst subst b ty)
 
   | Coercion co <- r
   = ASSERT( isCoVar b )
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index be9f463eb7..6fa55c91a3 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -1564,7 +1564,7 @@ dataConInstPat fss uniqs con inst_tys
                                        (zip3 ex_tvs ex_fss ex_uniqs)
 
     mk_ex_var :: TCvSubst -> (TyVar, FastString, Unique) -> (TCvSubst, TyVar)
-    mk_ex_var subst (tv, fs, uniq) = (Type.extendTCvSubst subst tv
+    mk_ex_var subst (tv, fs, uniq) = (Type.extendTvSubst subst tv
                                        (mkTyVarTy new_tv)
                                      , new_tv)
       where
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 09c7c6bb27..ee7e4308d8 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -505,7 +505,7 @@ toIfaceTcArgs tc ty_args
       | otherwise            = ITC_Invis t' ts'
       where
         t'  = toIfaceType t
-        ts' = go (extendTCvSubstBinder env bndr t) res ts
+        ts' = go (extendTvSubstBinder env bndr t) res ts
 
     go env (TyVarTy tv) ts
       | Just ki <- lookupTyVar env tv = go env ki ts
diff --git a/compiler/main/GhcPlugins.hs b/compiler/main/GhcPlugins.hs
index 2aef9b3510..2af2da8e7a 100644
--- a/compiler/main/GhcPlugins.hs
+++ b/compiler/main/GhcPlugins.hs
@@ -54,7 +54,7 @@ import Packages
 -- Important GHC types
 import Module
 import Type     hiding {- conflict with CoreSubst -}
-                ( substTy, extendTCvSubst, extendTCvSubstList, isInScope )
+                ( substTy, extendTvSubst, extendTvSubstList, isInScope )
 import Coercion hiding {- conflict with CoreSubst -}
                 ( substCo )
 import TyCon
diff --git a/compiler/simplCore/SimplEnv.hs b/compiler/simplCore/SimplEnv.hs
index ecb2e66d68..53fe9f4c38 100644
--- a/compiler/simplCore/SimplEnv.hs
+++ b/compiler/simplCore/SimplEnv.hs
@@ -16,7 +16,8 @@ module SimplEnv (
 
         -- Environments
         SimplEnv(..), StaticEnv, pprSimplEnv,   -- Temp not abstract
-        mkSimplEnv, extendIdSubst, SimplEnv.extendTCvSubst,
+        mkSimplEnv, extendIdSubst,
+        SimplEnv.extendTvSubst, SimplEnv.extendCvSubst,
         zapSubstEnv, setSubstEnv,
         getInScope, setInScope, setInScopeSet, modifyInScope, addNewInScopeIds,
         getSimplRules,
@@ -271,14 +272,15 @@ extendIdSubst env@(SimplEnv {seIdSubst = subst}) var res
   = ASSERT2( isId var && not (isCoVar var), ppr var )
     env {seIdSubst = extendVarEnv subst var res}
 
-extendTCvSubst :: SimplEnv -> TyVar -> Type -> SimplEnv
-extendTCvSubst env@(SimplEnv {seTvSubst = tsubst, seCvSubst = csubst}) var res
-  | isTyVar var
-  = env {seTvSubst = extendVarEnv tsubst var res}
-  | Just co <- isCoercionTy_maybe res
-  = env {seCvSubst = extendVarEnv csubst var co}
-  | otherwise
-  = pprPanic "SimplEnv.extendTCvSubst" (ppr res)
+extendTvSubst :: SimplEnv -> TyVar -> Type -> SimplEnv
+extendTvSubst env@(SimplEnv {seTvSubst = tsubst}) var res
+  = ASSERT( isTyVar var )
+    env {seTvSubst = extendVarEnv tsubst var res}
+
+extendCvSubst :: SimplEnv -> CoVar -> Coercion -> SimplEnv
+extendCvSubst env@(SimplEnv {seCvSubst = csubst}) var co
+  = ASSERT( isCoVar var )
+    env {seCvSubst = extendVarEnv csubst var co}
 
 ---------------------
 getInScope :: SimplEnv -> InScopeSet
diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs
index 4d31f5b1d1..0e5da9bc5a 100644
--- a/compiler/simplCore/Simplify.hs
+++ b/compiler/simplCore/Simplify.hs
@@ -12,7 +12,7 @@ module Simplify ( simplTopBinds, simplExpr, simplRules ) where
 
 import DynFlags
 import SimplMonad
-import Type hiding      ( substTy, substTyVar, extendTCvSubst )
+import Type hiding      ( substTy, substTyVar, extendTvSubst, extendCvSubst )
 import SimplEnv
 import SimplUtils
 import FamInstEnv       ( FamInstEnv )
@@ -385,7 +385,7 @@ simplNonRecX env bndr new_rhs
                   --   the binding c = (a,b)
 
   | Coercion co <- new_rhs
-  = return (extendTCvSubst env bndr (mkCoercionTy co))
+  = return (extendCvSubst env bndr co)
 
   | otherwise
   = do  { (env', bndr') <- simplBinder env bndr
@@ -665,7 +665,7 @@ completeBind :: SimplEnv
 completeBind env top_lvl old_bndr new_bndr new_rhs
  | isCoVar old_bndr
  = case new_rhs of
-     Coercion co -> return (extendTCvSubst env old_bndr (mkCoercionTy co))
+     Coercion co -> return (extendCvSubst env old_bndr co)
      _           -> return (addNonRec env new_bndr new_rhs)
 
  | otherwise
@@ -1237,7 +1237,7 @@ simplLam env [] body cont = simplExprF env body cont
 
 simplLam env (bndr:bndrs) body (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = cont })
   = do { tick (BetaReduction bndr)
-       ; simplLam (extendTCvSubst env bndr arg_ty) bndrs body cont }
+       ; simplLam (extendTvSubst env bndr arg_ty) bndrs body cont }
 
 simplLam env (bndr:bndrs) body (ApplyToVal { sc_arg = arg, sc_env = arg_se
                                            , sc_cont = cont })
@@ -1245,7 +1245,7 @@ simplLam env (bndr:bndrs) body (ApplyToVal { sc_arg = arg, sc_env = arg_se
         ; simplNonRecE env' (zap_unfolding bndr) (arg, arg_se) (bndrs, body) cont }
   where
     env' | Coercion co <- arg
-         = extendTCvSubst env bndr (mkCoercionTy co)
+         = extendCvSubst env bndr co
          | otherwise
          = env
 
@@ -1321,7 +1321,7 @@ simplNonRecE :: SimplEnv
 simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
   = ASSERT( isTyVar bndr )
     do  { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
-        ; simplLam (extendTCvSubst env bndr ty_arg') bndrs body cont }
+        ; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
 
 simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
   = do dflags <- getDynFlags
@@ -2260,11 +2260,11 @@ knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
 
     bind_args env' (b:bs') (Type ty : args)
       = ASSERT( isTyVar b )
-        bind_args (extendTCvSubst env' b ty) bs' args
+        bind_args (extendTvSubst env' b ty) bs' args
 
     bind_args env' (b:bs') (Coercion co : args)
       = ASSERT( isCoVar b )
-        bind_args (extendTCvSubst env' b (mkCoercionTy co)) bs' args
+        bind_args (extendCvSubst env' b co) bs' args
 
     bind_args env' (b:bs') (arg : args)
       = ASSERT( isId b )
diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs
index bccf600c10..443998b5fe 100644
--- a/compiler/specialise/Specialise.hs
+++ b/compiler/specialise/Specialise.hs
@@ -10,8 +10,8 @@ module Specialise ( specProgram, specUnfolding ) where
 #include "HsVersions.h"
 
 import Id
-import TcType hiding( substTy, extendTCvSubstList )
-import Type   hiding( substTy, extendTCvSubstList )
+import TcType hiding( substTy )
+import Type   hiding( substTy, extendTvSubstList )
 import Coercion( Coercion )
 import Module( Module, HasModule(..) )
 import CoreMonad
@@ -1241,7 +1241,7 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
                 -- spec_tyvars = [a,c]
                 -- ty_args     = [t1,b,t3]
                 spec_tv_binds = [(tv,ty) | (tv, Just ty) <- rhs_tyvars `zip` call_ts]
-                env1          = extendTCvSubstList env spec_tv_binds
+                env1          = extendTvSubstList env spec_tv_binds
                 (rhs_env, poly_tyvars) = substBndrs env1
                                             [tv | (tv, Nothing) <- rhs_tyvars `zip` call_ts]
 
@@ -2133,9 +2133,9 @@ mapAndCombineSM f (x:xs) = do (y, uds1) <- f x
                               (ys, uds2) <- mapAndCombineSM f xs
                               return (y:ys, uds1 `plusUDs` uds2)
 
-extendTCvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
-extendTCvSubstList env tv_binds
-  = env { se_subst = CoreSubst.extendTCvSubstList (se_subst env) tv_binds }
+extendTvSubstList :: SpecEnv -> [(TyVar,Type)] -> SpecEnv
+extendTvSubstList env tv_binds
+  = env { se_subst = CoreSubst.extendTvSubstList (se_subst env) tv_binds }
 
 substTy :: SpecEnv -> Type -> Type
 substTy env ty = CoreSubst.substTy (se_subst env) ty
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index f142dcaa75..b3da5ef5ea 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -228,7 +228,8 @@ deeplyInstantiate orig ty
                                                 , text "type" <+> ppr ty
                                                 , text "with" <+> ppr tvs'
                                                 , text "args:" <+> ppr ids1
-                                                , text "theta:" <+>  ppr theta' ])
+                                                , text "theta:" <+>  ppr theta'
+                                                , text "subst:" <+> ppr subst ])
        ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho)
        ; return (mkWpLams ids1
                     <.> wrap2
@@ -309,7 +310,7 @@ instDFunType dfun_id dfun_inst_tys
     go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
     go subst [] [] = return (subst, [])
     go subst (tv:tvs) (Just ty : mb_tys)
-      = do { (subst', tys) <- go (extendTCvSubst subst tv ty) tvs mb_tys
+      = do { (subst', tys) <- go (extendTvSubst subst tv ty) tvs mb_tys
            ; return (subst', ty : tys) }
     go subst (tv:tvs) (Nothing : mb_tys)
       = do { (subst', tv') <- newMetaTyVarX subst tv
diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs
index 1e84e4c8d9..8a67965234 100644
--- a/compiler/typecheck/TcClassDcl.hs
+++ b/compiler/typecheck/TcClassDcl.hs
@@ -479,7 +479,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
       | Just ty <- lookupVarEnv (getTvSubstEnv subst) tc_tv
       = (subst, ty)
       | otherwise
-      = (extendTCvSubst subst tc_tv ty', ty')
+      = (extendTvSubst subst tc_tv ty', ty')
       where
         ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
 
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 970d2465a6..d54fbc7644 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -860,7 +860,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
               --   c.f. TcMType.newMetaTyVars
               mk_inst_ty subst (tv, result_inst_ty)
                 | is_fixed_tv tv   -- Same as result type
-                = return (extendTCvSubst subst tv result_inst_ty, result_inst_ty)
+                = return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
                 | otherwise        -- Fresh type, of correct kind
                 = do { (subst', new_tv) <- newMetaTyVarX subst tv
                      ; return (subst', mkTyVarTy new_tv) }
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 266550db2a..c7b1470ab1 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -769,7 +769,7 @@ tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
            ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
                      tc_lhs_type mode' arg (substTyUnchecked subst $ binderType bndr)
            ; let subst' = case binderVar_maybe bndr of
-                   Just tv -> extendTCvSubst subst tv arg'
+                   Just tv -> extendTvSubst subst tv arg'
                    Nothing -> subst
            ; go subst' res_k args (n+1) (arg' : acc) }
 
@@ -830,7 +830,7 @@ tcInstBinderX :: Maybe (VarEnv Kind)
 tcInstBinderX mb_kind_info subst binder
   | Just tv <- binderVar_maybe binder
   = case lookup_tv tv of
-      Just ki -> return (extendTCvSubstAndInScope subst tv ki, ki)
+      Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
       Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
                     ; return (subst', mkTyVarTy tv') }
 
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index e4da9aa936..d058107cc9 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -81,7 +81,7 @@ module TcMType (
 #include "HsVersions.h"
 
 -- friends:
-import TyCoRep ( CoercionHole(..) )
+import TyCoRep
 import TcType
 import Type
 import Coercion
@@ -453,8 +453,7 @@ tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
 
 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
 tcSuperSkolTyVar subst tv
-  = (extendTCvSubst (extendTCvInScope subst new_tv) tv (mkTyVarTy new_tv)
-    , new_tv)
+  = (extendTvSubstWithClone subst tv new_tv, new_tv)
   where
     kind   = substTyUnchecked subst (tyVarKind tv)
     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
@@ -535,19 +534,16 @@ instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
 instSkolTyCoVarX mk_tcv subst tycovar
   = do  { uniq <- newUnique  -- using a new unique is critical. See
                              -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
-        ; let new_tv = mk_tcv uniq old_name kind
-        ; return (extendTCvSubst (extendTCvInScope subst new_tv) tycovar
-                   (mk_ty_co new_tv)
-                 , new_tv)
-        }
+        ; let new_tcv = mk_tcv uniq old_name kind
+              subst1 | isTyVar new_tcv
+                     = extendTvSubstWithClone subst tycovar new_tcv
+                     | otherwise
+                     = extendCvSubstWithClone subst tycovar new_tcv
+        ; return (subst1, new_tcv) }
   where
     old_name = tyVarName tycovar
     kind     = substTyUnchecked subst (tyVarKind tycovar)
 
-    mk_ty_co v
-      | isTyVar v = mkTyVarTy v
-      | otherwise = mkCoercionTy $ mkCoVarCo v
-
 newFskTyVar :: TcType -> TcM TcTyVar
 newFskTyVar fam_ty
   = do { uniq <- newUnique
@@ -777,29 +773,22 @@ newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
 newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 -- Make a new unification variable tyvar whose Name and Kind come from
 -- an existing TyVar. We substitute kind variables in the kind.
-newMetaTyVarX subst tyvar
-  = do  { uniq <- newUnique
-        ; details <- newMetaDetails TauTv
-        ; let name   = mkSystemName uniq (getOccName tyvar)
-                       -- See Note [Name of an instantiated type variable]
-              kind   = substTyUnchecked subst (tyVarKind tyvar)
-              new_tv = mkTcTyVar name kind details
-        ; return (extendTCvSubstAndInScope subst tyvar
-                   (mkTyVarTy new_tv)
-                 , new_tv)
-        }
+newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
 
 newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 -- Just like newMetaTyVarX, but make a SigTv
-newMetaSigTyVarX subst tyvar
+newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
+
+new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+new_meta_tv_x info subst tyvar
   = do  { uniq <- newUnique
-        ; details <- newMetaDetails SigTv
+        ; details <- newMetaDetails info
         ; let name   = mkSystemName uniq (getOccName tyvar)
-              kind   = substTy subst (tyVarKind tyvar)
+                       -- See Note [Name of an instantiated type variable]
+              kind   = substTyUnchecked subst (tyVarKind tyvar)
               new_tv = mkTcTyVar name kind details
-        ; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
-                   (mkTyVarTy new_tv)
-                 , new_tv) }
+              subst1 = extendTvSubstWithClone subst tyvar new_tv
+        ; return (subst1, new_tv) }
 
 {- Note [Name of an instantiated type variable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index b9240424e5..053c53b86a 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -2891,7 +2891,7 @@ instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTCvSubst tvs)
      inst_one subst tv
          = do { ty' <- instFlexiTcSHelper (tyVarName tv)
                                           (substTyUnchecked subst (tyVarKind tv))
-              ; return (extendTCvSubst subst tv ty', ty') }
+              ; return (extendTvSubst subst tv ty', ty') }
 
 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
 instFlexiTcSHelper tvname kind
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 05d2992e74..e68efd09f9 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1815,8 +1815,8 @@ mkGADTVars tmpl_tvs dc_tvs subst
             ,  tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
             -> -- simple, well-kinded variable substitution.
                choose (r_tv:univs) eqs
-                      (extendTCvSubst t_sub t_tv r_ty)
-                      (extendTCvSubst r_sub r_tv r_ty)
+                      (extendTvSubst t_sub t_tv r_ty)
+                      (extendTvSubst r_sub r_tv r_ty)
                       t_tvs
             where
               r_tv1  = setTyVarName r_tv (choose_tv_name r_tv t_tv)
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index c542b56520..0160310313 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -149,9 +149,10 @@ module TcType (
   zipTvSubst,
   mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
   getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
-  extendTCvInScopeList, extendTCvInScopeSet, extendTCvSubstAndInScope,
+  extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
   Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
-  extendTCvSubstList, isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
+  Type.extendTvSubst,
+  isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
   Type.substTy, substTys, substTyWith, substTyWithCoVars,
   substTyAddInScope,
   substTyUnchecked, substTysUnchecked, substThetaUnchecked,
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 6546288667..3d841e5bea 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -73,7 +73,7 @@ module Coercion (
         lookupCoVar,
         substCo, substCos, substCoVar, substCoVars, substCoWith,
         substCoVarBndr,
-        extendTCvSubstAndInScope, getCvSubstEnv,
+        extendTvSubstAndInScope, getCvSubstEnv,
 
         -- ** Lifting
         liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 0665e765ee..020dd78df4 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -1427,13 +1427,11 @@ flattenTys is defined here because of module dependencies.
 -}
 
 data FlattenEnv = FlattenEnv { fe_type_map :: TypeMap TyVar
-                             , fe_in_scope :: InScopeSet
                              , fe_subst    :: TCvSubst }
 
 emptyFlattenEnv :: InScopeSet -> FlattenEnv
 emptyFlattenEnv in_scope
   = FlattenEnv { fe_type_map = emptyTypeMap
-               , fe_in_scope = in_scope
                , fe_subst    = mkEmptyTCvSubst in_scope }
 
 -- See Note [Flattening]
@@ -1502,28 +1500,27 @@ coreFlattenCo env co
   where
     (env1, kind') = coreFlattenTy env (coercionType co)
     fresh_name    = mkFlattenFreshCoName
-    in_scope      = fe_in_scope env1
-    covar         = uniqAway in_scope $ mkCoVar fresh_name kind'
-    env2          = env1 { fe_in_scope = in_scope `extendInScopeSet` covar }
+    subst1        = fe_subst env1
+    in_scope      = getTCvInScope subst1
+    covar         = uniqAway in_scope (mkCoVar fresh_name kind')
+    env2          = env1 { fe_subst = subst1 `extendTCvInScope` covar }
 
 coreFlattenVarBndr :: FlattenEnv -> TyVar -> (FlattenEnv, TyVar)
 coreFlattenVarBndr env tv
   | kind' `eqType` kind
-  = ( env { fe_subst = extendTCvSubst old_subst tv (mkTyVarTy tv) }
+  = ( env { fe_subst = extendTvSubst old_subst tv (mkTyVarTy tv) }
              -- override any previous binding for tv
     , tv)
+
   | otherwise
-  = let new_tv    = uniqAway (fe_in_scope env) (setTyVarKind tv kind')
-        new_subst = extendTCvSubst old_subst tv (mkTyVarTy new_tv)
-        new_is    = extendInScopeSet old_in_scope new_tv
+  = let new_tv    = uniqAway (getTCvInScope old_subst) (setTyVarKind tv kind')
+        new_subst = extendTvSubstWithClone old_subst tv new_tv
     in
-    (env' { fe_in_scope = new_is
-          , fe_subst    = new_subst }, new_tv)
+    (env' { fe_subst = new_subst }, new_tv)
   where
     kind          = tyVarKind tv
     (env', kind') = coreFlattenTy env kind
     old_subst     = fe_subst env
-    old_in_scope  = fe_in_scope env
 
 coreFlattenTyFamApp :: FlattenEnv
                     -> TyCon         -- type family tycon
@@ -1538,14 +1535,14 @@ coreFlattenTyFamApp env fam_tc fam_args
               -- contains *all* tyvars, even locally bound ones elsewhere in the
               -- overall type, so this really is fresh.
       Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
-                     tv = uniqAway in_scope $ mkTyVar tyvar_name
-                                                      (typeKind fam_ty)
+                     tv = uniqAway (getTCvInScope subst) $
+                          mkTyVar tyvar_name (typeKind fam_ty)
                      env' = env { fe_type_map = extendTypeMap type_map fam_ty tv
-                                , fe_in_scope = extendInScopeSet in_scope tv }
+                                , fe_subst = extendTCvInScope subst tv }
                  in (env', tv)
   where fam_ty   = mkTyConApp fam_tc fam_args
         FlattenEnv { fe_type_map = type_map
-                   , fe_in_scope = in_scope } = env
+                   , fe_subst = subst } = env
 
 -- | Get the set of all type variables mentioned anywhere in the list
 -- of types. These variables are not necessarily free.
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 210fc22e7c..fb6c68e303 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -10,7 +10,7 @@ module OptCoercion ( optCoercion, checkAxInstCo ) where
 
 import TyCoRep
 import Coercion
-import Type hiding( substTyVarBndr, substTy, extendTCvSubst )
+import Type hiding( substTyVarBndr, substTy )
 import TcType       ( exactTyCoVarsOfType )
 import TyCon
 import CoAxiom
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 3930e5e5aa..ad583eab3f 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -83,14 +83,16 @@ module TyCoRep (
         getCvSubstEnv, getTCvInScope, isInScope, notElemTCvSubst,
         setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
         extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
-        extendTCvSubst, extendTCvSubstAndInScope, extendTCvSubstList,
-        extendTCvSubstBinder,
+        extendTCvSubst,
+        extendCvSubst, extendCvSubstWithClone,
+        extendTvSubst, extendTvSubstWithClone,
+        extendTvSubstList, extendTvSubstAndInScope,
+        extendTvSubstBinder,
         unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
         zipTvSubst, zipCvSubst,
         zipTyBinderSubst,
         mkTvSubstPrs,
 
-        substTelescope,
         substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
         substCoWith,
         substTy, substTyAddInScope,
@@ -239,8 +241,8 @@ data TyLit
 -- ('Named') or nondependent ('Anon'). They may also be visible or not.
 -- See also Note [TyBinder]
 data TyBinder
-  = Named TyVar VisibilityFlag
-  | Anon Type   -- visibility is determined by the type (Constraint vs. *)
+  = Named TyVar VisibilityFlag  -- Always a TyVar (not CoVar or Id)
+  | Anon Type   -- Visibility is determined by the type (Constraint vs. *)
     deriving (Data.Typeable, Data.Data)
 
 -- | Is something required to appear in source Haskell ('Visible'),
@@ -1517,7 +1519,7 @@ CoercionTy.
 
 Note [The substitution invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When calling substTy subst ty it should be the case that
+When calling (substTy subst ty) it should be the case that
 the in-scope set in the substitution is a superset of both:
 
   * The free vars of the range of the substitution
@@ -1624,39 +1626,50 @@ extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
 extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
   = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
 
-extendSubstEnvs :: (TvSubstEnv, CvSubstEnv) -> Var -> Type
-                -> (TvSubstEnv, CvSubstEnv)
-extendSubstEnvs (tenv, cenv) v ty
+extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
+extendTCvSubst subst v ty
   | isTyVar v
-  = ASSERT( not $ isCoercionTy ty )
-    (extendVarEnv tenv v ty, cenv)
-
-    -- NB: v might *not* be a proper covar, because it might be lifted.
-    -- This happens in tcCoercionToCoercion
+  = extendTvSubst subst v ty
   | CoercionTy co <- ty
-  = (tenv, extendVarEnv cenv v co)
+  = extendCvSubst subst v co
   | otherwise
-  = pprPanic "extendSubstEnvs" (ppr v <+> text "|->" <+> ppr ty)
-
-extendTCvSubst :: TCvSubst -> Var -> Type -> TCvSubst
-extendTCvSubst (TCvSubst in_scope tenv cenv) tv ty
-  = TCvSubst in_scope tenv' cenv'
-  where (tenv', cenv') = extendSubstEnvs (tenv, cenv) tv ty
-
-extendTCvSubstAndInScope :: TCvSubst -> TyCoVar -> Type -> TCvSubst
+  = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
+
+extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
+extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
+  = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
+
+extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
+-- Adds a new tv -> tv mapping, /and/ extends the in-scope set
+extendTvSubstWithClone (TCvSubst in_scope tenv cenv) tv tv'
+  = TCvSubst (extendInScopeSet in_scope tv')
+             (extendVarEnv tenv tv (mkTyVarTy tv'))
+             cenv
+
+extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
+extendCvSubst (TCvSubst in_scope tenv cenv) v co
+  = TCvSubst in_scope tenv (extendVarEnv cenv v co)
+
+extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
+extendCvSubstWithClone (TCvSubst in_scope tenv cenv) cv cv'
+  = TCvSubst (extendInScopeSet in_scope cv')
+             tenv
+             (extendVarEnv cenv cv (mkCoVarCo cv'))
+
+extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
 -- Also extends the in-scope set
-extendTCvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
+extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
   = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
-             tenv' cenv'
-  where (tenv', cenv') = extendSubstEnvs (tenv, cenv) tv ty
+             (extendVarEnv tenv tv ty)
+             cenv
 
-extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
-extendTCvSubstList subst tvs tys
-  = foldl2 extendTCvSubst subst tvs tys
+extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
+extendTvSubstList subst tvs tys
+  = foldl2 extendTvSubst subst tvs tys
 
-extendTCvSubstBinder :: TCvSubst -> TyBinder -> Type -> TCvSubst
-extendTCvSubstBinder env (Anon {})    _  = env
-extendTCvSubstBinder env (Named tv _) ty = extendTCvSubst env tv ty
+extendTvSubstBinder :: TCvSubst -> TyBinder -> Type -> TCvSubst
+extendTvSubstBinder env (Anon {})    _  = env
+extendTvSubstBinder env (Named tv _) ty = extendTvSubst env tv ty
 
 unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
 -- Works when the ranges are disjoint
@@ -1798,19 +1811,6 @@ ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
 
 -}
 
--- | Create a substitution from tyvars to types, but later types may depend
--- on earlier ones. Return the substed types and the built substitution.
-substTelescope :: [TyCoVar] -> [Type] -> ([Type], TCvSubst)
-substTelescope = go_subst emptyTCvSubst
-  where
-    go_subst :: TCvSubst -> [TyCoVar] -> [Type] -> ([Type], TCvSubst)
-    go_subst subst [] [] = ([], subst)
-    go_subst subst (tv:tvs) (k:ks)
-      = let k' = substTy subst k in
-        liftFst (k' :) $ go_subst (extendTCvSubst subst tv k') tvs ks
-    go_subst _ _ _ = panic "substTelescope"
-
-
 -- | Type substitution, see 'zipTvSubst'
 substTyWith ::
 -- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
@@ -1818,6 +1818,8 @@ substTyWith ::
     (?callStack :: CallStack) =>
 #endif
     [TyVar] -> [Type] -> Type -> Type
+-- Works only if the domain of the substitution is a
+-- superset of the type being substituted into
 substTyWith tvs tys = ASSERT( length tvs == length tys )
                       substTy (zipTvSubst tvs tys)
 
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 7b04cf573e..c8f41db699 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -157,7 +157,8 @@ module Type (
         getTvSubstEnv, setTvSubstEnv,
         zapTCvSubst, getTCvInScope,
         extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
-        extendTCvSubst, extendTCvSubstList, extendTCvSubstAndInScope,
+        extendTCvSubst, extendCvSubst,
+        extendTvSubst, extendTvSubstList, extendTvSubstAndInScope,
         isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
         isEmptyTCvSubst, unionTCvSubst,
 
@@ -168,7 +169,7 @@ module Type (
         substTyWithBindersUnchecked, substTyWithUnchecked,
         substCoUnchecked, substCoWithUnchecked,
         substTyVarBndr, substTyVar, substTyVars,
-        cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar, substTelescope,
+        cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
 
         -- * Pretty-printing
         pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing,
@@ -1370,7 +1371,7 @@ partitionInvisibles tc get_ty = go emptyTCvSubst (tyConKind tc)
       | isVisibleBinder bndr = second (x :) (go subst' res_ki xs)
       | otherwise            = first  (x :) (go subst' res_ki xs)
       where
-        subst' = extendTCvSubstBinder subst bndr (get_ty x)
+        subst' = extendTvSubstBinder subst bndr (get_ty x)
     go subst (TyVarTy tv) xs
       | Just ki <- lookupTyVar subst tv = go subst ki xs
     go _ _ xs = ([], xs)  -- something is ill-kinded. But this can happen