Treat kind/type variables identically, demolish FKTV

Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst
Fixes Trac #16334, Trac #16315

With this patch, scoping rules for type and kind variables have been
unified: kind variables no longer receieve special treatment. This
simplifies both the language and the implementation.

User-facing changes
-------------------

* Kind variables are no longer implicitly quantified when an explicit
  forall is used:

    p ::             Proxy (a :: k)    -- still accepted
    p :: forall k a. Proxy (a :: k)    -- still accepted
    p :: forall   a. Proxy (a :: k)    -- no longer accepted

  In other words, now we adhere to the "forall-or-nothing" rule more
  strictly.

  Related function: RnTypes.rnImplicitBndrs

* The -Wimplicit-kind-vars warning has been deprecated.

* Kind variables are no longer implicitly quantified in constructor
  declarations:

    data T a        = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- no longer accepted
    data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- still accepted

  Related function: RnTypes.extractRdrKindSigVars

* Implicitly quantified kind variables are no longer put in front of
  other variables:

    f :: Proxy (a :: k) -> Proxy (b :: j)

    f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b   -- old order
    f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b   -- new order

  This is a breaking change for users of TypeApplications. Note that
  we still respect the dpendency order: 'k' before 'a', 'j' before 'b'.
  See "Ordering of specified variables" in the User's Guide.

  Related function: RnTypes.rnImplicitBndrs

* In type synonyms and type family equations, free variables on the RHS
  are no longer implicitly quantified unless used in an outermost kind
  annotation:

    type T = Just (Nothing :: Maybe a)         -- no longer accepted
    type T = Just Nothing :: Maybe (Maybe a)   -- still accepted

  The latter form is a workaround due to temporary lack of an explicit
  quantification method. Ideally, we would write something along these
  lines:

    type T @a = Just (Nothing :: Maybe a)

  Related function: RnTypes.extractHsTyRdrTyVarsKindVars

* Named wildcards in kinds are fixed (Trac #16334):

    x :: (Int :: _t)    -- this compiles, infers (_t ~ Type)

  Related function: RnTypes.partition_nwcs

Implementation notes
--------------------

* One of the key changes is the removal of FKTV in RnTypes:

  - data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
  -                          , fktv_tys    :: [Located RdrName] }
  + type FreeKiTyVars = [Located RdrName]

  We used to keep track of type and kind variables separately, but
  now that they are on equal footing when it comes to scoping, we
  can put them in the same list.

* extract_lty and family are no longer parametrized by TypeOrKind,
  as we now do not distinguish kind variables from type variables.

