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.

2 files changed, 201 insertions, 295 deletions

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.
 --