Rework the handling of SkolemInfo

The main purpose of this patch is to attach a SkolemInfo directly to
each SkolemTv. This fixes the large number of bugs which have
accumulated over the years where we failed to report errors due to
having "no skolem info" for particular type variables. Now the origin of
each type varible is stored on the type variable we can always report
accurately where it cames from.

Fixes #20969 #20732 #20680 #19482 #20232 #19752 #10946
  #19760 #20063 #13499 #14040

The main changes of this patch are:

* SkolemTv now contains a SkolemInfo field which tells us how the
  SkolemTv was created. Used when reporting errors.

* Enforce invariants relating the SkolemInfoAnon and level of an implication (ic_info, ic_tclvl)
  to the SkolemInfo and level of the type variables in ic_skols.
    * All ic_skols are TcTyVars -- Check is currently disabled
    * All ic_skols are SkolemTv
    * The tv_lvl of the ic_skols agrees with the ic_tclvl
    * The ic_info agrees with the SkolInfo of the implication.

  These invariants are checked by a debug compiler by
  checkImplicationInvariants.

* Completely refactor kcCheckDeclHeader_sig which kept
  doing my head in. Plus, it wasn't right because it wasn't skolemising
  the binders as it decomposed the kind signature.

  The new story is described in Note [kcCheckDeclHeader_sig].  The code
  is considerably shorter than before (roughly 240 lines turns into 150
  lines).

  It still has the same awkward complexity around computing arity as
  before, but that is a language design issue.
  See Note [Arity inference in kcCheckDeclHeader_sig]

* I added new type synonyms MonoTcTyCon and PolyTcTyCon, and used
  them to be clear which TcTyCons have "finished" kinds etc, and
  which are monomorphic. See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]

* I renamed etaExpandAlgTyCon to splitTyConKind, becuase that's a
  better name, and it is very useful in kcCheckDeclHeader_sig, where
  eta-expansion isn't an issue.

* Kill off the nasty `ClassScopedTvEnv` entirely.

Co-authored-by: Simon Peyton Jones <simon.peytonjones@gmail.com>

8 files changed, 299 insertions, 220 deletions

diff --git a/compiler/GHC/Tc/Utils/Backpack.hs b/compiler/GHC/Tc/Utils/Backpack.hs
index 659fc8a474..20b81f8b3c 100644
--- a/compiler/GHC/Tc/Utils/Backpack.hs
+++ b/compiler/GHC/Tc/Utils/Backpack.hs
@@ -229,14 +229,14 @@ check_inst sig_inst = do
     mapM_ tcLookupImported_maybe (nameSetElemsStable (orphNamesOfClsInst sig_inst))
     -- Based off of 'simplifyDeriv'
     let ty = idType (instanceDFunId sig_inst)
-        skol_info = InstSkol
         -- Based off of tcSplitDFunTy
         (tvs, theta, pred) =
            case tcSplitForAllInvisTyVars ty of { (tvs, rho)    ->
            case splitFunTys rho             of { (theta, pred) ->
            (tvs, theta, pred) }}
         origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
