Break up TyCoRep

This breaks up the monstrous TyCoReps module into several new modules by
topic:

 * TyCoRep: Contains the `Coercion`, `Type`, and related type
   definitions and a few simple predicates but nothing further

 * TyCoPpr: Contains the the pretty-printer logic

 * TyCoFVs: Contains the free variable computations (and
   `tyConAppNeedsKindSig`, although I suspect this should change)

 * TyCoSubst: Contains the substitution logic for types and coercions

 * TyCoTidy: Contains the tidying logic for types

While we are able to eliminate a good number of `SOURCE` imports (and
make a few others smaller) with this change, we must introduce one new
`hs-boot` file for `TyCoPpr` so that `TyCoRep` can define `Outputable`
instances for the types it defines.

Metric Increase:
    haddock.Cabal
    haddock.compiler

1 files changed, 23 insertions, 2389 deletions

diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 1f2f8c6724..51ad630372 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -9,6 +9,10 @@ Note [The Type-related module hierarchy]
   CoAxiom
   TyCon    imports Class, CoAxiom
   TyCoRep  imports Class, CoAxiom, TyCon
+  TyCoPpr  imports TyCoRep
+  TyCoFVs  imports TyCoRep
+  TyCoSubst imports TyCoRep, TyCoFVs, TyCoPpr
+  TyCoTidy imports TyCoRep, TyCoFVs
   TysPrim  imports TyCoRep ( including mkTyConTy )
   Kind     imports TysPrim ( mainly for primitive kinds )
   Type     imports Kind
@@ -65,88 +69,6 @@ module TyCoRep (
         -- * Functions over coercions
         pickLR,
 
-        -- * Pretty-printing
-        pprType, pprParendType, pprPrecType, pprPrecTypeX,
-        pprTypeApp, pprTCvBndr, pprTCvBndrs,
-        pprSigmaType,
-        pprTheta, pprParendTheta, pprForAll, pprUserForAll,
-        pprTyVar, pprTyVars,
-        pprThetaArrowTy, pprClassPred,
-        pprKind, pprParendKind, pprTyLit,
-        PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
-        pprDataCons, pprWithExplicitKindsWhen,
-
-        pprCo, pprParendCo,
-
-        debugPprType,
-
-        -- * Free variables
-        tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
-        tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
-        tyCoFVsOfType, tyCoVarsOfTypeList,
-        tyCoFVsOfTypes, tyCoVarsOfTypesList,
-        coVarsOfType, coVarsOfTypes,
-        coVarsOfCo, coVarsOfCos,
-        tyCoVarsOfCo, tyCoVarsOfCos,
-        tyCoVarsOfCoDSet,
-        tyCoFVsOfCo, tyCoFVsOfCos,
-        tyCoVarsOfCoList, tyCoVarsOfProv,
-        almostDevoidCoVarOfCo,
-        injectiveVarsOfType, tyConAppNeedsKindSig,
-
-        noFreeVarsOfType, noFreeVarsOfCo,
-
-        -- * Substitutions
-        TCvSubst(..), TvSubstEnv, CvSubstEnv,
-        emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
-        emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
-        mkTCvSubst, mkTvSubst, mkCvSubst,
-        getTvSubstEnv,
-        getCvSubstEnv, getTCvInScope, getTCvSubstRangeFVs,
-        isInScope, notElemTCvSubst,
-        setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
-        extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
-        extendTCvSubst, extendTCvSubstWithClone,
-        extendCvSubst, extendCvSubstWithClone,
-        extendTvSubst, extendTvSubstBinderAndInScope, extendTvSubstWithClone,
-        extendTvSubstList, extendTvSubstAndInScope,
-        extendTCvSubstList,
-        unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
-        zipTvSubst, zipCvSubst,
-        zipTCvSubst,
-        mkTvSubstPrs,
-
-        substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
-        substCoWith,
-        substTy, substTyAddInScope,
-        substTyUnchecked, substTysUnchecked, substThetaUnchecked,
-        substTyWithUnchecked,
-        substCoUnchecked, substCoWithUnchecked,
-        substTyWithInScope,
-        substTys, substTheta,
-        lookupTyVar,
-        substCo, substCos, substCoVar, substCoVars, lookupCoVar,
-        cloneTyVarBndr, cloneTyVarBndrs,
-        substVarBndr, substVarBndrs,
-        substTyVarBndr, substTyVarBndrs,
-        substCoVarBndr,
-        substTyVar, substTyVars, substTyCoVars,
-        substForAllCoBndr,
-        substVarBndrUsing, substForAllCoBndrUsing,
-        checkValidSubst, isValidTCvSubst,
-
-        -- * Tidying type related things up for printing
-        tidyType,      tidyTypes,
-        tidyOpenType,  tidyOpenTypes,
-        tidyOpenKind,
-        tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars, avoidNameClashes,
-        tidyOpenTyCoVar, tidyOpenTyCoVars,
-        tidyTyCoVarOcc,
-        tidyTopType,
-        tidyKind,
-        tidyCo, tidyCos,
-        tidyTyCoVarBinder, tidyTyCoVarBinders,
-
         -- * Sizes
         typeSize, coercionSize, provSize
     ) where
