Be more careful when naming TyCon binders

This patch fixes two rather gnarly test cases:
  * Trac #16342 (mutual recursion)
    See Note [Tricky scoping in generaliseTcTyCon]

  * Trac #16221 (shadowing)
    See Note [Unification variables need fresh Names]

The main changes are:

* Substantial reworking of TcTyClsDecls.generaliseTcTyCon
  This is the big change, and involves the rather tricky
  function TcHsSyn.zonkRecTyVarBndrs.

  See Note [Inferring kinds for type declarations] and
  Note [Tricky scoping in generaliseTcTyCon] for the details.

* bindExplicitTKBndrs_Tv and bindImplicitTKBndrs_Tv both now
  allocate /freshly-named/ unification variables. Indeed, more
  generally, unification variables are always fresh; see
  Note [Unification variables need fresh Names] in TcMType

* Clarify the role of tcTyConScopedTyVars.
  See Note [Scoped tyvars in a TcTyCon] in TyCon

As usual, this dragged in some more refactoring:

* Renamed TcMType.zonkTyCoVarBndr to zonkAndSkolemise

* I renamed checkValidTelescope to checkTyConTelescope;
  it's only used on TyCons, and indeed takes a TyCon as argument.

* I folded the slightly-mysterious reportFloatingKvs into
  checkTyConTelescope. (Previously all its calls immediately
  followed a call to checkTyConTelescope.)  It makes much more
  sense there.

* I inlined some called-once functions to simplify
  checkValidTyFamEqn. It's less spaghetti-like now.

* This patch also fixes Trac #16251.  I'm not quite sure why #16251
  went wrong in the first place, nor how this patch fixes it, but
  hey, it's good, and life is short.

13 files changed, 607 insertions, 368 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 5e0976d1a2..67a05d647d 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -208,7 +208,7 @@ get_scoped_tvs (dL->L _ signature)
       | HsIB { hsib_ext = implicit_vars
              , hsib_body = hs_ty } <- sig
       , (explicit_vars, _) <- splitLHsForAllTy hs_ty
-      = implicit_vars ++ map hsLTyVarName explicit_vars
+      = implicit_vars ++ hsLTyVarNames explicit_vars
     get_scoped_tvs_from_sig (XHsImplicitBndrs _)
       = panic "get_scoped_tvs_from_sig"
 
@@ -1037,7 +1037,7 @@ addHsTyVarBinds :: [LHsTyVarBndr GhcRn]  -- the binders to be added
                 -> (Core [TH.TyVarBndrQ] -> DsM (Core (TH.Q a)))  -- action in the ext env
                 -> DsM (Core (TH.Q a))
 addHsTyVarBinds exp_tvs thing_inside
-  = do { fresh_exp_names <- mkGenSyms (map hsLTyVarName exp_tvs)
+  = do { fresh_exp_names <- mkGenSyms (hsLTyVarNames exp_tvs)
        ; term <- addBinds fresh_exp_names $
                  do { kbs <- repList tyVarBndrQTyConName mk_tv_bndr
                                      (exp_tvs `zip` fresh_exp_names)
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index aabe9f4597..85715a9282 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -53,7 +53,7 @@ module HsTypes (
         isHsKindedTyVar, hsTvbAllKinded, isLHsForAllTy,
         hsScopedTvs, hsWcScopedTvs, dropWildCards,
         hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
-        hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames,
+        hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
         splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
         splitLHsPatSynTy,
         splitLHsForAllTy, splitLHsForAllTyInvis,
@@ -949,7 +949,7 @@ hsWcScopedTvs sig_ty
          , hsib_body = sig_ty2 } <- sig_ty1
   = case sig_ty2 of
       L _ (HsForAllTy { hst_bndrs = tvs }) -> vars ++ nwcs ++
-                                              map hsLTyVarName tvs
+                                              hsLTyVarNames tvs
                -- include kind variables only if the type is headed by forall
                -- (this is consistent with GHC 7 behaviour)
       _                                    -> nwcs
@@ -962,7 +962,7 @@ hsScopedTvs sig_ty
   | HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty
   , L _ (HsForAllTy { hst_bndrs = tvs }) <- sig_ty2
-  = vars ++ map hsLTyVarName tvs
+  = vars ++ hsLTyVarNames tvs
   | otherwise
   = []
 
@@ -988,6 +988,9 @@ hsTyVarName (XTyVarBndr{}) = panic "hsTyVarName"
 hsLTyVarName :: LHsTyVarBndr pass -> IdP pass
 hsLTyVarName = hsTyVarName . unLoc
 
+hsLTyVarNames :: [LHsTyVarBndr pass] -> [IdP pass]
+hsLTyVarNames = map hsLTyVarName
+
 hsExplicitLTyVarNames :: LHsQTyVars pass -> [IdP pass]
 -- Explicit variables only
 hsExplicitLTyVarNames qtvs = map hsLTyVarName (hsQTvExplicit qtvs)
@@ -996,7 +999,7 @@ hsAllLTyVarNames :: LHsQTyVars GhcRn -> [Name]
 -- All variables
 hsAllLTyVarNames (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kvs }
                          , hsq_explicit = tvs })
-  = kvs ++ map hsLTyVarName tvs
+  = kvs ++ hsLTyVarNames tvs
 hsAllLTyVarNames (XLHsQTyVars _) = panic "hsAllLTyVarNames"
 
 hsLTyVarLocName :: LHsTyVarBndr pass -> Located (IdP pass)
@@ -1255,7 +1258,7 @@ splitLHsInstDeclTy :: LHsSigType GhcRn
 splitLHsInstDeclTy (HsIB { hsib_ext = itkvs
                          , hsib_body = inst_ty })
   | (tvs, cxt, body_ty) <- splitLHsSigmaTyInvis inst_ty
-  = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
+  = (itkvs ++ hsLTyVarNames tvs, cxt, body_ty)
          -- Return implicitly bound type and kind vars
          -- For an instance decl, all of them are in scope
 splitLHsInstDeclTy (XHsImplicitBndrs _) = panic "splitLHsInstDeclTy"
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 5155f3ab84..f902b0ef07 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -776,8 +776,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
                           inst_tvs = case mb_cls of
                                        Nothing            -> []
                                        Just (_, inst_tvs) -> inst_tvs
-                          all_nms = all_imp_var_names
-                                      ++ map hsLTyVarName bndrs'
+                          all_nms = all_imp_var_names ++ hsLTyVarNames bndrs'
                     ; warnUnusedTypePatterns all_nms nms_used
 
                     ; return ((bndrs', pats', payload'), rhs_fvs `plusFV` pat_fvs) }
@@ -1809,7 +1808,7 @@ rnLDerivStrategy doc mds thing_inside
              let HsIB { hsib_ext  = via_imp_tvs
                       , hsib_body = via_body } = via_ty'
                  (via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body
-                 via_exp_tvs = map hsLTyVarName via_exp_tv_bndrs
+                 via_exp_tvs = hsLTyVarNames via_exp_tv_bndrs
                  via_tvs = via_imp_tvs ++ via_exp_tvs
              (thing, fvs2) <- extendTyVarEnvFVRn via_tvs $
                               thing_inside via_tvs (ppr via_ty')
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 8b815bb0e7..7755daf44b 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -34,7 +34,7 @@ module TcHsSyn (
         zonkTopBndrs,
         ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
         zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
-        zonkTyBndrs, zonkTyBndrsX,
+        zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs,
         zonkTcTypeToType,  zonkTcTypeToTypeX,
         zonkTcTypesToTypes, zonkTcTypesToTypesX,
         zonkTyVarOcc,
@@ -278,7 +278,11 @@ data ZonkFlexi   -- See Note [Un-unified unification variables]
   | RuntimeUnkFlexi -- Used in the GHCi debugger
 
 instance Outputable ZonkEnv where
-  ppr (ZonkEnv { ze_id_env =  var_env}) = pprUFM var_env (vcat . map ppr)
+  ppr (ZonkEnv { ze_tv_env = tv_env
+               , ze_id_env = id_env })
+    = text "ZE" <+> braces (vcat
+         [ text "ze_tv_env =" <+> ppr tv_env
+         , text "ze_id_env =" <+> ppr id_env ])
 
 -- The EvBinds have to already be zonked, but that's usually the case.
 emptyZonkEnv :: TcM ZonkEnv
@@ -292,9 +296,9 @@ mkEmptyZonkEnv flexi
                          , ze_id_env = emptyVarEnv
                          , ze_meta_tv_env = mtv_env_ref }) }
 
-initZonkEnv :: (ZonkEnv -> a -> TcM b) -> a -> TcM b
-initZonkEnv do_it x = do { ze <- mkEmptyZonkEnv DefaultFlexi
-                         ; do_it ze x }
+initZonkEnv :: (ZonkEnv -> TcM b) -> TcM b
+initZonkEnv thing_inside = do { ze <- mkEmptyZonkEnv DefaultFlexi
+                              ; thing_inside ze }
 
 -- | Extend the knot-tied environment.
 extendIdZonkEnvRec :: ZonkEnv -> [Var] -> ZonkEnv
@@ -324,6 +328,12 @@ extendTyZonkEnv1 :: ZonkEnv -> TyVar -> ZonkEnv
 extendTyZonkEnv1 ze@(ZonkEnv { ze_tv_env = ty_env }) tv
   = ze { ze_tv_env = extendVarEnv ty_env tv tv }
 
+extendTyZonkEnvN :: ZonkEnv -> [(Name,TyVar)] -> ZonkEnv
+extendTyZonkEnvN ze@(ZonkEnv { ze_tv_env = ty_env }) pairs
+  = ze { ze_tv_env = foldl add ty_env pairs }
+  where
+    add env (name, tv) = extendVarEnv_Directly env (getUnique name) tv
+
 setZonkType :: ZonkEnv -> ZonkFlexi -> ZonkEnv
 setZonkType ze flexi = ze { ze_flexi = flexi }
 
@@ -374,7 +384,7 @@ zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
 zonkIdBndrs env ids = mapM (zonkIdBndr env) ids
 
 zonkTopBndrs :: [TcId] -> TcM [Id]
-zonkTopBndrs ids = initZonkEnv zonkIdBndrs ids
+zonkTopBndrs ids = initZonkEnv $ \ ze -> zonkIdBndrs ze ids
 
 zonkFieldOcc :: ZonkEnv -> FieldOcc GhcTcId -> TcM (FieldOcc GhcTc)
 zonkFieldOcc env (FieldOcc sel lbl)
@@ -419,7 +429,7 @@ zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var])
 zonkCoreBndrsX = mapAccumLM zonkCoreBndrX
 
 zonkTyBndrs :: [TcTyVar] -> TcM (ZonkEnv, [TyVar])
-zonkTyBndrs = initZonkEnv zonkTyBndrsX
+zonkTyBndrs tvs = initZonkEnv $ \ze -> zonkTyBndrsX ze tvs
 
 zonkTyBndrsX :: ZonkEnv -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
 zonkTyBndrsX = mapAccumLM zonkTyBndrX
@@ -436,7 +446,7 @@ zonkTyBndrX env tv
 
 zonkTyVarBinders ::  [VarBndr TcTyVar vis]
                  -> TcM (ZonkEnv, [VarBndr TyVar vis])
-zonkTyVarBinders = initZonkEnv zonkTyVarBindersX
+zonkTyVarBinders tvbs = initZonkEnv $ \ ze -> zonkTyVarBindersX ze tvbs
 
 zonkTyVarBindersX :: ZonkEnv -> [VarBndr TcTyVar vis]
                              -> TcM (ZonkEnv, [VarBndr TyVar vis])
@@ -449,11 +459,27 @@ zonkTyVarBinderX env (Bndr tv vis)
   = do { (env', tv') <- zonkTyBndrX env tv
        ; return (env', Bndr tv' vis) }
 
+zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
+-- This rather specialised function is used in exactly one place.
+-- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls.
+zonkRecTyVarBndrs names tc_tvs
+  = initZonkEnv $ \ ze ->
+    fixM $ \ ~(_, rec_new_tvs) ->
+    do { let ze' = extendTyZonkEnvN ze $
+                   zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv))
+                               tc_tvs rec_new_tvs
+       ; new_tvs <- zipWithM (zonk_one ze') names tc_tvs
+       ; return (ze', new_tvs) }
+  where
+    zonk_one ze name tc_tv
+      = do { ki <- zonkTcTypeToTypeX ze (tyVarKind tc_tv)
+           ; return (mkTyVar name ki) }
+
 zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc)
-zonkTopExpr e = initZonkEnv zonkExpr e
+zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e
 
 zonkTopLExpr :: LHsExpr GhcTcId -> TcM (LHsExpr GhcTc)
-zonkTopLExpr e = initZonkEnv zonkLExpr e
+zonkTopLExpr e = initZonkEnv $ \ ze -> zonkLExpr ze e
 
 zonkTopDecls :: Bag EvBind
              -> LHsBinds GhcTcId
@@ -466,7 +492,7 @@ zonkTopDecls :: Bag EvBind
                      [LTcSpecPrag],
                      [LRuleDecl    GhcTc])
 zonkTopDecls ev_binds binds rules imp_specs fords
