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.

8 files changed, 206 insertions, 481 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.