Finish fix for #14880.

The real change that fixes the ticket is described in
Note [Naughty quantification candidates] in TcMType.

Fixing this required reworking candidateQTyVarsOfType, the function
that extracts free variables as candidates for quantification.
One consequence is that we now must be more careful when quantifying:
any skolems around must be quantified manually, and quantifyTyVars
will now only quantify over metavariables. This makes good sense,
as skolems are generally user-written and are listed in the AST.

As a bonus, we now have more control over the ordering of such
skolems.

Along the way, this commit fixes #15711 and refines the fix
to #14552 (by accepted a program that was previously rejected,
as we can now accept that program by zapping variables to Any).

This commit also does a fair amount of rejiggering kind inference
of datatypes. Notably, we now can skip the generalization step
in kcTyClGroup for types with CUSKs, because we get the
kind right the first time. This commit also thus fixes #15743 and
 #15592, which both concern datatype kind generalisation.
(#15591 is also very relevant.) For this aspect of the commit, see
Note [Required, Specified, and Inferred in types] in TcTyClsDecls.

Test cases: dependent/should_fail/T14880{,-2},
            dependent/should_fail/T15743[cd]
            dependent/should_compile/T15743{,e}
            ghci/scripts/T15743b
            polykinds/T15592
            dependent/should_fail/T15591[bc]
            ghci/scripts/T15591

2 files changed, 190 insertions, 82 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 196350348f..e90854c73d 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -8904,6 +8904,78 @@ This rule has occasionally-surprising consequences (see
 The kind-polymorphism from the class declaration makes ``D1``
 kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F1``.
 
+.. _inferring-variable-order:
+
+Inferring the order of variables in a type/class declaration
+------------------------------------------------------------
+
+It is possible to get intricate dependencies among the type variables
+introduced in a type or class declaration. Here is an example::
+
+  data T a (b :: k) c = MkT (a c)
+
+After analysing this declaration, GHC will discover that ``a`` and
+``c`` can be kind-polymorphic, with ``a :: k2 -> Type`` and
+``c :: k2``. We thus infer the following kind::
+
+  T :: forall {k2 :: Type} (k :: Type). (k2 -> Type) -> k -> k2 -> Type
+
+Note that ``k2`` is placed *before* ``k``, and that ``k`` is placed *before*
+``a``. Also, note that ``k2`` is written here in braces. As explained with
+:extension:`TypeApplications` (:ref:`inferred-vs-specified`),
+type and kind variables that GHC generalises
+over, but not written in the original program, are not available for visible
+type application. (These are called *inferred* variables.)
+Such variables are written in braces with
+:ghc-flag:`-fprint-explicit-foralls` enabled.
+
+The general principle is this:
+
+  * Variables not available for type application come first.
+    
+  * Then come variables the user has written, implicitly brought into scope
+    in a type variable's kind.
+
+  * Lastly come the normal type variables of a declaration.
+
+  * Variables not given an explicit ordering by the user are sorted according
+    to ScopedSort (:ref:`ScopedSort`).
+
+With the ``T`` example above, we could bind ``k`` *after* ``a``; doing so
+would not violate dependency concerns. However, it would violate our general
+principle, and so ``k`` comes first.
+    
+Sometimes, this ordering does not respect dependency. For example::
+
+  data T2 k (a :: k) (c :: Proxy '[a, b])
+
+It must be that ``a`` and ``b`` have the same kind. Note also that ``b``
+is implicitly declared in ``c``\'s kind. Thus, according to our general
+principle, ``b`` must come *before* ``k``. However, ``b`` *depends on*
+``k``. We thus reject ``T2`` with a suitable error message.
+
+In keeping with the way that class methods list their class variables
+first, associated types also list class variables before others. This
+means that the inferred variables from the class come before the
+specified variables from the class, which come before other implicitly
+bound variables. Here is an example::
+
+  class C (a :: k) b where
+    type F (c :: j) (d :: Proxy m) a b
+
+We infer these kinds::
+
+  C :: forall {k2 :: Type} (k :: Type). k -> k2 -> Constraint
+  F :: forall {k2 :: Type} (k :: Type)
+              {k3 :: Type} (j :: Type) (m :: k3).
+	      j -> Proxy m -> k -> k2 -> Type
+
+The "general principle" described here is meant to make all this more
+predictable for users. It would not be hard to extend GHC to relax
+this principle. If you should want a change here, consider writing
+a `proposal <https://github.com/ghc-proposals/ghc-proposals/>`_ to
+do so.
+
 .. index::
    single: CUSK
    single: complete user-supplied kind signature
@@ -10654,14 +10726,108 @@ is an identifier (the common case), its type is considered known only when
 the identifier has been given a type signature. If the identifier does
 not have a type signature, visible type application cannot be used.
 
-Here are the details:
+.. _inferred-vs-specified:
+
+Inferred vs. specified type variables
+-------------------------------------
+
+.. index::
+   single: type variable; inferred vs. specified
+
+GHC tracks a distinction between what we call *inferred* and *specified*
+type variables. Only specified type variables are available for instantiation
+with visible type application. An example illustrates this well::
+
+  f :: (Eq b, Eq a) => a -> b -> Bool
+  f x y = (x == x) && (y == y)
+
+  g x y = (x == x) && (y == y)
+
+The functions ``f`` and ``g`` have the same body, but only ``f`` is given
+a type signature. When GHC is figuring out how to process a visible type application,
+it must know what variable to instantiate. It thus must be able to provide
+an ordering to the type variables in a function's type.
+
+If the user has supplied a type signature, as in ``f``, then this is easy:
+we just take the ordering from the type signature, going left to right and
+using the first occurrence of a variable to choose its position within the
+ordering. Thus, the variables in ``f`` will be ``b``, then ``a``.
+
+In contrast, there is no reliable way to do this for ``g``; we will not know
+whether ``Eq a`` or ``Eq b`` will be listed first in the constraint in ``g``\'s
+type. In order to have visible type application be robust between releases of
+GHC, we thus forbid its use with ``g``.
+
+We say that the type variables in ``f`` are *specified*, while those in
+``g`` are *inferred*. The general rule is this: if the user has written
+a type variable in the source program, it is *specified*; if not, it is
+*inferred*.
+
+Thus rule applies in datatype declarations, too. For example, if we have
+``data Proxy a = Proxy`` (and :extension:`PolyKinds` is enabled), then
+``a`` will be assigned kind ``k``, where ``k`` is a fresh kind variable.
+Because ``k`` was not written by the user, it will be unavailable for
+type application in the type of the constructor ``Proxy``; only the ``a``
+will be available.
+
+When :ghc-flag:`-fprint-explicit-foralls` is enabled, inferred variables
+are printed in braces. Thus, the type of the data constructor ``Proxy``
+from the previous example would be ``forall {k} (a :: k). Proxy a``.
+We can observe this behavior in a GHCi session: ::
+
+  > :set -XTypeApplications -fprint-explicit-foralls
+  > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
+  > :type +v myLength1
+  myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
+  > let myLength2 = length
+  > :type +v myLength2
+  myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+  > :type +v myLength2 @[]
+
+  <interactive>:1:1: error:
+      • Cannot apply expression of type ‘t0 a0 -> Int’
+        to a visible type argument ‘[]’
+      • In the expression: myLength2 @[]
+
+Notice that since ``myLength1`` was defined with an explicit type signature,
+:ghci-cmd:`:type +v` reports that all of its type variables are available
+for type application. On the other hand, ``myLength2`` was not given a type
+signature. As a result, all of its type variables are surrounded with braces,
+and trying to use visible type application with ``myLength2`` fails.
+
+Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
+of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
+that would be inferred for a variable assigned to the expression provided
+(that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
+``myLength2``, this type will have no variables available to visible type
+application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
+type of the expression provided. To illustrate this: ::
+
+  > :type myLength1
+  myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
+  > :type myLength2
+  myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+
+Using :ghci-cmd:`:type` might lead one to conclude that none of the type
+variables in ``myLength1``'s type signature are available for type
+application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
+if you want the most accurate information with respect to visible type
+application properties.
+
+.. _ScopedSort:
+
+.. index::
+   single: ScopedSort
+
+Ordering of specified variables
+-------------------------------
+
+In the simple case of the previous section, we can say that specified variables
+appear in left-to-right order. However, not all cases are so simple. Here are
+the rules in the subtler cases:
 
-- If an identifier's type signature does not include an
-  explicit ``forall``, the type variable arguments appear
-  in the left-to-right order in which the variables appear in the type.
-  So, ``foo :: Monad m => a b -> m (a c)``
-  will have its type variables
-  ordered as ``m, a, b, c``.
+- 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
@@ -10680,7 +10846,7 @@ Here are the details:
   of the variables are *kind* variables), the variables are reordered
   so that kind variables come before type variables, preserving the
   left-to-right order as much as possible. That is, GHC performs a
-  stable topological sort on the variables. Examples::
+  stable topological sort on the variables. Example::
 
     h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
       -- as if h :: forall j k a b. ...
@@ -10693,10 +10859,12 @@ Here are the details:
   are not reordered with respect to each other, even though doing so would
   not violate dependency conditions.
 
-- Visible type application is available to instantiate only user-specified
-  type variables. This means that in ``data Proxy a = Proxy``, the unmentioned
-  kind variable used in ``a``'s kind is *not* available for visible type
-  application.
+  A "stable topological sort" here, we mean that we perform this algorithm
+  (which we call *ScopedSort*):
+
+  * Work left-to-right through the input list of type variables, with a cursor.
+  * If variable ``v`` at the cursor is depended on by any earlier variable ``w``,
+    move ``v`` immediately before the leftmost such ``w``.
 
 - Class methods' type arguments include the class type
   variables, followed by any variables an individual method is polymorphic
@@ -10719,72 +10887,9 @@ Here are the details:
   necessary to specify :extension:`PartialTypeSignatures` and your
   code will not generate a warning informing you of the omitted type.
 
-- When printing types with :ghc-flag:`-fprint-explicit-foralls` enabled,
-  type variables not available for visible type application are printed
-  in braces. We can observe this behavior in a GHCi session: ::
-
-    > :set -XTypeApplications -fprint-explicit-foralls
-    > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
-    > :type +v myLength1
-    myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
-    > let myLength2 = length
-    > :type +v myLength2
-    myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
-    > :type +v myLength2 @[]
-
-    <interactive>:1:1: error:
-        • Cannot apply expression of type ‘t0 a0 -> Int’
-          to a visible type argument ‘[]’
-        • In the expression: myLength2 @[]
-
-  Notice that since ``myLength1`` was defined with an explicit type signature,
-  :ghci-cmd:`:type +v` reports that all of its type variables are available
-  for type application. On the other hand, ``myLength2`` was not given a type
-  signature. As a result, all of its type variables are surrounded with braces,
-  and trying to use visible type application with ``myLength2`` fails.
-
-  Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
-  of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
-  that would be inferred for a variable assigned to the expression provided
-  (that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
-  ``myLength2``, this type will have no variables available to visible type
-  application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
-  type of the expression provided. To illustrate this: ::
-
-    > :type myLength1
-    myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
-    > :type myLength2
-    myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
-
-  Using :ghci-cmd:`:type` might lead one to conclude that none of the type
-  variables in ``myLength1``'s type signature are available for type
-  application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
-  if you want the most accurate information with respect to visible type
-  application properties.
-
-- Although GHC supports visible *type* applications, it does not yet support
-  visible *kind* applications. However, GHC does follow similar rules for
-  quantifying variables in kind signatures as it does for quantifying type
-  signatures. For instance: ::
-
-    type family F (a :: j) (b :: k) :: l
-      -- F :: forall j k l. j -> k -> l
-
-  In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l``
-  is preserved.
-
-  If a family declaration is associated with a class, then class-bound
-  variables always come first in the kind of the family. For instance: ::
-
-    class C (a :: Type) where
-      type T (x :: f a)
-      -- T :: forall a f. f a -> Type
-
-  Contrast this with the kind of the following top-level family declaration: ::
-
-    type family T2 (x :: f a)
-    -- T2 :: forall f a. f a -> Type
-
+The section in this manual on kind polymorphism describes how variables
+in type and class declarations are ordered (:ref:`inferring-variable-order`).
+  
 .. _implicit-parameters:
 
 Implicit parameters
diff --git a/docs/users_guide/using.rst b/docs/users_guide/using.rst
index 4373a4a8d5..e0807a9620 100644
--- a/docs/users_guide/using.rst
+++ b/docs/users_guide/using.rst
@@ -764,10 +764,13 @@ messages and in GHCi:
 
            ghci> :i Data.Type.Equality.sym
            Data.Type.Equality.sym ::
-             forall (k :: BOX) (a :: k) (b :: k).
+             forall k (a :: k) (b :: k).
              (a Data.Type.Equality.:~: b) -> b Data.Type.Equality.:~: a
                    -- Defined in Data.Type.Equality
 
+    This flag also enables the printing of *inferred* type variables
+    inside braces. See :ref:`inferred-vs-specified`.
+		   
 .. ghc-flag:: -fprint-explicit-kinds
     :shortdesc: Print explicit kind foralls and kind arguments in types.
         See also :ghc-flag:`-XKindSignatures`
@@ -784,10 +787,10 @@ messages and in GHCi:
         ghci> :set -XPolyKinds
         ghci> data T a = MkT
         ghci> :t MkT
-        MkT :: forall (k :: BOX) (a :: k). T a
-        ghci> :set -fprint-explicit-foralls
+        MkT :: forall (k :: Type) (a :: k). T a
+        ghci> :set -fprint-explicit-kinds
         ghci> :t MkT
-        MkT :: forall (k :: BOX) (a :: k). T k a
+        MkT :: forall (k :: Type) (a :: k). T k a
 
 .. ghc-flag:: -fprint-explicit-runtime-reps
     :shortdesc: Print ``RuntimeRep`` variables in types which are