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

5 files changed, 17 insertions, 15 deletions

diff --git a/testsuite/tests/polykinds/PolyKinds06.stderr b/testsuite/tests/polykinds/PolyKinds06.stderr
index d6fa854c8f..e5c9daa8c3 100644
--- a/testsuite/tests/polykinds/PolyKinds06.stderr
+++ b/testsuite/tests/polykinds/PolyKinds06.stderr
@@ -1,5 +1,6 @@
 
-PolyKinds06.hs:9:11:
-    Type constructor ‘A’ cannot be used here
-      (it is defined and used in the same recursive group)
-    In the kind ‘A -> *’
+PolyKinds06.hs:9:11: error:
+    • Type constructor ‘A’ cannot be used here
+        (it is defined and used in the same recursive group)
+    • In the kind ‘A -> *’
+      In the data type declaration for ‘B’
diff --git a/testsuite/tests/polykinds/T13625.stderr b/testsuite/tests/polykinds/T13625.stderr
index 4e0d4b68d6..98208fcde3 100644
--- a/testsuite/tests/polykinds/T13625.stderr
+++ b/testsuite/tests/polykinds/T13625.stderr
@@ -3,3 +3,4 @@ T13625.hs:5:11: error:
     • Data constructor ‘Y’ cannot be used here
         (it is defined and used in the same recursive group)
     • In the kind ‘Y’
+      In the data type declaration for ‘X’
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 1d852031d9..062dc49e1f 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -3,8 +3,8 @@ T14846.hs:38:8: error:
     • Couldn't match type ‘ríki’ with ‘Hom riki’
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
-          i :: forall k5 (cls2 :: k5
-                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls2) (ríki :: Struct
+          i :: forall k5 k6 (cls2 :: k6
+                                     -> Constraint) (xx :: k5) (a :: Struct cls2) (ríki :: Struct
                                                                                              cls2
                                                                                            -> Struct
                                                                                                 cls2
@@ -16,12 +16,12 @@ T14846.hs:38:8: error:
         Actual type: Hom riki a a
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
-        Instance sig: forall k1 (cls :: k1
-                                        -> Constraint) k2 (xx :: k2) (a :: Struct cls).
+        Instance sig: forall k1 k2 (cls :: k2
+                                           -> Constraint) (xx :: k1) (a :: Struct cls).
                       StructI xx a =>
                       Hom riki a a
-           Class sig: forall k1 (cls :: k1
-                                        -> Constraint) k2 (xx :: k2) (a :: Struct
+           Class sig: forall k1 k2 (cls :: k2
+                                           -> Constraint) (xx :: k1) (a :: Struct
                                                                              cls) (ríki :: Struct
                                                                                              cls
                                                                                            -> Struct
@@ -32,12 +32,12 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:31: error:
-    • Couldn't match kind ‘k4’ with ‘Struct cls2’
-      ‘k4’ is a rigid type variable bound by
+    • Couldn't match kind ‘k3’ with ‘Struct cls2’
+      ‘k3’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
-        cls1 :: k4 -> Constraint
+        cls1 :: k3 -> Constraint
         cls0 :: Struct cls -> Constraint
       Expected kind ‘Struct cls0’,
         but ‘Structured a cls’ has kind ‘Struct cls1’
diff --git a/testsuite/tests/polykinds/T15592.hs b/testsuite/tests/polykinds/T15592.hs
index 7e81c42565..e351c82bf5 100644
--- a/testsuite/tests/polykinds/T15592.hs
+++ b/testsuite/tests/polykinds/T15592.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds, TypeFamilies #-}
 {-# OPTIONS_GHC -ddump-types -fprint-explicit-foralls #-}
 module T15592 where
 
diff --git a/testsuite/tests/polykinds/T7524.stderr b/testsuite/tests/polykinds/T7524.stderr
index 2340ce1aa6..26cfe39e8a 100644
--- a/testsuite/tests/polykinds/T7524.stderr
+++ b/testsuite/tests/polykinds/T7524.stderr
@@ -2,5 +2,5 @@
 T7524.hs:5:15: error:
     Conflicting family instance declarations:
       forall k2 (a :: k2). F a a = Int -- Defined at T7524.hs:5:15
-      forall k2 k1 (a :: k1) (b :: k2).
+      forall k1 k2 (a :: k1) (b :: k2).
         F a b = Bool -- Defined at T7524.hs:6:15