-  = do  { (env1, ev_binds') <- initZonkEnv zonkEvBinds ev_binds
+  = do  { (env1, ev_binds') <- initZonkEnv $ \ ze -> zonkEvBinds ze ev_binds
         ; (env2, binds')    <- zonkRecMonoBinds env1 binds
                         -- Top level is implicitly recursive
         ; rules' <- zonkRules env2 rules
@@ -1744,9 +1770,9 @@ Solution: (see Trac #15552 for other variants)
 
     * The map is of course stateful, held in a TcRef. (That is unlike
       the treatment of lexically-scoped variables in ze_tv_env and
-      ze_id_env.
+      ze_id_env.)
 
-    Is the extra work worth it.  Some non-sytematic perf measurements
+    Is the extra work worth it?  Some non-sytematic perf measurements
     suggest that compiler allocation is reduced overall (by 0.5% or so)
     but compile time really doesn't change.
 -}
@@ -1865,13 +1891,13 @@ zonkTcTyConToTyCon tc
 
 -- Confused by zonking? See Note [What is zonking?] in TcMType.
 zonkTcTypeToType :: TcType -> TcM Type
-zonkTcTypeToType = initZonkEnv zonkTcTypeToTypeX
+zonkTcTypeToType ty = initZonkEnv $ \ ze -> zonkTcTypeToTypeX ze ty
 
 zonkTcTypeToTypeX :: ZonkEnv -> TcType -> TcM Type
 zonkTcTypeToTypeX = mapType zonk_tycomapper
 
 zonkTcTypesToTypes :: [TcType] -> TcM [Type]
-zonkTcTypesToTypes = initZonkEnv zonkTcTypesToTypesX
+zonkTcTypesToTypes tys = initZonkEnv $ \ ze -> zonkTcTypesToTypesX ze tys
 
 zonkTcTypesToTypesX :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypesToTypesX env tys = mapM (zonkTcTypeToTypeX env) tys
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 24b416c6e8..b3c40274c4 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -190,9 +190,9 @@ tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
 kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
 kcHsSigType names (HsIB { hsib_body = hs_ty
                                   , hsib_ext = sig_vars })
-  = addSigCtxt (funsSigCtxt names) hs_ty $
-    discardResult $
-    bindImplicitTKBndrs_Skol sig_vars $
+  = discardResult                        $
+    addSigCtxt (funsSigCtxt names) hs_ty $
+    bindImplicitTKBndrs_Skol sig_vars    $
     tc_lhs_type typeLevelMode hs_ty liftedTypeKind
 
 kcHsSigType _ (XHsImplicitBndrs _) = panic "kcHsSigType"
@@ -238,7 +238,6 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
                  solveLocalEqualitiesX "tc_hs_sig_type" $
                  bindImplicitTKBndrs_Skol sig_vars      $
                  do { kind <- newExpectedKind ctxt_kind
-
                     ; tc_lhs_type typeLevelMode hs_ty kind }
        -- Any remaining variables (unsolved in the solveLocalEqualities)
        -- should be in the global tyvars, and therefore won't be quantified
@@ -1864,15 +1863,12 @@ kcLHsQTyVars_Cusk name flav
                               ++ map (mkRequiredTyConBinder mentioned_kv_set) tc_tvs
 
              all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
-             tycon = mkTcTyCon name
-                               final_tc_binders
-                               res_kind
-                               all_tv_prs
+             tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs
                                True {- it is generalised -} flav
          -- If the ordering from
          -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls
          -- doesn't work, we catch it here, before an error cascade
-       ; checkValidTelescope tycon
+       ; checkTyConTelescope tycon
 
        ; traceTc "kcLHsQTyVars: cusk" $
          vcat [ text "name" <+> ppr name
@@ -1921,8 +1917,13 @@ kcLHsQTyVars_NonCusk name flav
                -- Also, note that tc_binders has the tyvars from only the
                -- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
                -- in TcTyClsDecls
-             tycon = mkTcTyCon name tc_binders res_kind
-                               (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
+
+             all_tv_prs = (kv_ns                `zip` scoped_kvs) ++
+                          (hsLTyVarNames hs_tvs `zip` tc_tvs)
+               -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification
+               --     variables, hence the need to zip here.  Ditto bindExplicit..
+               -- See TcMType Note [Unification variables need fresh Names]
+             tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
                                False -- not yet generalised
                                flav
 
@@ -2046,32 +2047,24 @@ expectedKindInCtxt _                   = OpenKind
 
 bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
   bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
-  :: [Name]
-  -> TcM a
-  -> TcM ([TcTyVar], a)
+  :: [Name] -> TcM a -> TcM ([TcTyVar], a)
 bindImplicitTKBndrs_Skol   = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar
 bindImplicitTKBndrs_Tv     = bindImplicitTKBndrsX newFlexiKindedTyVarTyVar
 bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedSkolemTyVar)
 bindImplicitTKBndrs_Q_Tv   = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedTyVarTyVar)
 
-bindImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
-                    -> [Name]
-                    -> TcM a
-                    -> TcM ([TcTyVar], a)   -- these tyvars are dependency-ordered
--- * Guarantees to call solveLocalEqualities to unify
---   all constraints from thing_inside.
---
--- * Returned TcTyVars have the supplied HsTyVarBndrs,
---   but may be in different order to the original [Name]
---   (because of sorting to respect dependency)
---
--- * Returned TcTyVars have zonked kinds
---   See Note [Keeping scoped variables in order: Implicit]
+bindImplicitTKBndrsX
+   :: (Name -> TcM TcTyVar) -- new_tv function
+   -> [Name]
+   -> TcM a
+   -> TcM ([TcTyVar], a)   -- Returned [TcTyVar] are in 1-1 correspondence
+                           -- with the passed in [Name]
 bindImplicitTKBndrsX new_tv tv_names thing_inside
   = do { tkvs <- mapM new_tv tv_names
-       ; result <- tcExtendTyVarEnv tkvs thing_inside
        ; traceTc "bindImplicitTKBndrs" (ppr tv_names $$ ppr tkvs)
-       ; return (tkvs, result) }
+       ; res <- tcExtendNameTyVarEnv (tv_names `zip` tkvs)
+                thing_inside
+       ; return (tkvs, res) }
 
 newImplicitTyVarQ :: (Name -> TcM TcTyVar) ->  Name -> TcM TcTyVar
 -- Behave like new_tv, except that if the tyvar is in scope, use it
@@ -2091,6 +2084,7 @@ newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
 
 newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
 newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
+   -- See Note [Unification variables need fresh Names] in TcMType
 
 --------------------------------------
 -- Explicit binders
@@ -2119,7 +2113,8 @@ bindExplicitTKBndrsX
     :: (HsTyVarBndr GhcRn -> TcM TcTyVar)
     -> [LHsTyVarBndr GhcRn]
     -> TcM a
-    -> TcM ([TcTyVar], a)
+    -> TcM ([TcTyVar], a)  -- Returned [TcTyVar] are in 1-1 correspondence
+                           -- with the passed-in [LHsTyVarBndr]
 bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
   = do { traceTc "bindExplicTKBndrs" (ppr hs_tvs)
        ; go hs_tvs }
@@ -2128,7 +2123,13 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
                ; return ([], res) }
     go (L _ hs_tv : hs_tvs)
        = do { tv <- tc_tv hs_tv
-            ; (tvs, res) <- tcExtendTyVarEnv [tv] (go hs_tvs)
+            -- Extend the environment as we go, in case a binder
+            -- is mentioned in the kind of a later binder
+            --   e.g. forall k (a::k). blah
+            -- NB: tv's Name may differ from hs_tv's
+            -- See TcMType Note [Unification variables need fresh Names]
+            ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
+                           go hs_tvs
             ; return (tv:tvs, res) }
 
 -----------------
@@ -2192,7 +2193,7 @@ bindTyClTyVars tycon_name thing_inside
        ; let scoped_prs = tcTyConScopedTyVars tycon
              res_kind   = tyConResKind tycon
              binders    = tyConBinders tycon
-       ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders)
+       ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders $$ ppr scoped_prs)
        ; tcExtendNameTyVarEnv scoped_prs $
          thing_inside binders res_kind }
 
