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.

3 files changed, 105 insertions, 88 deletions

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