* PatSynExPE and the related Note [Pattern synonym existentials do not scope]
  have been removed (Trac #16315). With no implicit kind quantification,
  we can no longer trigger the error.

* reportFloatingKvs and the related Note [Free-floating kind vars]
  have been removed. With no implicit kind quantification,
  we can no longer trigger the error.

59 files changed, 400 insertions, 682 deletions

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index dca692ec83..d29fa4a9f9 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -3992,7 +3992,8 @@ wWarningFlagsDeps = [
   flagSpec "hi-shadowing"                Opt_WarnHiShadows,
   flagSpec "inaccessible-code"           Opt_WarnInaccessibleCode,
   flagSpec "implicit-prelude"            Opt_WarnImplicitPrelude,
-  flagSpec "implicit-kind-vars"          Opt_WarnImplicitKindVars,
+  depFlagSpec "implicit-kind-vars"       Opt_WarnImplicitKindVars
+    "it is now an error",
   flagSpec "incomplete-patterns"         Opt_WarnIncompletePatterns,
   flagSpec "incomplete-record-updates"   Opt_WarnIncompletePatternsRecUpd,
   flagSpec "incomplete-uni-patterns"     Opt_WarnIncompleteUniPatterns,
@@ -4830,7 +4831,6 @@ minusWcompatOpts
     = [ Opt_WarnMissingMonadFailInstances
       , Opt_WarnSemigroup
       , Opt_WarnNonCanonicalMonoidInstances
-      , Opt_WarnImplicitKindVars
       , Opt_WarnStarIsType
       ]
 
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 0699f80858..5155f3ab84 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -727,15 +727,11 @@ rnFamInstEqn doc mb_cls rhs_kvars
        ; let pat_kity_vars_with_dups = extractHsTyArgRdrKiTyVarsDup pats
              -- Use the "...Dups" form because it's needed
              -- below to report unsed binder on the LHS
-       ; let pat_kity_vars = rmDupsInRdrTyVars pat_kity_vars_with_dups
-
-         -- all pat vars not explicitly bound (see extractHsTvBndrs)
-       ; let mb_imp_kity_vars = extractHsTvBndrs <$> mb_bndrs <*> pure pat_kity_vars
-             imp_vars = case mb_imp_kity_vars of
-                          -- kind vars are the only ones free if we have an explicit forall
-                          Just nbnd_kity_vars -> freeKiTyVarsKindVars nbnd_kity_vars
-                          -- all pattern vars are free otherwise
-                          Nothing             -> freeKiTyVarsAllVars pat_kity_vars
+
+         -- Implicitly bound variables, empty if we have an explicit 'forall' according
+         -- to the "forall-or-nothing" rule.
+       ; let imp_vars | isNothing mb_bndrs = nubL pat_kity_vars_with_dups
+                      | otherwise = []
        ; imp_var_names <- mapM (newTyVarNameRn mb_cls) imp_vars
 
        ; let bndrs = fromMaybe [] mb_bndrs
@@ -766,7 +762,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
                        -- See Note [Unused type variables in family instances]
                     ; let groups :: [NonEmpty (Located RdrName)]
                           groups = equivClasses cmpLocated $
-                                   freeKiTyVarsAllVars pat_kity_vars_with_dups
+                                   pat_kity_vars_with_dups
                     ; nms_dups <- mapM (lookupOccRn . unLoc) $
                                      [ tv | (tv :| (_:_)) <- groups ]
                           -- Add to the used variables
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 8e390f0e17..499fd74bd9 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -26,14 +26,11 @@ module RnTypes (
         -- Binding related stuff
         bindLHsTyVarBndr, bindLHsTyVarBndrs, rnImplicitBndrs,
         bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames,
-        extractFilteredRdrTyVars, extractFilteredRdrTyVarsDups,
         extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars,
-        extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars,
-        extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars,
+        extractHsTysRdrTyVarsDups,
         extractRdrKindSigVars, extractDataDefnKindVars,
         extractHsTvBndrs, extractHsTyArgRdrKiTyVarsDup,
-        freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars,
-        elemRdr
+        nubL, elemRdr
   ) where
 
 import GhcPrelude
@@ -127,7 +124,7 @@ rn_hs_sig_wc_type scoping ctxt
                   (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
                   thing_inside
   = do { free_vars <- extractFilteredRdrTyVarsDups hs_ty
-       ; (tv_rdrs, nwc_rdrs') <- partition_nwcs free_vars
+       ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
              bind_free_tvs = case scoping of
                                AlwaysBind       -> True
@@ -148,7 +145,7 @@ rn_hs_sig_wc_type _ _ (XHsWildCardBndrs _) _
 rnHsWcType :: HsDocContext -> LHsWcType GhcPs -> RnM (LHsWcType GhcRn, FreeVars)
 rnHsWcType ctxt (HsWC { hswc_body = hs_ty })
   = do { free_vars <- extractFilteredRdrTyVars hs_ty
-       ; (_, nwc_rdrs) <- partition_nwcs free_vars
+       ; (nwc_rdrs, _) <- partition_nwcs free_vars
        ; (wcs, hs_ty', fvs) <- rnWcBody ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = hs_ty' }
        ; return (sig_ty', fvs) }
@@ -251,9 +248,7 @@ extraConstraintWildCardsAllowed env
 --   NB: this includes named wildcards, which look like perfectly
 --       ordinary type variables at this point
 extractFilteredRdrTyVars :: LHsType GhcPs -> RnM FreeKiTyVarsNoDups
-extractFilteredRdrTyVars hs_ty
-  = do { rdr_env <- getLocalRdrEnv
-       ; return (filterInScope rdr_env (extractHsTyRdrTyVars hs_ty)) }
+extractFilteredRdrTyVars hs_ty = filterInScopeM (extractHsTyRdrTyVars hs_ty)
 
 -- | Finds free type and kind variables in a type,
 --     with duplicates, but
@@ -261,22 +256,20 @@ extractFilteredRdrTyVars hs_ty
 --   NB: this includes named wildcards, which look like perfectly
 --       ordinary type variables at this point
 extractFilteredRdrTyVarsDups :: LHsType GhcPs -> RnM FreeKiTyVarsWithDups
-extractFilteredRdrTyVarsDups hs_ty
-  = do { rdr_env <- getLocalRdrEnv
-       ; return (filterInScope rdr_env (extractHsTyRdrTyVarsDups hs_ty)) }
+extractFilteredRdrTyVarsDups hs_ty = filterInScopeM (extractHsTyRdrTyVarsDups hs_ty)
 
 -- | When the NamedWildCards extension is enabled, partition_nwcs
 -- removes type variables that start with an underscore from the
 -- FreeKiTyVars in the argument and returns them in a separate list.
 -- When the extension is disabled, the function returns the argument
 -- and empty list.  See Note [Renaming named wild cards]
-partition_nwcs :: FreeKiTyVars -> RnM (FreeKiTyVars, [Located RdrName])
-partition_nwcs free_vars@(FKTV { fktv_tys = tys })
-  = do { wildcards_enabled <- fmap (xopt LangExt.NamedWildCards) getDynFlags
-       ; let (nwcs, no_nwcs) | wildcards_enabled = partition is_wildcard tys
-                             | otherwise         = ([], tys)
-             free_vars' = free_vars { fktv_tys = no_nwcs }
-       ; return (free_vars', nwcs) }
+partition_nwcs :: FreeKiTyVars -> RnM ([Located RdrName], FreeKiTyVars)
+partition_nwcs free_vars
+  = do { wildcards_enabled <- xoptM LangExt.NamedWildCards
+       ; return $
+           if wildcards_enabled
+           then partition is_wildcard free_vars
+           else ([], free_vars) }
   where
      is_wildcard :: Located RdrName -> Bool
      is_wildcard rdr = startsWithUnderscore (rdrNameOcc (unLoc rdr))
@@ -326,51 +319,20 @@ rnImplicitBndrs :: Bool    -- True <=> bring into scope any free type variables
                 -> ([Name] -> RnM (a, FreeVars))
                 -> RnM (a, FreeVars)
 rnImplicitBndrs bind_free_tvs
-                fvs_with_dups@(FKTV { fktv_kis = kvs_with_dups
-                                    , fktv_tys = tvs_with_dups })
+                fvs_with_dups
                 thing_inside
-  = do { let FKTV kvs tvs = rmDupsInRdrTyVars fvs_with_dups
-             real_tvs | bind_free_tvs = tvs
+  = do { let fvs = nubL fvs_with_dups
+             real_fvs | bind_free_tvs = fvs
                       | otherwise     = []
-             -- We always bind over free /kind/ variables.
-             -- Bind free /type/ variables only if there is no
-             -- explicit forall.  E.g.
-             --    f :: Proxy (a :: k) -> b
-             --         Quantify over {k} and {a,b}
-             --    g :: forall a. Proxy (a :: k) -> b
-             --         Quantify over {k} and {}
-             -- Note that we always do the implicit kind-quantification
-             -- but, rather arbitrarily, we switch off the type-quantification
-             -- if there is an explicit forall
-
-       ; traceRn "rnImplicitBndrs" (vcat [ ppr kvs, ppr tvs, ppr real_tvs ])
-
-       ; whenWOptM Opt_WarnImplicitKindVars $
-         unless (bind_free_tvs || null kvs) $
-         addWarnAt (Reason Opt_WarnImplicitKindVars) (getLoc (head kvs)) $
-         implicit_kind_vars_msg kvs
 
-       ; loc <- getSrcSpanM
-          -- NB: kinds before tvs, as mandated by
-          -- Note [Ordering of implicit variables]
-       ; vars <- mapM (newLocalBndrRn . cL loc . unLoc) (kvs ++ real_tvs)
+       ; traceRn "rnImplicitBndrs" $
+         vcat [ ppr fvs_with_dups, ppr fvs, ppr real_fvs ]
 
-       ; traceRn "checkMixedVars2" $
-           vcat [ text "kvs_with_dups" <+> ppr kvs_with_dups
-                , text "tvs_with_dups" <+> ppr tvs_with_dups ]
+       ; loc <- getSrcSpanM
+       ; vars <- mapM (newLocalBndrRn . cL loc . unLoc) real_fvs
 
        ; bindLocalNamesFV vars $
          thing_inside vars }
-  where
-    implicit_kind_vars_msg kvs =
-      vcat [ text "An explicit" <+> quotes (text "forall") <+>
-             text "was used, but the following kind variables" <+>
-             text "are not quantified:" <+>
-             hsep (punctuate comma (map (quotes . ppr) kvs))
-           , text "Despite this fact, GHC will introduce them into scope," <+>
-             text "but it will stop doing so in the future."
-           , text "Suggested fix: add" <+>
-             quotes (text "forall" <+> hsep (map ppr kvs) <> char '.') ]
 
 {- ******************************************************
 *                                                       *
@@ -1474,8 +1436,7 @@ opTyErr op overall_ty
 
 Note [Kind and type-variable binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In a type signature we may implicitly bind type variable and, more
-recently, kind variables.  For example:
+In a type signature we may implicitly bind type/kind variables. For example:
   *   f :: a -> a
       f = ...
     Here we need to find the free type variables of (a -> a),
@@ -1493,42 +1454,11 @@ recently, kind variables.  For example:
   *   type instance F (T (a :: Maybe k)) = ...a...k...
     Here we want to constrain the kind of 'a', and bind 'k'.
 
-In general we want to walk over a type, and find
-  * Its free type variables
-  * The free kind variables of any kind signatures in the type
-
-Hence we return a pair (kind-vars, type vars)
-(See Note [HsBSig binder lists] in HsTypes.)
-Moreover, we preserve the left-to-right order of the first occurrence of each
-variable, while preserving dependency order.
-(See Note [Ordering of implicit variables].)
-
-Most clients of this code just want to know the kind/type vars, without
-duplicates. The function rmDupsInRdrTyVars removes duplicates. That function
-also makes sure that no variable is reported as both a kind var and
-a type var, preferring kind vars. Why kind vars? Consider this:
-
- foo :: forall (a :: k). Proxy k -> Proxy a -> ...
+To do that, we need to walk over a type and find its free type/kind variables.
+We preserve the left-to-right order of each variable occurrence.
+See Note [Ordering of implicit variables].
 
-Should that be accepted?
-
-Normally, if a type signature has an explicit forall, it must list *all*
-tyvars mentioned in the type. But there's an exception for tyvars mentioned in
-a kind, as k is above. Note that k is also used "as a type variable", as the
-argument to the first Proxy. So, do we consider k to be type-variable-like and
-require it in the forall? Or do we consider k to be kind-variable-like and not
-require it?
-
-It's not just in type signatures: kind variables are implicitly brought into
-scope in a variety of places. Should vars used at both the type level and kind
-level be treated this way?
-
-GHC indeed allows kind variables to be brought into scope implicitly even when
-the kind variable is also used as a type variable. Thus, we must prefer to keep
-a variable listed as a kind var in rmDupsInRdrTyVars. If we kept it as a type
-var, then this would prevent it from being implicitly quantified (see
-rnImplicitBndrs). In the `foo` example above, that would have the consequence
-of the k in Proxy k being reported as out of scope.
+Clients of this code can remove duplicates with nubL.
 
 Note [Ordering of implicit variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1558,30 +1488,98 @@ See Note [ScopedSort] in Type.
 
 Implicitly bound variables are collected by any function which returns a
 FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably
-includes the `extract-` family of functions (extractHsTysRdrTyVars,
+includes the `extract-` family of functions (extractHsTysRdrTyVarsDups,
 extractHsTyVarBndrsKVs, etc.).
 These functions thus promise to keep left-to-right ordering.
-Look for pointers to this note to see the places where the action happens.
-
-Note that we also maintain this ordering in kind signatures. Even though
-there's no visible kind application (yet), having implicit variables be
-quantified in left-to-right order in kind signatures is nice since:
-
-* It's consistent with the treatment for type signatures.
-* It can affect how types are displayed with -fprint-explicit-kinds (see
-  #15568 for an example), which is a situation where knowing the order in
-  which implicit variables are quantified can be useful.
-* In the event that visible kind application is implemented, the order in
-  which we would expect implicit variables to be ordered in kinds will have
-  already been established.
+
+Note [Implicit quantification in type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We typically bind type/kind variables implicitly when they are in a kind
+annotation on the LHS, for example:
+
+  data Proxy (a :: k) = Proxy
+  type KindOf (a :: k) = k
+
+Here 'k' is in the kind annotation of a type variable binding, KindedTyVar, and
+we want to implicitly quantify over it.  This is easy: just extract all free
+variables from the kind signature. That's what we do in extract_hs_tv_bndrs_kvs
+
+By contrast, on the RHS we can't simply collect *all* free variables. Which of
+the following are allowed?
+
+  type TySyn1 = a :: Type
+  type TySyn2 = 'Nothing :: Maybe a
+  type TySyn3 = 'Just ('Nothing :: Maybe a)
+  type TySyn4 = 'Left a :: Either Type a
+
+After some design deliberations (see non-taken alternatives below), the answer
+is to reject TySyn1 and TySyn3, but allow TySyn2 and TySyn4, at least for now.
+We implicitly quantify over free variables of the outermost kind signature, if
+one exists:
+
+  * In TySyn1, the outermost kind signature is (:: Type), and it does not have
+    any free variables.
+  * In TySyn2, the outermost kind signature is (:: Maybe a), it contains a
+    free variable 'a', which we implicitly quantify over.
+  * In TySyn3, there is no outermost kind signature. The (:: Maybe a) signature
+    is hidden inside 'Just.
+  * In TySyn4, the outermost kind signature is (:: Either Type a), it contains
+    a free variable 'a', which we implicitly quantify over. That is why we can
+    also use it to the left of the double colon: 'Left a
+
+The logic resides in extractHsTyRdrTyVarsKindVars. We use it both for type
+synonyms and type family instances.
+
+This is something of a stopgap solution until we can explicitly bind invisible
+type/kind variables:
+
+  type TySyn3 :: forall a. Maybe a
+  type TySyn3 @a = 'Just ('Nothing :: Maybe a)
+
+Note [Implicit quantification in type synonyms: non-taken alternatives]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Alternative I: No quantification
+--------------------------------
+We could offer no implicit quantification on the RHS, accepting none of the
+TySyn<N> examples. The user would have to bind the variables explicitly:
+
+  type TySyn1 a = a :: Type
+  type TySyn2 a = 'Nothing :: Maybe a
+  type TySyn3 a = 'Just ('Nothing :: Maybe a)
+  type TySyn4 a = 'Left a :: Either Type a
+
+However, this would mean that one would have to specify 'a' at call sites every
+time, which could be undesired.
+
+Alternative II: Indiscriminate quantification
+---------------------------------------------
+We could implicitly quantify over all free variables on the RHS just like we do
+on the LHS. Then we would infer the following kinds:
+
+  TySyn1 :: forall {a}. Type
+  TySyn2 :: forall {a}. Maybe a
+  TySyn3 :: forall {a}. Maybe (Maybe a)
+  TySyn4 :: forall {a}. Either Type a
+
+This would work fine for TySyn<2,3,4>, but TySyn1 is clearly bogus: the variable
+is free-floating, not fixed by anything.
+
+Alternative III: reportFloatingKvs
+----------------------------------
+We could augment Alternative II by hunting down free-floating variables during
+type checking. While viable, this would mean we'd end up accepting this:
+
+  data Prox k (a :: k)
+  type T = Prox k
+
 -}
 
 -- See Note [Kind and type-variable binders]
 -- These lists are guaranteed to preserve left-to-right ordering of
 -- the types the variables were extracted from. See also
 -- Note [Ordering of implicit variables].
-data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
-                         , fktv_tys    :: [Located RdrName] }
+type FreeKiTyVars = [Located RdrName]
 
 -- | A 'FreeKiTyVars' list that is allowed to have duplicate variables.
 type FreeKiTyVarsWithDups = FreeKiTyVars
@@ -1589,94 +1587,70 @@ type FreeKiTyVarsWithDups = FreeKiTyVars
 -- | A 'FreeKiTyVars' list that contains no duplicate variables.
 type FreeKiTyVarsNoDups   = FreeKiTyVars
 
-instance Outputable FreeKiTyVars where
-  ppr (FKTV { fktv_kis = kis, fktv_tys = tys}) = ppr (kis, tys)
-
-emptyFKTV :: FreeKiTyVarsNoDups
-emptyFKTV = FKTV { fktv_kis = [], fktv_tys = [] }
-
-freeKiTyVarsAllVars :: FreeKiTyVars -> [Located RdrName]
-freeKiTyVarsAllVars (FKTV { fktv_kis = kvs, fktv_tys = tvs }) = kvs ++ tvs
-
-freeKiTyVarsKindVars :: FreeKiTyVars -> [Located RdrName]
-freeKiTyVarsKindVars = fktv_kis
-
-freeKiTyVarsTypeVars :: FreeKiTyVars -> [Located RdrName]
-freeKiTyVarsTypeVars = fktv_tys
-
 filterInScope :: LocalRdrEnv -> FreeKiTyVars -> FreeKiTyVars
-filterInScope rdr_env (FKTV { fktv_kis = kis, fktv_tys = tys })
-  = FKTV { fktv_kis = filterOut in_scope kis
-         , fktv_tys = filterOut in_scope tys }
-  where
-    in_scope = inScope rdr_env . unLoc
+filterInScope rdr_env = filterOut (inScope rdr_env . unLoc)
+
+filterInScopeM :: FreeKiTyVars -> RnM FreeKiTyVars
+filterInScopeM vars
+  = do { rdr_env <- getLocalRdrEnv
+       ; return (filterInScope rdr_env vars) }
 
 inScope :: LocalRdrEnv -> RdrName -> Bool
 inScope rdr_env rdr = rdr `elemLocalRdrEnv` rdr_env
 
--- | 'extractHsTyRdrTyVars' finds the
---        free (kind, type) variables of an 'HsType'
--- or the free (sort, kind) variables of an 'HsKind'.
--- It's used when making the @forall@s explicit.
--- Does not return any wildcards.
--- When the same name occurs multiple times in the types, only the first
--- occurrence is returned.
--- See Note [Kind and type-variable binders]
-
-
 extract_tyarg :: LHsTypeArg GhcPs -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_tyarg (HsValArg ty) acc = extract_lty TypeLevel ty acc
-extract_tyarg (HsTypeArg _ ki) acc = extract_lty KindLevel ki acc
+extract_tyarg (HsValArg ty) acc = extract_lty ty acc
+extract_tyarg (HsTypeArg _ ki) acc = extract_lty ki acc
 extract_tyarg (HsArgPar _) acc = acc
 
 extract_tyargs :: [LHsTypeArg GhcPs] -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
 extract_tyargs args acc = foldr extract_tyarg acc args
 
 extractHsTyArgRdrKiTyVarsDup :: [LHsTypeArg GhcPs] -> FreeKiTyVarsWithDups
-extractHsTyArgRdrKiTyVarsDup args = extract_tyargs args emptyFKTV
+extractHsTyArgRdrKiTyVarsDup args
+  = extract_tyargs args []
 
+-- | 'extractHsTyRdrTyVars' finds the type/kind variables
+--                          of a HsType/HsKind.
+-- It's used when making the @forall@s explicit.
+-- When the same name occurs multiple times in the types, only the first
+-- occurrence is returned.
+-- See Note [Kind and type-variable binders]
 extractHsTyRdrTyVars :: LHsType GhcPs -> FreeKiTyVarsNoDups
 extractHsTyRdrTyVars ty
-  = rmDupsInRdrTyVars (extractHsTyRdrTyVarsDups ty)
+  = nubL (extractHsTyRdrTyVarsDups ty)
 
--- | 'extractHsTyRdrTyVarsDups' find the
---        free (kind, type) variables of an 'HsType'
--- or the free (sort, kind) variables of an 'HsKind'.
+-- | 'extractHsTyRdrTyVarsDups' finds the type/kind variables
+--                              of a HsType/HsKind.
 -- It's used when making the @forall@s explicit.
--- Does not return any wildcards.
 -- When the same name occurs multiple times in the types, all occurrences
 -- are returned.
 extractHsTyRdrTyVarsDups :: LHsType GhcPs -> FreeKiTyVarsWithDups
 extractHsTyRdrTyVarsDups ty
-  = extract_lty TypeLevel ty emptyFKTV
+  = extract_lty ty []
 
--- | Extracts the free kind variables (but not the type variables) of an
--- 'HsType'. Does not return any wildcards.
+-- | Extracts the free type/kind variables from the kind signature of a HsType.
+--   This is used to implicitly quantify over @k@ in @type T = Nothing :: Maybe k@.
 -- When the same name occurs multiple times in the type, only the first
 -- occurrence is returned, and the left-to-right order of variables is
 -- preserved.
 -- See Note [Kind and type-variable binders] and
--- Note [Ordering of implicit variables].
-extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> [Located RdrName]
-extractHsTyRdrTyVarsKindVars ty
-  = freeKiTyVarsKindVars (extractHsTyRdrTyVars ty)
-
--- | Extracts free type and kind variables from types in a list.
--- When the same name occurs multiple times in the types, only the first
--- occurrence is returned and the rest is filtered out.
--- See Note [Kind and type-variable binders]
-extractHsTysRdrTyVars :: [LHsType GhcPs] -> FreeKiTyVarsNoDups
-extractHsTysRdrTyVars tys
-  = rmDupsInRdrTyVars (extractHsTysRdrTyVarsDups tys)
+--     Note [Ordering of implicit variables] and
+--     Note [Implicit quantification in type synonyms].
+extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> FreeKiTyVarsNoDups
+extractHsTyRdrTyVarsKindVars (unLoc -> ty) =
+  case ty of
+    HsParTy _ ty -> extractHsTyRdrTyVarsKindVars ty
+    HsKindSig _ _ ki -> extractHsTyRdrTyVars ki
+    _ -> []
 
 -- | Extracts free type and kind variables from types in a list.
 -- When the same name occurs multiple times in the types, all occurrences
 -- are returned.
 extractHsTysRdrTyVarsDups :: [LHsType GhcPs] -> FreeKiTyVarsWithDups
 extractHsTysRdrTyVarsDups tys
-  = extract_ltys TypeLevel tys emptyFKTV
+  = extract_ltys tys []
 
-extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> [Located RdrName]
 -- Returns the free kind variables of any explictly-kinded binders, returning
 -- variable occurrences in left-to-right order.
 -- See Note [Ordering of implicit variables].
@@ -1684,124 +1658,76 @@ extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> [Located RdrName]
 --     However duplicates are removed
 --     E.g. given  [k1, a:k1, b:k2]
 --          the function returns [k1,k2], even though k1 is bound here
+extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> FreeKiTyVarsNoDups
 extractHsTyVarBndrsKVs tv_bndrs
   = nubL (extract_hs_tv_bndrs_kvs tv_bndrs)
 
--- | Removes multiple occurrences of the same name from FreeKiTyVars. If a
--- variable occurs as both a kind and a type variable, only keep the occurrence
--- as a kind variable.
--- See also Note [Kind and type-variable binders]
-rmDupsInRdrTyVars :: FreeKiTyVarsWithDups -> FreeKiTyVarsNoDups
-rmDupsInRdrTyVars (FKTV { fktv_kis = kis, fktv_tys = tys })
-  = FKTV { fktv_kis = kis'
-         , fktv_tys = nubL (filterOut (`elemRdr` kis') tys) }
-  where
-    kis' = nubL kis
-
-extractRdrKindSigVars :: LFamilyResultSig GhcPs -> [Located RdrName]
 -- Returns the free kind variables in a type family result signature, returning
 -- variable occurrences in left-to-right order.
 -- See Note [Ordering of implicit variables].
+extractRdrKindSigVars :: LFamilyResultSig GhcPs -> [Located RdrName]
 extractRdrKindSigVars (dL->L _ resultSig)
-  | KindSig _ k                              <- resultSig = kindRdrNameFromSig k
-  | TyVarSig _ (dL->L _ (KindedTyVar _ _ k)) <- resultSig = kindRdrNameFromSig k
+  | KindSig _ k                              <- resultSig = extractHsTyRdrTyVars k
+  | TyVarSig _ (dL->L _ (KindedTyVar _ _ k)) <- resultSig = extractHsTyRdrTyVars k
   | otherwise =  []
-    where
-      kindRdrNameFromSig k = freeKiTyVarsAllVars (extractHsTyRdrTyVars k)
 
-extractDataDefnKindVars :: HsDataDefn GhcPs -> [Located RdrName]
--- Get the scoped kind variables mentioned free in the constructor decls
--- Eg: data T a = T1 (S (a :: k) | forall (b::k). T2 (S b)
---     Here k should scope over the whole definition
+-- Get type/kind variables mentioned in the kind signature, preserving
+-- left-to-right order and without duplicates:
 --
--- However, do NOT collect free kind vars from the deriving clauses:
--- Eg: (Trac #14331)    class C p q
---                      data D = D deriving ( C (a :: k) )
---     Here k should /not/ scope over the whole definition.  We intend
---     this to elaborate to:
---         class C @k1 @k2 (p::k1) (q::k2)
---         data D = D
---         instance forall k (a::k). C @k @* a D where ...
+--  * data T a (b :: k1) :: k2 -> k1 -> k2 -> Type   -- result: [k2,k1]
+--  * data T a (b :: k1)                             -- result: []
 --
--- This returns variable occurrences in left-to-right order.
 -- See Note [Ordering of implicit variables].
-extractDataDefnKindVars (HsDataDefn { dd_ctxt = ctxt, dd_kindSig = ksig
-                                    , dd_cons = cons })
-  = (nubL . freeKiTyVarsKindVars) $
-    (extract_lctxt TypeLevel ctxt  $
-     extract_mb extract_lkind ksig $
-     foldr (extract_con . unLoc) emptyFKTV cons)
-  where
-    extract_con (ConDeclGADT { }) acc = acc
-    extract_con (ConDeclH98 { con_ex_tvs = ex_tvs
-                            , con_mb_cxt = ctxt, con_args = args }) acc
-      = extract_hs_tv_bndrs ex_tvs acc $
-        extract_mlctxt ctxt            $
-        extract_ltys TypeLevel (hsConDeclArgTys args) emptyFKTV
-    extract_con (XConDecl { }) _ = panic "extractDataDefnKindVars"
+extractDataDefnKindVars :: HsDataDefn GhcPs ->  FreeKiTyVarsNoDups
+extractDataDefnKindVars (HsDataDefn { dd_kindSig = ksig })
+  = maybe [] extractHsTyRdrTyVars ksig
 extractDataDefnKindVars (XHsDataDefn _) = panic "extractDataDefnKindVars"
 
-extract_mlctxt :: Maybe (LHsContext GhcPs)
-               -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_mlctxt Nothing     acc = acc
-extract_mlctxt (Just ctxt) acc = extract_lctxt TypeLevel ctxt acc
-
-extract_lctxt :: TypeOrKind
-              -> LHsContext GhcPs
+extract_lctxt :: LHsContext GhcPs
               -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_lctxt t_or_k ctxt = extract_ltys t_or_k (unLoc ctxt)
+extract_lctxt ctxt = extract_ltys (unLoc ctxt)
 
-extract_ltys :: TypeOrKind
-             -> [LHsType GhcPs]
+extract_ltys :: [LHsType GhcPs]
              -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_ltys t_or_k tys acc = foldr (extract_lty t_or_k) acc tys
+extract_ltys tys acc = foldr extract_lty acc tys
 
-extract_mb :: (a -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups)
-           -> Maybe a
-           -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_mb _ Nothing  acc = acc
-extract_mb f (Just x) acc = f x acc
-
-extract_lkind :: LHsType GhcPs -> FreeKiTyVars -> FreeKiTyVars
-extract_lkind = extract_lty KindLevel
-
-extract_lty :: TypeOrKind -> LHsType GhcPs
+extract_lty :: LHsType GhcPs
             -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_lty t_or_k (dL->L _ ty) acc
+extract_lty (dL->L _ ty) acc
   = case ty of
-      HsTyVar _ _  ltv            -> extract_tv t_or_k ltv acc
-      HsBangTy _ _ ty             -> extract_lty t_or_k ty acc
-      HsRecTy _ flds              -> foldr (extract_lty t_or_k
+      HsTyVar _ _  ltv            -> extract_tv ltv acc
+      HsBangTy _ _ ty             -> extract_lty ty acc
+      HsRecTy _ flds              -> foldr (extract_lty
                                             . cd_fld_type . unLoc) acc
                                            flds
-      HsAppTy _ ty1 ty2           -> extract_lty t_or_k ty1 $
-                                     extract_lty t_or_k ty2 acc
-      HsAppKindTy _ ty k          -> extract_lty t_or_k ty $
-                                     extract_lty KindLevel k acc
-      HsListTy _ ty               -> extract_lty t_or_k ty acc
-      HsTupleTy _ _ tys           -> extract_ltys t_or_k tys acc
-      HsSumTy _ tys               -> extract_ltys t_or_k tys acc
-      HsFunTy _ ty1 ty2           -> extract_lty t_or_k ty1 $
-                                     extract_lty t_or_k ty2 acc
-      HsIParamTy _ _ ty           -> extract_lty t_or_k ty acc
-      HsOpTy _ ty1 tv ty2         -> extract_tv t_or_k tv   $
-                                     extract_lty t_or_k ty1 $
-                                     extract_lty t_or_k ty2 acc
-      HsParTy _ ty                -> extract_lty t_or_k ty acc
+      HsAppTy _ ty1 ty2           -> extract_lty ty1 $
+                                     extract_lty ty2 acc
+      HsAppKindTy _ ty k          -> extract_lty ty $
+                                     extract_lty k acc
+      HsListTy _ ty               -> extract_lty ty acc
+      HsTupleTy _ _ tys           -> extract_ltys tys acc
+      HsSumTy _ tys               -> extract_ltys tys acc
+      HsFunTy _ ty1 ty2           -> extract_lty ty1 $
+                                     extract_lty ty2 acc
+      HsIParamTy _ _ ty           -> extract_lty ty acc
+      HsOpTy _ ty1 tv ty2         -> extract_tv tv $
+                                     extract_lty ty1 $
+                                     extract_lty ty2 acc
+      HsParTy _ ty                -> extract_lty ty acc
       HsSpliceTy {}               -> acc  -- Type splices mention no tvs
-      HsDocTy _ ty _              -> extract_lty t_or_k ty acc
-      HsExplicitListTy _ _ tys    -> extract_ltys t_or_k tys acc
-      HsExplicitTupleTy _ tys     -> extract_ltys t_or_k tys acc
+      HsDocTy _ ty _              -> extract_lty ty acc
+      HsExplicitListTy _ _ tys    -> extract_ltys tys acc
+      HsExplicitTupleTy _ tys     -> extract_ltys tys acc
       HsTyLit _ _                 -> acc
       HsStarTy _ _                -> acc
-      HsKindSig _ ty ki           -> extract_lty t_or_k ty $
-                                     extract_lkind ki acc
+      HsKindSig _ ty ki           -> extract_lty ty $
+                                     extract_lty ki acc
       HsForAllTy { hst_bndrs = tvs, hst_body = ty }
                                   -> extract_hs_tv_bndrs tvs acc $
-                                     extract_lty t_or_k ty emptyFKTV
+                                     extract_lty ty []
       HsQualTy { hst_ctxt = ctxt, hst_body = ty }
-                                  -> extract_lctxt t_or_k ctxt $
-                                     extract_lty t_or_k ty acc
+                                  -> extract_lctxt ctxt $
+                                     extract_lty ty acc
       XHsType {}                  -> acc
       -- We deal with these separately in rnLHsTypeWithWildCards
       HsWildCardTy {}             -> acc
@@ -1810,7 +1736,7 @@ extractHsTvBndrs :: [LHsTyVarBndr GhcPs]
                  -> FreeKiTyVarsWithDups           -- Free in body
                  -> FreeKiTyVarsWithDups       -- Free in result
 extractHsTvBndrs tv_bndrs body_fvs
-  = extract_hs_tv_bndrs tv_bndrs emptyFKTV body_fvs
+  = extract_hs_tv_bndrs tv_bndrs [] body_fvs
 
 extract_hs_tv_bndrs :: [LHsTyVarBndr GhcPs]
                     -> FreeKiTyVarsWithDups  -- Accumulator
@@ -1820,27 +1746,14 @@ extract_hs_tv_bndrs :: [LHsTyVarBndr GhcPs]
 --     'a' is bound by the forall
 --     'b' is a free type variable
 --     'e' is a free kind variable
-extract_hs_tv_bndrs tv_bndrs
-      (FKTV { fktv_kis = acc_kvs,  fktv_tys = acc_tvs })   -- Accumulator
-      (FKTV { fktv_kis = body_kvs, fktv_tys = body_tvs })  -- Free in the body
-  | null tv_bndrs
-  = FKTV { fktv_kis = body_kvs ++ acc_kvs
-         , fktv_tys = body_tvs ++ acc_tvs }
-  | otherwise
-  = FKTV { fktv_kis = filterOut (`elemRdr` tv_bndr_rdrs) all_kv_occs
-                      -- NB: delete all tv_bndr_rdrs from bndr_kvs as well
-                      -- as body_kvs; see Note [Kind variable scoping]
-                      ++ acc_kvs
-         , fktv_tys = filterOut (`elemRdr` tv_bndr_rdrs) body_tvs ++ acc_tvs }
+extract_hs_tv_bndrs tv_bndrs acc_vars body_vars
+  | null tv_bndrs = body_vars ++ acc_vars
+  | otherwise = filterOut (`elemRdr` tv_bndr_rdrs) (bndr_vars ++ body_vars) ++ acc_vars
+    -- NB: delete all tv_bndr_rdrs from bndr_vars as well as body_vars.
+    -- See Note [Kind variable scoping]
   where
-    bndr_kvs = extract_hs_tv_bndrs_kvs tv_bndrs
-
-    tv_bndr_rdrs, all_kv_occs :: [Located RdrName]
+    bndr_vars = extract_hs_tv_bndrs_kvs tv_bndrs
     tv_bndr_rdrs = map hsLTyVarLocName tv_bndrs
-    all_kv_occs = bndr_kvs ++ body_kvs
-       -- We must include both kind variables from the binding as well
-       -- as the body of the `forall` type.
-       -- See Note [Variables used as both types and kinds].
 
 extract_hs_tv_bndrs_kvs :: [LHsTyVarBndr GhcPs] -> [Located RdrName]
 -- Returns the free kind variables of any explictly-kinded binders, returning
@@ -1850,17 +1763,14 @@ extract_hs_tv_bndrs_kvs :: [LHsTyVarBndr GhcPs] -> [Located RdrName]
 --     Duplicates are /not/ removed
 --     E.g. given  [k1, a:k1, b:k2]
 --          the function returns [k1,k2], even though k1 is bound here
-extract_hs_tv_bndrs_kvs tv_bndrs
-  = freeKiTyVarsKindVars $        -- There will /be/ no free tyvars!
-    foldr extract_lkind emptyFKTV
+extract_hs_tv_bndrs_kvs tv_bndrs =
+    foldr extract_lty []
           [k | (dL->L _ (KindedTyVar _ _ k)) <- tv_bndrs]
 
-extract_tv :: TypeOrKind -> Located RdrName
-           -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups
-extract_tv t_or_k ltv@(dL->L _ tv) acc@(FKTV kvs tvs)
-  | not (isRdrTyVar tv) = acc
-  | isTypeLevel t_or_k  = FKTV { fktv_kis = kvs, fktv_tys = ltv : tvs }
-  | otherwise           = FKTV { fktv_kis = ltv : kvs, fktv_tys = tvs }
+extract_tv :: Located RdrName
+           -> [Located RdrName] -> [Located RdrName]
+extract_tv tv acc =
+  if isRdrTyVar (unLoc tv) then tv:acc else acc
 
 -- Deletes duplicates in a list of Located things.
 --
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 467c60465a..ef038e119b 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -47,7 +47,6 @@ module TcHsType (
         typeLevelMode, kindLevelMode,
 
         kindGeneralize, checkExpectedKind_pp,
-        reportFloatingKvs,
 
         -- Sort-checking kinds
         tcLHsKindSig, badKindSig,
@@ -1871,13 +1870,6 @@ kcLHsQTyVars_Cusk name flav
          -- doesn't work, we catch it here, before an error cascade
        ; checkValidTelescope tycon
 
-          -- If any of the specified tyvars aren't actually mentioned in a binder's
-          -- kind (or the return kind), then we're in the CUSK case from
-          -- Note [Free-floating kind vars]
-       ; let unmentioned_kvs   = filterOut (`elemVarSet` mentioned_kv_set) specified
-       ; reportFloatingKvs name flav (map binderVar final_tc_binders) unmentioned_kvs
-
-
        ; traceTc "kcLHsQTyVars: cusk" $
          vcat [ text "name" <+> ppr name
               , text "kv_ns" <+> ppr kv_ns
@@ -2889,8 +2881,6 @@ promotionErr name err
                NoDataKindsTC  -> text "perhaps you intended to use DataKinds"
                NoDataKindsDC  -> text "perhaps you intended to use DataKinds"
                PatSynPE       -> text "pattern synonyms cannot be promoted"
-               PatSynExPE     -> sep [ text "the existential variables of a pattern synonym"
-                                     , text "signature do not scope over the pattern" ]
                _ -> text "it is defined and used in the same recursive group"
 
 {-
@@ -2919,112 +2909,6 @@ badPatTyVarTvs sig_ty bad_tvs
 -}
 
 
-{- Note [Free-floating kind vars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  data S a = MkS (Proxy (a :: k))
-
-According to the rules around implicitly-bound kind variables,
-that k scopes over the whole declaration. The renamer grabs
-it and adds it to the hsq_implicits field of the HsQTyVars of the
-tycon.  So we get
-   S :: forall {k}. k -> Type
-
-That's fine.  But consider this variant:
-  data T = MkT (forall (a :: k). Proxy a)
-  -- from test ghci/scripts/T7873
-
-This is not an existential datatype, but a higher-rank one (the forall
-to the right of MkT). Again, 'k' scopes over the whole declaration,
-but we do not want to get
-   T :: forall {k}. Type
-Why not? Because the kind variable isn't fixed by anything. For
-a variable like k to be implicit, it needs to be mentioned in the kind
-of a tycon tyvar. But it isn't.
-
-Rejecting T depends on whether or not the datatype has a CUSK.
-
-Non-CUSK (handled in TcTyClsDecls.kcTyClGroup (generalise)):
-   When generalising the TyCon we check that every Specified 'k'
-   appears free in the kind of the TyCon; that is, in the kind of
-   one of its Required arguments, or the result kind.
-
-CUSK (handled in TcHsType.kcLHsQTyVars, the CUSK case):
-   When we determine the tycon's final, never-to-be-changed kind
-   in kcLHsQTyVars, we check to make sure all implicitly-bound kind
-   vars are indeed mentioned in a kind somewhere. If not, error.
-
-We also perform free-floating kind var analysis for type family instances
-(see #13985). 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 free-floating. Contrast that with this example:
-
-    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 -> *)
--}
-
--- See Note [Free-floating kind vars]
-reportFloatingKvs :: Name         -- of the tycon
-                  -> TyConFlavour -- What sort of TyCon it is
-                  -> [TcTyVar]    -- all tyvars, not necessarily zonked
-                  -> [TcTyVar]    -- floating tyvars
-                  -> TcM ()
-reportFloatingKvs tycon_name flav all_tvs bad_tvs
-  = unless (null bad_tvs) $  -- don't bother zonking if there's no error
-    do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs
-       ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs
-       ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs
-             tidy_bad_tvs             = map (tidyTyCoVarOcc tidy_env) bad_tvs
-       ; mapM_ (report tidy_all_tvs) tidy_bad_tvs }
-  where
-    report tidy_all_tvs tidy_bad_tv
-      = addErr $
-        vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+>
-               text "is implicitly bound in" <+> ppr flav
-             , quotes (ppr tycon_name) <> comma <+>
-               text "but does not appear as the kind of any"
-             , text "of its type variables. Perhaps you meant"
-             , text "to bind it explicitly somewhere?"
-             , ppWhen (not (null tidy_all_tvs)) $
-                 hang (text "Type variables with inferred kinds:")
-                 2 (ppr_tv_bndrs tidy_all_tvs) ]
-
-    ppr_tv_bndrs tvs = sep (map pp_tv tvs)
-    pp_tv tv         = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv))
-
 -- | If the inner action emits constraints, report them as errors and fail;
 -- otherwise, propagates the return value. Useful as a wrapper around
 -- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index d46ade1028..50721dc67a 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -384,9 +384,6 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details
            ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
            pushLevelAndCaptureConstraints            $
            tcExtendTyVarEnv univ_tvs                 $
-           tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
-                               | ex_tv <- extra_ex] $
-               -- See Note [Pattern synonym existentials do not scope]
            tcPat PatSyn lpat (mkCheckExpType pat_ty) $
            do { let in_scope    = mkInScopeSet (mkVarSet univ_tvs)
                     empty_subst = mkEmptyTCvSubst in_scope
@@ -451,54 +448,6 @@ This should work.  But in the matcher we must match against MkT, and then
 instantiate its argument 'x', to get a function of type (Int -> Int).
 Equality is not enough!  Trac #13752 was an example.
 
-Note [Pattern synonym existentials do not scope]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this (Trac #14498):
-  pattern SS :: forall (t :: k). () =>
-                => forall (a :: kk -> k) (n :: kk).
-                => TypeRep n -> TypeRep t
-  pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n)
-
-Here 'k' is implicitly bound in the signature, but (with
--XScopedTypeVariables) it does still scope over the pattern-synonym
-definition.  But what about 'kk', which is oexistential?  It too is
-implicitly bound in the signature; should it too scope?  And if so,
-what type variable is it bound to?
-
-The trouble is that the type variable to which it is bound is itself
-only brought into scope in part the pattern, so it makes no sense for
-'kk' to scope over the whole pattern.  See the discussion on
-Trac #14498, esp comment:16ff. Here is a simpler example:
-  data T where { MkT :: x -> (x->Int) -> T }
-  pattern P :: () => forall x. x -> (x->Int) -> T
-  pattern P a b = (MkT a b, True)
-
-Here it would make no sense to mention 'x' in the True pattern,
-like this:
-  pattern P a b = (MkT a b, True :: x)
-
-The 'x' only makes sense "under" the MkT pattern. Conclusion: the
-existential type variables of a pattern-synonym signature should not
-scope.
-
-But it's not that easy to implement, because we don't know
-exactly what the existentials /are/ until we get to type checking.
-(See Note [The pattern-synonym signature splitting rule], and
-the partition of implicit_tvs in tcCheckPatSynDecl.)
-
-So we do this:
-
-- The reaner brings all the implicitly-bound kind variables into
-  scope, without trying to distinguish universal from existential
-
-- tcCheckPatSynDecl uses tcExtendKindEnvList to bind the
-  implicitly-bound existentials to
-      APromotionErr PatSynExPE
-  It's not really a promotion error, but it's a way to bind the Name
-  (which the renamer has not complained about) to something that, when
-  looked up, will cause a complaint (in this case
-  TcHsType.promotionErr)
-
 
 Note [The pattern-synonym signature splitting rule]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 797a421956..9cf338b9d0 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1107,9 +1107,6 @@ data PromotionErr
   | PatSynPE         -- Pattern synonyms
                      -- See Note [Don't promote pattern synonyms] in TcEnv
 
-  | PatSynExPE       -- Pattern synonym existential type variable
-                     -- See Note [Pattern synonym existentials do not scope] in TcPatSyn
-
   | RecDataConPE     -- Data constructor in a recursive loop
                      -- See Note [Recursion and promoting data constructors] in TcTyClsDecls
   | NoDataKindsTC    -- -XDataKinds not enabled (for a tycon)
@@ -1303,7 +1300,6 @@ instance Outputable PromotionErr where
   ppr ClassPE                     = text "ClassPE"
   ppr TyConPE                     = text "TyConPE"
   ppr PatSynPE                    = text "PatSynPE"
-  ppr PatSynExPE                  = text "PatSynExPE"
   ppr FamDataConPE                = text "FamDataConPE"
   ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
                                       <+> parens (ppr pred)
@@ -1322,7 +1318,6 @@ pprPECategory :: PromotionErr -> SDoc
 pprPECategory ClassPE                = text "Class"
 pprPECategory TyConPE                = text "Type constructor"
 pprPECategory PatSynPE               = text "Pattern synonym"
-pprPECategory PatSynExPE             = text "Pattern synonym existential"
 pprPECategory FamDataConPE           = text "Data constructor"
 pprPECategory ConstrainedDataConPE{} = text "Data constructor"
 pprPECategory RecDataConPE           = text "Data constructor"
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 121193d6e2..631c777ab7 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1252,7 +1252,7 @@ reifyInstances th_nm th_tys
         ; rdr_ty <- cvt loc (mkThAppTs (TH.ConT th_nm) th_tys)
           -- #9262 says to bring vars into scope, like in HsForAllTy case
           -- of rnHsTyKi
-        ; let tv_rdrs = freeKiTyVarsAllVars (extractHsTyRdrTyVars rdr_ty)
+        ; let tv_rdrs = extractHsTyRdrTyVars rdr_ty
           -- Rename  to HsType Name
         ; ((tv_names, rn_ty), _fvs)
             <- checkNoErrs $ -- If there are out-of-scope Names here, then we
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 28b692f2e8..eb8a066529 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -537,7 +537,6 @@ generaliseTcTyCon tc
   = setSrcSpan (getSrcSpan tc) $
     addTyConCtxt tc $
     do { let tc_name     = tyConName tc
-             tc_flav     = tyConFlavour tc
              tc_res_kind = tyConResKind tc
              tc_tvs      = tyConTyVars  tc
 
@@ -610,21 +609,13 @@ generaliseTcTyCon tc
               , text "required_tcbs =" <+> ppr required_tcbs
               , text "final_tcbs =" <+> ppr final_tcbs ]
 
-       -- Step 8: check for floating kind vars
-       -- See Note [Free-floating kind vars]
-       -- They are easily identified by the fact that they
-       -- have not been skolemised by quantifyTyVars
-       ; let floating_specified = filter isTyVarTyVar scoped_tvs
-       ; reportFloatingKvs tc_name tc_flav
-                           scoped_tvs floating_specified
-
-       -- Step 9: Check for duplicates
+       -- 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 10: Check for validity.
+       -- 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.
diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index cf67246abf..cfe07deb81 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -16,6 +16,34 @@ Full details
 Language
 ~~~~~~~~
 
+- Kind variables are no longer implicitly quantified when an explicit ``forall`` is used, see
+  `GHC proposal #24
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__.
+  :ghc-flag:`-Wimplicit-kind-vars` is now obsolete.
+
+- Kind variables are no longer implicitly quantified in constructor declarations: ::
+
+    data T a        = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- no longer accepted
+    data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- still accepted
+
+- Implicitly quantified kind variables are no longer put in front of other variables: ::
+
+    f :: Proxy (a :: k) -> Proxy (b :: j)
+
+    ghci> :t +v f   -- old order:
+    f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b
+
+    ghci> :t +v f   -- new order:
+    f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b
+
+  This is a breaking change for users of :extension:`TypeApplications`.
+
+- In type synonyms and type family equations, free variables on the RHS are no longer
+  implicitly quantified unless used in an outermost kind annotation: ::
+
+    type T = Just (Nothing :: Maybe a)         -- no longer accepted
+    type T = Just Nothing :: Maybe (Maybe a)   -- still accepted
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index eae0283f6c..9ba8fa2daf 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7574,16 +7574,16 @@ instance for ``GMap`` is ::
 In this example, the declaration has only one variant. In general, it
 can be any number.
 
-When :extension:`ExplicitForAll` is enabled, type or kind variables used on
+When :extension:`ExplicitForAll` is enabled, type and kind variables used on
 the left hand side can be explicitly bound. For example: ::
 
     data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool
 
-When an explicit ``forall`` is present, all *type* variables mentioned which
-are not already in scope must be bound by the ``forall``. Kind variables will
-be implicitly bound if necessary, for example: ::
+When an explicit ``forall`` is present, *all* type and kind variables mentioned
+which are not already in scope must be bound by the ``forall``:
 
-    data instance forall (a :: k). F a = FOtherwise
+    data instance forall   (a :: k). F a = FOtherwise  -- rejected: k not in scope
+    data instance forall k (a :: k). F a = FOtherwise  -- accepted
 
 When the flag :ghc-flag:`-Wunused-type-patterns` is enabled, type
 variables that are mentioned in the patterns on the left hand side, but not
@@ -9184,17 +9184,74 @@ a type variable ``a`` of kind ``k``. In general, there is no limit to how
 deeply nested this sort of dependency can work. However, the dependency must
 be well-scoped: ``forall (a :: k) k. ...`` is an error.
 
-For backward compatibility, kind variables *do not* need to be bound explicitly,
-even if the type starts with ``forall``.
+Implicit quantification in type synonyms and type family instances
+------------------------------------------------------------------
 
-Accordingly, the rule for kind quantification in higher-rank contexts has
-changed slightly. In GHC 7, if a kind variable was mentioned for the first
-time in the kind of a variable bound in a non-top-level ``forall``, the kind
-variable was bound there, too.
-That is, in ``f :: (forall (a :: k). ...) -> ...``, the ``k`` was bound
-by the same ``forall`` as the ``a``. In GHC 8, however, all kind variables
-mentioned in a type are bound at the outermost level. If you want one bound
-in a higher-rank ``forall``, include it explicitly.
+Consider the scoping rules for type synonyms and type family instances, such as
+these::
+
+   type          TS a (b :: k) = <rhs>
+   type instance TF a (b :: k) = <rhs>
+
+The basic principle is that all variables mentioned on the right hand side
+``<rhs>`` must be bound on the left hand side::
+
+  type TS a (b :: k) = (k, a, Proxy b)    -- accepted
+  type TS a (b :: k) = (k, a, Proxy b, z) -- rejected: z not in scope
+
+But there is one exception: free variables mentioned in the outermost kind
+signature on the right hand side are quantified implicitly. Thus, in the
+following example the variables ``a``, ``b``, and ``k`` are all in scope on the
+right hand side of ``S``::
+
+  type S a b = <rhs> :: k -> k
+
+The reason for this exception is that there may be no other way to bind ``k``.
+For example, suppose we wanted ``S`` to have the the following kind with an
+*invisible* parameter ``k``::
+
+  S :: forall k. Type -> Type -> k -> k
+
+In this case, we could not simply bind ``k`` on the left-hand side, as ``k``
+would become a *visible* parameter::
+
+  type S k a b = <rhs> :: k -> k
+  S :: forall k -> Type -> Type -> k -> k
+
+Note that we only look at the *outermost* kind signature to decide which
+variables to quantify implicitly. As a counter-example, consider ``M1``: ::
+
+  type M1 = 'Just ('Nothing :: Maybe k)    -- rejected: k not in scope
+
+Here, the kind signature is hidden inside ``'Just``, and there is no outermost
+kind signature. We can fix this example by providing an outermost kind signature: ::
+
+  type M2 = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k)
+
+Here, ``k`` is brought into scope by ``:: Maybe (Maybe k)``.
+
+A kind signature is considered to be outermost regardless of redundant
+parentheses: ::
+
+  type P =    'Nothing :: Maybe a    -- accepted
+  type P = ((('Nothing :: Maybe a))) -- accepted
+
+Closed type family instances are subject to the same rules: ::
+
+  type family F where
+    F = 'Nothing :: Maybe k            -- accepted
+
+  type family F where
+    F = 'Just ('Nothing :: Maybe k)    -- rejected: k not in scope
+
+  type family F where
+    F = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k)  -- accepted
+
+  type family F :: Maybe (Maybe k) where
+    F = 'Just ('Nothing :: Maybe k)    -- rejected: k not in scope
+
+  type family F :: Maybe (Maybe k) where
+    F @k = 'Just ('Nothing :: Maybe k) -- accepted
 
 Kind-indexed GADTs
 ------------------
@@ -10832,19 +10889,6 @@ the rules in the subtler cases:
 - If an identifier's type has a ``forall``, then the order of type variables
   as written in the ``forall`` is retained.
 
-- If the type signature includes any kind annotations (either on variable
-  binders or as annotations on types), any variables used in kind
-  annotations come before any variables never used in kind annotations.
-  This rule is not recursive: if there is an annotation within an annotation,
-  then the variables used therein are on equal footing. Examples::
-
-    f :: Proxy (a :: k) -> Proxy (b :: j) -> ()
-      -- as if f :: forall k j a b. ...
-
-    g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> ()
-      -- as if g :: forall j k b a. ...
-      -- NB: k is in a kind annotation within a kind annotation
-
 - If any of the variables depend on other variables (that is, if some
   of the variables are *kind* variables), the variables are reordered
   so that kind variables come before type variables, preserving the
@@ -10854,13 +10898,11 @@ the rules in the subtler cases:
     h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
       -- as if h :: forall j k a b. ...
 
-  In this example, all of ``a``, ``j``, and ``k`` are considered kind
-  variables and will always be placed before ``b``, a lowly type variable.
-  (Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears
-  lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first,
-  because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k``
-  are not reordered with respect to each other, even though doing so would
-  not violate dependency conditions.
+  In this example, ``a`` depends on ``j`` and ``k``, and ``b`` depends on ``a``.
+  Even though ``a`` appears lexically before ``j`` and ``k``, ``j`` and ``k``
+  are quantified first, because ``a`` depends on ``j`` and ``k``. Note further
+  that ``j`` and ``k`` are not reordered with respect to each other, even
+  though doing so would not violate dependency conditions.
 
   A "stable topological sort" here, we mean that we perform this algorithm
   (which we call *ScopedSort*):
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index c392ab38df..9f9e4d948d 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -123,7 +123,6 @@ The following flags are simple ways to select standard "packages" of warnings:
         * :ghc-flag:`-Wmissing-monadfail-instances`
         * :ghc-flag:`-Wsemigroup`
         * :ghc-flag:`-Wnoncanonical-monoid-instances`
-        * :ghc-flag:`-Wimplicit-kind-vars`
         * :ghc-flag:`-Wstar-is-type`
 
 .. ghc-flag:: -Wno-compat
@@ -776,58 +775,6 @@ of ``-W(no-)*``.
 
     This warning is off by default.
 
-.. ghc-flag:: -Wimplicit-kind-vars
-    :shortdesc: warn when kind variables are brought into scope implicitly despite
-        the "forall-or-nothing" rule
-    :type: dynamic
-    :reverse: -Wno-implicit-kind-vars
-    :category:
-
-    :since: 8.6
-
-    `GHC proposal #24
-    <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__
-    prescribes to treat kind variables and type variables identically in
-    ``forall``, removing the legacy distinction between them.
-
-    Consider the following examples: ::
-
-        f :: Proxy a -> Proxy b -> ()
-        g :: forall a b. Proxy a -> Proxy b -> ()
-
-    ``f`` does not use an explicit ``forall``, so type variables ``a`` and ``b``
-    are brought into scope implicitly. ``g`` quantifies both ``a`` and ``b``
-    explicitly. Both ``f`` and ``g`` work today and will continue to work in the
-    future because they adhere to the "forall-or-nothing" rule: either all type
-    variables in a function definition are introduced explicitly or implicitly,
-    there is no middle ground.
-
-    A violation of the "forall-or-nothing" rule looks like this: ::
-
-        m :: forall a. Proxy a -> Proxy b -> ()
-
-    ``m`` does not introduce one of the variables, ``b``, and thus is rejected.
-
-    However, consider the following example: ::
-
-        n :: forall a. Proxy (a :: k) -> ()
-
-    While ``n`` uses ``k`` without introducing it and thus violates the rule, it
-    is currently accepted. This is because ``k`` in ``n`` is considered a kind
-    variable, as it occurs in a kind signature. In reality, the line between
-    type variables and kind variables is blurry, as the following example
-    demonstrates: ::
-
-        kindOf :: forall a. Proxy (a :: k) -> Proxy k
-
-    In ``kindOf``, the ``k`` variable is used both in a kind position and a type
-    position. Currently, ``kindOf`` happens to be accepted as well.
-
-    In a future release of GHC, both ``n`` and ``kindOf`` will be rejected per
-    the "forall-or-nothing" rule. This warning, being part of the
-    :ghc-flag:`-Wcompat` option group, allows to detect this before the actual
-    breaking change takes place.
-
 .. ghc-flag:: -Wincomplete-patterns
     :shortdesc: warn when a pattern match could fail
     :type: dynamic
diff --git a/testsuite/tests/codeGen/should_fail/T13233.hs b/testsuite/tests/codeGen/should_fail/T13233.hs
index 1facb77914..f24fc03bfb 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.hs
+++ b/testsuite/tests/codeGen/should_fail/T13233.hs
@@ -8,9 +8,9 @@ module Bug where
 import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
 
 class Foo (a :: TYPE rep) where
-  bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
+  bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
 
-baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
+baz :: forall rep (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
 baz = bar (#,#)
 
 obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
diff --git a/testsuite/tests/dependent/should_compile/T15264.stderr b/testsuite/tests/dependent/should_compile/T15264.stderr
deleted file mode 100644
index 222d686513..0000000000
--- a/testsuite/tests/dependent/should_compile/T15264.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-T15264.hs:8:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
-    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k’
-    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
-    Suggested fix: add ‘forall k.’
-
-T15264.hs:11:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
-    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k1’, ‘k2’
-    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
-    Suggested fix: add ‘forall k1 k2.’
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index fa39c9a69a..ca5f436174 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -48,7 +48,6 @@ test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
 test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
-test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
index b12adbd8e3..e33fdf110e 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -10,5 +10,5 @@ data SameKind :: k -> k -> *
 foo :: forall a k (b :: k). SameKind a b
 foo = undefined
 
-bar :: forall a (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
+bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
 bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 55a484910c..a8c4b689ae 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -5,9 +5,9 @@ BadTelescope2.hs:10:8: error:
         k (a :: k) (b :: k)
     • In the type signature: foo :: forall a k (b :: k). SameKind a b
 
-BadTelescope2.hs:13:70: error:
-    • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+BadTelescope2.hs:13:81: error:
+    • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
     • In the second argument of ‘SameKind’, namely ‘d’
       In the type signature:
-        bar :: forall a (c :: Proxy b) (d :: Proxy a).
+        bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
                Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_compile/T15264.hs b/testsuite/tests/dependent/should_fail/T15264.hs
index f3dec42564..394c53a013 100644
--- a/testsuite/tests/dependent/should_compile/T15264.hs
+++ b/testsuite/tests/dependent/should_fail/T15264.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE ExplicitForAll, PolyKinds #-}
-{-# OPTIONS -Wcompat -Wno-error=implicit-kind-vars #-}
 
 module T15264 where
 
diff --git a/testsuite/tests/dependent/should_fail/T15264.stderr b/testsuite/tests/dependent/should_fail/T15264.stderr
new file mode 100644
index 0000000000..6d5f597823
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15264.stderr
@@ -0,0 +1,6 @@
+
+T15264.hs:7:22: error: Not in scope: type variable ‘k’
+
+T15264.hs:10:22: error: Not in scope: type variable ‘k1’
+
+T15264.hs:10:32: error: Not in scope: type variable ‘k2’
diff --git a/testsuite/tests/dependent/should_fail/T15825.hs b/testsuite/tests/dependent/should_fail/T15825.hs
index 01227a8696..651525b21d 100644
--- a/testsuite/tests/dependent/should_fail/T15825.hs
+++ b/testsuite/tests/dependent/should_fail/T15825.hs
@@ -10,5 +10,5 @@ module T15825 where
 
 type C k = (forall (x::k). *)
 
-class                       X (a :: *)
-instance forall (a :: C k). X (a :: *)
+class                         X (a :: *)
+instance forall k (a :: C k). X (a :: *)
diff --git a/testsuite/tests/dependent/should_fail/T15825.stderr b/testsuite/tests/dependent/should_fail/T15825.stderr
index d64cab0494..97582ba952 100644
--- a/testsuite/tests/dependent/should_fail/T15825.stderr
+++ b/testsuite/tests/dependent/should_fail/T15825.stderr
@@ -1,5 +1,5 @@
 
-T15825.hs:14:29: error:
+T15825.hs:14:31: error:
     • Illegal type synonym family application ‘GHC.Types.Any
                                                  @k’ in instance:
         X (a @(GHC.Types.Any @k))
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index f1272200ba..4b258cc065 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -39,3 +39,4 @@ test('T15743c', normal, compile_fail, [''])
 test('T15743d', normal, compile_fail, [''])
 test('T15825', normal, compile_fail, [''])
 test('T15859', normal, compile_fail, [''])
+test('T15264', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr
index b4759714c2..8ec10322c8 100644
--- a/testsuite/tests/ghci/scripts/T7873.stderr
+++ b/testsuite/tests/ghci/scripts/T7873.stderr
@@ -1,8 +1,2 @@
 
-<interactive>:2:1: error:
-    • Kind variable ‘k’ is implicitly bound in data type
-      ‘D1’, but does not appear as the kind of any
-      of its type variables. Perhaps you meant
-      to bind it explicitly somewhere?
-      Type variables with inferred kinds: (k :: *)
-    • In the data type declaration for ‘D1’
+<interactive>:2:32: error: Not in scope: type variable ‘k’
diff --git a/testsuite/tests/ghci/scripts/T9293.stdout b/testsuite/tests/ghci/scripts/T9293.stdout
index 6d140bc9f7..87b950654d 100644
--- a/testsuite/tests/ghci/scripts/T9293.stdout
+++ b/testsuite/tests/ghci/scripts/T9293.stdout
@@ -13,7 +13,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -37,7 +36,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -60,7 +58,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -85,7 +82,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
diff --git a/testsuite/tests/ghci/scripts/ghci024.stdout b/testsuite/tests/ghci/scripts/ghci024.stdout
index 863184ad49..138da30075 100644
--- a/testsuite/tests/ghci/scripts/ghci024.stdout
+++ b/testsuite/tests/ghci/scripts/ghci024.stdout
@@ -14,7 +14,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
diff --git a/testsuite/tests/ghci/scripts/ghci057.stdout b/testsuite/tests/ghci/scripts/ghci057.stdout
index 6d140bc9f7..87b950654d 100644
--- a/testsuite/tests/ghci/scripts/ghci057.stdout
+++ b/testsuite/tests/ghci/scripts/ghci057.stdout
@@ -13,7 +13,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -37,7 +36,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -60,7 +58,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -85,7 +82,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
diff --git a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
index 067127cf8a..c16e4e0156 100644
--- a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
+++ b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
@@ -26,6 +26,6 @@ type family H a b where
 -- More tests
 
 type family D a b where
-  forall (a :: Type -> Type) (b :: a Int) (c :: k). D (Proxy b) (Proxy c) = ()
+  forall (a :: Type -> Type) (b :: a Int) k (c :: k). D (Proxy b) (Proxy c) = ()
   forall (a :: Bool) (b :: Proxy a). D (Proxy b) () = Int
   forall (a :: Type). D a a = Maybe a
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index d6cfe26b40..9a0c6b8e6e 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -287,8 +287,8 @@
         (NoExt)
         (DataFamInstDecl
          (HsIB
-          [{Name: k}
-          ,{Name: a}]
+          [{Name: a}
+          ,{Name: k}]
           (FamEqn
            (NoExt)
            ({ DumpRenamedAst.hs:18:18-20 }
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
index 1563a2eb23..d07ce73230 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
@@ -27,7 +27,7 @@ T15039a.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict (a ~~ b) -> ()
+                 ex3 :: forall a k (b :: k). Dict (a ~~ b) -> ()
                at T15039a.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
index c28b94879b..8f9c2c8a45 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
@@ -28,7 +28,7 @@ T15039b.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         standing for ‘Dict ((a :: *) ~~ (b :: k))’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
+                 ex3 :: forall a k (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
                at T15039b.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
index 40c126f061..261a82e91a 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
@@ -27,7 +27,7 @@ T15039c.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict (a ~~ b) -> ()
+                 ex3 :: forall a k (b :: k). Dict (a ~~ b) -> ()
                at T15039c.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
index cca94416b8..8548356001 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
@@ -29,7 +29,7 @@ T15039d.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         standing for ‘Dict ((a :: *) ~~ (b :: k))’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
+                 ex3 :: forall a k (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
                at T15039d.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T16334.hs b/testsuite/tests/partial-sigs/should_compile/T16334.hs
new file mode 100644
index 0000000000..c01ef5cc16
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16334.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE NamedWildCards, PartialTypeSignatures, PolyKinds, NoStarIsType #-}
+
+module T16334 where
+
+k :: (Int :: _t)
+k = 42
diff --git a/testsuite/tests/partial-sigs/should_compile/T16334.stderr b/testsuite/tests/partial-sigs/should_compile/T16334.stderr
new file mode 100644
index 0000000000..83429e0d33
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16334.stderr
@@ -0,0 +1,4 @@
+
+T16334.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_t’ standing for ‘Type’
+    • In the type signature: k :: (Int :: _t)
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index d6eaa7727a..3e62552a20 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -89,3 +89,4 @@ test('T15039b', normal, compile, ['-fprint-explicit-kinds'])
 test('T15039c', normal, compile, ['-fprint-equality-relations'])
 test('T15039d', normal, compile,
                 ['-fprint-explicit-kinds -fprint-equality-relations'])
+test('T16334', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T14498.hs b/testsuite/tests/patsyn/should_compile/T14498.hs
index 0744310aee..b7f7db4d8a 100644
--- a/testsuite/tests/patsyn/should_fail/T14498.hs
+++ b/testsuite/tests/patsyn/should_compile/T14498.hs
@@ -23,9 +23,9 @@ type SN = (TypeRep :: N -> Type)
 pattern SO = (Typeable :: TypeRep (O::N))
 
 pattern SS ::
-     forall (t :: k').
+     forall k' (t :: k').
      ()
-  => forall (a :: kk -> k') (n :: kk).
+  => forall kk (a :: kk -> k') (n :: kk).
      (t ~ a n)
   =>
   TypeRep n -> TypeRep t
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 54775a80a2..6eb9e2db8a 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -76,3 +76,4 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])],
 test('T14326', normal, compile, [''])
 test('T14394', normal, ghci_script, ['T14394.script'])
 test('T14552', normal, compile, [''])
+test('T14498', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T14507.hs b/testsuite/tests/patsyn/should_fail/T14507.hs
index b36425ced6..9599b73c77 100644
--- a/testsuite/tests/patsyn/should_fail/T14507.hs
+++ b/testsuite/tests/patsyn/should_fail/T14507.hs
@@ -13,7 +13,7 @@ foo rep = error "urk"
 type family SING :: k -> Type where
   SING = (TypeRep :: Bool -> Type)
 
-pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
+pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
 pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
                            , tr :: TypeRep (a::Bool)))
 
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 7cdef908a6..5431e8b76a 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -40,7 +40,6 @@ test('T13470', normal, compile_fail, [''])
 test('T14112', normal, compile_fail, [''])
 test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
-test('T14498', normal, compile_fail, [''])
 test('T14507', normal, compile_fail, ['-dsuppress-uniques'])
 test('T15289', normal, compile_fail, [''])
 test('T15685', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/BadKindVar.hs b/testsuite/tests/polykinds/BadKindVar.hs
index c24657f3d2..9275d453c5 100644
--- a/testsuite/tests/polykinds/BadKindVar.hs
+++ b/testsuite/tests/polykinds/BadKindVar.hs
@@ -5,5 +5,5 @@ module Foo where
 import Data.Proxy
 
 -- Should be illegal without PolyKinds
-f :: forall (a :: k). Proxy a
+f :: forall k (a :: k). Proxy a
 f = f
diff --git a/testsuite/tests/polykinds/BadKindVar.stderr b/testsuite/tests/polykinds/BadKindVar.stderr
index beeed2b3c8..3312350602 100644
--- a/testsuite/tests/polykinds/BadKindVar.stderr
+++ b/testsuite/tests/polykinds/BadKindVar.stderr
@@ -1,5 +1,5 @@
 
-BadKindVar.hs:8:19: error:
+BadKindVar.hs:8:21: error:
     Unexpected kind variable ‘k’
     Perhaps you intended to use PolyKinds
     In the type signature for ‘f’
diff --git a/testsuite/tests/polykinds/KindVarOrder.script b/testsuite/tests/polykinds/KindVarOrder.script
new file mode 100644
index 0000000000..c4b4165dcf
--- /dev/null
+++ b/testsuite/tests/polykinds/KindVarOrder.script
@@ -0,0 +1,9 @@
+:set -XPolyKinds -XDataKinds
+import Data.Kind (Type)
+data Proxy (a :: k)
+f :: Proxy (a :: k) -> Proxy (b :: j) -> (); f = f
+g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> (); g = g
+h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> (); h = h
+:t +v f
+:t +v g
+:t +v h
diff --git a/testsuite/tests/polykinds/KindVarOrder.stdout b/testsuite/tests/polykinds/KindVarOrder.stdout
new file mode 100644
index 0000000000..66a950dc23
--- /dev/null
+++ b/testsuite/tests/polykinds/KindVarOrder.stdout
@@ -0,0 +1,5 @@
+f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -> ()
+g :: forall j (b :: j) k (a :: Proxy Proxy).
+     Proxy b -> Proxy a -> ()
+h :: forall j k (a :: (j, k)) (b :: Proxy a).
+     Proxy a -> Proxy b -> ()
diff --git a/testsuite/tests/polykinds/T10503.hs b/testsuite/tests/polykinds/T10503.hs
index 2cc1ee717e..2b9900652f 100644
--- a/testsuite/tests/polykinds/T10503.hs
+++ b/testsuite/tests/polykinds/T10503.hs
@@ -5,5 +5,5 @@ data Proxy p = Proxy
 
 data KProxy (a :: *) = KProxy
 
-h :: forall r . (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r
+h :: forall k r . (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r
 h = undefined
diff --git a/testsuite/tests/polykinds/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr
index 9fb87e9be7..a47a872253 100644
--- a/testsuite/tests/polykinds/T10503.stderr
+++ b/testsuite/tests/polykinds/T10503.stderr
@@ -4,14 +4,14 @@ T10503.hs:8:6: error:
       from the context: Proxy 'KProxy ~ Proxy 'KProxy
         bound by a type expected by the context:
                    (Proxy 'KProxy ~ Proxy 'KProxy) => r
-        at T10503.hs:8:6-85
+        at T10503.hs:8:6-87
       ‘k’ is a rigid type variable bound by
         the type signature for:
           h :: forall k r. ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
-        at T10503.hs:8:6-85
+        at T10503.hs:8:6-87
     • In the ambiguity check for ‘h’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
-        h :: forall r.
+        h :: forall k r.
              (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r)
              -> r
diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr
index 2df92c34da..ba07f3cda1 100644
--- a/testsuite/tests/polykinds/T13985.stderr
+++ b/testsuite/tests/polykinds/T13985.stderr
@@ -1,28 +1,10 @@
 
-T13985.hs:13:41: error:
-    • Type variable ‘k’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the data instance declaration for ‘Fam’
+T13985.hs:13:41: error: Not in scope: type variable ‘k’
 
-T13985.hs:16:43: error:
-    • Type variable ‘a’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the type instance declaration for ‘T’
+T13985.hs:16:43: error: Not in scope: type variable ‘a’
 
-T13985.hs:23:26: error:
-    • Type variable ‘k’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the data instance declaration for ‘CD’
-      In the instance declaration for ‘C Type’
+T13985.hs:23:26: error: Not in scope: type variable ‘k’
 
-T13985.hs:24:37: error:
-    • Type variable ‘a’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the type instance declaration for ‘CT’
-      In the instance declaration for ‘C Type’
+T13985.hs:24:37: error: Not in scope: type variable ‘a’
 
-T13985.hs:28:39: error:
-    • Type variable ‘x’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the default type instance declaration for ‘ZT’
-      In the class declaration for ‘Z’
+T13985.hs:28:39: error: Not in scope: type variable ‘x’
diff --git a/testsuite/tests/polykinds/T14561.hs b/testsuite/tests/polykinds/T14561.hs
index 7b1f17e08e..8c74ab4740 100644
--- a/testsuite/tests/polykinds/T14561.hs
+++ b/testsuite/tests/polykinds/T14561.hs
@@ -8,7 +8,7 @@ module T14561 where
 import GHC.Types
 import GHC.Prim
 
-badId :: forall (a :: TYPE r). a -> a
+badId :: forall r (a :: TYPE r). a -> a
 badId = unsafeCoerce#
 -- Un-saturated application of a levity-polymorphic
 -- function that must be eta-expanded
diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs
index bdc05dd6df..aefa12b59e 100644
--- a/testsuite/tests/polykinds/T14563.hs
+++ b/testsuite/tests/polykinds/T14563.hs
@@ -5,5 +5,5 @@ import GHC.Types (TYPE)
 import Data.Kind
 
 data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where
-  Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a.
+  Lan :: forall rep rep' xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a.
          (g xx -> a) -> h xx -> Lan g h a
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 43d81c5e1e..6e8384542f 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -23,13 +23,13 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:12: error:
-    • Couldn't match kind ‘k3’ with ‘Struct cls2’
-      ‘k3’ is a rigid type variable bound by
+    • Couldn't match kind ‘k4’ with ‘Struct cls2’
+      ‘k4’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
         cls0 :: Struct cls -> Constraint
-        cls1 :: k3 -> Constraint
+        cls1 :: k4 -> Constraint
     • In the expression: struct :: AStruct (Structured a cls)
       In the expression: case struct :: AStruct (Structured a cls) of
       In an equation for ‘i’:
@@ -38,12 +38,12 @@ T14846.hs:39:12: error:
         i :: Hom riki a a (bound at T14846.hs:39:3)
 
 T14846.hs:39:31: error:
-    • Couldn't match kind ‘k3’ with ‘Struct cls2’
-      ‘k3’ is a rigid type variable bound by
+    • Couldn't match kind ‘k4’ with ‘Struct cls2’
+      ‘k4’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
-        cls1 :: k3 -> Constraint
+        cls1 :: k4 -> Constraint
         cls0 :: Struct cls -> Constraint
       Expected kind ‘Struct cls0’,
         but ‘Structured a cls’ has kind ‘Struct cls1’
diff --git a/testsuite/tests/polykinds/T14887a.hs b/testsuite/tests/polykinds/T14887a.hs
index 2e5cf02212..4179862cad 100644
--- a/testsuite/tests/polykinds/T14887a.hs
+++ b/testsuite/tests/polykinds/T14887a.hs
@@ -1,16 +1,10 @@
 {-# LANGUAGE PartialTypeSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-implicit-kind-vars #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 module Bug where
 
 import Data.Proxy
 
-f1 :: forall (x :: a). Proxy (x :: _)
--- This one has an implicitly-quantified kind var 'a', which
--- we will stop accepting in the future, under the forall-or-nothing
--- rule.  Hence -Wno-implicit-kind-vars
-f1 = Proxy
-
 f2 :: forall a (x :: a). Proxy (x :: _)
 f2 = Proxy
diff --git a/testsuite/tests/polykinds/T8616.hs b/testsuite/tests/polykinds/T8616.hs
index 47e31bcc94..e8f4c682bf 100644
--- a/testsuite/tests/polykinds/T8616.hs
+++ b/testsuite/tests/polykinds/T8616.hs
@@ -4,11 +4,11 @@ module T8616 where
 import Data.Proxy
 import GHC.Exts
 
-withSomeSing :: forall (kproxy :: k). Proxy kproxy
+withSomeSing :: forall k (kproxy :: k). Proxy kproxy
 withSomeSing = undefined :: (Any :: k)
   -- The 'k' is bought into scope by the type signature
   -- This is a type error, but should not crash GHC
 
-foo = (undefined :: Proxy (a :: k)) :: forall (a :: k). Proxy a
+foo = (undefined :: Proxy (a :: k)) :: forall k (a :: k). Proxy a
   -- Again, the 'k' is bought into scope by the type signature
-  -- No type error though
\ No newline at end of file
+  -- No type error though
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index f9e5132a34..4341b3051a 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -4,7 +4,7 @@ T8616.hs:8:16: error:
       ‘k’ is a rigid type variable bound by
         the type signature for:
           withSomeSing :: forall k (kproxy :: k). Proxy kproxy
-        at T8616.hs:7:1-50
+        at T8616.hs:7:1-52
       When matching types
         a0 :: *
         Any :: k
diff --git a/testsuite/tests/polykinds/T9144.hs b/testsuite/tests/polykinds/T9144.hs
index 0a9ef08afa..85e1b24dbe 100644
--- a/testsuite/tests/polykinds/T9144.hs
+++ b/testsuite/tests/polykinds/T9144.hs
@@ -8,7 +8,7 @@ import GHC.TypeLits
 data family Sing (a :: k)
 
 data SomeSing :: KProxy k -> * where
-  SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
+  SomeSing :: forall k (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
 
 class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where
   fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k)
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 8a885b39a5..1cfb2aa424 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -206,3 +206,4 @@ test('T14887a', normal, compile, [''])
 test('T14847', normal, compile, [''])
 test('T15795', normal, compile, [''])
 test('T15795a', normal, compile, [''])
+test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script'])
diff --git a/testsuite/tests/typecheck/should_compile/T13343.hs b/testsuite/tests/typecheck/should_compile/T13343.hs
index fcff9db1a4..2f3f120c72 100644
--- a/testsuite/tests/typecheck/should_compile/T13343.hs
+++ b/testsuite/tests/typecheck/should_compile/T13343.hs
@@ -4,6 +4,6 @@ module Bug where
 
 import GHC.Exts
 
-type Bad = forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1
+type Bad = (forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1) :: TYPE v
 
 -- should be accepted because GHC will generalize over v. Note v /= v1.
diff --git a/testsuite/tests/typecheck/should_fail/T12973.hs b/testsuite/tests/typecheck/should_fail/T12973.hs
index b0a33a8213..765e02f34b 100644
--- a/testsuite/tests/typecheck/should_fail/T12973.hs
+++ b/testsuite/tests/typecheck/should_fail/T12973.hs
@@ -9,7 +9,7 @@ class Num (a :: TYPE r) where
   (+) :: a -> a -> a
   fromInteger :: P.Integer -> a
 
-foo :: forall (a :: TYPE r). Num a => a
+foo :: forall r (a :: TYPE r). Num a => a
 foo = 3 + 4
 
 
diff --git a/testsuite/tests/typecheck/should_fail/T13983.stderr b/testsuite/tests/typecheck/should_fail/T13983.stderr
index d1b2fe067b..aba88bc9f2 100644
--- a/testsuite/tests/typecheck/should_fail/T13983.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13983.stderr
@@ -1,8 +1,2 @@
 
-T13983.hs:7:1: error:
-    • Kind variable ‘k’ is implicitly bound in type synonym
-      ‘Wat’, but does not appear as the kind of any
-      of its type variables. Perhaps you meant
-      to bind it explicitly somewhere?
-      Type variables with inferred kinds: (k :: *)
-    • In the type synonym declaration for ‘Wat’
+T13983.hs:7:25: error: Not in scope: type variable ‘k’
diff --git a/testsuite/tests/typecheck/should_fail/T15629.hs b/testsuite/tests/typecheck/should_fail/T15629.hs
index fdbba60ccc..6d1d0b8897 100644
--- a/testsuite/tests/typecheck/should_fail/T15629.hs
+++ b/testsuite/tests/typecheck/should_fail/T15629.hs
@@ -23,5 +23,5 @@ sg _ _ = Proxy
 f :: forall (x :: Type). Proxy x -> ()
 f _ = ()
   where
-    g :: forall ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+    g :: forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
     g = sg Proxy Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr
index ce77bb04a3..a0e0f42286 100644
--- a/testsuite/tests/typecheck/should_fail/T15629.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15629.stderr
@@ -1,12 +1,12 @@
 
-T15629.hs:26:35: error:
+T15629.hs:26:37: error:
     • Expected kind ‘x1 ~> F x1 ab1’,
         but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z’
     • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’
       In the first argument of ‘Proxy’, namely
         ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’
       In the type signature:
-        g :: forall ab.
+        g :: forall z ab.
              Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
 
 T15629.hs:27:9: error:
@@ -14,11 +14,11 @@ T15629.hs:27:9: error:
       ‘ab1’ is a rigid type variable bound by
         the type signature for:
           g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym)
-        at T15629.hs:26:5-82
+        at T15629.hs:26:5-84
       ‘z’ is a rigid type variable bound by
         the type signature for:
           g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym)
-        at T15629.hs:26:5-82
+        at T15629.hs:26:5-84
       When matching types
         f0 :: x ~> F x ab
         F1Sym :: TyFun x1 (F x1 z) -> *
@@ -31,7 +31,7 @@ T15629.hs:27:9: error:
             = ()
             where
                 g ::
-                  forall ab.
+                  forall z ab.
                   Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
                 g = sg Proxy Proxy
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T15797.hs b/testsuite/tests/typecheck/should_fail/T15797.hs
index eadd8cb972..925674fecf 100644
--- a/testsuite/tests/typecheck/should_fail/T15797.hs
+++ b/testsuite/tests/typecheck/should_fail/T15797.hs
@@ -13,7 +13,7 @@ import Data.Kind
 
 class Ríki (obj :: Type) where
   type Obj :: obj -> Constraint
-  type Obj = Bæ @obj
+  type Obj = Bæ @k :: k -> Constraint
 
 class    Bæ    (a :: k)
 instance Bæ @k (a :: k)