@@ -2215,8 +2216,8 @@ kcLookupTcTyCon nm
 
 zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
 zonkAndScopedSort spec_tkvs
-  = do { spec_tkvs <- mapM zonkTcTyCoVarBndr spec_tkvs
-          -- Use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
+  = do { spec_tkvs <- mapM zonkAndSkolemise spec_tkvs
+          -- Use zonkAndSkolemise because a skol_tv might be a TyVarTv
 
        -- Do a stable topological sort, following
        -- Note [Ordering of implicit variables] in RnTypes
@@ -2503,7 +2504,7 @@ tcHsPartialSigType ctxt sig_ty
          -- in partial type signatures that bind scoped type variables, as
          -- we bring the wrong name into scope in the function body.
          -- Test case: partial-sigs/should_compile/LocalDefinitionBug
-       ; let tv_names = map tyVarName (implicit_tvs ++ explicit_tvs)
+       ; let tv_names = implicit_hs_tvs ++ hsLTyVarNames explicit_hs_tvs
 
        -- Spit out the wildcards (including the extra-constraints one)
        -- as "hole" constraints, so that they'll be reported if necessary
@@ -2520,7 +2521,7 @@ tcHsPartialSigType ctxt sig_ty
          -- we need to promote the TyVarTvs so we don't violate the TcLevel
          -- invariant
        ; implicit_tvs <- zonkAndScopedSort implicit_tvs
-       ; explicit_tvs <- mapM zonkTcTyCoVarBndr explicit_tvs
+       ; explicit_tvs <- mapM zonkAndSkolemise explicit_tvs
        ; theta        <- mapM zonkTcType theta
        ; tau          <- zonkTcType tau
 
@@ -2605,17 +2606,17 @@ tcHsPatSigType :: UserTypeCtxt
 -- See Note [Recipe for checking a signature]
 tcHsPatSigType ctxt sig_ty
   | HsWC { hswc_ext = sig_wcs,   hswc_body = ib_ty } <- sig_ty
-  , HsIB { hsib_ext = sig_vars
+  , HsIB { hsib_ext = sig_ns
          , hsib_body = hs_ty } <- ib_ty
   = addSigCtxt ctxt hs_ty $
-    do { sig_tkvs <- mapM new_implicit_tv sig_vars
+    do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
        ; (wcs, sig_ty)
             <- solveLocalEqualities "tcHsPatSigType" $
                  -- Always solve local equalities if possible,
                  -- else casts get in the way of deep skolemisation
                  -- (Trac #16033)
-               tcWildCardBinders sig_wcs  $ \ wcs ->
-               tcExtendTyVarEnv sig_tkvs                           $
+               tcWildCardBinders sig_wcs        $ \ wcs ->
+               tcExtendNameTyVarEnv sig_tkv_prs $
                do { sig_ty <- tcHsOpenType hs_ty
                   ; return (wcs, sig_ty) }
 
@@ -2629,19 +2630,17 @@ tcHsPatSigType ctxt sig_ty
         ; sig_ty <- zonkPromoteType sig_ty
         ; checkValidType ctxt sig_ty
 
-        ; let tv_pairs = mkTyVarNamePairs sig_tkvs
-
-        ; traceTc "tcHsPatSigType" (ppr sig_vars)
-        ; return (wcs, tv_pairs, sig_ty) }
+        ; traceTc "tcHsPatSigType" (ppr sig_tkv_prs)
+        ; return (wcs, sig_tkv_prs, sig_ty) }
   where
-    new_implicit_tv name = do { kind <- newMetaKindVar
-                              ; new_tv name kind }
-
-    new_tv = case ctxt of
-               RuleSigCtxt {} -> newSkolemTyVar
-               _              -> newTauTyVar
-      -- See Note [Pattern signature binders]
-
+    new_implicit_tv name
+      = do { kind <- newMetaKindVar
+           ; tv   <- case ctxt of
+                       RuleSigCtxt {} -> newSkolemTyVar name kind
+                       _              -> newPatSigTyVar name kind
+                       -- See Note [Pattern signature binders]
+             -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
+           ; return (name, tv) }
 
 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
 tcHsPatSigType _ (XHsWildCardBndrs _)          = panic "tcHsPatSigType"
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 19fbadeacf..0c9e0e223e 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -52,7 +52,7 @@ module TcMType (
   -- Instantiation
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
   newMetaTyVarTyVars, newMetaTyVarTyVarX,
-  newTyVarTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
+  newTyVarTyVar, newPatSigTyVar, newSkolemTyVar, newWildCardX,
   tcInstType,
   tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
   tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
@@ -70,9 +70,8 @@ module TcMType (
   candidateQTyVarsOfType,  candidateQTyVarsOfKind,
   candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
   CandidatesQTvs(..), delCandidates, candidateKindVars,
-  skolemiseQuantifiedTyVar, defaultTyVar,
-  quantifyTyVars,
-  zonkTcTyCoVarBndr, zonkTyConBinders,
+  zonkAndSkolemise, skolemiseQuantifiedTyVar,
+  defaultTyVar, quantifyTyVars,
   zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind,
 
@@ -141,11 +140,12 @@ kind_var_occ :: OccName -- Just one for all MetaKindVars
 kind_var_occ = mkOccName tvName "k"
 
 newMetaKindVar :: TcM TcKind
-newMetaKindVar = do { uniq <- newUnique
-                    ; details <- newMetaDetails TauTv
-                    ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
-                    ; traceTc "newMetaKindVar" (ppr kv)
-                    ; return (mkTyVarTy kv) }
+newMetaKindVar
+  = do { details <- newMetaDetails TauTv
+       ; uniq <- newUnique
+       ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
+       ; traceTc "newMetaKindVar" (ppr kv)
+       ; return (mkTyVarTy kv) }
 
 newMetaKindVars :: Int -> TcM [TcKind]
 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
@@ -661,42 +661,118 @@ The remaining uses of newTyVarTyVars are
 * In partial type signatures, see Note [Quantified variables in partial type signatures]
 -}
 
--- see Note [TyVarTv]
+newMetaTyVarName :: FastString -> TcM Name
+-- Makes a /System/ Name, which is eagerly eliminated by
+-- the unifier; see TcUnify.nicer_to_update_tv1, and
+-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
+newMetaTyVarName str
+  = do { uniq <- newUnique
+       ; return (mkSystemName uniq (mkTyVarOccFS str)) }
+
+cloneMetaTyVarName :: Name -> TcM Name
+cloneMetaTyVarName name
+  = do { uniq <- newUnique
+       ; return (mkSystemName uniq (nameOccName name)) }
+         -- See Note [Name of an instantiated type variable]
+
+{- Note [Name of an instantiated type variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+At the moment we give a unification variable a System Name, which
+influences the way it is tidied; see TypeRep.tidyTyVarBndr.
+
+Note [Unification variables need fresh Names]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Whenever we allocate a unification variable (MetaTyVar) we give
+it a fresh name.   Trac #16221 is a very tricky case that illustrates
+why this is important:
+
+   data SameKind :: k -> k -> *
+   data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int
+
+When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl
+we allocate a unification variable kappa2 for k2, and then we
+end up unifying kappa1 := kappa2 (because of the (SameKind a b).
+
+Now we generalise over kappa2; but if kappa2's Name is k2,
+we'll end up giving T0 the kind forall k2. k2 -> *.  Nothing
+directly wrong with that but when we typecheck the data constrautor
+we end up giving it the type
+  MkT0 :: forall k1 (a :: k1) k2 (b :: k2).
+          SameKind @k2 a b -> Int -> T0 @{k2} a
+which is bogus.  The result type should be T0 @{k1} a.
+
+And there no reason /not/ to clone the Name when making a
+unification variable.  So that's what we do.
+-}
+
+newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
+-- Make a new meta tyvar out of thin air
+newAnonMetaTyVar meta_info kind
+  = do  { let s = case meta_info of
+                        TauTv       -> fsLit "t"
+                        FlatMetaTv  -> fsLit "fmv"
+                        FlatSkolTv  -> fsLit "fsk"
+                        TyVarTv      -> fsLit "a"
+        ; name    <- newMetaTyVarName s
+        ; details <- newMetaDetails meta_info
+        ; let tyvar = mkTcTyVar name kind details
+        ; traceTc "newAnonMetaTyVar" (ppr tyvar)
+        ; return tyvar }
+
+-- makes a new skolem tv
+newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
+newSkolemTyVar name kind
+  = do { lvl <- getTcLevel
+       ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
+
 newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
+-- See Note [TyVarTv]
+-- See Note [Unification variables need fresh Names]
 newTyVarTyVar name kind
   = do { details <- newMetaDetails TyVarTv
-       ; let tyvar = mkTcTyVar name kind details
+       ; uniq <- newUnique
+       ; let name' = name `setNameUnique` uniq
+             tyvar = mkTcTyVar name' kind details
+         -- Don't use cloneMetaTyVar, which makes a SystemName
+         -- We want to keep the original more user-friendly Name
+         -- In practical terms that means that in error messages,
+         -- when the Name is tidied we get 'a' rather than 'a0'
        ; traceTc "newTyVarTyVar" (ppr tyvar)
        ; return tyvar }
 
+newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
+newPatSigTyVar name kind
+  = do { details <- newMetaDetails TauTv
+       ; uniq <- newUnique
+       ; let name' = name `setNameUnique` uniq
+             tyvar = mkTcTyVar name' kind details
+         -- Don't use cloneMetaTyVar;
+         -- same reasoning as in newTyVarTyVar
+       ; traceTc "newPatSigTyVar" (ppr tyvar)
+       ; return tyvar }
 
--- makes a new skolem tv
-newSkolemTyVar :: Name -> Kind -> TcM TcTyVar
-newSkolemTyVar name kind = do { lvl <- getTcLevel
-                              ; return (mkTcTyVar name kind (SkolemTv lvl False)) }
+cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
+-- Make a fresh MetaTyVar, basing the name
+-- on that of the supplied TyVar
+cloneAnonMetaTyVar info tv kind
+  = do  { details <- newMetaDetails info
+        ; name    <- cloneMetaTyVarName (tyVarName tv)
+        ; let tyvar = mkTcTyVar name kind details
+        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
+        ; return tyvar }
 
 newFskTyVar :: TcType -> TcM TcTyVar
 newFskTyVar fam_ty
-  = do { uniq <- newUnique
-       ; ref  <- newMutVar Flexi
-       ; tclvl <- getTcLevel
-       ; let details = MetaTv { mtv_info  = FlatSkolTv
-                              , mtv_ref   = ref
-                              , mtv_tclvl = tclvl }
-             name = mkMetaTyVarName uniq (fsLit "fsk")
+  = do { details <- newMetaDetails FlatSkolTv
+       ; name <- newMetaTyVarName (fsLit "fsk")
        ; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
 
 newFmvTyVar :: TcType -> TcM TcTyVar
 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
 -- so that the fmv is untouchable.
 newFmvTyVar fam_ty
-  = do { uniq <- newUnique
-       ; ref  <- newMutVar Flexi
-       ; tclvl <- getTcLevel
-       ; let details = MetaTv { mtv_info  = FlatMetaTv
-                              , mtv_ref   = ref
-                              , mtv_tclvl = tclvl }
-             name = mkMetaTyVarName uniq (fsLit "s")
+  = do { details <- newMetaDetails FlatMetaTv
+       ; name <- newMetaTyVarName (fsLit "s")
        ; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
 
 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
@@ -710,10 +786,9 @@ newMetaDetails info
 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
 cloneMetaTyVar tv
   = ASSERT( isTcTyVar tv )
-    do  { uniq <- newUnique
-        ; ref  <- newMutVar Flexi
-        ; let name'    = setNameUnique (tyVarName tv) uniq
-              details' = case tcTyVarDetails tv of
+    do  { ref  <- newMutVar Flexi
+        ; name' <- cloneMetaTyVarName (tyVarName tv)
+        ; let details' = case tcTyVarDetails tv of
                            details@(MetaTv {}) -> details { mtv_ref = ref }
                            _ -> pprPanic "cloneMetaTyVar" (ppr tv)
               tyvar = mkTcTyVar name' (tyVarKind tv) details'
@@ -859,51 +934,6 @@ coercion variables, except for the special case of the promoted Eq#. But,
 that can't ever appear in user code, so we're safe!
 -}
 
-newTauTyVar :: Name -> Kind -> TcM TcTyVar
-newTauTyVar name kind
-  = do { details <- newMetaDetails TauTv
-       ; let tyvar = mkTcTyVar name kind details
-       ; traceTc "newTauTyVar" (ppr tyvar)
-       ; return tyvar }
-
-
-mkMetaTyVarName :: Unique -> FastString -> Name
--- Makes a /System/ Name, which is eagerly eliminated by
--- the unifier; see TcUnify.nicer_to_update_tv1, and
--- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
-mkMetaTyVarName uniq str = mkSystemName uniq (mkTyVarOccFS str)
-
-newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
--- Make a new meta tyvar out of thin air
-newAnonMetaTyVar meta_info kind
-  = do  { uniq <- newUnique
-        ; let name = mkMetaTyVarName uniq s
-              s = case meta_info of
-                        TauTv       -> fsLit "t"
-                        FlatMetaTv  -> fsLit "fmv"
-                        FlatSkolTv  -> fsLit "fsk"
-                        TyVarTv      -> fsLit "a"
-        ; details <- newMetaDetails meta_info
-        ; let tyvar = mkTcTyVar name kind details
-        ; traceTc "newAnonMetaTyVar" (ppr tyvar)
-        ; return tyvar }
-
-cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
--- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
-cloneAnonMetaTyVar info tv kind
-  = do  { uniq    <- newUnique
-        ; details <- newMetaDetails info
-        ; let name = mkSystemName uniq (getOccName tv)
-                       -- See Note [Name of an instantiated type variable]
-              tyvar = mkTcTyVar name kind details
-        ; traceTc "cloneAnonMetaTyVar" (ppr tyvar)
-        ; return tyvar }
-
-{- Note [Name of an instantiated type variable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-At the moment we give a unification variable a System Name, which
-influences the way it is tidied; see TypeRep.tidyTyVarBndr.
--}
 
 newFlexiTyVar :: Kind -> TcM TcTyVar
 newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
@@ -978,10 +1008,9 @@ new_meta_tv_x info subst tv
 
 newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
 newMetaTyVarTyAtLevel tc_lvl kind
-  = do  { uniq <- newUnique
-        ; ref  <- newMutVar Flexi
-        ; let name = mkMetaTyVarName uniq (fsLit "p")
-              details = MetaTv { mtv_info  = TauTv
+  = do  { ref  <- newMutVar Flexi
+        ; name <- newMetaTyVarName (fsLit "p")
+        ; let details = MetaTv { mtv_info  = TauTv
                                , mtv_ref   = ref
                                , mtv_tclvl = tc_lvl }
         ; return (mkTyVarTy (mkTcTyVar name kind details)) }
@@ -1472,6 +1501,24 @@ quantifiableTv outer_tclvl tcv
   | otherwise
   = False
 
+zonkAndSkolemise :: 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
+  | 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 }
+
+  | otherwise
+  = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
+    zonkTyCoVarKind tyvar
+
 skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables
@@ -1973,35 +2020,6 @@ zonkTcType = mapType zonkTcTypeMapper ()
 zonkCo :: Coercion -> TcM Coercion
 zonkCo = mapCoercion zonkTcTypeMapper ()
 
-zonkTcTyCoVarBndr :: 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.
-zonkTcTyCoVarBndr 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_ty <- zonkTcTyVar tyvar
-       ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty
-             zonked_name  = getName zonked_tyvar
-             reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar)
-       ; return (setTyVarName zonked_tyvar reloc'd_name) }
-
-  | otherwise
-  = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar )
-    zonkTyCoVarKind tyvar
-
-zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder]
-zonkTyConBinders = mapM zonk1
-  where
-    zonk1 (Bndr tv vis)
-      = do { tv' <- zonkTcTyCoVarBndr tv
-           ; return (Bndr tv' vis) }
-
 zonkTcTyVar :: TcTyVar -> TcM TcType
 -- Simply look through all Flexis
 zonkTcTyVar tv
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 17e3f54893..9146b10fe2 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -382,8 +382,8 @@ tcPatSynSig name sig_ty
                      -- e.g. pattern Zero <- 0#   (Trac #12094)
                  ; return (req, prov, body_ty) }
 
-       ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs req
-                                                 ex_tvs prov body_ty
+       ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs
+                                                 req ex_tvs prov body_ty
 
        -- Kind generalisation
        ; kvs <- kindGeneralize ungen_patsyn_ty
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index eb8a066529..8d413139ba 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -536,94 +536,121 @@ generaliseTcTyCon tc
   -- See Note [Required, Specified, and Inferred for types]
   = setSrcSpan (getSrcSpan tc) $
     addTyConCtxt tc $
-    do { let tc_name     = tyConName tc
-             tc_res_kind = tyConResKind tc
-             tc_tvs      = tyConTyVars  tc
-
-             (scoped_tv_names, scoped_tvs) = unzip (tcTyConScopedTyVars tc)
-             -- NB: scoped_tvs includes both specified and required (tc_tvs)
-             -- ToDo: Is this a good idea?
-
-       -- Step 1: find all the variables we want to quantify over,
-       --         including Inferred, Specfied, and Required
-       ; dvs <- candidateQTyVarsOfKinds $
-                (tc_res_kind : map tyVarKind scoped_tvs)
-       ; tc_tvs      <- mapM zonkTcTyVarToTyVar tc_tvs
-       ; let full_dvs = dvs { dv_tvs = mkDVarSet tc_tvs }
-
-       -- Step 2: quantify, mainly meaning skolemise the free variables
-       ; qtkvs <- quantifyTyVars emptyVarSet full_dvs
-                  -- Returned 'qtkvs' are scope-sorted and skolemised
-
-       -- Step 3: find the final identity of the Specified and Required tc_tvs
+    do { let tc_name      = tyConName tc
+             tc_res_kind  = tyConResKind tc
+             spec_req_prs = tcTyConScopedTyVars tc
+
+             (spec_req_names, spec_req_tvs) = unzip spec_req_prs
+             -- NB: spec_req_tvs includes both Specified and Required
+             -- Running example in Note [Inferring kinds for type declarations]
+             --    spec_req_prs = [ ("k1",kk1), ("a", (aa::kk1))
+             --                   , ("k2",kk2), ("x", (xx::kk2))]
+             -- where "k1" dnotes the Name k1, and kk1, aa, etc are MetaTyVarss,
+             -- specifically TyVarTvs
+
+       -- Step 0: zonk and skolemise the Specified and Required binders
+       -- It's essential that they are skolems, not MetaTyVars,
+       -- for Step 3 to work right
+       ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs
+             -- Running example, where kk1 := kk2, so we get
+             --   [kk2,kk2]
+
+       -- Step 1: Check for duplicates
+       -- E.g. data SameKind (a::k) (b::k)
+       --      data T (a::k1) (b::k2) = MkT (SameKind a b)
+       -- Here k1 and k2 start as TyVarTvs, and get unified with each other
+       -- If this happens, things get very confused later, so fail fast
+       ; checkDuplicateTyConBinders spec_req_names spec_req_tvs
+
+       -- Step 2a: find all the Inferred variables we want to quantify over
+       -- NB: candidateQTyVarsOfKinds zonks as it goes
+       ; dvs1 <- candidateQTyVarsOfKinds $
+                (tc_res_kind : map tyVarKind spec_req_tvs)
+       ; let dvs2 = dvs1 `delCandidates` spec_req_tvs
+
+       -- Step 2b: quantify, mainly meaning skolemise the free variables
+       -- Returned 'inferred' are scope-sorted and skolemised
+       ; inferred <- quantifyTyVars emptyVarSet dvs2
+
+       -- Step 3a: rename all the Specified and Required tyvars back to
+       -- TyVars with their oroginal user-specified name.  Example
+       --     class C a_r23 where ....
+       -- By this point we have scoped_prs = [(a_r23, a_r89[TyVarTv])]
+       -- We return with the TyVar a_r23[TyVar],
+       --    and ze mapping a_r89 :-> a_r23[TyVar]
+       ; traceTc "generaliseTcTyCon: before zonkRec"
+           (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
+                 , text "inferred =" <+> pprTyVars inferred ])
+       ; (ze, final_spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs
+           -- So ze maps from the tyvars that have ended up
+
+       -- Step 3b: Apply that mapping to the other variables
        -- (remember they all started as TyVarTvs).
        -- They have been skolemised by quantifyTyVars.
-       ; scoped_tvs  <- mapM zonkTcTyVarToTyVar scoped_tvs
-       ; tc_tvs      <- mapM zonkTcTyVarToTyVar tc_tvs
-       ; tc_res_kind <- zonkTcType tc_res_kind
+       ; (ze, inferred) <- zonkTyBndrsX ze inferred
+       ; tc_res_kind    <- zonkTcTypeToTypeX ze tc_res_kind
 
-       ; traceTc "Generalise kind pre" $
+       ; traceTc "generaliseTcTyCon: post zonk" $
          vcat [ text "tycon =" <+> ppr tc
-              , text "tc_tvs =" <+> pprTyVars tc_tvs
-              , text "scoped_tvs =" <+> pprTyVars scoped_tvs ]
+              , text "inferred =" <+> pprTyVars inferred
+              , text "ze =" <+> ppr ze
+              , text "spec_req_prs =" <+> ppr spec_req_prs
+              , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs
+              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs ]
 
        -- Step 4: Find the Specified and Inferred variables
-       -- First, delete the Required tc_tvs from qtkvs; then
-       -- partition by whether they are scoped (if so, Specified)
-       ; let qtkv_set      = mkVarSet qtkvs
-             tc_tv_set     = mkVarSet tc_tvs
-             specified     = scopedSort $
-                             [ tv | tv <- scoped_tvs
-                                  , not (tv `elemVarSet` tc_tv_set)
-                                  , tv `elemVarSet` qtkv_set ]
+       -- NB: spec_req_tvs = spec_tvs ++ req_tvs
+       --     And req_tvs is 1-1 with tyConTyVars
+       --     See Note [Scoped tyvars in a TcTyCon] in TyCon
+       ; let n_spec        = length final_spec_req_tvs - tyConArity tc
+             (spec_tvs, req_tvs) = splitAt n_spec final_spec_req_tvs
+             specified     = scopedSort spec_tvs
                              -- NB: maintain the L-R order of scoped_tvs
-             spec_req_set  = mkVarSet specified `unionVarSet` tc_tv_set
-             inferred      = filterOut (`elemVarSet` spec_req_set) qtkvs
 
        -- Step 5: Make the TyConBinders.
-             dep_fv_set     = candidateKindVars dvs
+             to_user tv     = lookupTyVarOcc ze tv `orElse` tv
+             dep_fv_set     = mapVarSet to_user (candidateKindVars dvs1)
              inferred_tcbs  = mkNamedTyConBinders Inferred inferred
              specified_tcbs = mkNamedTyConBinders Specified specified
-             required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) tc_tvs
+             required_tcbs  = map (mkRequiredTyConBinder dep_fv_set) req_tvs
 
        -- Step 6: Assemble the final list.
              final_tcbs = concat [ inferred_tcbs
                                  , specified_tcbs
                                  , required_tcbs ]
 
-             scoped_tv_pairs = scoped_tv_names `zip` scoped_tvs
-
        -- Step 7: Make the result TcTyCon
              tycon = mkTcTyCon tc_name final_tcbs tc_res_kind
-                            scoped_tv_pairs
+                            (mkTyVarNamePairs final_spec_req_tvs)
                             True {- it's generalised now -}
                             (tyConFlavour tc)
 
-       ; traceTc "Generalise kind" $
+       ; traceTc "generaliseTcTyCon done" $
          vcat [ text "tycon =" <+> ppr tc
-              , text "tc_tvs =" <+> pprTyVars tc_tvs
               , text "tc_res_kind =" <+> ppr tc_res_kind
-              , text "scoped_tvs =" <+> pprTyVars scoped_tvs
+              , text "dep_fv_set =" <+> ppr dep_fv_set
+              , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs
               , text "inferred =" <+> pprTyVars inferred
               , text "specified =" <+> pprTyVars specified
               , text "required_tcbs =" <+> ppr required_tcbs
               , text "final_tcbs =" <+> ppr final_tcbs ]
 
-       -- Step 8: Check for duplicates
-       -- E.g. data SameKind (a::k) (b::k)
-       --      data T (a::k1) (b::k2) = MkT (SameKind a b)
-       -- Here k1 and k2 start as TyVarTvs, and get unified with each other
-       ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_tv_pairs)
-
-       -- Step 9: Check for validity.
-       -- We do this here because we're about to put the tycon into
-       -- the environment, and we don't want anything malformed in the
-       -- environment.
-       ; checkValidTelescope tycon
+       -- Step 8: Check for validity.
+       -- We do this here because we're about to put the tycon into the
+       -- the environment, and we don't want anything malformed there
+       ; checkTyConTelescope tycon
 
        ; return tycon }
+
+checkDuplicateTyConBinders :: [Name] -> [TcTyVar] -> TcM ()
+checkDuplicateTyConBinders spec_req_names spec_req_tvs
+  | null dups = return ()
+  | otherwise = mapM_ report_dup dups >> failM
   where
-    report_sig_tv_err (n1, n2)
+    dups :: [(Name,Name)]
+    dups = findDupTyVarTvs $ spec_req_names `zip` spec_req_tvs
+
+    report_dup (n1, n2)
       = setSrcSpan (getSrcSpan n2) $
         addErrTc (text "Couldn't match" <+> quotes (ppr n1)
                         <+> text "with" <+> quotes (ppr n2))
@@ -669,7 +696,7 @@ Example:
   data SameKind :: k -> k -> *
   data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d)
 
-For X:
+For Bad:
   - a, c, d, x are Required; they are explicitly listed by the user
     as the positional arguments of Bad
   - b is Specified; it appears explicitly in a kind signature
@@ -711,7 +738,7 @@ How it works
 These design choices are implemented by two completely different code
 paths for
 
-  * Declarations with a compulete user-specified kind signature (CUSK)
+  * Declarations with a complete user-specified kind signature (CUSK)
     Handed by the CUSK case of kcLHsQTyVars.
 
   * Declarations without a CUSK are handled by kcTyClDecl; see
@@ -726,7 +753,6 @@ tyvars; Specified are always included there.
 
 Design alternatives
 ~~~~~~~~~~~~~~~~~~~
-
 * For associated types we considered putting the class variables
   before the local variables, in a nod to the treatment for class
   methods. But it got too compilicated; see Trac #15592, comment:21ff.
@@ -761,41 +787,62 @@ that do not have a CUSK.  Consider
 
 We do kind inference as follows:
 
-* Step 1: Assign initial monomorophic kinds to S, T
+* Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk.
+  Make a unification variable for each of the Required and Specified
+  type varialbes in the header.
+
+  Record the connection between the Names the user wrote and the
+  fresh unification variables in the tcTyConScopedTyVars field
+  of the TcTyCon we are making
+      [ (a,  aa)
+      , (k1, kk1)
+      , (k2, kk2)
+      , (x,  xx) ]
+  (I'm using the convention that double letter like 'aa' or 'kk'
+  mean a unification variable.)
+
+  These unification variables
+    - Are TyVarTvs: that is, unification variables that can
+      unify only with other type variables.
+      See Note [Signature skolems] in TcType
+
+    - Have complete fresh Names; see TcMType
+      Note [Unification variables need fresh Names]
+
+  Assign initial monomorophic kinds to S, T
           S :: kk1 -> * -> kk2 -> *
           T :: kk3 -> * -> kk4 -> *
-  Here kk1 etc are TyVarTvs: that is, unification variables that
-  are allowed to unify only with other type variables. See
-  Note [Signature skolems] in TcType
 
-* Step 2: Extend the environment with a TcTyCon for S and T, with
-  these monomophic kinds.  Now kind-check the declarations, and solve
-  the resulting equalities.  The goal here is to discover constraints
-  on all these unification variables.
+* Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and
+  T, with these monomophic kinds.  Now kind-check the declarations,
+  and solve the resulting equalities.  The goal here is to discover
+  constraints on all these unification variables.
 
   Here we find that kk1 := kk3, and kk2 := kk4.
 
   This is why we can't use skolems for kk1 etc; they have to
   unify with each other.
 
-* Step 3. Generalise each TyCon in turn (generaliseTcTyCon).
+* Step 3: generaliseTcTyCon. Generalise each TyCon in turn.
   We find the free variables of the kind, skolemise them,
   sort them out into Inferred/Required/Specified (see the above
   Note [Required, Specified, and Inferred for types]),
   and perform some validity checks.
 
-  This makes the utterly-final TyConBinders for the TyCon
+  This makes the utterly-final TyConBinders for the TyCon.
 
   All this is very similar at the level of terms: see TcBinds
   Note [Quantified variables in partial type signatures]
 
+  But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]
+
 * Step 4.  Extend the type environment with a TcTyCon for S and T, now
   with their utterly-final polymorphic kinds (needed for recursive
   occurrences of S, T).  Now typecheck the declarations, and build the
   final AlgTyCOn for S and T resp.
 
-The first three steps are in kcTyClGroup;
-the fourth is in tcTyClDecls.
+The first three steps are in kcTyClGroup; the fourth is in
+tcTyClDecls.
 
 There are some wrinkles
 
@@ -834,7 +881,51 @@ There are some wrinkles
     a) when collecting quantification candidates, in
        candidateQTyVarsOfKind, we must collect skolems
     b) quantifyTyVars should be a no-op on such a skolem
--}
+
+Note [Tricky scoping in generaliseTcTyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider Trac #16342
+  class C (a::ka) x where
+    cop :: D a x => x -> Proxy a -> Proxy a
+    cop _ x = x :: Proxy (a::ka)
+
+  class D (b::kb) y where
+    dop :: C b y => y -> Proxy b -> Proxy b
+    dop _ x = x :: Proxy (b::kb)
+
+C and D are mutually recursive, by the time we get to
+generaliseTcTyCon we'll have unified kka := kkb.
+
+But when typechecking the default declarations for 'cop' and 'dop' in
+tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope.
+But at that point all we have is the utterly-final Class itself.
+
+Conclusion: the classTyVars of a class must have the same Mame as
+that originally assigned by the user.  In our example, C must have
+classTyVars {a, ka, x} while D has classTyVars {a, kb, y}.  Despite
+the fact that kka and kkb got unified!
+
+We achieve this sleight of hand in generaliseTcTyCon, using
+the specialised function zonkRecTyVarBndrs.  We make the call
+   zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx]
+where the [ka,a,x] are the Names originally assigned by the user, and
+[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars.
+zonkRecTyVarBndrs builds a recursive ZonkEnv that binds
+   kkb :-> (ka :: <zonked kind of kkb>)
+   aa  :-> (a  :: <konked kind of aa>)
+   etc
+That is, it maps each skolemised TcTyVars to the utterly-final
+TyVar to put in the class, with its correct user-specified name.
+When generalising D we'll do the same thing, but the ZonkEnv will map
+   kkb :-> (kb :: <zonked kind of kkb>)
+   bb  :-> (b  :: <konked kind of bb>)
+   etc
+Note that 'kkb' again appears in the domain of the mapping, but this
+time mapped to 'kb'.  That's how C and D end up with differently-named
+final TyVars despite the fact that we unified kka:=kkb
+
+zonkRecTyVarBndrs we need to do knot-tying because of the need to
+apply this same substitution to the kind of each.  -}
 
 --------------
 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
@@ -1051,7 +1142,7 @@ kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
                       , con_mb_cxt = ex_ctxt, con_args = args })
   = addErrCtxt (dataConCtxtName [name]) $
     discardResult                   $
-    bindExplicitTKBndrs_Skol ex_tvs $
+    bindExplicitTKBndrs_Tv ex_tvs $
     do { _ <- tcHsMbContext ex_ctxt
        ; traceTc "kcConDecl {" (ppr name $$ ppr args)
        ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index d17ac0f567..90c2b5a4a7 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -13,7 +13,7 @@ module TcValidity (
   checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn, checkConsistentFamInst,
   badATErr, arityErr,
-  checkValidTelescope,
+  checkTyConTelescope,
   allDistinctTyVars
   ) where
 
@@ -40,7 +40,7 @@ import TyCon
 
 -- others:
 import IfaceType( pprIfaceType, pprIfaceTypeApp )
-import ToIface( toIfaceType, toIfaceTyCon, toIfaceTcArgs )
+import ToIface  ( toIfaceTyCon, toIfaceTcArgs, toIfaceType )
 import HsSyn            -- HsType
 import TcRnMonad        -- TcType, amongst others
 import TcEnv       ( tcInitTidyEnv, tcInitOpenTidyEnv )
@@ -2033,7 +2033,20 @@ checkValidTyFamEqn :: TyCon   -- ^ of the type family
                    -> Type    -- ^ Rhs
                    -> TcM ()
 checkValidTyFamEqn fam_tc qvs typats rhs
-  = do { checkValidFamPats fam_tc qvs typats rhs
+  = do { checkValidTypePats fam_tc typats
+
+         -- Check for things used on the right but not bound on the left
+       ; checkFamPatBinders fam_tc qvs typats rhs
+
+         -- Check for oversaturated visible kind arguments in a type family
+         -- equation.
+         -- See Note [Oversaturated type family equations]
+       ; when (isTypeFamilyTyCon fam_tc) $
+           case drop (tyConArity fam_tc) typats of
+             [] -> pure ()
+             spec_arg:_ ->
+               addErr $ text "Illegal oversaturated visible kind argument:"
+                    <+> quotes (char '@' <> pprParendType spec_arg)
 
          -- The argument patterns, and RHS, are all boxed tau types
          -- E.g  Reject type family F (a :: k1) :: k2
@@ -2078,23 +2091,6 @@ checkFamInstRhs lhs_tc lhs_tys famInsts
                        --   [a,b,a,a] \\ [a,a] = [b,a]
                        -- So we are counting repetitions
 
-checkValidFamPats :: TyCon -> [Var]
-                  -> [Type]   -- ^ patterns
-                  -> Type     -- ^ RHS
-                  -> TcM ()
--- Patterns in a 'type instance' or 'data instance' decl should
--- a) Shoule contain no type family applications
---    (vanilla synonyms are fine, though)
--- b) For associated types, are consistently instantiated
-checkValidFamPats fam_tc qvs pats rhs
-  = do { checkValidTypePats fam_tc pats
-
-         -- Check for things used on the right but not bound on the left
-       ; checkFamPatBinders fam_tc qvs pats rhs
-
-       ; traceTc "checkValidFamPats" (ppr fam_tc <+> ppr pats)
-       }
-
 -----------------
 checkFamPatBinders :: TyCon
                    -> [TcTyVar]   -- Bound on LHS of family instance
@@ -2122,24 +2118,17 @@ checkFamPatBinders fam_tc qtvs pats rhs
          --    data family D Int = MkD (forall (a::k). blah)
          -- In both cases, 'k' is not bound on the LHS, but is used on the RHS
          -- We catch the former in kcLHsQTyVars, and the latter right here
+         -- See Note [Check type-family instance binders]
        ; check_tvs bad_rhs_tvs (text "mentioned in the RHS")
                                (text "bound on the LHS of")
 
          -- Check for explicitly forall'd variable that is not bound on LHS
          --    data instance forall a.  T Int = MkT Int
          -- See Note [Unused explicitly bound variables in a family pattern]
+         -- See Note [Check type-family instance binders]
        ; check_tvs bad_qtvs (text "bound by a forall")
                             (text "used in")
-
-         -- Check for oversaturated visible kind arguments in a type family
-         -- equation.
-         -- See Note [Oversaturated type family equations]
-       ; when (isTypeFamilyTyCon fam_tc) $
-           case drop (tyConArity fam_tc) pats of
-             [] -> pure ()
-             spec_arg:_ ->
-               addErr $ text "Illegal oversaturated visible kind argument:"
-                    <+> quotes (char '@' <> pprParendType spec_arg) }
+       }
   where
     pat_tvs       = tyCoVarsOfTypes pats
     exact_pat_tvs = exactTyCoVarsOfTypes pats
@@ -2166,21 +2155,26 @@ checkFamPatBinders fam_tc qtvs pats rhs
                       2 (pprTypeApp fam_tc (map expandTypeSynonyms pats))
 
 
--- | Checks for occurrences of type families in class instances and type/data
--- family instances.
+-- | Checks that a list of type patterns is valid in a matching (LHS)
+-- position of a class instances or type/data family instance.
+--
+-- Specifically:
+--    * All monotypes
+--    * No type-family applications
 checkValidTypePats :: TyCon -> [Type] -> TcM ()
-checkValidTypePats tc pat_ty_args = do
-  -- Check that each of pat_ty_args is a monotype.
-  -- One could imagine generalising to allow
-  --      instance C (forall a. a->a)
-  -- but we don't know what all the consequences might be.
-  traverse_ checkValidMonoType pat_ty_args
-
-  -- Ensure that no type family instances occur a type pattern
-  case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
-    [] -> pure ()
-    ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
-      ty_fam_inst_illegal_err tf_is_invis_arg (mkTyConApp tf_tc tf_args)
+checkValidTypePats tc pat_ty_args
+  = do { -- Check that each of pat_ty_args is a monotype.
+         -- One could imagine generalising to allow
+         --      instance C (forall a. a->a)
+         -- but we don't know what all the consequences might be.
+         traverse_ checkValidMonoType pat_ty_args
+
+       -- Ensure that no type family applications occur a type pattern
+       ; case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
+            [] -> pure ()
+            ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
+               ty_fam_inst_illegal_err tf_is_invis_arg
+                                       (mkTyConApp tf_tc tf_args) }
   where
     inst_ty = mkTyConApp tc pat_ty_args
 
@@ -2294,8 +2288,52 @@ checkConsistentFamInst (InClsInst { ai_class = clas
                | otherwise                   = BindMe
 
 
-{- Note [Matching in the consistent-instantation check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Check type-family instance binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a type family instance, we require (of course), type variables
+used on the RHS are matched on the LHS. This is checked by
+checkFamPatBinders.  Here is an interesting example:
+
+    type family   T :: k
+    type instance T = (Nothing :: Maybe a)
+
+Upon a cursory glance, it may appear that the kind variable `a` is
+free-floating above, since there are no (visible) LHS patterns in
+`T`. However, there is an *invisible* pattern due to the return kind,
+so inside of GHC, the instance looks closer to this:
+
+    type family T @k :: k
+    type instance T @(Maybe a) = (Nothing :: Maybe a)
+
+Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in
+fact not unbound. Contrast that with this example (Trac #13985)
+
+    type instance T = Proxy (Nothing :: Maybe a)
+
+This would looks like this inside of GHC:
+
+    type instance T @(*) = Proxy (Nothing :: Maybe a)
+
+So this time, `a` is neither bound by a visible nor invisible type pattern on
+the LHS, so it would be reported as free-floating.
+
+Finally, here's one more brain-teaser (from #9574). In the example below:
+
+    class Funct f where
+      type Codomain f :: *
+    instance Funct ('KProxy :: KProxy o) where
+      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+
+As it turns out, `o` is not free-floating in this example. That is because `o`
+bound by the kind signature of the LHS type pattern 'KProxy. To make this more
+obvious, one can also write the instance like so:
+
+    instance Funct ('KProxy :: KProxy o) where
+      type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *)
+
+
+Note [Matching in the consistent-instantation check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Matching the class-instance header to family-instance tyvars is
 tricker than it sounds.  Consider (Trac #13972)
     class C (a :: k) where
@@ -2547,8 +2585,8 @@ family instance equations: see Note [Arity of data families] in FamInstEnv.
 *                                                                      *
 ************************************************************************
 
-Note [Bad telescopes]
-~~~~~~~~~~~~~~~~~~~~~
+Note [Bad TyCon telescopes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Now that we can mix type and kind variables, there are an awful lot of
 ways to shoot yourself in the foot. Here are some.
 
@@ -2566,54 +2604,93 @@ Note that b is not bound. Yet its kind mentions a. Because we have
 a nice rule that all implicitly bound variables come before others,
 this is bogus.
 
-To catch these errors, we call checkValidTelescope during kind-checking
-datatype declarations. See also
-Note [Required, Specified, and Inferred for types] in TcTyClsDecls.
+To catch these errors, we call checkTyConTelescope during kind-checking
+datatype declarations.  This checks for
+
+* Ill-scoped binders. From (1) and (2) above we can get putative
+  kinds like
+       T1 :: forall (a:k) (k:*) (b:k). SameKind a b -> *
+  where 'k' is mentioned a's kind before k is bound
+
+  This is easy to check for: just look for
+  out-of-scope variables in the kind
 
-Note [Keeping scoped variables in order: Explicit] discusses how this
-check works for `forall x y z.` written in a type.
+* We should arguably also check for ambiguous binders
+  but we don't.  See Note [Ambiguous kind vars].
 
+See also
+  * Note [Required, Specified, and Inferred for types] in TcTyClsDecls.
+  * Note [Keeping scoped variables in order: Explicit] discusses how
+    this check works for `forall x y z.` written in a type.
+
+Note [Ambiguous kind vars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We used to be concerned about ambiguous binders. Suppose we have the kind
+     S1 :: forall k -> * -> *
+     S2 :: forall k. * -> *
+Here S1 is OK, because k is Required, and at a use of S1 we will
+see (S1 *) or (S1 (*->*)) or whatever.
+
+But S2 is /not/ OK because 'k' is Specfied (and hence invisible) and
+we have no way (ever) to figure out how 'k' should be instantiated.
+For example if we see (S2 Int), that tells us nothing about k's
+instantiation.  (In this case we'll instantiate it to Any, but that
+seems wrong.)  This is really the same test as we make for ambiguous
+type in term type signatures.
+
+Now, it's impossible for a Specified variable not to occur
+at all in the kind -- after all, it is Specified so it must have
+occurred.  (It /used/ to be possible; see tests T13983 and T7873.  But
+with the advent of the forall-or-nothing rule for kind variables,
+those strange cases went away.)
+
+But one might worry about
+    type v k = *
+    S3 :: forall k. V k -> *
+which appears to mention 'k' but doesn't really.  Or
+    S4 :: forall k. F k -> *
+where F is a type function.  But we simply don't check for
+those cases of ambiguity, yet anyway.  The worst that can happen
+is ambiguity at the call sites.
+
+Historical note: this test used to be called reportFloatingKvs.
 -}
 
 -- | Check a list of binders to see if they make a valid telescope.
--- The key property we're checking for is scoping. For example:
--- > data SameKind :: k -> k -> *
--- > data X a k (b :: k) (c :: SameKind a b)
--- Kind inference says that a's kind should be k. But that's impossible,
--- because k isn't in scope when a is bound. This check has to come before
--- general validity checking, because once we kind-generalise, this sort
--- of problem is harder to spot (as we'll generalise over the unbound
--- k in a's type.)
---
--- See Note [Generalisation for type constructors] in TcTyClsDecls for
---     data type declarations
--- and Note [Keeping scoped variables in order: Explicit] in TcHsType
---     for foralls
-checkValidTelescope :: TyCon -> TcM ()
-checkValidTelescope tc
-  = unless (null bad_tcbs) $ addErr $
+-- See Note [Bad TyCon telescopes]
+type TelescopeAcc
+      = ( TyVarSet   -- Bound earlier in the telescope
+        , Bool       -- At least one binder occurred (in a kind) before
+                     -- it was bound in the telescope.  E.g.
+        )            --    T :: forall (a::k) k. blah
+
+checkTyConTelescope :: TyCon -> TcM ()
+checkTyConTelescope tc
+  | bad_scope
+  = -- See "Ill-scoped binders" in Note [Bad TyCon telescopes]
+    addErr $
     vcat [ hang (text "The kind of" <+> quotes (ppr tc) <+> text "is ill-scoped")
-              2 (text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc))
+              2 pp_tc_kind
          , extra
          , hang (text "Perhaps try this order instead:")
-              2 (pprTyVars sorted_tidied_tvs) ]
+              2 (pprTyVars sorted_tvs) ]
+
+  | otherwise
+  = return ()
   where
-    ppr_untidy ty = pprIfaceType (toIfaceType ty)
     tcbs = tyConBinders tc
-    tvs = binderVars tcbs
-    (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (scopedSort tvs)
+    tvs  = binderVars tcbs
+    sorted_tvs = scopedSort tvs
 
-    (_, bad_tcbs) = foldl add_one (mkVarSet tvs, []) tcbs
+    (_, bad_scope) = foldl add_one (emptyVarSet, False) tcbs
 
-    add_one :: (TyVarSet, [TyConBinder])
-            -> TyConBinder -> (TyVarSet, [TyConBinder])
-    add_one (bad_bndrs, acc) tvb
-      | fkvs `intersectsVarSet` bad_bndrs = (bad', tvb : acc)
-      | otherwise                         = (bad', acc)
+    add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc
+    add_one (bound, bad_scope) tcb
+      = ( bound `extendVarSet` tv
+        , bad_scope || not (isEmptyVarSet (fkvs `minusVarSet` bound)) )
       where
-        tv = binderVar tvb
+        tv = binderVar tcb
         fkvs = tyCoVarsOfType (tyVarKind tv)
-        bad' = bad_bndrs `delVarSet` tv
 
     inferred_tvs  = [ binderVar tcb
                     | tcb <- tcbs, Inferred == tyConBinderArgFlag tcb ]
@@ -2623,6 +2700,14 @@ checkValidTelescope tc
     pp_inf  = parens (text "namely:" <+> pprTyVars inferred_tvs)
     pp_spec = parens (text "namely:" <+> pprTyVars specified_tvs)
 
+    pp_tc_kind = text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc)
+    ppr_untidy ty = pprIfaceType (toIfaceType ty)
+      -- We need ppr_untidy here because pprType will tidy the type, which
+      -- will turn the bogus kind we are trying to report
+      --     T :: forall (a::k) k (b::k) -> blah
+      -- into a misleadingly sanitised version
+      --     T :: forall (a::k) k1 (b::k1) -> blah
+
     extra
       | null inferred_tvs && null specified_tvs
       = empty
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 4557ad6388..ce40d74278 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -871,24 +871,42 @@ data TyCon
 
         -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyConBinder], -- ^ Full binders
-        tyConTyVars  :: [TyVar],          -- ^ TyVar binders
-        tyConResKind :: Kind,             -- ^ Result kind
-        tyConKind    :: Kind,             -- ^ Kind of this TyCon
-        tyConArity   :: Arity,            -- ^ Arity
+        tyConTyVars  :: [TyVar],       -- ^ TyVar binders
+        tyConResKind :: Kind,          -- ^ Result kind
+        tyConKind    :: Kind,          -- ^ Kind of this TyCon
+        tyConArity   :: Arity,         -- ^ Arity
+
+          -- NB: the TyConArity of a TcTyCon must match
+          -- the number of Required (positional, user-specified)
+          -- arguments to the type constructor; see the use
+          -- of tyConArity in generaliseTcTyCon
 
         tcTyConScopedTyVars :: [(Name,TyVar)],
-                           -- ^ Scoped tyvars over the tycon's body
-                           -- See Note [How TcTyCons work] in TcTyClsDecls
-                           -- Order *does* matter: for TcTyCons with a CUSK,
-                           -- it's the correct dependency order. For TcTyCons
-                           -- without a CUSK, it's the original left-to-right
-                           -- that the user wrote. Nec'y for getting Specified
-                           -- variables in the right order.
+          -- ^ Scoped tyvars over the tycon's body
+          -- See Note [Scoped tyvars in a TcTyCon]
+
         tcTyConIsPoly     :: Bool, -- ^ Is this TcTyCon already generalized?
 
         tcTyConFlavour :: TyConFlavour
                            -- ^ What sort of 'TyCon' this represents.
       }
+{- Note [Scoped tyvars in a TcTyCon]
+
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The tcTyConScopedTyVars field records the lexicial-binding connection
+between the original, user-specified Name (i.e. thing in scope) and
+the TcTyVar that the Name is bound to.
+
+Order *does* matter; the tcTyConScopedTyvars list consists of
+     specified_tvs ++ required_tvs
+
+where
+   * specified ones first
+   * required_tvs the same as tyConTyVars
+   * tyConArity = length required_tvs
+
+See also Note [How TcTyCons work] in TcTyClsDecls
+-}
 
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
 data AlgTyConRhs
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 8aef2e7673..4e29910c21 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -69,7 +69,7 @@ test('T2664a', normal, compile, [''])
 test('T2544', normal, compile_fail, [''])
 test('T1897b', normal, compile_fail, [''])
 test('T5439', normal, compile_fail, [''])
-test('T5515', when(compiler_debugged(), expect_broken(16251)), compile_fail, [''])
+test('T5515', normal, compile_fail, [''])
 test('T5934', normal, compile_fail, [''])
 test('T6123', normal, compile_fail, [''])
 test('ExtraTcsUntch', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index f0cfdefd03..b0d4ef7f25 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -7,22 +7,22 @@ tc141.hs:11:12: error:
       In a pattern binding: (p :: a, q :: a) = x
 
 tc141.hs:11:31: error:
-    • Couldn't match expected type ‘a2’ with actual type ‘a’
-      ‘a2’ is a rigid type variable bound by
+    • Couldn't match expected type ‘a1’ with actual type ‘b’
+      ‘a1’ is a rigid type variable bound by
         an expression type signature:
-          forall a2. a2
+          forall a1. a1
         at tc141.hs:11:34
-      ‘a’ is a rigid type variable bound by
-        the inferred type of f :: (a, a) -> (a1, a)
+      ‘b’ is a rigid type variable bound by
+        the inferred type of f :: (b, b) -> (a, b)
         at tc141.hs:11:1-37
     • In the expression: q :: a
       In the expression: (q :: a, p)
       In the expression: let (p :: a, q :: a) = x in (q :: a, p)
     • Relevant bindings include
-        p :: a (bound at tc141.hs:11:12)
-        q :: a (bound at tc141.hs:11:17)
-        x :: (a, a) (bound at tc141.hs:11:3)
-        f :: (a, a) -> (a1, a) (bound at tc141.hs:11:1)
+        p :: b (bound at tc141.hs:11:12)
+        q :: b (bound at tc141.hs:11:17)
+        x :: (b, b) (bound at tc141.hs:11:3)
+        f :: (b, b) -> (a, b) (bound at tc141.hs:11:1)
 
 tc141.hs:13:13: error:
     • You cannot bind scoped type variable ‘a’
diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr
index 63379a03b9..f7980d2734 100644
--- a/testsuite/tests/typecheck/should_fail/T2688.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2688.stderr
@@ -3,10 +3,10 @@ T2688.hs:8:14: error:
     • Couldn't match expected type ‘v’ with actual type ‘s’
       ‘s’ is a rigid type variable bound by
         the class declaration for ‘VectorSpace’
-        at T2688.hs:(5,1)-(8,23)
+        at T2688.hs:5:21
       ‘v’ is a rigid type variable bound by
         the class declaration for ‘VectorSpace’
-        at T2688.hs:(5,1)-(8,23)
+        at T2688.hs:5:19
     • In the expression: v *^ (1 / s)
       In an equation for ‘^/’: v ^/ s = v *^ (1 / s)
     • Relevant bindings include