-    (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
+    skol_info <- mkSkolemInfo InstSkol
+    (skol_subst, tvs_skols) <- tcInstSkolTyVars skol_info tvs -- Skolemize
     (tclvl,cts) <- pushTcLevelM $ do
        wanted <- newWanted origin
                            (Just TypeLevel)
@@ -253,7 +253,7 @@ check_inst sig_inst = do
        return $ wanted : givens
     unsolved <- simplifyWantedsTcM cts
 
-    (implic, _) <- buildImplicationFor tclvl skol_info tvs_skols [] unsolved
+    (implic, _) <- buildImplicationFor tclvl (getSkolemInfo skol_info) tvs_skols [] unsolved
     reportAllUnsolved (mkImplicWC implic)
 
 -- | For a module @modname@ of type 'HscSource', determine the list
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index 90c8b9b529..7c270e39bd 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -536,6 +536,7 @@ tcExtendKindEnv extra_env thing_inside
 -- Scoped type and kind variables
 tcExtendTyVarEnv :: [TyVar] -> TcM r -> TcM r
 tcExtendTyVarEnv tvs thing_inside
+  -- MP: This silently coerces TyVar to TcTyVar.
   = tcExtendNameTyVarEnv (mkTyVarNamePairs tvs) thing_inside
 
 tcExtendNameTyVarEnv :: [(Name,TcTyVar)] -> TcM r -> TcM r
@@ -745,7 +746,7 @@ tcInitTidyEnv
        = do { let (env', occ') = tidyOccName env (nameOccName name)
                   name'  = tidyNameOcc name occ'
                   tyvar1 = setTyVarName tyvar name'
-            ; tyvar2 <- zonkTcTyVarToTyVar tyvar1
+            ; tyvar2 <- zonkTcTyVarToTcTyVar tyvar1
               -- Be sure to zonk here!  Tidying applies to zonked
               -- types, so if we don't zonk we may create an
               -- ill-kinded type (#14175)
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index dace3d08f6..4193514665 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -19,7 +19,8 @@ module GHC.Tc.Utils.Instantiate (
      newWanted, newWanteds,
 
      tcInstType, tcInstTypeBndrs,
-     tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
+     tcSkolemiseInvisibleBndrs,
+     tcInstSkolTyVars, tcInstSkolTyVarsX,
      tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
 
      freshenTyVarBndrs, freshenCoVarBndrsX,
@@ -168,13 +169,14 @@ In general,
 
 -}
 
-topSkolemise :: TcSigmaType
+topSkolemise :: SkolemInfo
+             -> TcSigmaType
              -> TcM ( HsWrapper
                     , [(Name,TyVar)]     -- All skolemised variables
                     , [EvVar]            -- All "given"s
                     , TcRhoType )
 -- See Note [Skolemisation]
-topSkolemise ty
+topSkolemise skolem_info ty
   = go init_subst idHsWrapper [] [] ty
   where
     init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
@@ -183,7 +185,7 @@ topSkolemise ty
     go subst wrap tv_prs ev_vars ty
       | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty
       , not (null tvs && null theta)
-      = do { (subst', tvs1) <- tcInstSkolTyVarsX subst tvs
+      = do { (subst', tvs1) <- tcInstSkolTyVarsX skolem_info subst tvs
            ; ev_vars1       <- newEvVars (substTheta subst' theta)
            ; go subst'
                 (wrap <.> mkWpTyLams tvs1 <.> mkWpLams ev_vars1)
@@ -496,69 +498,98 @@ tcInstTypeBndrs id
       = do { (subst', tv') <- newMetaTyVarTyVarX subst tv
            ; return (subst', Bndr tv' spec) }
 
-tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
+--------------------------
+tcSkolDFunType :: SkolemInfo -> DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type signature with skolem constants.
 -- This freshens the names, but no need to do so
-tcSkolDFunType dfun
-  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
+tcSkolDFunType skol_info dfun
+  = do { (tv_prs, theta, tau) <- tcInstType (tcInstSuperSkolTyVars skol_info) dfun
        ; return (map snd tv_prs, theta, tau) }
 
-tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
+tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (TCvSubst, [TcTyVar])
 -- Make skolem constants, but do *not* give them new names, as above
--- Moreover, make them "super skolems"; see comments with superSkolemTv
--- see Note [Kind substitution when instantiating]
+-- As always, allocate them one level in
+-- Moreover, make them "super skolems"; see GHC.Core.InstEnv
+--    Note [Binding when looking up instances]
+-- See Note [Kind substitution when instantiating]
 -- Precondition: tyvars should be ordered by scoping
-tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
-
-tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
-tcSuperSkolTyVar subst tv
-  = (extendTvSubstWithClone subst tv new_tv, new_tv)
+tcSuperSkolTyVars tc_lvl skol_info = mapAccumL do_one emptyTCvSubst
   where
-    kind   = substTyUnchecked subst (tyVarKind tv)
-    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
+    details = SkolemTv skol_info (pushTcLevel tc_lvl)
+                       True   -- The "super" bit
+    do_one subst tv = (extendTvSubstWithClone subst tv new_tv, new_tv)
+      where
+        kind   = substTyUnchecked subst (tyVarKind tv)
+        new_tv = mkTcTyVar (tyVarName tv) kind details
 
 -- | Given a list of @['TyVar']@, skolemize the type variables,
 -- returning a substitution mapping the original tyvars to the
 -- skolems, and the list of newly bound skolems.
-tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
-tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
+tcInstSkolTyVars skol_info = tcInstSkolTyVarsX skol_info emptyTCvSubst
 
-tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
-tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
+tcInstSkolTyVarsX skol_info = tcInstSkolTyVarsPushLevel skol_info False
 
-tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
 -- This version freshens the names and creates "super skolems";
 -- see comments around superSkolemTv.
-tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
+tcInstSuperSkolTyVars skol_info = tcInstSuperSkolTyVarsX skol_info emptyTCvSubst
 
-tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSuperSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- See Note [Skolemising type variables]
 -- This version freshens the names and creates "super skolems";
 -- see comments around superSkolemTv.
-tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
+tcInstSuperSkolTyVarsX skol_info subst = tcInstSkolTyVarsPushLevel skol_info True subst
 
-tcInstSkolTyVarsPushLevel :: Bool  -- True <=> make "super skolem"
+tcInstSkolTyVarsPushLevel :: SkolemInfo -> Bool  -- True <=> make "super skolem"
                           -> TCvSubst -> [TyVar]
                           -> TcM (TCvSubst, [TcTyVar])
 -- Skolemise one level deeper, hence pushTcLevel
 -- See Note [Skolemising type variables]
-tcInstSkolTyVarsPushLevel overlappable subst tvs
+tcInstSkolTyVarsPushLevel skol_info overlappable subst tvs
   = do { tc_lvl <- getTcLevel
        -- Do not retain the whole TcLclEnv
        ; let !pushed_lvl = pushTcLevel tc_lvl
-       ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
+       ; tcInstSkolTyVarsAt skol_info pushed_lvl overlappable subst tvs }
 
-tcInstSkolTyVarsAt :: TcLevel -> Bool
+tcInstSkolTyVarsAt :: SkolemInfo -> TcLevel -> Bool
                    -> TCvSubst -> [TyVar]
                    -> TcM (TCvSubst, [TcTyVar])
-tcInstSkolTyVarsAt lvl overlappable subst tvs
+tcInstSkolTyVarsAt skol_info lvl overlappable subst tvs
   = freshenTyCoVarsX new_skol_tv subst tvs
   where
-    details = SkolemTv lvl overlappable
-    new_skol_tv name kind = mkTcTyVar name kind details
+    sk_details = SkolemTv skol_info lvl overlappable
+    new_skol_tv name kind = mkTcTyVar name kind sk_details
+
+tcSkolemiseInvisibleBndrs :: SkolemInfoAnon -> Type -> TcM ([TcTyVar], TcType)
+-- Skolemise the outer invisible binders of a type
+-- Do /not/ freshen them, because their scope is broader than
+-- just this type.  It's a bit dubious, but used in very limited ways.
+tcSkolemiseInvisibleBndrs skol_info ty
+  = do { let (tvs, body_ty) = tcSplitForAllInvisTyVars ty
+       ; lvl           <- getTcLevel
+       ; skol_info     <- mkSkolemInfo skol_info
+       ; let details = SkolemTv skol_info lvl False
+             mk_skol_tv name kind = return (mkTcTyVar name kind details)  -- No freshening
+       ; (subst, tvs') <- instantiateTyVarsX mk_skol_tv emptyTCvSubst tvs
+       ; return (tvs', substTy subst body_ty) }
+
+instantiateTyVarsX :: (Name -> Kind -> TcM TcTyVar)
+                   -> TCvSubst -> [TyVar]
+                   -> TcM (TCvSubst, [TcTyVar])
+-- Instantiate each type variable in turn with the specified function
+instantiateTyVarsX mk_tv subst tvs
+  = case tvs of
+      []       -> return (subst, [])
+      (tv:tvs) -> do { let kind1 = substTyUnchecked subst (tyVarKind tv)
+                     ; tv' <- mk_tv (tyVarName tv) kind1
+                     ; let subst1 = extendTCvSubstWithClone subst tv tv'
+                     ; (subst', tvs') <- instantiateTyVarsX mk_tv subst1 tvs
+                     ; return (subst', tv':tvs') }
 
 ------------------
 freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
@@ -580,25 +611,21 @@ freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
 freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
                  -> TCvSubst -> [TyCoVar]
                  -> TcM (TCvSubst, [TyCoVar])
-freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
-
-freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
-                -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
 -- This a complete freshening operation:
 -- the skolems have a fresh unique, and a location from the monad
 -- See Note [Skolemising type variables]
-freshenTyCoVarX mk_tcv subst tycovar
-  = do { loc  <- getSrcSpanM
-       ; uniq <- newUnique
-       ; let old_name = tyVarName tycovar
-             -- Force so we don't retain reference to the old name and id
-             -- See (#19619) for more discussion
-             !old_occ_name = getOccName old_name
-             new_name = mkInternalName uniq old_occ_name loc
-             new_kind = substTyUnchecked subst (tyVarKind tycovar)
-             new_tcv  = mk_tcv new_name new_kind
-             subst1   = extendTCvSubstWithClone subst tycovar new_tcv
-       ; return (subst1, new_tcv) }
+freshenTyCoVarsX mk_tcv
+  = instantiateTyVarsX freshen_tcv
+  where
+    freshen_tcv :: Name -> Kind -> TcM TcTyVar
+    freshen_tcv name kind
+      = do { loc  <- getSrcSpanM
+           ; uniq <- newUnique
+           ; let !occ_name = getOccName name
+                    -- Force so we don't retain reference to the old
+                    -- name and id.   See (#19619) for more discussion
+                 new_name = mkInternalName uniq occ_name loc
+           ; return (mk_tcv new_name kind) }
 
 {- Note [Skolemising type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 2c26915503..3a0fdca51a 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE TupleSections   #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+{-# LANGUAGE LambdaCase #-}
 {-
 (c) The University of Glasgow 2006
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
@@ -67,27 +68,29 @@ module GHC.Tc.Utils.TcMType (
   --------------------------------
   -- Zonking and tidying
   zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
-  tidyEvVar, tidyCt, tidyHole, tidySkolemInfo,
+  tidyEvVar, tidyCt, tidyHole,
     zonkTcTyVar, zonkTcTyVars,
-  zonkTcTyVarToTyVar, zonkInvisTVBinder,
+  zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars,
+  zonkInvisTVBinder,
   zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
   zonkTyCoVarsAndFVList,
 
   zonkTcType, zonkTcTypes, zonkCo,
-  zonkTyCoVarKind, zonkTyCoVarKindBinder,
+  zonkTyCoVarKind,
   zonkEvVar, zonkWC, zonkImplication, zonkSimples,
   zonkId, zonkCoVar,
-  zonkCt, zonkSkolemInfo,
+  zonkCt, zonkSkolemInfo, zonkSkolemInfoAnon,
 
   ---------------------------------
   -- Promotion, defaulting, skolemisation
   defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
   quantifyTyVars, isQuantifiableTv,
-  skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
+  zonkAndSkolemise, skolemiseQuantifiedTyVar,
   doNotQuantifyTyVars,
 
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
+  candidateQTyVarsWithBinders,
   CandidatesQTvs(..), delCandidates,
   candidateKindVars, partitionCandidates,
 
@@ -108,6 +111,7 @@ import GHC.Tc.Types.Evidence
 import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} )
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Errors.Types
+import GHC.Tc.Errors.Ppr
 
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr
@@ -126,7 +130,6 @@ import GHC.Types.Var.Set
 import GHC.Builtin.Types
 import GHC.Types.Error
 import GHC.Types.Var.Env
-import GHC.Types.Name.Env
 import GHC.Types.Unique.Set
 import GHC.Types.Basic ( TypeOrKind(..)
                        , NonStandardDefaultingStrategy(..)
@@ -848,10 +851,10 @@ newNamedAnonMetaTyVar tyvar_name meta_info kind
         ; return tyvar }
 
 -- makes a new skolem tv
-newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
-newSkolemTyVar name kind
+newSkolemTyVar :: SkolemInfo -> Name -> Kind -> TcM TcTyVar
+newSkolemTyVar skol_info name kind
   = do { lvl <- getTcLevel
-       ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
+       ; return (mkTcTyVar name kind (SkolemTv skol_info lvl False)) }
 
 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
 -- See Note [TyVarTv]
@@ -940,7 +943,10 @@ readMetaTyVar tyvar = assertPpr (isMetaTyVar tyvar) (ppr tyvar) $
 
 isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type)
 isFilledMetaTyVar_maybe tv
- | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
+-- TODO: This should be an assertion that tv is definitely a TcTyVar but it fails
+-- at the moment (Jan 22)
+ | isTcTyVar tv
+ , MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
  = do { cts <- readTcRef ref
       ; case cts of
           Indirect ty -> return (Just ty)
@@ -1357,6 +1363,12 @@ candidateVars (DV { dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
 candidateKindVars :: CandidatesQTvs -> TyVarSet
 candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
 
+delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
+delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
+  = DV { dv_kvs = kvs `delDVarSetList` vars
+       , dv_tvs = tvs `delDVarSetList` vars
+       , dv_cvs = cvs `delVarSetList`  vars }
+
 partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs)
 -- The selected TyVars are returned as a non-deterministic TyVarSet
 partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
@@ -1366,6 +1378,17 @@ partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred
     (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs
     extracted = dVarSetToVarSet extracted_kvs `unionVarSet` dVarSetToVarSet extracted_tvs
 
+candidateQTyVarsWithBinders :: [TyVar] -> Type -> TcM CandidatesQTvs
+-- (candidateQTyVarsWithBinders tvs ty) returns the candidateQTyVars
+-- of (forall tvs. ty), but do not treat 'tvs' as bound for the purpose
+-- of Note [Naughty quantification candidates].  Why?
+-- Because we are going to scoped-sort the quantified variables
+-- in among the tvs
+candidateQTyVarsWithBinders bound_tvs ty
+  = do { kvs <- candidateQTyVarsOfKinds (map tyVarKind bound_tvs)
+       ; all_tvs <- collect_cand_qtvs ty False emptyVarSet kvs ty
+       ; return (all_tvs `delCandidates` bound_tvs) }
+
 -- | Gathers free variables to use as quantification candidates (in
 -- 'quantifyTyVars'). This might output the same var
 -- in both sets, if it's used in both a type and a kind.
@@ -1397,12 +1420,6 @@ candidateQTyVarsOfKinds :: [TcKind]    -- Not necessarily zonked
 candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty)
                                     mempty tys
 
-delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs
-delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
-  = DV { dv_kvs = kvs `delDVarSetList` vars
-       , dv_tvs = tvs `delDVarSetList` vars
-       , dv_cvs = cvs `delVarSetList`  vars }
-
 collect_cand_qtvs
   :: TcType          -- original type that we started recurring into; for errors
   -> Bool            -- True <=> consider every fv in Type to be dependent
@@ -1485,6 +1502,11 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
                 -> return dv   -- this variable is from an outer context; skip
                                -- See Note [Use level numbers for quantification]
 
+                | case tcTyVarDetails tv of
+                     SkolemTv _ lvl _ -> lvl > pushTcLevel cur_lvl
+                     _                -> False
+                -> return dv  -- Skip inner skolems; ToDo: explain
+
                 |  intersectsVarSet bound tv_kind_vars
                    -- the tyvar must not be from an outer context, but we have
                    -- already checked for this.
@@ -1701,7 +1723,8 @@ For more information about deterministic sets see
 Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
 -}
 
-quantifyTyVars :: NonStandardDefaultingStrategy
+quantifyTyVars :: SkolemInfo
+               -> NonStandardDefaultingStrategy
                -> CandidatesQTvs   -- See Note [Dependent type variables]
                                    -- Already zonked
                -> TcM [TcTyVar]
@@ -1712,7 +1735,7 @@ quantifyTyVars :: NonStandardDefaultingStrategy
 -- invariants on CandidateQTvs, we do not have to filter out variables
 -- free in the environment here. Just quantify unconditionally, subject
 -- to the restrictions in Note [quantifyTyVars].
-quantifyTyVars ns_strat dvs
+quantifyTyVars skol_info ns_strat dvs
        -- short-circuit common case
   | isEmptyCandidates dvs
   = do { traceTc "quantifyTyVars has nothing to quantify" empty
@@ -1744,12 +1767,14 @@ quantifyTyVars ns_strat dvs
       = return Nothing   -- this can happen for a covar that's associated with
                          -- a coercion hole. Test case: typecheck/should_compile/T2494
 
-      | not (isTcTyVar tkv)
-      = return (Just tkv)  -- For associated types in a class with a standalone
-                           -- kind signature, we have the class variables in
-                           -- scope, and they are TyVars not TcTyVars
+-- Omit: no TyVars now
+--      | not (isTcTyVar tkv)
+--      = return (Just tkv)  -- For associated types in a class with a standalone
+--                           -- kind signature, we have the class variables in
+--                           -- scope, and they are TyVars not TcTyVars
+
       | otherwise
-      = Just <$> skolemiseQuantifiedTyVar tkv
+      = Just <$> skolemiseQuantifiedTyVar skol_info tkv
 
 isQuantifiableTv :: TcLevel   -- Level of the context, outside the quantification
                  -> TcTyVar
@@ -1760,25 +1785,25 @@ isQuantifiableTv outer_tclvl tcv
   | otherwise
   = False
 
-zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar
+zonkAndSkolemise :: SkolemInfo -> TcTyCoVar -> TcM TcTyCoVar
 -- A tyvar binder is never a unification variable (TauTv),
 -- rather it is always a skolem. It *might* be a TyVarTv.
 -- (Because non-CUSK type declarations use TyVarTvs.)
 -- Regardless, it may have a kind that has not yet been zonked,
 -- and may include kind unification variables.
-zonkAndSkolemise tyvar
+zonkAndSkolemise skol_info tyvar
   | isTyVarTyVar tyvar
      -- We want to preserve the binding location of the original TyVarTv.
      -- This is important for error messages. If we don't do this, then
      -- we get bad locations in, e.g., typecheck/should_fail/T2688
-  = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar
-       ; skolemiseQuantifiedTyVar zonked_tyvar }
+  = do { zonked_tyvar <- zonkTcTyVarToTcTyVar tyvar
+       ; skolemiseQuantifiedTyVar skol_info zonked_tyvar }
 
   | otherwise
   = assertPpr (isImmutableTyVar tyvar || isCoVar tyvar) (pprTyVar tyvar) $
     zonkTyCoVarKind tyvar
 
-skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
+skolemiseQuantifiedTyVar :: SkolemInfo -> TcTyVar -> TcM TcTyVar
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables
 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any
@@ -1790,14 +1815,14 @@ skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- This function is called on both kind and type variables,
 -- but kind variables *only* if PolyKinds is on.
 
-skolemiseQuantifiedTyVar tv
+skolemiseQuantifiedTyVar skol_info tv
   = case tcTyVarDetails tv of
       SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
                         ; return (setTyVarKind tv kind) }
         -- It might be a skolem type variable,
         -- for example from a user type signature
 
-      MetaTv {} -> skolemiseUnboundMetaTyVar tv
+      MetaTv {} -> skolemiseUnboundMetaTyVar skol_info tv
 
       _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk
 
@@ -1909,32 +1934,42 @@ defaultTyVars ns_strat dvs
   where
     (dep_kvs, nondep_tvs) = candidateVars dvs
 
-skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
+skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
 -- We have a Meta tyvar with a ref-cell inside it
 -- Skolemise it, so that we are totally out of Meta-tyvar-land
 -- We create a skolem TcTyVar, not a regular TyVar
 --   See Note [Zonking to Skolem]
-skolemiseUnboundMetaTyVar tv
+--
+-- Its level should be one greater than the ambient level, which will typically
+-- be the same as the level on the meta-tyvar. But not invariably; for example
+--    f :: (forall a b. SameKind a b) -> Int
+-- The skolems 'a' and 'b' are bound by tcTKTelescope, at level 2; and they each
+-- have a level-2 kind unification variable, since it might get unified with another
+-- of the level-2 skolems e.g. 'k' in this version
+--    f :: (forall k (a :: k) b. SameKind a b) -> Int
+-- So when we quantify the kind vars at the top level of the signature, the ambient
+-- level is 1, but we will quantify over kappa[2].
+
+skolemiseUnboundMetaTyVar skol_info tv
   = assertPpr (isMetaTyVar tv) (ppr tv) $
-    do  { when debugIsOn (check_empty tv)
-        ; here <- getSrcSpanM    -- Get the location from "here"
-                                 -- ie where we are generalising
-        ; kind <- zonkTcType (tyVarKind tv)
-        ; let tv_name     = tyVarName tv
+    do  { check_empty tv
+        ; tc_lvl <- getTcLevel   -- Get the location and level from "here"
+        ; here   <- getSrcSpanM  -- i.e. where we are generalising
+        ; kind   <- zonkTcType (tyVarKind tv)
+        ; let tv_name = tyVarName tv
               -- See Note [Skolemising and identity]
               final_name | isSystemName tv_name
                          = mkInternalName (nameUnique tv_name)
                                           (nameOccName tv_name) here
                          | otherwise
                          = tv_name
-              final_tv = mkTcTyVar final_name kind details
+              details    = SkolemTv skol_info (pushTcLevel tc_lvl) False
+              final_tv   = mkTcTyVar final_name kind details
 
         ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv)
         ; writeMetaTyVar tv (mkTyVarTy final_tv)
         ; return final_tv }
-
   where
-    details = SkolemTv (metaTyVarTcLevel tv) False
     check_empty tv       -- [Sept 04] Check for non-empty.
       = when debugIsOn $  -- See note [Silly Type Synonym]
         do { cts <- readMetaTyVar tv
@@ -2319,10 +2354,6 @@ zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
                         ; return (setTyVarKind tv kind') }
 
-zonkTyCoVarKindBinder :: (VarBndr TyCoVar fl) -> TcM (VarBndr TyCoVar fl)
-zonkTyCoVarKindBinder (Bndr tv fl) = do { kind' <- zonkTcType (tyVarKind tv)
-                                        ; return $ Bndr (setTyVarKind tv kind') fl }
-
 {-
 ************************************************************************
 *                                                                      *
@@ -2339,7 +2370,7 @@ zonkImplication implic@(Implic { ic_skols  = skols
   = do { skols'  <- mapM zonkTyCoVarKind skols  -- Need to zonk their kinds!
                                                 -- as #7230 showed
        ; given'  <- mapM zonkEvVar given
-       ; info'   <- zonkSkolemInfo info
+       ; info'   <- zonkSkolemInfoAnon info
        ; wanted' <- zonkWCRec wanted
        ; return (implic { ic_skols  = skols'
                         , ic_given  = given'
@@ -2422,13 +2453,16 @@ zonkCtEvidence ctev
        }
 
 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
-zonkSkolemInfo (SigSkol cx ty tv_prs)  = do { ty' <- zonkTcType ty
+zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk
+
+zonkSkolemInfoAnon :: SkolemInfoAnon -> TcM SkolemInfoAnon
+zonkSkolemInfoAnon (SigSkol cx ty tv_prs)  = do { ty' <- zonkTcType ty
                                             ; return (SigSkol cx ty' tv_prs) }
-zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
+zonkSkolemInfoAnon (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                      ; return (InferSkol ntys') }
   where
     do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
-zonkSkolemInfo skol_info = return skol_info
+zonkSkolemInfoAnon skol_info = return skol_info
 
 {-
 %************************************************************************
@@ -2503,17 +2537,20 @@ zonkTcTyVar tv
 
 -- Variant that assumes that any result of zonking is still a TyVar.
 -- Should be used only on skolems and TyVarTvs
-zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
-zonkTcTyVarToTyVar tv
+zonkTcTyVarsToTcTyVars :: HasDebugCallStack => [TcTyVar] -> TcM [TcTyVar]
+zonkTcTyVarsToTcTyVars = mapM zonkTcTyVarToTcTyVar
+
+zonkTcTyVarToTcTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
+zonkTcTyVarToTcTyVar tv
   = do { ty <- zonkTcTyVar tv
        ; let tv' = case tcGetTyVar_maybe ty of
                      Just tv' -> tv'
-                     Nothing  -> pprPanic "zonkTcTyVarToTyVar"
+                     Nothing  -> pprPanic "zonkTcTyVarToTcTyVar"
                                           (ppr tv $$ ppr ty)
        ; return tv' }
 
-zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TyVar spec)
-zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv
+zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TcTyVar spec)
+zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTcTyVar tv
                                       ; return (Bndr tv' spec) }
 
 -- zonkId is used *during* typechecking just to zonk the Id's type
@@ -2563,12 +2600,12 @@ zonkTidyTcTypes = zonkTidyTcTypes' []
 
 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
 zonkTidyOrigin env (GivenOrigin skol_info)
-  = do { skol_info1 <- zonkSkolemInfo skol_info
-       ; let skol_info2 = tidySkolemInfo env skol_info1
+  = do { skol_info1 <- zonkSkolemInfoAnon skol_info
+       ; let skol_info2 = tidySkolemInfoAnon env skol_info1
        ; return (env, GivenOrigin skol_info2) }
 zonkTidyOrigin env (OtherSCOrigin sc_depth skol_info)
-  = do { skol_info1 <- zonkSkolemInfo skol_info
-       ; let skol_info2 = tidySkolemInfo env skol_info1
+  = do { skol_info1 <- zonkSkolemInfoAnon skol_info
+       ; let skol_info2 = tidySkolemInfoAnon env skol_info1
        ; return (env, OtherSCOrigin sc_depth skol_info2) }
 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual   = act
                                       , uo_expected = exp })
@@ -2622,43 +2659,6 @@ tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty }
 tidyEvVar :: TidyEnv -> EvVar -> EvVar
 tidyEvVar env var = updateIdTypeAndMult (tidyType env) var
 
-----------------
-tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
-tidySkolemInfo env (DerivSkol ty)         = DerivSkol (tidyType env ty)
-tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs
-tidySkolemInfo env (InferSkol ids)        = InferSkol (mapSnd (tidyType env) ids)
-tidySkolemInfo env (UnifyForAllSkol ty)   = UnifyForAllSkol (tidyType env ty)
-tidySkolemInfo _   info                   = info
-
-tidySigSkol :: TidyEnv -> UserTypeCtxt
-            -> TcType -> [(Name,TcTyVar)] -> SkolemInfo
--- We need to take special care when tidying SigSkol
--- See Note [SigSkol SkolemInfo] in "GHC.Tc.Types.Origin"
-tidySigSkol env cx ty tv_prs
-  = SigSkol cx (tidy_ty env ty) tv_prs'
-  where
-    tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs
-    inst_env = mkNameEnv tv_prs'
-
-    tidy_ty env (ForAllTy (Bndr tv vis) ty)
-      = ForAllTy (Bndr tv' vis) (tidy_ty env' ty)
-      where
-        (env', tv') = tidy_tv_bndr env tv
-
-    tidy_ty env ty@(FunTy InvisArg w arg res) -- Look under  c => t
-      = ty { ft_mult = tidy_ty env w,
-             ft_arg = tidyType env arg,
-             ft_res = tidy_ty env res }
-
-    tidy_ty env ty = tidyType env ty
-
-    tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
-    tidy_tv_bndr env@(occ_env, subst) tv
-      | Just tv' <- lookupNameEnv inst_env (tyVarName tv)
-      = ((occ_env, extendVarEnv subst tv tv'), tv')
-
-      | otherwise
-      = tidyVarBndr env tv
 
 -------------------------------------------------------------------------
 {-
@@ -2700,7 +2700,7 @@ naughtyQuantification :: TcType   -- original type user wanted to quantify
 naughtyQuantification orig_ty tv escapees
   = do { orig_ty1 <- zonkTcType orig_ty  -- in case it's not zonked
 
-       ; escapees' <- mapM zonkTcTyVarToTyVar $
+       ; escapees' <- zonkTcTyVarsToTcTyVars $
                       nonDetEltsUniqSet escapees
                      -- we'll just be printing, so no harmful non-determinism
 
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index a4dfead21b..363ece84b2 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -25,7 +25,7 @@ module GHC.Tc.Utils.TcType (
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
   TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
   TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder,
-  TcTyCon, KnotTied,
+  TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied,
 
   ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
 
@@ -35,11 +35,10 @@ module GHC.Tc.Utils.TcType (
   TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
   strictlyDeeperThan, deeperThanOrSame, sameDepthAs,
   tcTypeLevel, tcTyVarLevel, maxTcLevel,
-  promoteSkolem, promoteSkolemX, promoteSkolemsX,
   --------------------------------
   -- MetaDetails
-  TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
-  MetaDetails(Flexi, Indirect), MetaInfo(..),
+  TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTvUnk,
+  MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo,
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
   tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar,  isTyConableTyVar,
   isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
@@ -230,10 +229,10 @@ import GHC.Utils.Panic.Plain
 import GHC.Utils.Error( Validity'(..), Validity )
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List  ( mapAccumL )
--- import Data.Functor.Identity( Identity(..) )
 import Data.IORef
 import Data.List.NonEmpty( NonEmpty(..) )
+import {-# SOURCE #-} GHC.Tc.Types.Origin ( unkSkol, SkolemInfo )
+
 
 {-
 ************************************************************************
@@ -341,7 +340,12 @@ type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
 type TcTyVarBinder     = TyVarBinder
 type TcInvisTVBinder   = InvisTVBinder
 type TcReqTVBinder     = ReqTVBinder
-type TcTyCon           = TyCon   -- these can be the TcTyCon constructor
+
+-- See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]
+type TcTyCon       = TyCon
+type MonoTcTyCon   = TcTyCon
+type PolyTcTyCon   = TcTyCon
+type TcTyConBinder = TyConBinder -- With skolem TcTyVars
 
 -- These types do not have boxy type variables in them
 type TcPredType     = PredType
@@ -355,6 +359,51 @@ type TcTyCoVarSet   = TyCoVarSet
 type TcDTyVarSet    = DTyVarSet
 type TcDTyCoVarSet  = DTyCoVarSet
 
+{- Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See Note [How TcTyCons work] in GHC.Tc.TyCl
+
+Invariants:
+
+* TcTyCon: a TyCon built with the TcTyCon constructor
+
+* TcTyConBinder: a TyConBinder with a TcTyVar inside (not a TyVar)
+
+* TcTyCons contain TcTyVars
+
+* MonoTcTyCon:
+  - Flag tcTyConIsPoly = False
+
+  - tyConScopedTyVars is important; maps a Name to a TyVarTv unification variable
+    The order is important: Specified then Required variables.   E.g. in
+        data T a (b :: k) = ...
+    the order will be [k, a, b].
+
+    NB: There are no Inferred binders in tyConScopedTyVars; 'a' may
+    also be poly-kinded, but that kind variable will be added by
+    generaliseTcTyCon, in the passage to a PolyTcTyCon.
+
+  - tyConBinders are irrelevant; we just use tcTyConScopedTyVars
+    Well not /quite/ irrelevant: its length gives the number of Required binders,
+    and so allows up to distinguish between the Specified and Required elements of
+    tyConScopedTyVars.
+
+* PolyTcTyCon:
+  - Flag tcTyConIsPoly = True; this is used only to short-cut zonking
+
+  - tyConBinders are still TcTyConBinders, but they are /skolem/ TcTyVars,
+    with fixed kinds: no unification variables here
+
+    tyConBinders includes the Inferred binders if any
+
+    tyConBinders uses the Names from the original, renamed program.
+
+  - tcTyConScopedTyVars is irrelevant: just use (binderVars tyConBinders)
+    All the types have been swizzled back to use the original Names
+    See Note [tyConBinders and lexical scoping] in GHC.Core.TyCon
+
+-}
+
 {- *********************************************************************
 *                                                                      *
           ExpType: an "expected type" in the type checker
@@ -480,6 +529,7 @@ we would need to enforce the separation.
 -- See Note [TyVars and TcTyVars]
 data TcTyVarDetails
   = SkolemTv      -- A skolem
+       SkolemInfo
        TcLevel    -- Level of the implication that binds it
                   -- See GHC.Tc.Utils.Unify Note [Deeper level on the left] for
                   --     how this level number is used
@@ -494,12 +544,8 @@ data TcTyVarDetails
            , mtv_ref   :: IORef MetaDetails
            , mtv_tclvl :: TcLevel }  -- See Note [TcLevel invariants]
 
-vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
--- See Note [Binding when looking up instances] in GHC.Core.InstEnv
-vanillaSkolemTv = SkolemTv topTcLevel False  -- Might be instantiated
-superSkolemTv   = SkolemTv topTcLevel True   -- Treat this as a completely distinct type
-                  -- The choice of level number here is a bit dodgy, but
-                  -- topTcLevel works in the places that vanillaSkolemTv is used
+vanillaSkolemTvUnk :: HasCallStack => TcTyVarDetails
+vanillaSkolemTvUnk = SkolemTv unkSkol topTcLevel False
 
 instance Outputable TcTyVarDetails where
   ppr = pprTcTyVarDetails
@@ -507,8 +553,8 @@ instance Outputable TcTyVarDetails where
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 -- For debugging
 pprTcTyVarDetails (RuntimeUnk {})      = text "rt"
-pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
-pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
+pprTcTyVarDetails (SkolemTv _sk lvl True)  = text "ssk" <> colon <> ppr lvl
+pprTcTyVarDetails (SkolemTv _sk lvl False) = text "sk"  <> colon <> ppr lvl
 pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
   = ppr info <> colon <> ppr tclvl
 
@@ -678,7 +724,7 @@ tcTyVarLevel :: TcTyVar -> TcLevel
 tcTyVarLevel tv
   = case tcTyVarDetails tv of
           MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
-          SkolemTv tv_lvl _             -> tv_lvl
+          SkolemTv _ tv_lvl _           -> tv_lvl
           RuntimeUnk                    -> topTcLevel
 
 
@@ -696,32 +742,6 @@ tcTypeLevel ty
 instance Outputable TcLevel where
   ppr (TcLevel us) = ppr us
 
-promoteSkolem :: TcLevel -> TcTyVar -> TcTyVar
-promoteSkolem tclvl skol
-  | tclvl < tcTyVarLevel skol
-  = assert (isTcTyVar skol && isSkolemTyVar skol )
-    setTcTyVarDetails skol (SkolemTv tclvl (isOverlappableTyVar skol))
-
-  | otherwise
-  = skol
-
--- | Change the TcLevel in a skolem, extending a substitution
-promoteSkolemX :: TcLevel -> TCvSubst -> TcTyVar -> (TCvSubst, TcTyVar)
-promoteSkolemX tclvl subst skol
-  = assert (isTcTyVar skol && isSkolemTyVar skol )
-    (new_subst, new_skol)
-  where
-    new_skol
-      | tclvl < tcTyVarLevel skol
-      = setTcTyVarDetails (updateTyVarKind (substTy subst) skol)
-                          (SkolemTv tclvl (isOverlappableTyVar skol))
-      | otherwise
-      = updateTyVarKind (substTy subst) skol
-    new_subst = extendTvSubstWithClone subst skol new_skol
-
-promoteSkolemsX :: TcLevel -> TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar])
-promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
-
 {- *********************************************************************
 *                                                                      *
     Finding type family instances
@@ -1034,10 +1054,19 @@ isSkolemTyVar tv
         MetaTv {} -> False
         _other    -> True
 
+skolemSkolInfo :: TcTyVar -> SkolemInfo
+skolemSkolInfo tv
+  = assert (isSkolemTyVar tv) $
+    case tcTyVarDetails tv of
+      SkolemTv skol_info _ _ -> skol_info
+      RuntimeUnk -> panic "RuntimeUnk"
+      MetaTv {} -> panic "skolemSkolInfo"
+
+
 isOverlappableTyVar tv
   | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = case tcTyVarDetails tv of
-        SkolemTv _ overlappable -> overlappable
+        SkolemTv _ _ overlappable -> overlappable
         _                       -> False
   | otherwise = False
 
diff --git a/compiler/GHC/Tc/Utils/TcType.hs-boot b/compiler/GHC/Tc/Utils/TcType.hs-boot
index 2a7a34dc97..08602fa5ac 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs-boot
+++ b/compiler/GHC/Tc/Utils/TcType.hs-boot
@@ -4,13 +4,15 @@ import GHC.Prelude ( Bool )
 import {-# SOURCE #-} GHC.Types.Var ( TcTyVar )
 import {-# SOURCE #-} GHC.Core.TyCo.Rep
 import GHC.Utils.Misc ( HasDebugCallStack )
+import GHC.Stack
 
 data MetaDetails
 
 data TcTyVarDetails
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-vanillaSkolemTv :: TcTyVarDetails
+vanillaSkolemTvUnk :: HasCallStack => TcTyVarDetails
 isMetaTyVar :: TcTyVar -> Bool
 isTyConableTyVar :: TcTyVar -> Bool
 
 tcEqType :: HasDebugCallStack => Type -> Type -> Bool
+
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index aa1a753369..1ff6c044dc 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
+{-# LANGUAGE RecursiveDo       #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -863,12 +864,14 @@ tcSkolemise, tcSkolemiseScoped
 -- tcSkolemiseScoped and tcSkolemise
 
 tcSkolemiseScoped ctxt expected_ty thing_inside
-  = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
-       ; let skol_tvs  = map snd tv_prs
-             skol_info = SigSkol ctxt expected_ty tv_prs
+  = do {
+       ; rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
+             ; let skol_tvs  = map snd tv_prs
+             ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs)
+       }
 
        ; (ev_binds, res)
-             <- checkConstraints skol_info skol_tvs given $
+             <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
                 tcExtendNameTyVarEnv tv_prs               $
                 thing_inside rho_ty
 
@@ -879,13 +882,15 @@ tcSkolemise ctxt expected_ty thing_inside
   = do { res <- thing_inside expected_ty
        ; return (idHsWrapper, res) }
   | otherwise
-  = do  { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
+  = do  {
+        ; rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
 
-        ; let skol_tvs  = map snd tv_prs
-              skol_info = SigSkol ctxt expected_ty tv_prs
+              ; let skol_tvs  = map snd tv_prs
+              ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs)
+        }
 
         ; (ev_binds, result)
-              <- checkConstraints skol_info skol_tvs given $
+              <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
                  thing_inside rho_ty
 
         ; return (wrap <.> mkWpLet ev_binds, result) }
@@ -902,7 +907,7 @@ tcSkolemiseET ctxt (Check ty) thing_inside
   = tcSkolemise ctxt ty $ \rho_ty ->
     thing_inside (mkCheckExpType rho_ty)
 
-checkConstraints :: SkolemInfo
+checkConstraints :: SkolemInfoAnon
                  -> [TcTyVar]           -- Skolems
                  -> [EvVar]             -- Given
                  -> TcM result
@@ -938,33 +943,39 @@ emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
                          -> TcLevel -> WantedConstraints -> TcM ()
 emitResidualTvConstraint skol_info skol_tvs tclvl wanted
   | not (isEmptyWC wanted) ||
-    checkTelescopeSkol skol_info
+    checkTelescopeSkol skol_info_anon
   = -- checkTelescopeSkol: in this case, /always/ emit this implication
     -- even if 'wanted' is empty. We need the implication so that we check
     -- for a bad telescope. See Note [Skolem escape and forall-types] in
     -- GHC.Tc.Gen.HsType
-    do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
+    do { implic <- buildTvImplication skol_info_anon skol_tvs tclvl wanted
        ; emitImplication implic }
 
   | otherwise  -- Empty 'wanted', emit nothing
   = return ()
+  where
+     skol_info_anon = getSkolemInfo skol_info
 
-buildTvImplication :: SkolemInfo -> [TcTyVar]
+buildTvImplication :: SkolemInfoAnon -> [TcTyVar]
                    -> TcLevel -> WantedConstraints -> TcM Implication
 buildTvImplication skol_info skol_tvs tclvl wanted
-  = do { ev_binds <- newNoTcEvBinds  -- Used for equalities only, so all the constraints
+  = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
+    do { ev_binds <- newNoTcEvBinds  -- Used for equalities only, so all the constraints
                                      -- are solved by filling in coercion holes, not
                                      -- by creating a value-level evidence binding
        ; implic   <- newImplication
 
-       ; return (implic { ic_tclvl     = tclvl
-                        , ic_skols     = skol_tvs
-                        , ic_given_eqs = NoGivenEqs
-                        , ic_wanted    = wanted
-                        , ic_binds     = ev_binds
-                        , ic_info      = skol_info }) }
+       ; let implic' = implic { ic_tclvl     = tclvl
+                              , ic_skols     = skol_tvs
+                              , ic_given_eqs = NoGivenEqs
+                              , ic_wanted    = wanted
+                              , ic_binds     = ev_binds
+                              , ic_info      = skol_info }
+
+       ; checkImplicationInvariants implic'
+       ; return implic' }
 
-implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
+implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
 -- See Note [When to build an implication]
 implicationNeeded skol_info skol_tvs given
   | null skol_tvs
@@ -984,7 +995,7 @@ implicationNeeded skol_info skol_tvs given
   | otherwise     -- Non-empty skolems or givens
   = return True   -- Definitely need an implication
 
-alwaysBuildImplication :: SkolemInfo -> Bool
+alwaysBuildImplication :: SkolemInfoAnon -> Bool
 -- See Note [When to build an implication]
 alwaysBuildImplication _ = False
 
@@ -1001,7 +1012,7 @@ alwaysBuildImplication (FamInstSkol {})   = True
 alwaysBuildImplication _                  = False
 -}
 
-buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
+buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar]
                    -> [EvVar] -> WantedConstraints
                    -> TcM (Bag Implication, TcEvBinds)
 buildImplicationFor tclvl skol_info skol_tvs given wanted
@@ -1026,6 +1037,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
                               , ic_wanted = wanted
                               , ic_binds  = ev_binds_var
                               , ic_info   = skol_info }
+       ; checkImplicationInvariants implic'
 
        ; return (unitBag implic', TcEvBinds ev_binds_var) }
 
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index cc09edd778..805d6a483d 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -37,7 +37,7 @@ module GHC.Tc.Utils.Zonk (
         zonkCoToCo,
         zonkEvBinds, zonkTcEvBinds,
         zonkTcMethInfoToMethInfoX,
-        lookupTyVarOcc
+        lookupTyVarX
   ) where
 
 import GHC.Prelude
@@ -1776,7 +1776,7 @@ change.  But in some cases it makes a HUGE difference: see test
 T9198 and #19668.  So yes, it seems worth it.
 -}
 
-zonkTyVarOcc :: ZonkEnv -> TyVar -> TcM TcType
+zonkTyVarOcc :: ZonkEnv -> TcTyVar -> TcM Type
 zonkTyVarOcc env@(ZonkEnv { ze_flexi = flexi
                           , ze_tv_env = tv_env
                           , ze_meta_tv_env = mtv_env_ref }) tv
@@ -1791,13 +1791,19 @@ zonkTyVarOcc env@(ZonkEnv { ze_flexi = flexi
                   Just ty -> return ty
                   Nothing -> do { mtv_details <- readTcRef ref
                                 ; zonk_meta ref mtv_details } }
-  | otherwise
+  | otherwise  -- This should never really happen;
+               -- TyVars should not occur in the typechecker
   = lookup_in_tv_env
 
   where
     lookup_in_tv_env    -- Look up in the env just as we do for Ids
       = case lookupVarEnv tv_env tv of
-          Nothing  -> mkTyVarTy <$> updateTyVarKindM (zonkTcTypeToTypeX env) tv
+          Nothing  -> -- TyVar/SkolemTv/RuntimeUnk that isn't in the ZonkEnv
+                      -- This can happen for RuntimeUnk variables (which
+                      -- should stay as RuntimeUnk), but I think it should
+                      -- not happen for SkolemTv.
+                      mkTyVarTy <$> updateTyVarKindM (zonkTcTypeToTypeX env) tv
+
           Just tv' -> return (mkTyVarTy tv')
 
     zonk_meta ref Flexi
@@ -1814,9 +1820,11 @@ zonkTyVarOcc env@(ZonkEnv { ze_flexi = flexi
       = do { updTcRef mtv_env_ref (\env -> extendVarEnv env tv ty)
            ; return ty }
 
-lookupTyVarOcc :: ZonkEnv -> TcTyVar -> Maybe TyVar
-lookupTyVarOcc (ZonkEnv { ze_tv_env = tv_env }) tv
-  = lookupVarEnv tv_env tv
+lookupTyVarX :: ZonkEnv -> TcTyVar -> TyVar
+lookupTyVarX (ZonkEnv { ze_tv_env = tv_env }) tv
+  = case lookupVarEnv tv_env tv of
+       Just tv -> tv
+       Nothing -> pprPanic "lookupTyVarOcc" (ppr tv $$ ppr tv_env)
 
 commitFlexi :: ZonkFlexi -> TcTyVar -> Kind -> TcM Type
 -- Only monadic so we can do tc-tracing