@@ -155,48 +77,30 @@ module TyCoRep (
 
 import GhcPrelude
 
-import {-# SOURCE #-} DataCon( dataConFullSig
-                             , dataConUserTyVarBinders
-                             , DataCon )
-import {-# SOURCE #-} Type( isCoercionTy, mkAppTy, mkCastTy
-                          , tyCoVarsOfTypeWellScoped
-                          , tyCoVarsOfTypesWellScoped
-                          , scopedSort
-                          , coreView )
+import {-# SOURCE #-} Type( coreView )
+import {-# SOURCE #-} TyCoPpr ( pprType, pprCo, pprTyLit )
+
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
-import {-# SOURCE #-} Coercion
 import {-# SOURCE #-} ConLike ( ConLike(..), conLikeName )
-import {-# SOURCE #-} ToIface( toIfaceTypeX, toIfaceTyLit, toIfaceForAllBndr
-                             , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
 
 -- friends:
 import IfaceType
 import Var
-import VarEnv
 import VarSet
 import Name hiding ( varName )
 import TyCon
-import Class
 import CoAxiom
-import FV
 
 -- others
-import BasicTypes ( LeftOrRight(..), PprPrec(..), topPrec, sigPrec, opPrec
-                  , funPrec, appPrec, maybeParen, pickLR )
+import BasicTypes ( LeftOrRight(..), pickLR )
 import PrelNames
 import Outputable
-import DynFlags
 import FastString
-import Pair
-import UniqSupply
 import Util
-import UniqFM
-import UniqSet
 
 -- libraries
 import qualified Data.Data as Data hiding ( TyCon )
-import Data.List
 import Data.IORef ( IORef )   -- for CoercionHole
 
 {-
@@ -333,6 +237,9 @@ data Type
 
   deriving Data.Data
 
+instance Outputable Type where
+  ppr = pprType
+
 -- NOTE:  Other parts of the code assume that type literals do not contain
 -- types or type variables.
 data TyLit
@@ -340,6 +247,8 @@ data TyLit
   | StrTyLit FastString
   deriving (Eq, Ord, Data.Data)
 
+instance Outputable TyLit where
+   ppr = pprTyLit
 
 {- Note [Function types]
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -727,6 +636,13 @@ data TyCoBinder
                            -- Visibility is determined by the AnonArgFlag
   deriving Data.Data
 
+instance Outputable TyCoBinder where
+  ppr (Anon af ty) = ppr af <+> ppr ty
+  ppr (Named (Bndr v Required))  = ppr v
+  ppr (Named (Bndr v Specified)) = char '@' <> ppr v
+  ppr (Named (Bndr v Inferred))  = braces (ppr v)
+
+
 -- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder'
 -- in the 'Named' field.
 type TyBinder = TyCoBinder
@@ -1246,6 +1162,9 @@ type CoercionR = Coercion       -- always representational
 type CoercionP = Coercion       -- always phantom
 type KindCoercion = CoercionN   -- always nominal
 
+instance Outputable Coercion where
+  ppr = pprCo
+
 -- | A semantically more meaningful type to represent what may or may not be a
 -- useful 'Coercion'.
 data MCoercion
@@ -1798,2293 +1717,8 @@ Here,
   where
     co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
     co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
-
-
-%************************************************************************
-%*                                                                      *
-                 Free variables of types and coercions
-%*                                                                      *
-%************************************************************************
--}
-
-{- Note [Free variables of types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
-a VarSet that is closed over the types of its variables.  More precisely,
-  if    S = tyCoVarsOfType( t )
-  and   (a:k) is in S
-  then  tyCoVarsOftype( k ) is a subset of S
-
-Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.
-
-We could /not/ close over the kinds of the variable occurrences, and
-instead do so at call sites, but it seems that we always want to do
-so, so it's easiest to do it here.
-
-It turns out that getting the free variables of types is performance critical,
-so we profiled several versions, exploring different implementation strategies.
-
-1. Baseline version: uses FV naively. Essentially:
-
-   tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty
-
-   This is not nice, because FV introduces some overhead to implement
-   determinism, and throught its "interesting var" function, neither of which
-   we need here, so they are a complete waste.
-
-2. UnionVarSet version: instead of reusing the FV-based code, we simply used
-   VarSets directly, trying to avoid the overhead of FV. E.g.:
-
-   -- FV version:
-   tyCoFVsOfType (AppTy fun arg)    a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c
-
-   -- UnionVarSet version:
-   tyCoVarsOfType (AppTy fun arg)    = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg)
-
-   This looks deceptively similar, but while FV internally builds a list- and
-   set-generating function, the VarSet functions manipulate sets directly, and
-   the latter peforms a lot worse than the naive FV version.
-
-3. Accumulator-style VarSet version: this is what we use now. We do use VarSet
-   as our data structure, but delegate the actual work to a new
-   ty_co_vars_of_...  family of functions, which use accumulator style and the
-   "in-scope set" filter found in the internals of FV, but without the
-   determinism overhead.
-
-See #14880.
-
-Note [Closing over free variable kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over
-free variable kinds. In previous GHC versions, this happened naively: whenever
-we would encounter an occurrence of a free type variable, we would close over
-its kind. This, however is wrong for two reasons (see #14880):
-
-1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k), then
-   we don't want to have to traverse k more than once.
-
-2. Correctness. Imagine we have forall k. b -> k, where b has
-   kind k, for some k bound in an outer scope. If we look at b's kind inside
-   the forall, we'll collect that k is free and then remove k from the set of
-   free variables. This is plain wrong. We must instead compute that b is free
-   and then conclude that b's kind is free.
-
-An obvious first approach is to move the closing-over-kinds from the
-occurrences of a type variable to after finding the free vars - however, this
-turns out to introduce performance regressions, and isn't even entirely
-correct.
-
-In fact, it isn't even important *when* we close over kinds; what matters is
-that we handle each type var exactly once, and that we do it in the right
-context.
-
-So the next approach we tried was to use the "in-scope set" part of FV or the
-equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to
-say "don't bother with variables we have already closed over". This should work
-fine in theory, but the code is complicated and doesn't perform well.
-
-But there is a simpler way, which is implemented here. Consider the two points
-above:
-
-1. Efficiency: we now have an accumulator, so the second time we encounter 'a',
-   we'll ignore it, certainly not looking at its kind - this is why
-   pre-checking set membership before inserting ends up not only being faster,
-   but also being correct.
-
-2. Correctness: we have an "in-scope set" (I think we should call it it a
-  "bound-var set"), specifying variables that are bound by a forall in the type
-  we are traversing; we simply ignore these variables, certainly not looking at
-  their kind.
-
-So now consider:
-
-    forall k. b -> k
-
-where b :: k->Type is free; but of course, it's a different k! When looking at
-b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose
-this is our first encounter with b; we want the free vars of its kind. But we
-want to behave as if we took the free vars of its kind at the end; that is,
-with no bound vars in scope.
-
-So the solution is easy. The old code was this:
-
-  ty_co_vars_of_type (TyVarTy v) is acc
-    | v `elemVarSet` is  = acc
-    | v `elemVarSet` acc = acc
-    | otherwise          = ty_co_vars_of_type (tyVarKind v) is (extendVarSet acc v)
-
-Now all we need to do is take the free vars of tyVarKind v *with an empty
-bound-var set*, thus:
-
-ty_co_vars_of_type (TyVarTy v) is acc
-  | v `elemVarSet` is  = acc
-  | v `elemVarSet` acc = acc
-  | otherwise          = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
-                                                          ^^^^^^^^^^^
-
-And that's it.
-
--}
-
-tyCoVarsOfType :: Type -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfType ty = ty_co_vars_of_type ty emptyVarSet emptyVarSet
-
-tyCoVarsOfTypes :: [Type] -> TyCoVarSet
-tyCoVarsOfTypes tys = ty_co_vars_of_types tys emptyVarSet emptyVarSet
-
-ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_type (TyVarTy v) is acc
-  | v `elemVarSet` is  = acc
-  | v `elemVarSet` acc = acc
-  | otherwise          = ty_co_vars_of_type (tyVarKind v)
-                            emptyVarSet  -- See Note [Closing over free variable kinds]
-                            (extendVarSet acc v)
-
-ty_co_vars_of_type (TyConApp _ tys)   is acc = ty_co_vars_of_types tys is acc
-ty_co_vars_of_type (LitTy {})         _  acc = acc
-ty_co_vars_of_type (AppTy fun arg)    is acc = ty_co_vars_of_type fun is (ty_co_vars_of_type arg is acc)
-ty_co_vars_of_type (FunTy _ arg res)  is acc = ty_co_vars_of_type arg is (ty_co_vars_of_type res is acc)
-ty_co_vars_of_type (ForAllTy (Bndr tv _) ty) is acc = ty_co_vars_of_type (varType tv) is $
-                                                      ty_co_vars_of_type ty (extendVarSet is tv) acc
-ty_co_vars_of_type (CastTy ty co)     is acc = ty_co_vars_of_type ty is (ty_co_vars_of_co co is acc)
-ty_co_vars_of_type (CoercionTy co)    is acc = ty_co_vars_of_co co is acc
-
-ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_types []       _  acc = acc
-ty_co_vars_of_types (ty:tys) is acc = ty_co_vars_of_type ty is (ty_co_vars_of_types tys is acc)
-
-tyCoVarsOfCo :: Coercion -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfCo co = ty_co_vars_of_co co emptyVarSet emptyVarSet
-
-tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
-tyCoVarsOfCos cos = ty_co_vars_of_cos cos emptyVarSet emptyVarSet
-
-
-ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_co (Refl ty)            is acc = ty_co_vars_of_type ty is acc
-ty_co_vars_of_co (GRefl _ ty mco)     is acc = ty_co_vars_of_type ty is $
-                                               ty_co_vars_of_mco mco is acc
-ty_co_vars_of_co (TyConAppCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
-ty_co_vars_of_co (AppCo co arg)       is acc = ty_co_vars_of_co co is $
-                                               ty_co_vars_of_co arg is acc
-ty_co_vars_of_co (ForAllCo tv kind_co co) is acc = ty_co_vars_of_co kind_co is $
-                                                   ty_co_vars_of_co co (extendVarSet is tv) acc
-ty_co_vars_of_co (FunCo _ co1 co2)    is acc = ty_co_vars_of_co co1 is $
-                                               ty_co_vars_of_co co2 is acc
-ty_co_vars_of_co (CoVarCo v)          is acc = ty_co_vars_of_co_var v is acc
-ty_co_vars_of_co (HoleCo h)           is acc = ty_co_vars_of_co_var (coHoleCoVar h) is acc
-    -- See Note [CoercionHoles and coercion free variables]
-ty_co_vars_of_co (AxiomInstCo _ _ cos) is acc = ty_co_vars_of_cos cos is acc
-ty_co_vars_of_co (UnivCo p _ t1 t2)    is acc = ty_co_vars_of_prov p is $
-                                                ty_co_vars_of_type t1 is $
-                                                ty_co_vars_of_type t2 is acc
-ty_co_vars_of_co (SymCo co)          is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (TransCo co1 co2)   is acc = ty_co_vars_of_co co1 is $
-                                              ty_co_vars_of_co co2 is acc
-ty_co_vars_of_co (NthCo _ _ co)      is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (LRCo _ co)         is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (InstCo co arg)     is acc = ty_co_vars_of_co co is $
-                                              ty_co_vars_of_co arg is acc
-ty_co_vars_of_co (KindCo co)         is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (SubCo co)          is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_co (AxiomRuleCo _ cs)  is acc = ty_co_vars_of_cos cs is acc
-
-ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_mco MRefl    _is acc = acc
-ty_co_vars_of_mco (MCo co) is  acc = ty_co_vars_of_co co is acc
-
-ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_co_var v is acc
-  | v `elemVarSet` is  = acc
-  | v `elemVarSet` acc = acc
-  | otherwise          = ty_co_vars_of_type (varType v)
-                            emptyVarSet  -- See Note [Closing over free variable kinds]
-                            (extendVarSet acc v)
-
-ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_cos []       _  acc = acc
-ty_co_vars_of_cos (co:cos) is acc = ty_co_vars_of_co co is (ty_co_vars_of_cos cos is acc)
-
-tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
-tyCoVarsOfProv prov = ty_co_vars_of_prov prov emptyVarSet emptyVarSet
-
-ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
-ty_co_vars_of_prov (PhantomProv co)    is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_prov (ProofIrrelProv co) is acc = ty_co_vars_of_co co is acc
-ty_co_vars_of_prov UnsafeCoerceProv    _  acc = acc
-ty_co_vars_of_prov (PluginProv _)      _  acc = acc
-
--- | Generates an in-scope set from the free variables in a list of types
--- and a list of coercions
-mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
-mkTyCoInScopeSet tys cos
-  = mkInScopeSet (ty_co_vars_of_types tys emptyVarSet $
-                  ty_co_vars_of_cos   cos emptyVarSet emptyVarSet)
-
--- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
--- set. For explanation of why using `VarSet` is not deterministic see
--- Note [Deterministic FV] in FV.
-tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty
-
--- | `tyCoFVsOfType` that returns free variables of a type in deterministic
--- order. For explanation of why using `VarSet` is not deterministic see
--- Note [Deterministic FV] in FV.
-tyCoVarsOfTypeList :: Type -> [TyCoVar]
--- See Note [Free variables of types]
-tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
-
--- | Returns free variables of types, including kind variables as
--- a non-deterministic set. For type synonyms it does /not/ expand the
--- synonym.
-tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfTypesSet tys = tyCoVarsOfTypes $ nonDetEltsUFM tys
-  -- It's OK to use nonDetEltsUFM here because we immediately forget the
-  -- ordering by returning a set
-
--- | Returns free variables of types, including kind variables as
--- a deterministic set. For type synonyms it does /not/ expand the
--- synonym.
-tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys
-
--- | Returns free variables of types, including kind variables as
--- a deterministically ordered list. For type synonyms it does /not/ expand the
--- synonym.
-tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
--- See Note [Free variables of types]
-tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
-
--- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
--- The previous implementation used `unionVarSet` which is O(n+m) and can
--- make the function quadratic.
--- It's exported, so that it can be composed with
--- other functions that compute free variables.
--- See Note [FV naming conventions] in FV.
---
--- Eta-expanded because that makes it run faster (apparently)
--- See Note [FV eta expansion] in FV for explanation.
-tyCoFVsOfType :: Type -> FV
--- See Note [Free variables of types]
-tyCoFVsOfType (TyVarTy v)        f bound_vars (acc_list, acc_set)
-  | not (f v) = (acc_list, acc_set)
-  | v `elemVarSet` bound_vars = (acc_list, acc_set)
-  | v `elemVarSet` acc_set = (acc_list, acc_set)
-  | otherwise = tyCoFVsOfType (tyVarKind v) f
-                               emptyVarSet   -- See Note [Closing over free variable kinds]
-                               (v:acc_list, extendVarSet acc_set v)
-tyCoFVsOfType (TyConApp _ tys)   f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc
-tyCoFVsOfType (LitTy {})         f bound_vars acc = emptyFV f bound_vars acc
-tyCoFVsOfType (AppTy fun arg)    f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc
-tyCoFVsOfType (FunTy _ arg res)  f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc
-tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty)  f bound_vars acc
-tyCoFVsOfType (CastTy ty co)     f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc
-tyCoFVsOfType (CoercionTy co)    f bound_vars acc = tyCoFVsOfCo co f bound_vars acc
-
-tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
--- Free vars of (forall b. <thing with fvs>)
-tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs
-
-tyCoFVsVarBndrs :: [Var] -> FV -> FV
-tyCoFVsVarBndrs vars fvs = foldr tyCoFVsVarBndr fvs vars
-
-tyCoFVsVarBndr :: Var -> FV -> FV
-tyCoFVsVarBndr var fvs
-  = tyCoFVsOfType (varType var)   -- Free vars of its type/kind
-    `unionFV` delFV var fvs       -- Delete it from the thing-inside
-
-tyCoFVsOfTypes :: [Type] -> FV
--- See Note [Free variables of types]
-tyCoFVsOfTypes (ty:tys) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfTypes tys) fv_cand in_scope acc
-tyCoFVsOfTypes []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-
--- | Get a deterministic set of the vars free in a coercion
-tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
--- See Note [Free variables of types]
-tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co
-
-tyCoVarsOfCoList :: Coercion -> [TyCoVar]
--- See Note [Free variables of types]
-tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
-
-tyCoFVsOfMCo :: MCoercion -> FV
-tyCoFVsOfMCo MRefl    = emptyFV
-tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co
-
-tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
-tyCoVarsOfCosSet cos = tyCoVarsOfCos $ nonDetEltsUFM cos
-  -- It's OK to use nonDetEltsUFM here because we immediately forget the
-  -- ordering by returning a set
-
-tyCoFVsOfCo :: Coercion -> FV
--- Extracts type and coercion variables from a coercion
--- See Note [Free variables of types]
-tyCoFVsOfCo (Refl ty) fv_cand in_scope acc
-  = tyCoFVsOfType ty fv_cand in_scope acc
-tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
-  = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc
-tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
-tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
-  = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
-tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
-  = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
-tyCoFVsOfCo (FunCo _ co1 co2)    fv_cand in_scope acc
-  = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
-tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
-  = tyCoFVsOfCoVar v fv_cand in_scope acc
-tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
-  = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
-    -- See Note [CoercionHoles and coercion free variables]
-tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
-tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
-  = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1
-                     `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
-tyCoFVsOfCo (SymCo co)          fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfCo (TransCo co1 co2)   fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
-tyCoFVsOfCo (NthCo _ _ co)      fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfCo (LRCo _ co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfCo (InstCo co arg)     fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
-tyCoFVsOfCo (KindCo co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfCo (SubCo co)          fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfCo (AxiomRuleCo _ cs)  fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
-
-tyCoFVsOfCoVar :: CoVar -> FV
-tyCoFVsOfCoVar v fv_cand in_scope acc
-  = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
-
-tyCoFVsOfProv :: UnivCoProvenance -> FV
-tyCoFVsOfProv UnsafeCoerceProv    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-
-tyCoFVsOfCos :: [Coercion] -> FV
-tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCos cos) fv_cand in_scope acc
-
-
-------------- Extracting the CoVars of a type or coercion -----------
-
-{-
-
-Note [CoVarsOfX and the InterestingVarFun]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The coVarsOfType, coVarsOfTypes, coVarsOfCo, and coVarsOfCos functions are
-implemented in terms of the respective FV equivalents (tyCoFVsOf...), rather
-than the VarSet-based flavors (tyCoVarsOf...), despite the performance
-considerations outlined in Note [Free variables of types].
-
-This is because FV includes the InterestingVarFun, which is useful here,
-because we can cleverly use it to restrict our calculations to CoVars - this
-is what getCoVarSet achieves.
-
-See #14880.
-
--}
-
-getCoVarSet :: FV -> CoVarSet
-getCoVarSet fv = snd (fv isCoVar emptyVarSet ([], emptyVarSet))
-
-coVarsOfType :: Type -> CoVarSet
-coVarsOfType ty = getCoVarSet (tyCoFVsOfType ty)
-
-coVarsOfTypes :: [Type] -> TyCoVarSet
-coVarsOfTypes tys = getCoVarSet (tyCoFVsOfTypes tys)
-
-coVarsOfCo :: Coercion -> CoVarSet
-coVarsOfCo co = getCoVarSet (tyCoFVsOfCo co)
-
-coVarsOfCos :: [Coercion] -> CoVarSet
-coVarsOfCos cos = getCoVarSet (tyCoFVsOfCos cos)
-
------ Whether a covar is /Almost Devoid/ in a type or coercion ----
-
--- | Given a covar and a coercion, returns True if covar is almost devoid in
--- the coercion. That is, covar can only appear in Refl and GRefl.
--- See last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion
-almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
-almostDevoidCoVarOfCo cv co =
-  almost_devoid_co_var_of_co co cv
-
-almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
-almost_devoid_co_var_of_co (Refl {}) _ = True   -- covar is allowed in Refl and
-almost_devoid_co_var_of_co (GRefl {}) _ = True  -- GRefl, so we don't look into
-                                                -- the coercions
-almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv
-  = almost_devoid_co_var_of_cos cos cv
-almost_devoid_co_var_of_co (AppCo co arg) cv
-  = almost_devoid_co_var_of_co co cv
-  && almost_devoid_co_var_of_co arg cv
-almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv
-  = almost_devoid_co_var_of_co kind_co cv
-  && (v == cv || almost_devoid_co_var_of_co co cv)
-almost_devoid_co_var_of_co (FunCo _ co1 co2) cv
-  = almost_devoid_co_var_of_co co1 cv
-  && almost_devoid_co_var_of_co co2 cv
-almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv
-almost_devoid_co_var_of_co (HoleCo h)  cv = (coHoleCoVar h) /= cv
-almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv
-  = almost_devoid_co_var_of_cos cos cv
-almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv
-  = almost_devoid_co_var_of_prov p cv
-  && almost_devoid_co_var_of_type t1 cv
-  && almost_devoid_co_var_of_type t2 cv
-almost_devoid_co_var_of_co (SymCo co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_co (TransCo co1 co2) cv
-  = almost_devoid_co_var_of_co co1 cv
-  && almost_devoid_co_var_of_co co2 cv
-almost_devoid_co_var_of_co (NthCo _ _ co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_co (LRCo _ co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_co (InstCo co arg) cv
-  = almost_devoid_co_var_of_co co cv
-  && almost_devoid_co_var_of_co arg cv
-almost_devoid_co_var_of_co (KindCo co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_co (SubCo co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
-  = almost_devoid_co_var_of_cos cs cv
-
-almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
-almost_devoid_co_var_of_cos [] _ = True
-almost_devoid_co_var_of_cos (co:cos) cv
-  = almost_devoid_co_var_of_co co cv
-  && almost_devoid_co_var_of_cos cos cv
-
-almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
-almost_devoid_co_var_of_prov (PhantomProv co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
-  = almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_prov UnsafeCoerceProv _ = True
-almost_devoid_co_var_of_prov (PluginProv _) _ = True
-
-almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
-almost_devoid_co_var_of_type (TyVarTy _) _ = True
-almost_devoid_co_var_of_type (TyConApp _ tys) cv
-  = almost_devoid_co_var_of_types tys cv
-almost_devoid_co_var_of_type (LitTy {}) _ = True
-almost_devoid_co_var_of_type (AppTy fun arg) cv
-  = almost_devoid_co_var_of_type fun cv
-  && almost_devoid_co_var_of_type arg cv
-almost_devoid_co_var_of_type (FunTy _ arg res) cv
-  = almost_devoid_co_var_of_type arg cv
-  && almost_devoid_co_var_of_type res cv
-almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv
-  = almost_devoid_co_var_of_type (varType v) cv
-  && (v == cv || almost_devoid_co_var_of_type ty cv)
-almost_devoid_co_var_of_type (CastTy ty co) cv
-  = almost_devoid_co_var_of_type ty cv
-  && almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_type (CoercionTy co) cv
-  = almost_devoid_co_var_of_co co cv
-
-almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
-almost_devoid_co_var_of_types [] _ = True
-almost_devoid_co_var_of_types (ty:tys) cv
-  = almost_devoid_co_var_of_type ty cv
-  && almost_devoid_co_var_of_types tys cv
-
-------------- Injective free vars -----------------
-
--- | Returns the free variables of a 'Type' that are in injective positions.
--- For example, if @F@ is a non-injective type family, then:
---
--- @
--- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
--- @
---
--- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
--- More formally, if
--- @a@ is in @'injectiveVarsOfType' ty@
--- and  @S1(ty) ~ S2(ty)@,
--- then @S1(a)  ~ S2(a)@,
--- where @S1@ and @S2@ are arbitrary substitutions.
---
--- See @Note [When does a tycon application need an explicit kind signature?]@.
-injectiveVarsOfType :: Type -> FV
-injectiveVarsOfType = go
-  where
-    go ty                 | Just ty' <- coreView ty
-                          = go ty'
-    go (TyVarTy v)        = unitFV v `unionFV` go (tyVarKind v)
-    go (AppTy f a)        = go f `unionFV` go a
-    go (FunTy _ ty1 ty2)  = go ty1 `unionFV` go ty2
-    go (TyConApp tc tys)  =
-      case tyConInjectivityInfo tc of
-        NotInjective  -> emptyFV
-        Injective inj -> mapUnionFV go $
-                         filterByList (inj ++ repeat True) tys
-                         -- Oversaturated arguments to a tycon are
-                         -- always injective, hence the repeat True
-    go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty
-    go LitTy{}           = emptyFV
-    go (CastTy ty _)     = go ty
-    go CoercionTy{}      = emptyFV
-
--- | Does a 'TyCon' (that is applied to some number of arguments) need to be
--- ascribed with an explicit kind signature to resolve ambiguity if rendered as
--- a source-syntax type?
--- (See @Note [When does a tycon application need an explicit kind signature?]@
--- for a full explanation of what this function checks for.)
-
--- Morally, this function ought to belong in TyCon.hs, not TyCoRep.hs, but
--- accomplishing this requires a fair deal of futzing aruond with .hs-boot
--- files.
-tyConAppNeedsKindSig
-  :: Bool  -- ^ Should specified binders count towards injective positions in
-           --   the kind of the TyCon? (If you're using visible kind
-           --   applications, then you want True here.
-  -> TyCon
-  -> Int   -- ^ The number of args the 'TyCon' is applied to.
-  -> Bool  -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the
-           --   number of arguments)
-tyConAppNeedsKindSig spec_inj_pos tc n_args
-  | LT <- listLengthCmp tc_binders n_args
-  = False
-  | otherwise
-  = let (dropped_binders, remaining_binders)
-          = splitAt n_args tc_binders
-        result_kind  = mkTyConKind remaining_binders tc_res_kind
-        result_vars  = tyCoVarsOfType result_kind
-        dropped_vars = fvVarSet $
-                       mapUnionFV injective_vars_of_binder dropped_binders
-
-    in not (subVarSet result_vars dropped_vars)
-  where
-    tc_binders  = tyConBinders tc
-    tc_res_kind = tyConResKind tc
-
-    -- Returns the variables that would be fixed by knowing a TyConBinder. See
-    -- Note [When does a tycon application need an explicit kind signature?]
-    -- for a more detailed explanation of what this function does.
-    injective_vars_of_binder :: TyConBinder -> FV
-    injective_vars_of_binder (Bndr tv vis) =
-      case vis of
-        AnonTCB VisArg -> injectiveVarsOfType (varType tv)
-        NamedTCB argf  | source_of_injectivity argf
-                       -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
-        _              -> emptyFV
-
-    source_of_injectivity Required  = True
-    source_of_injectivity Specified = spec_inj_pos
-    source_of_injectivity Inferred  = False
-
-{-
-Note [When does a tycon application need an explicit kind signature?]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are a couple of places in GHC where we convert Core Types into forms that
-more closely resemble user-written syntax. These include:
-
-1. Template Haskell Type reification (see, for instance, TcSplice.reify_tc_app)
-2. Converting Types to LHsTypes (in HsUtils.typeToLHsType, or in Haddock)
-
-This conversion presents a challenge: how do we ensure that the resulting type
-has enough kind information so as not to be ambiguous? To better motivate this
-question, consider the following Core type:
-
-  -- Foo :: Type -> Type
-  type Foo = Proxy Type
-
-There is nothing ambiguous about the RHS of Foo in Core. But if we were to,
-say, reify it into a TH Type, then it's tempting to just drop the invisible
-Type argument and simply return `Proxy`. But now we've lost crucial kind
-information: we don't know if we're dealing with `Proxy Type` or `Proxy Bool`
-or `Proxy Int` or something else! We've inadvertently introduced ambiguity.
-
-Unlike in other situations in GHC, we can't just turn on
--fprint-explicit-kinds, as we need to produce something which has the same
-structure as a source-syntax type. Moreover, we can't rely on visible kind
-application, since the first kind argument to Proxy is inferred, not specified.
-Our solution is to annotate certain tycons with their kinds whenever they
-appear in applied form in order to resolve the ambiguity. For instance, we
-would reify the RHS of Foo like so:
-
-  type Foo = (Proxy :: Type -> Type)
-
-We need to devise an algorithm that determines precisely which tycons need
-these explicit kind signatures. We certainly don't want to annotate _every_
-tycon with a kind signature, or else we might end up with horribly bloated
-types like the following:
-
-  (Either :: Type -> Type -> Type) (Int :: Type) (Char :: Type)
-
-We only want to annotate tycons that absolutely require kind signatures in
-order to resolve some sort of ambiguity, and nothing more.
-
-Suppose we have a tycon application (T ty_1 ... ty_n). Why might this type
-require a kind signature? It might require it when we need to fill in any of
-T's omitted arguments. By "omitted argument", we mean one that is dropped when
-reifying ty_1 ... ty_n. Sometimes, the omitted arguments are inferred and
-specified arguments (e.g., TH reification in TcSplice), and sometimes the
-omitted arguments are only the inferred ones (e.g., in HsUtils.typeToLHsType,
-which reifies specified arguments through visible kind application).
-Regardless, the key idea is that _some_ arguments are going to be omitted after
-reification, and the only mechanism we have at our disposal for filling them in
-is through explicit kind signatures.
-
-What do we mean by "fill in"? Let's consider this small example:
-
-  T :: forall {k}. Type -> (k -> Type) -> k
-
-Moreover, we have this application of T:
-
-  T @{j} Int aty
-
-When we reify this type, we omit the inferred argument @{j}. Is it fixed by the
-other (non-inferred) arguments? Yes! If we know the kind of (aty :: blah), then
-we'll generate an equality constraint (kappa -> Type) and, assuming we can
-solve it, that will fix `kappa`. (Here, `kappa` is the unification variable
-that we instantiate `k` with.)
-
-Therefore, for any application of a tycon T to some arguments, the Question We
-Must Answer is:
-
-* Given the first n arguments of T, do the kinds of the non-omitted arguments
-  fill in the omitted arguments?
-
-(This is still a bit hand-wavey, but we'll refine this question incrementally
-as we explain more of the machinery underlying this process.)
-
-Answering this question is precisely the role that the `injectiveVarsOfType`
-and `injective_vars_of_binder` functions exist to serve. If an omitted argument
-`a` appears in the set returned by `injectiveVarsOfType ty`, then knowing
-`ty` determines (i.e., fills in) `a`. (More on `injective_vars_of_binder` in a
-bit.)
-
-More formally, if
-`a` is in `injectiveVarsOfType ty`
-and  S1(ty) ~ S2(ty),
-then S1(a)  ~ S2(a),
-where S1 and S2 are arbitrary substitutions.
-
-For example, is `F` is a non-injective type family, then
-
-  injectiveVarsOfType(Either c (Maybe (a, F b c))) = {a, c}
-
-Now that we know what this function does, here is a second attempt at the
-Question We Must Answer:
-
-* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
-  of T that are instantiated by non-omitted arguments. Do the injective
-  variables of these binders fill in the remainder of T's kind?
-
-Alright, we're getting closer. Next, we need to clarify what the injective
-variables of a tycon binder are. This the role that the
-`injective_vars_of_binder` function serves. Here is what this function does for
-each form of tycon binder:
-
-* Anonymous binders are injective positions. For example, in the promoted data
-  constructor '(:):
-
-    '(:) :: forall a. a -> [a] -> [a]
-
-  The second and third tyvar binders (of kinds `a` and `[a]`) are both
-  anonymous, so if we had '(:) 'True '[], then the kinds of 'True and
-  '[] would contribute to the kind of '(:) 'True '[]. Therefore,
-  injective_vars_of_binder(_ :: a) = injectiveVarsOfType(a) = {a}.
-  (Similarly, injective_vars_of_binder(_ :: [a]) = {a}.)
-* Named binders:
-  - Inferred binders are never injective positions. For example, in this data
-    type:
-
-      data Proxy a
-      Proxy :: forall {k}. k -> Type
-
-    If we had Proxy 'True, then the kind of 'True would not contribute to the
-    kind of Proxy 'True. Therefore,
-    injective_vars_of_binder(forall {k}. ...) = {}.
-  - Required binders are injective positions. For example, in this data type:
-
-      data Wurble k (a :: k) :: k
-      Wurble :: forall k -> k -> k
-
-  The first tyvar binder (of kind `forall k`) has required visibility, so if
-  we had Wurble (Maybe a) Nothing, then the kind of Maybe a would
-  contribute to the kind of Wurble (Maybe a) Nothing. Hence,
-  injective_vars_of_binder(forall a -> ...) = {a}.
-  - Specified binders /might/ be injective positions, depending on how you
-    approach things. Continuing the '(:) example:
-
-      '(:) :: forall a. a -> [a] -> [a]
-
-    Normally, the (forall a. ...) tyvar binder wouldn't contribute to the kind
-    of '(:) 'True '[], since it's not explicitly instantiated by the user. But
-    if visible kind application is enabled, then this is possible, since the
-    user can write '(:) @Bool 'True '[]. (In that case,
-    injective_vars_of_binder(forall a. ...) = {a}.)
-
-    There are some situations where using visible kind application is appropriate
-    (e.g., HsUtils.typeToLHsType) and others where it is not (e.g., TH
-    reification), so the `injective_vars_of_binder` function is parametrized by
-    a Bool which decides if specified binders should be counted towards
-    injective positions or not.
-
-Now that we've defined injective_vars_of_binder, we can refine the Question We
-Must Answer once more:
-
-* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
-  of T that are instantiated by non-omitted arguments. For each such binder
-  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
-  superset of the free variables of the remainder of T's kind?
-
-If the answer to this question is "no", then (T ty_1 ... ty_n) needs an
-explicit kind signature, since T's kind has kind variables leftover that
-aren't fixed by the non-omitted arguments.
-
-One last sticking point: what does "the remainder of T's kind" mean? You might
-be tempted to think that it corresponds to all of the arguments in the kind of
-T that would normally be instantiated by omitted arguments. But this isn't
-quite right, strictly speaking. Consider the following (silly) example:
-
-  S :: forall {k}. Type -> Type
-
-And suppose we have this application of S:
-
-  S Int Bool
-
-The Int argument would be omitted, and
-injective_vars_of_binder(_ :: Type) = {}. This is not a superset of {k}, which
-might suggest that (S Bool) needs an explicit kind signature. But
-(S Bool :: Type) doesn't actually fix `k`! This is because the kind signature
-only affects the /result/ of the application, not all of the individual
-arguments. So adding a kind signature here won't make a difference. Therefore,
-the fourth (and final) iteration of the Question We Must Answer is:
-
-* Given the first n arguments of T (ty_1 ... ty_n), consider the binders
-  of T that are instantiated by non-omitted arguments. For each such binder
-  b_i, take the union of all injective_vars_of_binder(b_i). Is this set a
-  superset of the free variables of the kind of (T ty_1 ... ty_n)?
-
-Phew, that was a lot of work!
-
-How can be sure that this is correct? That is, how can we be sure that in the
-event that we leave off a kind annotation, that one could infer the kind of the
-tycon application from its arguments? It's essentially a proof by induction: if
-we can infer the kinds of every subtree of a type, then the whole tycon
-application will have an inferrable kind--unless, of course, the remainder of
-the tycon application's kind has uninstantiated kind variables.
-
-What happens if T is oversaturated? That is, if T's kind has fewer than n
-arguments, in the case that the concrete application instantiates a result
-kind variable with an arrow kind? If we run out of arguments, we do not attach
-a kind annotation. This should be a rare case, indeed. Here is an example:
-
-   data T1 :: k1 -> k2 -> *
-   data T2 :: k1 -> k2 -> *
-
-   type family G (a :: k) :: k
-   type instance G T1 = T2
-
-   type instance F Char = (G T1 Bool :: (* -> *) -> *)   -- F from above
-
-Here G's kind is (forall k. k -> k), and the desugared RHS of that last
-instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to
-the algorithm above, there are 3 arguments to G so we should peel off 3
-arguments in G's kind. But G's kind has only two arguments. This is the
-rare special case, and we choose not to annotate the application of G with
-a kind signature. After all, we needn't do this, since that instance would
-be reified as:
-
-   type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
-
-So the kind of G isn't ambiguous anymore due to the explicit kind annotation
-on its argument. See #8953 and test th/T8953.
--}
-
-------------- No free vars -----------------
-
--- | Returns True if this type has no free variables. Should be the same as
--- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case.
-noFreeVarsOfType :: Type -> Bool
-noFreeVarsOfType (TyVarTy _)      = False
-noFreeVarsOfType (AppTy t1 t2)    = noFreeVarsOfType t1 && noFreeVarsOfType t2
-noFreeVarsOfType (TyConApp _ tys) = all noFreeVarsOfType tys
-noFreeVarsOfType ty@(ForAllTy {}) = isEmptyVarSet (tyCoVarsOfType ty)
-noFreeVarsOfType (FunTy _ t1 t2)  = noFreeVarsOfType t1 && noFreeVarsOfType t2
-noFreeVarsOfType (LitTy _)        = True
-noFreeVarsOfType (CastTy ty co)   = noFreeVarsOfType ty && noFreeVarsOfCo co
-noFreeVarsOfType (CoercionTy co)  = noFreeVarsOfCo co
-
-noFreeVarsOfMCo :: MCoercion -> Bool
-noFreeVarsOfMCo MRefl    = True
-noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co
-
-noFreeVarsOfTypes :: [Type] -> Bool
-noFreeVarsOfTypes = all noFreeVarsOfType
-
--- | Returns True if this coercion has no free variables. Should be the same as
--- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.
-noFreeVarsOfCo :: Coercion -> Bool
-noFreeVarsOfCo (Refl ty)              = noFreeVarsOfType ty
-noFreeVarsOfCo (GRefl _ ty co)        = noFreeVarsOfType ty && noFreeVarsOfMCo co
-noFreeVarsOfCo (TyConAppCo _ _ args)  = all noFreeVarsOfCo args
-noFreeVarsOfCo (AppCo c1 c2)          = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
-noFreeVarsOfCo co@(ForAllCo {})       = isEmptyVarSet (tyCoVarsOfCo co)
-noFreeVarsOfCo (FunCo _ c1 c2)        = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
-noFreeVarsOfCo (CoVarCo _)            = False
-noFreeVarsOfCo (HoleCo {})            = True    -- I'm unsure; probably never happens
-noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args
-noFreeVarsOfCo (UnivCo p _ t1 t2)     = noFreeVarsOfProv p &&
-                                        noFreeVarsOfType t1 &&
-                                        noFreeVarsOfType t2
-noFreeVarsOfCo (SymCo co)             = noFreeVarsOfCo co
-noFreeVarsOfCo (TransCo co1 co2)      = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
-noFreeVarsOfCo (NthCo _ _ co)         = noFreeVarsOfCo co
-noFreeVarsOfCo (LRCo _ co)            = noFreeVarsOfCo co
-noFreeVarsOfCo (InstCo co1 co2)       = noFreeVarsOfCo co1 && noFreeVarsOfCo co2
-noFreeVarsOfCo (KindCo co)            = noFreeVarsOfCo co
-noFreeVarsOfCo (SubCo co)             = noFreeVarsOfCo co
-noFreeVarsOfCo (AxiomRuleCo _ cs)     = all noFreeVarsOfCo cs
-
--- | Returns True if this UnivCoProv has no free variables. Should be the same as
--- isEmptyVarSet . tyCoVarsOfProv, but faster in the non-forall case.
-noFreeVarsOfProv :: UnivCoProvenance -> Bool
-noFreeVarsOfProv UnsafeCoerceProv    = True
-noFreeVarsOfProv (PhantomProv co)    = noFreeVarsOfCo co
-noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co
-noFreeVarsOfProv (PluginProv {})     = True
-
-{-
-%************************************************************************
-%*                                                                      *
-                        Substitutions
-      Data type defined here to avoid unnecessary mutual recursion
-%*                                                                      *
-%************************************************************************
--}
-
--- | Type & coercion substitution
---
--- #tcvsubst_invariant#
--- The following invariants must hold of a 'TCvSubst':
---
--- 1. The in-scope set is needed /only/ to
--- guide the generation of fresh uniques
---
--- 2. In particular, the /kind/ of the type variables in
--- the in-scope set is not relevant
---
--- 3. The substitution is only applied ONCE! This is because
--- in general such application will not reach a fixed point.
-data TCvSubst
-  = TCvSubst InScopeSet -- The in-scope type and kind variables
-             TvSubstEnv -- Substitutes both type and kind variables
-             CvSubstEnv -- Substitutes coercion variables
-        -- See Note [Substitutions apply only once]
-        -- and Note [Extending the TvSubstEnv]
-        -- and Note [Substituting types and coercions]
-        -- and Note [The substitution invariant]
-
--- | A substitution of 'Type's for 'TyVar's
---                 and 'Kind's for 'KindVar's
-type TvSubstEnv = TyVarEnv Type
-  -- NB: A TvSubstEnv is used
-  --   both inside a TCvSubst (with the apply-once invariant
-  --        discussed in Note [Substitutions apply only once],
-  --   and  also independently in the middle of matching,
-  --        and unification (see Types.Unify).
-  -- So you have to look at the context to know if it's idempotent or
-  -- apply-once or whatever
-
--- | A substitution of 'Coercion's for 'CoVar's
-type CvSubstEnv = CoVarEnv Coercion
-
-{- Note [The substitution invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When calling (substTy subst ty) it should be the case that
-the in-scope set in the substitution is a superset of both:
-
-  (SIa) The free vars of the range of the substitution
-  (SIb) The free vars of ty minus the domain of the substitution
-
-The same rules apply to other substitutions (notably CoreSubst.Subst)
-
-* Reason for (SIa). Consider
-      substTy [a :-> Maybe b] (forall b. b->a)
-  we must rename the forall b, to get
-      forall b2. b2 -> Maybe b
-  Making 'b' part of the in-scope set forces this renaming to
-  take place.
-
-* Reason for (SIb). Consider
-     substTy [a :-> Maybe b] (forall b. (a,b,x))
-  Then if we use the in-scope set {b}, satisfying (SIa), there is
-  a danger we will rename the forall'd variable to 'x' by mistake,
-  getting this:
-      forall x. (Maybe b, x, x)
-  Breaking (SIb) caused the bug from #11371.
-
-Note: if the free vars of the range of the substitution are freshly created,
-then the problems of (SIa) can't happen, and so it would be sound to
-ignore (SIa).
-
-Note [Substitutions apply only once]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We use TCvSubsts to instantiate things, and we might instantiate
-        forall a b. ty
-with the types
-        [a, b], or [b, a].
-So the substitution might go [a->b, b->a].  A similar situation arises in Core
-when we find a beta redex like
-        (/\ a /\ b -> e) b a
-Then we also end up with a substitution that permutes type variables. Other
-variations happen to; for example [a -> (a, b)].
-
-        ********************************************************
-        *** So a substitution must be applied precisely once ***
-        ********************************************************
-
-A TCvSubst is not idempotent, but, unlike the non-idempotent substitution
-we use during unifications, it must not be repeatedly applied.
-
-Note [Extending the TvSubstEnv]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See #tcvsubst_invariant# for the invariants that must hold.
-
-This invariant allows a short-cut when the subst envs are empty:
-if the TvSubstEnv and CvSubstEnv are empty --- i.e. (isEmptyTCvSubst subst)
-holds --- then (substTy subst ty) does nothing.
-
-For example, consider:
-        (/\a. /\b:(a~Int). ...b..) Int
-We substitute Int for 'a'.  The Unique of 'b' does not change, but
-nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
-
-This invariant has several crucial consequences:
-
-* In substVarBndr, we need extend the TvSubstEnv
-        - if the unique has changed
-        - or if the kind has changed
-
-* In substTyVar, we do not need to consult the in-scope set;
-  the TvSubstEnv is enough
-
-* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
-
-Note [Substituting types and coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Types and coercions are mutually recursive, and either may have variables
-"belonging" to the other. Thus, every time we wish to substitute in a
-type, we may also need to substitute in a coercion, and vice versa.
-However, the constructor used to create type variables is distinct from
-that of coercion variables, so we carry two VarEnvs in a TCvSubst. Note
-that it would be possible to use the CoercionTy constructor to combine
-these environments, but that seems like a false economy.
-
-Note that the TvSubstEnv should *never* map a CoVar (built with the Id
-constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
-the range of the TvSubstEnv should *never* include a type headed with
-CoercionTy.
--}
-
-emptyTvSubstEnv :: TvSubstEnv
-emptyTvSubstEnv = emptyVarEnv
-
-emptyCvSubstEnv :: CvSubstEnv
-emptyCvSubstEnv = emptyVarEnv
-
-composeTCvSubstEnv :: InScopeSet
-                   -> (TvSubstEnv, CvSubstEnv)
-                   -> (TvSubstEnv, CvSubstEnv)
-                   -> (TvSubstEnv, CvSubstEnv)
--- ^ @(compose env1 env2)(x)@ is @env1(env2(x))@; i.e. apply @env2@ then @env1@.
--- It assumes that both are idempotent.
--- Typically, @env1@ is the refinement to a base substitution @env2@
-composeTCvSubstEnv in_scope (tenv1, cenv1) (tenv2, cenv2)
-  = ( tenv1 `plusVarEnv` mapVarEnv (substTy subst1) tenv2
-    , cenv1 `plusVarEnv` mapVarEnv (substCo subst1) cenv2 )
-        -- First apply env1 to the range of env2
-        -- Then combine the two, making sure that env1 loses if
-        -- both bind the same variable; that's why env1 is the
-        --  *left* argument to plusVarEnv, because the right arg wins
-  where
-    subst1 = TCvSubst in_scope tenv1 cenv1
-
--- | Composes two substitutions, applying the second one provided first,
--- like in function composition.
-composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
-composeTCvSubst (TCvSubst is1 tenv1 cenv1) (TCvSubst is2 tenv2 cenv2)
-  = TCvSubst is3 tenv3 cenv3
-  where
-    is3 = is1 `unionInScope` is2
-    (tenv3, cenv3) = composeTCvSubstEnv is3 (tenv1, cenv1) (tenv2, cenv2)
-
-emptyTCvSubst :: TCvSubst
-emptyTCvSubst = TCvSubst emptyInScopeSet emptyTvSubstEnv emptyCvSubstEnv
-
-mkEmptyTCvSubst :: InScopeSet -> TCvSubst
-mkEmptyTCvSubst is = TCvSubst is emptyTvSubstEnv emptyCvSubstEnv
-
-isEmptyTCvSubst :: TCvSubst -> Bool
-         -- See Note [Extending the TvSubstEnv]
-isEmptyTCvSubst (TCvSubst _ tenv cenv) = isEmptyVarEnv tenv && isEmptyVarEnv cenv
-
-mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
-mkTCvSubst in_scope (tenv, cenv) = TCvSubst in_scope tenv cenv
-
-mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
--- ^ Make a TCvSubst with specified tyvar subst and empty covar subst
-mkTvSubst in_scope tenv = TCvSubst in_scope tenv emptyCvSubstEnv
-
-mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst
--- ^ Make a TCvSubst with specified covar subst and empty tyvar subst
-mkCvSubst in_scope cenv = TCvSubst in_scope emptyTvSubstEnv cenv
-
-getTvSubstEnv :: TCvSubst -> TvSubstEnv
-getTvSubstEnv (TCvSubst _ env _) = env
-
-getCvSubstEnv :: TCvSubst -> CvSubstEnv
-getCvSubstEnv (TCvSubst _ _ env) = env
-
-getTCvInScope :: TCvSubst -> InScopeSet
-getTCvInScope (TCvSubst in_scope _ _) = in_scope
-
--- | Returns the free variables of the types in the range of a substitution as
--- a non-deterministic set.
-getTCvSubstRangeFVs :: TCvSubst -> VarSet
-getTCvSubstRangeFVs (TCvSubst _ tenv cenv)
-    = unionVarSet tenvFVs cenvFVs
-  where
-    tenvFVs = tyCoVarsOfTypesSet tenv
-    cenvFVs = tyCoVarsOfCosSet cenv
-
-isInScope :: Var -> TCvSubst -> Bool
-isInScope v (TCvSubst in_scope _ _) = v `elemInScopeSet` in_scope
-
-notElemTCvSubst :: Var -> TCvSubst -> Bool
-notElemTCvSubst v (TCvSubst _ tenv cenv)
-  | isTyVar v
-  = not (v `elemVarEnv` tenv)
-  | otherwise
-  = not (v `elemVarEnv` cenv)
-
-setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
-setTvSubstEnv (TCvSubst in_scope _ cenv) tenv = TCvSubst in_scope tenv cenv
-
-setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
-setCvSubstEnv (TCvSubst in_scope tenv _) cenv = TCvSubst in_scope tenv cenv
-
-zapTCvSubst :: TCvSubst -> TCvSubst
-zapTCvSubst (TCvSubst in_scope _ _) = TCvSubst in_scope emptyVarEnv emptyVarEnv
-
-extendTCvInScope :: TCvSubst -> Var -> TCvSubst
-extendTCvInScope (TCvSubst in_scope tenv cenv) var
-  = TCvSubst (extendInScopeSet in_scope var) tenv cenv
-
-extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
-extendTCvInScopeList (TCvSubst in_scope tenv cenv) vars
-  = TCvSubst (extendInScopeSetList in_scope vars) tenv cenv
-
-extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
-extendTCvInScopeSet (TCvSubst in_scope tenv cenv) vars
-  = TCvSubst (extendInScopeSetSet in_scope vars) tenv cenv
-
-extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
-extendTCvSubst subst v ty
-  | isTyVar v
-  = extendTvSubst subst v ty
-  | CoercionTy co <- ty
-  = extendCvSubst subst v co
-  | otherwise
-  = pprPanic "extendTCvSubst" (ppr v <+> text "|->" <+> ppr ty)
-
-extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst
-extendTCvSubstWithClone subst tcv
-  | isTyVar tcv = extendTvSubstWithClone subst tcv
-  | otherwise   = extendCvSubstWithClone subst tcv
-
-extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
-extendTvSubst (TCvSubst in_scope tenv cenv) tv ty
-  = TCvSubst in_scope (extendVarEnv tenv tv ty) cenv
-
-extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
-extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty
-  = ASSERT( isTyVar v )
-    extendTvSubstAndInScope subst v ty
-extendTvSubstBinderAndInScope subst (Anon {}) _
-  = subst
-
-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 (extendInScopeSetSet in_scope new_in_scope)
-             (extendVarEnv tenv tv (mkTyVarTy tv'))
-             cenv
-  where
-    new_in_scope = tyCoVarsOfType (tyVarKind tv') `extendVarSet` tv'
-
-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 (extendInScopeSetSet in_scope new_in_scope)
-             tenv
-             (extendVarEnv cenv cv (mkCoVarCo cv'))
-  where
-    new_in_scope = tyCoVarsOfType (varType cv') `extendVarSet` cv'
-
-extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
--- Also extends the in-scope set
-extendTvSubstAndInScope (TCvSubst in_scope tenv cenv) tv ty
-  = TCvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfType ty)
-             (extendVarEnv tenv tv ty)
-             cenv
-
-extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
-extendTvSubstList subst tvs tys
-  = foldl2 extendTvSubst subst tvs tys
-
-extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
-extendTCvSubstList subst tvs tys
-  = foldl2 extendTCvSubst subst tvs tys
-
-unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
--- Works when the ranges are disjoint
-unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
-  = ASSERT( not (tenv1 `intersectsVarEnv` tenv2)
-         && not (cenv1 `intersectsVarEnv` cenv2) )
-    TCvSubst (in_scope1 `unionInScope` in_scope2)
-             (tenv1     `plusVarEnv`   tenv2)
-             (cenv1     `plusVarEnv`   cenv2)
-
--- mkTvSubstPrs and zipTvSubst generate the in-scope set from
--- the types given; but it's just a thunk so with a bit of luck
--- it'll never be evaluated
-
--- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
--- environment. No CoVars, please!
-zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
-zipTvSubst tvs tys
-  = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv
-  where
-    tenv = zipTyEnv tvs tys
-
--- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
--- environment.  No TyVars, please!
-zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
-zipCvSubst cvs cos
-  = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv
-  where
-    cenv = zipCoEnv cvs cos
-
-zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
-zipTCvSubst tcvs tys
-  = zip_tcvsubst tcvs tys (mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes tys))
-  where zip_tcvsubst :: [TyCoVar] -> [Type] -> TCvSubst -> TCvSubst
-        zip_tcvsubst (tv:tvs) (ty:tys) subst
-          = zip_tcvsubst tvs tys (extendTCvSubst subst tv ty)
-        zip_tcvsubst [] [] subst = subst -- empty case
-        zip_tcvsubst _  _  _     = pprPanic "zipTCvSubst: length mismatch"
-                                            (ppr tcvs <+> ppr tys)
-
--- | Generates the in-scope set for the 'TCvSubst' from the types in the
--- incoming environment. No CoVars, please!
-mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst
-mkTvSubstPrs prs =
-    ASSERT2( onlyTyVarsAndNoCoercionTy, text "prs" <+> ppr prs )
-    mkTvSubst in_scope tenv
-  where tenv = mkVarEnv prs
-        in_scope = mkInScopeSet $ tyCoVarsOfTypes $ map snd prs
-        onlyTyVarsAndNoCoercionTy =
-          and [ isTyVar tv && not (isCoercionTy ty)
-              | (tv, ty) <- prs ]
-
-zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
-zipTyEnv tyvars tys
-  | debugIsOn
-  , not (all isTyVar tyvars)
-  = pprPanic "zipTyEnv" (ppr tyvars <+> ppr tys)
-  | otherwise
-  = ASSERT( all (not . isCoercionTy) tys )
-    mkVarEnv (zipEqual "zipTyEnv" tyvars tys)
-        -- There used to be a special case for when
-        --      ty == TyVarTy tv
-        -- (a not-uncommon case) in which case the substitution was dropped.
-        -- But the type-tidier changes the print-name of a type variable without
-        -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
-        -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
-        -- And it happened that t was the type variable of the class.  Post-tiding,
-        -- it got turned into {Foo t2}.  The ext-core printer expanded this using
-        -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
-        -- and so generated a rep type mentioning t not t2.
-        --
-        -- Simplest fix is to nuke the "optimisation"
-
-zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
-zipCoEnv cvs cos
-  | debugIsOn
-  , not (all isCoVar cvs)
-  = pprPanic "zipCoEnv" (ppr cvs <+> ppr cos)
-  | otherwise
-  = mkVarEnv (zipEqual "zipCoEnv" cvs cos)
-
-instance Outputable TCvSubst where
-  ppr (TCvSubst ins tenv cenv)
-    = brackets $ sep[ text "TCvSubst",
-                      nest 2 (text "In scope:" <+> ppr ins),
-                      nest 2 (text "Type env:" <+> ppr tenv),
-                      nest 2 (text "Co env:" <+> ppr cenv) ]
-
-{-
-%************************************************************************
-%*                                                                      *
-                Performing type or kind substitutions
-%*                                                                      *
-%************************************************************************
-
-Note [Sym and ForAllCo]
-~~~~~~~~~~~~~~~~~~~~~~~
-In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
-how do we push sym into a ForAllCo? It's a little ugly.
-
-Here is the typing rule:
-
-h : k1 ~# k2
-(tv : k1) |- g : ty1 ~# ty2
-----------------------------
-ForAllCo tv h g : (ForAllTy (tv : k1) ty1) ~#
-                  (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h]))
-
-Here is what we want:
-
-ForAllCo tv h' g' : (ForAllTy (tv : k2) (ty2[tv |-> tv |> sym h])) ~#
-                    (ForAllTy (tv : k1) ty1)
-
-
-Because the kinds of the type variables to the right of the colon are the kinds
-coerced by h', we know (h' : k2 ~# k1). Thus, (h' = sym h).
-
-Now, we can rewrite ty1 to be (ty1[tv |-> tv |> sym h' |> h']). We thus want
-
-ForAllCo tv h' g' :
-  (ForAllTy (tv : k2) (ty2[tv |-> tv |> h'])) ~#
-  (ForAllTy (tv : k1) (ty1[tv |-> tv |> h'][tv |-> tv |> sym h']))
-
-We thus see that we want
-
-g' : ty2[tv |-> tv |> h'] ~# ty1[tv |-> tv |> h']
-
-and thus g' = sym (g[tv |-> tv |> h']).
-
-Putting it all together, we get this:
-
-sym (ForAllCo tv h g)
-==>
-ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
-
-Note [Substituting in a coercion hole]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It seems highly suspicious to be substituting in a coercion that still
-has coercion holes. Yet, this can happen in a situation like this:
-
-  f :: forall k. k :~: Type -> ()
-  f Refl = let x :: forall (a :: k). [a] -> ...
-               x = ...
-
-When we check x's type signature, we require that k ~ Type. We indeed
-know this due to the Refl pattern match, but the eager unifier can't
-make use of givens. So, when we're done looking at x's type, a coercion
-hole will remain. Then, when we're checking x's definition, we skolemise
-x's type (in order to, e.g., bring the scoped type variable `a` into scope).
-This requires performing a substitution for the fresh skolem variables.
-
-This subsitution needs to affect the kind of the coercion hole, too --
-otherwise, the kind will have an out-of-scope variable in it. More problematically
-in practice (we won't actually notice the out-of-scope variable ever), skolems
-in the kind might have too high a level, triggering a failure to uphold the
-invariant that no free variables in a type have a higher level than the
-ambient level in the type checker. In the event of having free variables in the
-hole's kind, I'm pretty sure we'll always have an erroneous program, so we
-don't need to worry what will happen when the hole gets filled in. After all,
-a hole relating a locally-bound type variable will be unable to be solved. This
-is why it's OK not to look through the IORef of a coercion hole during
-substitution.
-
--}
-
--- | Type substitution, see 'zipTvSubst'
-substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
--- Works only if the domain of the substitution is a
--- superset of the type being substituted into
-substTyWith tvs tys = {-#SCC "substTyWith" #-}
-                      ASSERT( tvs `equalLength` tys )
-                      substTy (zipTvSubst tvs tys)
-
--- | Type substitution, see 'zipTvSubst'. Disables sanity checks.
--- The problems that the sanity checks in substTy catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substTyUnchecked to
--- substTy and remove this function. Please don't use in new code.
-substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
-substTyWithUnchecked tvs tys
-  = ASSERT( tvs `equalLength` tys )
-    substTyUnchecked (zipTvSubst tvs tys)
-
--- | Substitute tyvars within a type using a known 'InScopeSet'.
--- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
--- invariant]; specifically it should include the free vars of 'tys',
--- and of 'ty' minus the domain of the subst.
-substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
-substTyWithInScope in_scope tvs tys ty =
-  ASSERT( tvs `equalLength` tys )
-  substTy (mkTvSubst in_scope tenv) ty
-  where tenv = zipTyEnv tvs tys
-
--- | Coercion substitution, see 'zipTvSubst'
-substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
-substCoWith tvs tys = ASSERT( tvs `equalLength` tys )
-                      substCo (zipTvSubst tvs tys)
-
--- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
--- The problems that the sanity checks in substCo catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substCoUnchecked to
--- substCo and remove this function. Please don't use in new code.
-substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
-substCoWithUnchecked tvs tys
-  = ASSERT( tvs `equalLength` tys )
-    substCoUnchecked (zipTvSubst tvs tys)
-
-
-
--- | Substitute covars within a type
-substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
-substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
-
--- | Type substitution, see 'zipTvSubst'
-substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
-substTysWith tvs tys = ASSERT( tvs `equalLength` tys )
-                       substTys (zipTvSubst tvs tys)
-
--- | Type substitution, see 'zipTvSubst'
-substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
-substTysWithCoVars cvs cos = ASSERT( cvs `equalLength` cos )
-                             substTys (zipCvSubst cvs cos)
-
--- | Substitute within a 'Type' after adding the free variables of the type
--- to the in-scope set. This is useful for the case when the free variables
--- aren't already in the in-scope set or easily available.
--- See also Note [The substitution invariant].
-substTyAddInScope :: TCvSubst -> Type -> Type
-substTyAddInScope subst ty =
-  substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
-
--- | When calling `substTy` it should be the case that the in-scope set in
--- the substitution is a superset of the free vars of the range of the
--- substitution.
--- See also Note [The substitution invariant].
-isValidTCvSubst :: TCvSubst -> Bool
-isValidTCvSubst (TCvSubst in_scope tenv cenv) =
-  (tenvFVs `varSetInScope` in_scope) &&
-  (cenvFVs `varSetInScope` in_scope)
-  where
-  tenvFVs = tyCoVarsOfTypesSet tenv
-  cenvFVs = tyCoVarsOfCosSet cenv
-
--- | This checks if the substitution satisfies the invariant from
--- Note [The substitution invariant].
-checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
-checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
-  = ASSERT2( isValidTCvSubst subst,
-             text "in_scope" <+> ppr in_scope $$
-             text "tenv" <+> ppr tenv $$
-             text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$
-             text "cenv" <+> ppr cenv $$
-             text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$
-             text "tys" <+> ppr tys $$
-             text "cos" <+> ppr cos )
-    ASSERT2( tysCosFVsInScope,
-             text "in_scope" <+> ppr in_scope $$
-             text "tenv" <+> ppr tenv $$
-             text "cenv" <+> ppr cenv $$
-             text "tys" <+> ppr tys $$
-             text "cos" <+> ppr cos $$
-             text "needInScope" <+> ppr needInScope )
-    a
-  where
-  substDomain = nonDetKeysUFM tenv ++ nonDetKeysUFM cenv
-    -- It's OK to use nonDetKeysUFM here, because we only use this list to
-    -- remove some elements from a set
-  needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
-                  `delListFromUniqSet_Directly` substDomain
-  tysCosFVsInScope = needInScope `varSetInScope` in_scope
-
-
--- | Substitute within a 'Type'
--- The substitution has to satisfy the invariants described in
--- Note [The substitution invariant].
-substTy :: HasCallStack => TCvSubst -> Type  -> Type
-substTy subst ty
-  | isEmptyTCvSubst subst = ty
-  | otherwise             = checkValidSubst subst [ty] [] $
-                            subst_ty subst ty
-
--- | Substitute within a 'Type' disabling the sanity checks.
--- The problems that the sanity checks in substTy catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substTyUnchecked to
--- substTy and remove this function. Please don't use in new code.
-substTyUnchecked :: TCvSubst -> Type -> Type
-substTyUnchecked subst ty
-                 | isEmptyTCvSubst subst = ty
-                 | otherwise             = subst_ty subst ty
-
--- | Substitute within several 'Type's
--- The substitution has to satisfy the invariants described in
--- Note [The substitution invariant].
-substTys :: HasCallStack => TCvSubst -> [Type] -> [Type]
-substTys subst tys
-  | isEmptyTCvSubst subst = tys
-  | otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
-
--- | Substitute within several 'Type's disabling the sanity checks.
--- The problems that the sanity checks in substTys catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substTysUnchecked to
--- substTys and remove this function. Please don't use in new code.
-substTysUnchecked :: TCvSubst -> [Type] -> [Type]
-substTysUnchecked subst tys
-                 | isEmptyTCvSubst subst = tys
-                 | otherwise             = map (subst_ty subst) tys
-
--- | Substitute within a 'ThetaType'
--- The substitution has to satisfy the invariants described in
--- Note [The substitution invariant].
-substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType
-substTheta = substTys
-
--- | Substitute within a 'ThetaType' disabling the sanity checks.
--- The problems that the sanity checks in substTys catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substThetaUnchecked to
--- substTheta and remove this function. Please don't use in new code.
-substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
-substThetaUnchecked = substTysUnchecked
-
-
-subst_ty :: TCvSubst -> 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 (TyConApp tc tys) = let args = map go tys
-                           in  args `seqList` TyConApp tc args
-    go ty@(FunTy { ft_arg = arg, ft_res = res })
-      = let !arg' = go arg
-            !res' = go res
-        in ty { ft_arg = arg', ft_res = res' }
-    go (ForAllTy (Bndr tv vis) ty)
-                         = case substVarBndrUnchecked subst tv of
-                             (subst', tv') ->
-                               (ForAllTy $! ((Bndr $! tv') vis)) $!
-                                            (subst_ty subst' ty)
-    go (LitTy n)         = LitTy $! n
-    go (CastTy ty co)    = (mkCastTy $! (go ty)) $! (subst_co subst co)
-    go (CoercionTy co)   = CoercionTy $! (subst_co subst co)
-
-substTyVar :: TCvSubst -> TyVar -> Type
-substTyVar (TCvSubst _ tenv _) tv
-  = ASSERT( isTyVar tv )
-    case lookupVarEnv tenv tv of
-      Just ty -> ty
-      Nothing -> TyVarTy tv
-
-substTyVars :: TCvSubst -> [TyVar] -> [Type]
-substTyVars subst = map $ substTyVar subst
-
-substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type]
-substTyCoVars subst = map $ substTyCoVar subst
-
-substTyCoVar :: TCvSubst -> TyCoVar -> Type
-substTyCoVar subst tv
-  | isTyVar tv = substTyVar subst tv
-  | otherwise = CoercionTy $ substCoVar subst tv
-
-lookupTyVar :: TCvSubst -> TyVar  -> Maybe Type
-        -- See Note [Extending the TCvSubst]
-lookupTyVar (TCvSubst _ tenv _) tv
-  = ASSERT( isTyVar tv )
-    lookupVarEnv tenv tv
-
--- | Substitute within a 'Coercion'
--- The substitution has to satisfy the invariants described in
--- Note [The substitution invariant].
-substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion
-substCo subst co
-  | isEmptyTCvSubst subst = co
-  | otherwise = checkValidSubst subst [] [co] $ subst_co subst co
-
--- | Substitute within a 'Coercion' disabling sanity checks.
--- The problems that the sanity checks in substCo catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substCoUnchecked to
--- substCo and remove this function. Please don't use in new code.
-substCoUnchecked :: TCvSubst -> Coercion -> Coercion
-substCoUnchecked subst co
-  | isEmptyTCvSubst subst = co
-  | otherwise = subst_co subst co
-
--- | Substitute within several 'Coercion's
--- The substitution has to satisfy the invariants described in
--- Note [The substitution invariant].
-substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]
-substCos subst cos
-  | isEmptyTCvSubst subst = cos
-  | otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
-
-subst_co :: TCvSubst -> 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)= let args' = map go args
-                               in  args' `seqList` mkTyConAppCo r tc args'
-    go (AppCo co arg)        = (mkAppCo $! go co) $! go arg
-    go (ForAllCo tv kind_co co)
-      = case substForAllCoBndrUnchecked subst tv kind_co of
-         (subst', tv', kind_co') ->
-          ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co
-    go (FunCo r co1 co2)     = (mkFunCo r $! go co1) $! go co2
-    go (CoVarCo cv)          = substCoVar subst cv
-    go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
-    go (UnivCo p r t1 t2)    = (((mkUnivCo $! go_prov p) $! r) $!
-                                (go_ty t1)) $! (go_ty t2)
-    go (SymCo co)            = mkSymCo $! (go co)
-    go (TransCo co1 co2)     = (mkTransCo $! (go co1)) $! (go co2)
-    go (NthCo r d co)        = mkNthCo r 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 (AxiomRuleCo c cs)    = let cs1 = map go cs
-                                in cs1 `seqList` AxiomRuleCo c cs1
-    go (HoleCo h)            = HoleCo $! go_hole h
-
-    go_prov UnsafeCoerceProv     = UnsafeCoerceProv
-    go_prov (PhantomProv kco)    = PhantomProv (go kco)
-    go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
-    go_prov p@(PluginProv _)     = p
-
-    -- See Note [Substituting in a coercion hole]
-    go_hole h@(CoercionHole { ch_co_var = cv })
-      = h { ch_co_var = updateVarType go_ty cv }
-
-substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion
-                  -> (TCvSubst, TyCoVar, Coercion)
-substForAllCoBndr subst
-  = substForAllCoBndrUsing False (substCo subst) subst
-
--- | Like 'substForAllCoBndr', but disables sanity checks.
--- The problems that the sanity checks in substCo catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substCoUnchecked to
--- substCo and remove this function. Please don't use in new code.
-substForAllCoBndrUnchecked :: TCvSubst -> TyCoVar -> KindCoercion
-                           -> (TCvSubst, TyCoVar, Coercion)
-substForAllCoBndrUnchecked subst
-  = substForAllCoBndrUsing False (substCoUnchecked subst) subst
-
--- See Note [Sym and ForAllCo]
-substForAllCoBndrUsing :: Bool  -- apply sym to binder?
-                       -> (Coercion -> Coercion)  -- transformation to kind co
-                       -> TCvSubst -> TyCoVar -> KindCoercion
-                       -> (TCvSubst, TyCoVar, KindCoercion)
-substForAllCoBndrUsing sym sco subst old_var
-  | isTyVar old_var = substForAllCoTyVarBndrUsing sym sco subst old_var
-  | otherwise       = substForAllCoCoVarBndrUsing sym sco subst old_var
-
-substForAllCoTyVarBndrUsing :: Bool  -- apply sym to binder?
-                            -> (Coercion -> Coercion)  -- transformation to kind co
-                            -> TCvSubst -> TyVar -> KindCoercion
-                            -> (TCvSubst, TyVar, KindCoercion)
-substForAllCoTyVarBndrUsing sym sco (TCvSubst in_scope tenv cenv) old_var old_kind_co
-  = ASSERT( isTyVar old_var )
-    ( TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv
-    , new_var, new_kind_co )
-  where
-    new_env | no_change && not sym = delVarEnv tenv old_var
-            | sym       = extendVarEnv tenv old_var $
-                          TyVarTy new_var `CastTy` new_kind_co
-            | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
-
-    no_kind_change = noFreeVarsOfCo old_kind_co
-    no_change = no_kind_change && (new_var == old_var)
-
-    new_kind_co | no_kind_change = old_kind_co
-                | otherwise      = sco old_kind_co
-
-    Pair new_ki1 _ = coercionKind new_kind_co
-    -- We could do substitution to (tyVarKind old_var). We don't do so because
-    -- we already substituted new_kind_co, which contains the kind information
-    -- we want. We don't want to do substitution once more. Also, in most cases,
-    -- new_kind_co is a Refl, in which case coercionKind is really fast.
-
-    new_var  = uniqAway in_scope (setTyVarKind old_var new_ki1)
-
-substForAllCoCoVarBndrUsing :: Bool  -- apply sym to binder?
-                            -> (Coercion -> Coercion)  -- transformation to kind co
-                            -> TCvSubst -> CoVar -> KindCoercion
-                            -> (TCvSubst, CoVar, KindCoercion)
-substForAllCoCoVarBndrUsing sym sco (TCvSubst in_scope tenv cenv)
-                            old_var old_kind_co
-  = ASSERT( isCoVar old_var )
-    ( TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv
-    , new_var, new_kind_co )
-  where
-    new_cenv | no_change && not sym = delVarEnv cenv old_var
-             | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var)
-
-    no_kind_change = noFreeVarsOfCo old_kind_co
-    no_change = no_kind_change && (new_var == old_var)
-
-    new_kind_co | no_kind_change = old_kind_co
-                | otherwise      = sco old_kind_co
-
-    Pair h1 h2 = coercionKind new_kind_co
-
-    new_var       = uniqAway in_scope $ mkCoVar (varName old_var) new_var_type
-    new_var_type  | sym       = h2
-                  | otherwise = h1
-
-substCoVar :: TCvSubst -> CoVar -> Coercion
-substCoVar (TCvSubst _ _ cenv) cv
-  = case lookupVarEnv cenv cv of
-      Just co -> co
-      Nothing -> CoVarCo cv
-
-substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
-substCoVars subst cvs = map (substCoVar subst) cvs
-
-lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
-lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
-
-substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
-substTyVarBndr = substTyVarBndrUsing substTy
-
-substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar])
-substTyVarBndrs = mapAccumL substTyVarBndr
-
-substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
-substVarBndr = substVarBndrUsing substTy
-
-substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar])
-substVarBndrs = mapAccumL substVarBndr
-
-substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
-substCoVarBndr = substCoVarBndrUsing substTy
-
--- | Like 'substVarBndr', but disables sanity checks.
--- The problems that the sanity checks in substTy catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substTyUnchecked to
--- substTy and remove this function. Please don't use in new code.
-substVarBndrUnchecked :: TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
-substVarBndrUnchecked = substVarBndrUsing substTyUnchecked
-
-substVarBndrUsing :: (TCvSubst -> Type -> Type)
-                  -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
-substVarBndrUsing subst_fn subst v
-  | isTyVar v = substTyVarBndrUsing subst_fn subst v
-  | otherwise = substCoVarBndrUsing subst_fn subst v
-
--- | Substitute a tyvar in a binding position, returning an
--- extended subst and a new tyvar.
--- Use the supplied function to substitute in the kind
-substTyVarBndrUsing
-  :: (TCvSubst -> Type -> Type)  -- ^ Use this to substitute in the kind
-  -> TCvSubst -> TyVar -> (TCvSubst, TyVar)
-substTyVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
-  = ASSERT2( _no_capture, pprTyVar old_var $$ pprTyVar new_var $$ ppr subst )
-    ASSERT( isTyVar old_var )
-    (TCvSubst (in_scope `extendInScopeSet` new_var) new_env cenv, new_var)
-  where
-    new_env | no_change = delVarEnv tenv old_var
-            | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
-
-    _no_capture = not (new_var `elemVarSet` tyCoVarsOfTypesSet tenv)
-    -- Assertion check that we are not capturing something in the substitution
-
-    old_ki = tyVarKind old_var
-    no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed
-    no_change = no_kind_change && (new_var == old_var)
-        -- no_change means that the new_var is identical in
-        -- all respects to the old_var (same unique, same kind)
-        -- See Note [Extending the TCvSubst]
-        --
-        -- In that case we don't need to extend the substitution
-        -- to map old to new.  But instead we must zap any
-        -- current substitution for the variable. For example:
-        --      (\x.e) with id_subst = [x |-> e']
-        -- Here we must simply zap the substitution for x
-
-    new_var | no_kind_change = uniqAway in_scope old_var
-            | otherwise = uniqAway in_scope $
-                          setTyVarKind old_var (subst_fn subst old_ki)
-        -- The uniqAway part makes sure the new variable is not already in scope
-
--- | Substitute a covar in a binding position, returning an
--- extended subst and a new covar.
--- Use the supplied function to substitute in the kind
-substCoVarBndrUsing
-  :: (TCvSubst -> Type -> Type)
-  -> TCvSubst -> CoVar -> (TCvSubst, CoVar)
-substCoVarBndrUsing subst_fn subst@(TCvSubst in_scope tenv cenv) old_var
-  = ASSERT( isCoVar old_var )
-    (TCvSubst (in_scope `extendInScopeSet` new_var) tenv new_cenv, new_var)
-  where
-    new_co         = mkCoVarCo new_var
-    no_kind_change = noFreeVarsOfTypes [t1, t2]
-    no_change      = new_var == old_var && no_kind_change
-
-    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) new_var_type
-
-    (_, _, t1, t2, role) = coVarKindsTypesRole old_var
-    t1' = subst_fn subst t1
-    t2' = subst_fn subst t2
-    new_var_type = mkCoercionType role t1' t2'
-                  -- It's important to do the substitution for coercions,
-                  -- because they can have free type variables
-
-cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
-cloneTyVarBndr subst@(TCvSubst in_scope tv_env cv_env) tv uniq
-  = ASSERT2( isTyVar tv, ppr tv )   -- I think it's only called on TyVars
-    (TCvSubst (extendInScopeSet in_scope tv')
-              (extendVarEnv tv_env tv (mkTyVarTy tv')) cv_env, tv')
-  where
-    old_ki = tyVarKind tv
-    no_kind_change = noFreeVarsOfType old_ki -- verify that kind is closed
-
-    tv1 | no_kind_change = tv
-        | otherwise      = setTyVarKind tv (substTy subst old_ki)
-
-    tv' = setVarUnique tv1 uniq
-
-cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
-cloneTyVarBndrs subst []     _usupply = (subst, [])
-cloneTyVarBndrs subst (t:ts)  usupply = (subst'', tv:tvs)
-  where
-    (uniq, usupply') = takeUniqFromSupply usupply
-    (subst' , tv )   = cloneTyVarBndr subst t uniq
-    (subst'', tvs)   = cloneTyVarBndrs subst' ts usupply'
-
-{-
-%************************************************************************
-%*                                                                      *
-                   Pretty-printing types
-
-       Defined very early because of debug printing in assertions
-%*                                                                      *
-%************************************************************************
-
-@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
-defined to use this.  @pprParendType@ is the same, except it puts
-parens around the type, except for the atomic cases.  @pprParendType@
-works just by setting the initial context precedence very high.
-
-Note that any function which pretty-prints a @Type@ first converts the @Type@
-to an @IfaceType@. See Note [IfaceType and pretty-printing] in IfaceType.
-
-See Note [Precedence in types] in BasicTypes.
--}
-
---------------------------------------------------------
--- When pretty-printing types, we convert to IfaceType,
---   and pretty-print that.
--- See Note [Pretty printing via IfaceSyn] in PprTyThing
---------------------------------------------------------
-
-pprType, pprParendType :: Type -> SDoc
-pprType       = pprPrecType topPrec
-pprParendType = pprPrecType appPrec
-
-pprPrecType :: PprPrec -> Type -> SDoc
-pprPrecType = pprPrecTypeX emptyTidyEnv
-
-pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc
-pprPrecTypeX env prec ty
-  = getPprStyle $ \sty ->
-    if debugStyle sty           -- Use debugPprType when in
-    then debug_ppr_ty prec ty   -- when in debug-style
-    else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty)
-    -- NB: debug-style is used for -dppr-debug
-    --     dump-style  is used for -ddump-tc-trace etc
-
-pprTyLit :: TyLit -> SDoc
-pprTyLit = pprIfaceTyLit . toIfaceTyLit
-
-pprKind, pprParendKind :: Kind -> SDoc
-pprKind       = pprType
-pprParendKind = pprParendType
-
-tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
-tidyToIfaceTypeStyX env ty sty
-  | userStyle sty = tidyToIfaceTypeX env ty
-  | otherwise     = toIfaceTypeX (tyCoVarsOfType ty) ty
-     -- in latter case, don't tidy, as we'll be printing uniques.
-
-tidyToIfaceType :: Type -> IfaceType
-tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv
-
-tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
--- It's vital to tidy before converting to an IfaceType
--- or nested binders will become indistinguishable!
---
--- Also for the free type variables, tell toIfaceTypeX to
--- leave them as IfaceFreeTyVar.  This is super-important
--- for debug printing.
-tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty)
-  where
-    env'      = tidyFreeTyCoVars env free_tcvs
-    free_tcvs = tyCoVarsOfTypeWellScoped ty
-
-------------
-pprCo, pprParendCo :: Coercion -> SDoc
-pprCo       co = getPprStyle $ \ sty -> pprIfaceCoercion (tidyToIfaceCoSty co sty)
-pprParendCo co = getPprStyle $ \ sty -> pprParendIfaceCoercion (tidyToIfaceCoSty co sty)
-
-tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion
-tidyToIfaceCoSty co sty
-  | userStyle sty = tidyToIfaceCo co
-  | otherwise     = toIfaceCoercionX (tyCoVarsOfCo co) co
-     -- in latter case, don't tidy, as we'll be printing uniques.
-
-tidyToIfaceCo :: Coercion -> IfaceCoercion
--- It's vital to tidy before converting to an IfaceType
--- or nested binders will become indistinguishable!
---
--- Also for the free type variables, tell toIfaceCoercionX to
--- leave them as IfaceFreeCoVar.  This is super-important
--- for debug printing.
-tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co)
-  where
-    env       = tidyFreeTyCoVars emptyTidyEnv free_tcvs
-    free_tcvs = scopedSort $ tyCoVarsOfCoList co
-------------
-pprClassPred :: Class -> [Type] -> SDoc
-pprClassPred clas tys = pprTypeApp (classTyCon clas) tys
-
-------------
-pprTheta :: ThetaType -> SDoc
-pprTheta = pprIfaceContext topPrec . map tidyToIfaceType
-
-pprParendTheta :: ThetaType -> SDoc
-pprParendTheta = pprIfaceContext appPrec . map tidyToIfaceType
-
-pprThetaArrowTy :: ThetaType -> SDoc
-pprThetaArrowTy = pprIfaceContextArr . map tidyToIfaceType
-
-------------------
-instance Outputable Type where
-    ppr ty = pprType ty
-
-instance Outputable TyLit where
-   ppr = pprTyLit
-
-------------------
-pprSigmaType :: Type -> SDoc
-pprSigmaType = pprIfaceSigmaType ShowForAllWhen . tidyToIfaceType
-
-pprForAll :: [TyCoVarBinder] -> SDoc
-pprForAll tvs = pprIfaceForAll (map toIfaceForAllBndr tvs)
-
--- | Print a user-level forall; see Note [When to print foralls]
-pprUserForAll :: [TyCoVarBinder] -> SDoc
-pprUserForAll = pprUserIfaceForAll . map toIfaceForAllBndr
-
-pprTCvBndrs :: [TyCoVarBinder] -> SDoc
-pprTCvBndrs tvs = sep (map pprTCvBndr tvs)
-
-pprTCvBndr :: TyCoVarBinder -> SDoc
-pprTCvBndr = pprTyVar . binderVar
-
-pprTyVars :: [TyVar] -> SDoc
-pprTyVars tvs = sep (map pprTyVar tvs)
-
-pprTyVar :: TyVar -> SDoc
--- Print a type variable binder with its kind (but not if *)
--- Here we do not go via IfaceType, because the duplication with
--- pprIfaceTvBndr is minimal, and the loss of uniques etc in
--- debug printing is disastrous
-pprTyVar tv
-  | isLiftedTypeKind kind = ppr tv
-  | otherwise             = parens (ppr tv <+> dcolon <+> ppr kind)
-  where
-    kind = tyVarKind tv
-
-instance Outputable TyCoBinder where
-  ppr (Anon af ty) = ppr af <+> ppr ty
-  ppr (Named (Bndr v Required))  = ppr v
-  ppr (Named (Bndr v Specified)) = char '@' <> ppr v
-  ppr (Named (Bndr v Inferred))  = braces (ppr v)
-
------------------
-instance Outputable Coercion where -- defined here to avoid orphans
-  ppr = pprCo
-
-debugPprType :: Type -> SDoc
--- ^ debugPprType is a simple pretty printer that prints a type
--- without going through IfaceType.  It does not format as prettily
--- as the normal route, but it's much more direct, and that can
--- be useful for debugging.  E.g. with -dppr-debug it prints the
--- kind on type-variable /occurrences/ which the normal route
--- fundamentally cannot do.
-debugPprType ty = debug_ppr_ty topPrec ty
-
-debug_ppr_ty :: PprPrec -> Type -> SDoc
-debug_ppr_ty _ (LitTy l)
-  = ppr l
-
-debug_ppr_ty _ (TyVarTy tv)
-  = ppr tv  -- With -dppr-debug we get (tv :: kind)
-
-debug_ppr_ty prec (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
-  = maybeParen prec funPrec $
-    sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res]
-  where
-    arrow = case af of
-              VisArg   -> text "->"
-              InvisArg -> text "=>"
-
-debug_ppr_ty prec (TyConApp tc tys)
-  | null tys  = ppr tc
-  | otherwise = maybeParen prec appPrec $
-                hang (ppr tc) 2 (sep (map (debug_ppr_ty appPrec) tys))
-
-debug_ppr_ty _ (AppTy t1 t2)
-  = hang (debug_ppr_ty appPrec t1)  -- Print parens so we see ((a b) c)
-       2 (debug_ppr_ty appPrec t2)  -- so that we can distinguish
-                                    -- TyConApp from AppTy
-
-debug_ppr_ty prec (CastTy ty co)
-  = maybeParen prec topPrec $
-    hang (debug_ppr_ty topPrec ty)
-       2 (text "|>" <+> ppr co)
-
-debug_ppr_ty _ (CoercionTy co)
-  = parens (text "CO" <+> ppr co)
-
-debug_ppr_ty prec ty@(ForAllTy {})
-  | (tvs, body) <- split ty
-  = maybeParen prec funPrec $
-    hang (text "forall" <+> fsep (map ppr tvs) <> dot)
-         -- The (map ppr tvs) will print kind-annotated
-         -- tvs, because we are (usually) in debug-style
-       2 (ppr body)
-  where
-    split ty | ForAllTy tv ty' <- ty
-             , (tvs, body) <- split ty'
-             = (tv:tvs, body)
-             | otherwise
-             = ([], ty)
-
-{-
-Note [When to print foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Mostly we want to print top-level foralls when (and only when) the user specifies
--fprint-explicit-foralls.  But when kind polymorphism is at work, that suppresses
-too much information; see #9018.
-
-So I'm trying out this rule: print explicit foralls if
-  a) User specifies -fprint-explicit-foralls, or
-  b) Any of the quantified type variables has a kind
-     that mentions a kind variable
-
-This catches common situations, such as a type siguature
-     f :: m a
-which means
-      f :: forall k. forall (m :: k->*) (a :: k). m a
-We really want to see both the "forall k" and the kind signatures
-on m and a.  The latter comes from pprTCvBndr.
-
-Note [Infix type variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-With TypeOperators you can say
-
-   f :: (a ~> b) -> b
-
-and the (~>) is considered a type variable.  However, the type
-pretty-printer in this module will just see (a ~> b) as
-
-   App (App (TyVarTy "~>") (TyVarTy "a")) (TyVarTy "b")
-
-So it'll print the type in prefix form.  To avoid confusion we must
-remember to parenthesise the operator, thus
-
-   (~>) a b -> b
-
-See #2766.
--}
-
-pprDataCons :: TyCon -> SDoc
-pprDataCons = sepWithVBars . fmap pprDataConWithArgs . tyConDataCons
-  where
-    sepWithVBars [] = empty
-    sepWithVBars docs = sep (punctuate (space <> vbar) docs)
-
-pprDataConWithArgs :: DataCon -> SDoc
-pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc]
-  where
-    (_univ_tvs, _ex_tvs, _eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc
-    user_bndrs = dataConUserTyVarBinders dc
-    forAllDoc  = pprUserForAll user_bndrs
-    thetaDoc   = pprThetaArrowTy theta
-    argsDoc    = hsep (fmap pprParendType arg_tys)
-
-
-pprTypeApp :: TyCon -> [Type] -> SDoc
-pprTypeApp tc tys
-  = pprIfaceTypeApp topPrec (toIfaceTyCon tc)
-                            (toIfaceTcArgs tc tys)
-    -- TODO: toIfaceTcArgs seems rather wasteful here
-
-------------------
--- | Display all kind information (with @-fprint-explicit-kinds@) when the
--- provided 'Bool' argument is 'True'.
--- See @Note [Kind arguments in error messages]@ in "TcErrors".
-pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
-pprWithExplicitKindsWhen b
-  = updSDocDynFlags $ \dflags ->
-      if b then gopt_set dflags Opt_PrintExplicitKinds
-           else dflags
-
-{-
-%************************************************************************
-%*                                                                      *
-\subsection{TidyType}
-%*                                                                      *
-%************************************************************************
 -}
 
--- | This tidies up a type for printing in an error message, or in
--- an interface file.
---
--- It doesn't change the uniques at all, just the print names.
-tidyVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
-tidyVarBndrs tidy_env tvs
-  = mapAccumL tidyVarBndr (avoidNameClashes tvs tidy_env) tvs
-
-tidyVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
-tidyVarBndr tidy_env@(occ_env, subst) var
-  = case tidyOccName occ_env (getHelpfulOccName var) of
-      (occ_env', occ') -> ((occ_env', subst'), var')
-        where
-          subst' = extendVarEnv subst var var'
-          var'   = setVarType (setVarName var name') type'
-          type'  = tidyType tidy_env (varType var)
-          name'  = tidyNameOcc name occ'
-          name   = varName var
-
-avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
--- Seed the occ_env with clashes among the names, see
--- Note [Tidying multiple names at once] in OccName
-avoidNameClashes tvs (occ_env, subst)
-  = (avoidClashesOccEnv occ_env occs, subst)
-  where
-    occs = map getHelpfulOccName tvs
-
-getHelpfulOccName :: TyCoVar -> OccName
--- A TcTyVar with a System Name is probably a
--- unification variable; when we tidy them we give them a trailing
--- "0" (or 1 etc) so that they don't take precedence for the
--- un-modified name. Plus, indicating a unification variable in
--- this way is a helpful clue for users
-getHelpfulOccName tv
-  | isSystemName name, isTcTyVar tv
-  = mkTyVarOcc (occNameString occ ++ "0")
-  | otherwise
-  = occ
-  where
-   name = varName tv
-   occ  = getOccName name
-
-tidyTyCoVarBinder :: TidyEnv -> VarBndr TyCoVar vis
-                  -> (TidyEnv, VarBndr TyCoVar vis)
-tidyTyCoVarBinder tidy_env (Bndr tv vis)
-  = (tidy_env', Bndr tv' vis)
-  where
-    (tidy_env', tv') = tidyVarBndr tidy_env tv
-
-tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
-                   -> (TidyEnv, [VarBndr TyCoVar vis])
-tidyTyCoVarBinders tidy_env tvbs
-  = mapAccumL tidyTyCoVarBinder
-              (avoidNameClashes (binderVars tvbs) tidy_env) tvbs
-
----------------
-tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
--- ^ Add the free 'TyVar's to the env in tidy form,
--- so that we can tidy the type they are free in
-tidyFreeTyCoVars (full_occ_env, var_env) tyvars
-  = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars)
-
----------------
-tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
-tidyOpenTyCoVars env tyvars = mapAccumL tidyOpenTyCoVar env tyvars
-
----------------
-tidyOpenTyCoVar :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
--- ^ Treat a new 'TyCoVar' as a binder, and give it a fresh tidy name
--- using the environment if one has not already been allocated. See
--- also 'tidyVarBndr'
-tidyOpenTyCoVar env@(_, subst) tyvar
-  = case lookupVarEnv subst tyvar of
-        Just tyvar' -> (env, tyvar')              -- Already substituted
-        Nothing     ->
-          let env' = tidyFreeTyCoVars env (tyCoVarsOfTypeList (tyVarKind tyvar))
-          in tidyVarBndr env' tyvar  -- Treat it as a binder
-
----------------
-tidyTyCoVarOcc :: TidyEnv -> TyCoVar -> TyCoVar
-tidyTyCoVarOcc env@(_, subst) tv
-  = case lookupVarEnv subst tv of
-        Nothing  -> updateVarType (tidyType env) tv
-        Just tv' -> tv'
-
----------------
-tidyTypes :: TidyEnv -> [Type] -> [Type]
-tidyTypes env tys = map (tidyType env) tys
-
----------------
-tidyType :: TidyEnv -> Type -> Type
-tidyType _   (LitTy n)             = LitTy n
-tidyType env (TyVarTy tv)          = TyVarTy (tidyTyCoVarOcc env tv)
-tidyType env (TyConApp tycon tys)  = let args = tidyTypes env tys
-                                     in args `seqList` TyConApp tycon args
-tidyType env (AppTy fun arg)       = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
-tidyType env ty@(FunTy _ arg res)  = let { !arg' = tidyType env arg
-                                         ; !res' = tidyType env res }
-                                     in ty { ft_arg = arg', ft_res = res' }
-tidyType env (ty@(ForAllTy{}))     = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty
-  where
-    (tvs, vis, body_ty) = splitForAllTys' ty
-    (env', tvs') = tidyVarBndrs env tvs
-tidyType env (CastTy ty co)       = (CastTy $! tidyType env ty) $! (tidyCo env co)
-tidyType env (CoercionTy co)      = CoercionTy $! (tidyCo env co)
-
-
--- The following two functions differ from mkForAllTys and splitForAllTys in that
--- they expect/preserve the ArgFlag argument. Thes belong to types/Type.hs, but
--- how should they be named?
-mkForAllTys' :: [(TyCoVar, ArgFlag)] -> Type -> Type
-mkForAllTys' tvvs ty = foldr strictMkForAllTy ty tvvs
-  where
-    strictMkForAllTy (tv,vis) ty = (ForAllTy $! ((Bndr $! tv) $! vis)) $! ty
-
-splitForAllTys' :: Type -> ([TyCoVar], [ArgFlag], Type)
-splitForAllTys' ty = go ty [] []
-  where
-    go (ForAllTy (Bndr tv vis) ty) tvs viss = go ty (tv:tvs) (vis:viss)
-    go ty                          tvs viss = (reverse tvs, reverse viss, ty)
-
-
----------------
--- | Grabs the free type variables, tidies them
--- and then uses 'tidyType' to work over the type itself
-tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
-tidyOpenTypes env tys
-  = (env', tidyTypes (trimmed_occ_env, var_env) tys)
-  where
-    (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $
-                                tyCoVarsOfTypesWellScoped tys
-    trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
-      -- The idea here was that we restrict the new TidyEnv to the
-      -- _free_ vars of the types, so that we don't gratuitously rename
-      -- the _bound_ variables of the types.
-
----------------
-tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
-tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in
-                      (env', ty')
-
----------------
--- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
-tidyTopType :: Type -> Type
-tidyTopType ty = tidyType emptyTidyEnv ty
-
----------------
-tidyOpenKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
-tidyOpenKind = tidyOpenType
-
-tidyKind :: TidyEnv -> Kind -> Kind
-tidyKind = tidyType
-
-----------------
-tidyCo :: TidyEnv -> Coercion -> Coercion
-tidyCo env@(_, subst) co
-  = go co
-  where
-    go_mco MRefl    = MRefl
-    go_mco (MCo co) = MCo (go co)
-
-    go (Refl ty)             = Refl (tidyType env ty)
-    go (GRefl r ty mco)      = GRefl r (tidyType env ty) $! go_mco mco
-    go (TyConAppCo r tc cos) = let args = map go cos
-                               in args `seqList` TyConAppCo r tc args
-    go (AppCo co1 co2)       = (AppCo $! go co1) $! go co2
-    go (ForAllCo tv h co)    = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co)
-                               where (envp, tvp) = tidyVarBndr env tv
-            -- the case above duplicates a bit of work in tidying h and the kind
-            -- of tv. But the alternative is to use coercionKind, which seems worse.
-    go (FunCo r co1 co2)     = (FunCo r $! go co1) $! go co2
-    go (CoVarCo cv)          = case lookupVarEnv subst cv of
-                                 Nothing  -> CoVarCo cv
-                                 Just cv' -> CoVarCo cv'
-    go (HoleCo h)            = HoleCo h
-    go (AxiomInstCo con ind cos) = let args = map go cos
-                               in  args `seqList` AxiomInstCo con ind args
-    go (UnivCo p r t1 t2)    = (((UnivCo $! (go_prov p)) $! r) $!
-                                tidyType env t1) $! tidyType env t2
-    go (SymCo co)            = SymCo $! go co
-    go (TransCo co1 co2)     = (TransCo $! go co1) $! go co2
-    go (NthCo r d co)        = NthCo r d $! go co
-    go (LRCo lr co)          = LRCo lr $! go co
-    go (InstCo co ty)        = (InstCo $! go co) $! go ty
-    go (KindCo co)           = KindCo $! go co
-    go (SubCo co)            = SubCo $! go co
-    go (AxiomRuleCo ax cos)  = let cos1 = tidyCos env cos
-                               in cos1 `seqList` AxiomRuleCo ax cos1
-
-    go_prov UnsafeCoerceProv    = UnsafeCoerceProv
-    go_prov (PhantomProv co)    = PhantomProv (go co)
-    go_prov (ProofIrrelProv co) = ProofIrrelProv (go co)
-    go_prov p@(PluginProv _)    = p
-
-tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
-tidyCos env = map (tidyCo env)
-
 
 {- *********************************************************************
 *                                                                      *