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

48 files changed, 291 insertions, 64 deletions

diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs
index c2bec19d44..c2bec19d44 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.hs
+++ b/testsuite/tests/dependent/should_compile/InferDependency.hs
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
index 610e434d6c..906695f3f7 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.stderr
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -1,5 +1,5 @@
 
 T14066a.hs:13:3: warning:
     Type family instance equation is overlapped:
-      forall d c (x :: c) (y :: d).
+      forall c d (x :: c) (y :: d).
         Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_compile/T14880-2.hs b/testsuite/tests/dependent/should_compile/T14880-2.hs
new file mode 100644
index 0000000000..e7057a3f00
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14880-2.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type
+
+quux :: forall arg. Proxy (Foo arg) -> ()
+quux (_ :: _) = ()
diff --git a/testsuite/tests/dependent/should_compile/T14880-2.stderr b/testsuite/tests/dependent/should_compile/T14880-2.stderr
new file mode 100644
index 0000000000..758924dd41
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14880-2.stderr
@@ -0,0 +1,12 @@
+
+T14880-2.hs:13:12: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Proxy (Foo arg)’
+      Where: ‘arg’ is a rigid type variable bound by
+               the type signature for:
+                 quux :: forall arg. Proxy (Foo arg) -> ()
+               at T14880-2.hs:12:1-41
+    • In a pattern type signature: _
+      In the pattern: _ :: _
+      In an equation for ‘quux’: quux (_ :: _) = ()
+    • Relevant bindings include
+        quux :: Proxy (Foo arg) -> () (bound at T14880-2.hs:13:1)
diff --git a/testsuite/tests/dependent/should_compile/T14880.hs b/testsuite/tests/dependent/should_compile/T14880.hs
new file mode 100644
index 0000000000..91cfb20a4a
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14880.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type
+
+data Bar :: Type -> Type where
+    MkBar :: forall x arg.
+             -- Commenting out the line below makes the issue go away
+             Foo arg ~ Foo arg =>
+             Bar x
diff --git a/testsuite/tests/dependent/should_compile/T15743.hs b/testsuite/tests/dependent/should_compile/T15743.hs
new file mode 100644
index 0000000000..1ba10aeb9a
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15743.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies #-}
+
+module T15743 where
+
+import Data.Proxy
+
+data T (b :: Proxy (k2 :: k)) c (a :: k)
diff --git a/testsuite/tests/dependent/should_compile/T15743.stderr b/testsuite/tests/dependent/should_compile/T15743.stderr
new file mode 100644
index 0000000000..7162a877a2
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15743.stderr
@@ -0,0 +1,6 @@
+TYPE CONSTRUCTORS
+  type role T nominal nominal nominal phantom phantom phantom
+  T :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> *
+Dependent modules: []
+Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
+                     integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/dependent/should_compile/T15743e.hs b/testsuite/tests/dependent/should_compile/T15743e.hs
new file mode 100644
index 0000000000..37e0cbb2cd
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15743e.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE RankNTypes, PolyKinds, DataKinds, GADTs #-}
+
+module T15743e where
+
+import Data.Proxy
+import Data.Kind
+
+-- NO CUSK.
+data T k (a :: k) (b :: Proxy k2) f c :: forall k3. Proxy k3 -> forall (k4 :: k5). Proxy k4 -> Type where
+  MkT :: f c -> T k a b f c d e
+
+-- Want:
+-- T :: forall {k3} {k7} {k6} (k2 :: k3) (k5 :: Type).
+--      forall k -> k -> Proxy k2 -> (k7 -> Type) -> k4 ->
+--      forall (k3 :: k6). Proxy k3 -> forall (k4 :: k5). Proxy k4 -> Type
+--
+--
+
+-- CUSK
+data T2 (k :: Type) (a :: k) (b :: Proxy k2) (f :: k7 -> Type) (c :: k7) :: forall k3. Proxy k3 -> forall k5 (k4 :: k5). Proxy k4 -> Type where
+  MkT2 :: f c -> T2 k a b f c d e
diff --git a/testsuite/tests/dependent/should_compile/T15743e.stderr b/testsuite/tests/dependent/should_compile/T15743e.stderr
new file mode 100644
index 0000000000..c77bf3849c
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T15743e.stderr
@@ -0,0 +1,32 @@
+TYPE CONSTRUCTORS
+  type role T
+    nominal nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal phantom
+  T ::
+    forall {k1} {k2} {k3} (k4 :: k2) k5. forall k6 ->
+    k6
+    -> Proxy k4
+    -> (k3 -> *)
+    -> k3
+    -> forall (k7 :: k1). Proxy k7 -> forall (k8 :: k5). Proxy k8 -> *
+  type role T2
+    nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal nominal phantom
+  T2 ::
+    forall {k1} {k2} (k3 :: k1) k7. forall k4 ->
+    k4
+    -> Proxy k3
+    -> (k7 -> *)
+    -> k7
+    -> forall (k5 :: k2).
+       Proxy k5 -> forall k6 (k8 :: k6). Proxy k8 -> *
+DATA CONSTRUCTORS
+  MkT2 :: forall {k7} {k1} {k2 :: k1} {k3} {k4 :: k3} {k5} {k6 :: k5}
+                 (f :: k7 -> *) (c :: k7) k8 (a :: k8) (b :: Proxy k2)
+                 (d :: Proxy k4) (e :: Proxy k6).
+          f c -> T2 k8 a b f c d e
+  MkT :: forall {k1} {k2} {k3 :: k2} {k4} {k5 :: k4} {k6} {k7 :: k6}
+                (f :: k1 -> *) (c :: k1) k8 (a :: k8) (b :: Proxy k3)
+                (d :: Proxy k5) (e :: Proxy k7).
+         f c -> T k8 a b f c d e
+Dependent modules: []
+Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
+                     integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 1bf6cc7142..16c6d13ba9 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -56,3 +56,8 @@ test('T15419', normal, compile, [''])
 test('T14066h', normal, compile, [''])
 test('T15666', normal, compile, [''])
 test('T15725', normal, compile, [''])
+test('T14880', normal, compile, [''])
+test('T14880-2', normal, compile, [''])
+test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
+test('InferDependency', normal, compile, [''])
+test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls'])
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
deleted file mode 100644
index cc852ee58c..0000000000
--- a/testsuite/tests/dependent/should_fail/InferDependency.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-InferDependency.hs:6:13: error:
-    • Type constructor argument ‘k’ is used dependently.
-      Any dependent arguments must be obviously so, not inferred
-      by the type-checker.
-      Inferred argument kinds:
-        k :: *
-        a :: k
-      Suggestion: use ‘k’ in a kind to make the dependency clearer.
-    • In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr
index 8ac4be8c0c..3c90f5444b 100644
--- a/testsuite/tests/dependent/should_fail/SelfDep.stderr
+++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr
@@ -3,3 +3,4 @@ SelfDep.hs:5:11: error:
     • Type constructor ‘T’ cannot be used here
         (it is defined and used in the same recursive group)
     • In the kind ‘T -> *’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
index 3e8bef6858..3ced11a79d 100644
--- a/testsuite/tests/dependent/should_fail/T13895.stderr
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -1,19 +1,15 @@
 
 T13895.hs:8:14: error:
-    • Could not deduce (Typeable (t dict0))
+    • Could not deduce (Typeable (t dict))
       from the context: (Data a, Typeable (t dict))
         bound by the type signature for:
-                   dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable
-                                                                          *) a (c :: *
-                                                                                     -> *) (t :: forall k1.
-                                                                                                 Typeable
-                                                                                                   k1 =>
-                                                                                                 k1
-                                                                                                 -> *).
+                   dataCast1 :: forall k1 a (c :: * -> *) (t :: forall k2.
+                                                                Typeable k2 =>
+                                                                k2 -> *).
                                 (Data a, Typeable (t dict)) =>
                                 (forall d. Data d => c (t dict1 d)) -> Maybe (c a)
         at T13895.hs:(8,14)-(14,24)
-      The type variable ‘dict0’ is ambiguous
+      The type variable ‘k0’ is ambiguous
     • In the ambiguity check for ‘dataCast1’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
index 8ece51029b..23b8577a1b 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -15,7 +15,7 @@ T14066d.hs:11:35: error:
       In the expression: g y
       In the expression: (fstOf3 y :: Proxy Maybe, g y)
     • Relevant bindings include
-        y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b)
+        y :: forall k1 k2 (a :: k1) (c :: k2). (Proxy a, Proxy c, b)
           (bound at T14066d.hs:15:5)
         x :: b (bound at T14066d.hs:11:3)
         f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
index 193c74d193..a6bf647bee 100644
--- a/testsuite/tests/dependent/should_fail/T14066e.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -1,15 +1,15 @@
 
 T14066e.hs:13:59: error:
-    • Couldn't match kind ‘k1’ with ‘*’
-      ‘k1’ is a rigid type variable bound by
+    • Couldn't match kind ‘k’ with ‘*’
+      ‘k’ is a rigid type variable bound by
         the type signature for:
-          j :: forall k k1 (c :: k1) (b :: k).
+          j :: forall k k1 (c :: k) (b :: k1).
                Proxy a -> Proxy b -> Proxy c -> Proxy b
         at T14066e.hs:12:5-61
       When matching kinds
-        k :: *
-        c :: k1
-      Expected kind ‘c’, but ‘b'’ has kind ‘k’
+        k1 :: *
+        c :: k
+      Expected kind ‘c’, but ‘b'’ has kind ‘k1’
     • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
       In an expression type signature: Proxy (b' :: c')
       In the expression: (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T15591b.hs b/testsuite/tests/dependent/should_fail/T15591b.hs
new file mode 100644
index 0000000000..fb23aca2e5
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15591b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds, MultiParamTypeClasses, DataKinds, TypeFamilies #-}
+
+module T15591b where
+
+import Data.Proxy
+import Data.Kind
+
+class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where
+  type T4 a c
diff --git a/testsuite/tests/dependent/should_fail/T15591b.stderr b/testsuite/tests/dependent/should_fail/T15591b.stderr
new file mode 100644
index 0000000000..838ee51c8f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15591b.stderr
@@ -0,0 +1,7 @@
+
+T15591b.hs:9:3: error:
+    • These kind and type variables: a c
+      are out of dependency order. Perhaps try this ordering:
+        a (b :: Proxy a) (c :: Proxy b)
+      NB: Implicitly declared variables come before others.
+    • In the associated type family declaration for ‘T4’
diff --git a/testsuite/tests/dependent/should_fail/T15591c.hs b/testsuite/tests/dependent/should_fail/T15591c.hs
new file mode 100644
index 0000000000..b9fcb9cc96
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15591c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds, MultiParamTypeClasses, DataKinds, TypeFamilies #-}
+
+module T15591c where
+
+import Data.Proxy
+import Data.Kind
+
+class C3 (a :: Type) (b :: Proxy a) (c :: Proxy b) where
+  type T5 c a
diff --git a/testsuite/tests/dependent/should_fail/T15591c.stderr b/testsuite/tests/dependent/should_fail/T15591c.stderr
new file mode 100644
index 0000000000..2f2b47fc8d
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15591c.stderr
@@ -0,0 +1,7 @@
+
+T15591c.hs:9:3: error:
+    • These kind and type variables: c a
+      are out of dependency order. Perhaps try this ordering:
+        a (b :: Proxy a) (c :: Proxy b)
+      NB: Implicitly declared variables come before others.
+    • In the associated type family declaration for ‘T5’
diff --git a/testsuite/tests/dependent/should_fail/T15743c.hs b/testsuite/tests/dependent/should_fail/T15743c.hs
new file mode 100644
index 0000000000..eb8f68349f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15743c.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PolyKinds, DataKinds, ExplicitForAll #-}
+
+module T15743 where
+
+import Data.Kind
+import Data.Proxy
+
+data SimilarKind :: forall (c :: k) (d :: k). Proxy c -> Proxy d -> Type
+
+data T k (c :: k) (a :: Proxy c) b (x :: SimilarKind a b)
+data T2 k (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b)
diff --git a/testsuite/tests/dependent/should_fail/T15743c.stderr b/testsuite/tests/dependent/should_fail/T15743c.stderr
new file mode 100644
index 0000000000..9d28b68998
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15743c.stderr
@@ -0,0 +1,16 @@
+
+T15743c.hs:10:1: error:
+    • These kind and type variables: k
+                                     (c :: k)
+                                     (a :: Proxy c)
+                                     b
+                                     (x :: SimilarKind a b)
+      are out of dependency order. Perhaps try this ordering:
+        k
+        (d :: k)
+        (c :: k)
+        (a :: Proxy c)
+        (b :: Proxy d)
+        (x :: SimilarKind a b)
+      NB: Implicitly declared variables come before others.
+    • In the data type declaration for ‘T’
diff --git a/testsuite/tests/dependent/should_fail/T15743d.hs b/testsuite/tests/dependent/should_fail/T15743d.hs
new file mode 100644
index 0000000000..67d8faebed
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15743d.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds, DataKinds, ExplicitForAll #-}
+
+module T15743 where
+
+import Data.Kind
+import Data.Proxy
+
+data SimilarKind :: forall (c :: k) (d :: k). Proxy c -> Proxy d -> Type
+
+data T2 k (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b)
diff --git a/testsuite/tests/dependent/should_fail/T15743d.stderr b/testsuite/tests/dependent/should_fail/T15743d.stderr
new file mode 100644
index 0000000000..d982d16980
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15743d.stderr
@@ -0,0 +1,16 @@
+
+T15743d.hs:10:1: error:
+    • These kind and type variables: k
+                                     (c :: k)
+                                     (a :: Proxy c)
+                                     (b :: Proxy d)
+                                     (x :: SimilarKind a b)
+      are out of dependency order. Perhaps try this ordering:
+        k
+        (d :: k)
+        (c :: k)
+        (a :: Proxy c)
+        (b :: Proxy d)
+        (x :: SimilarKind a b)
+      NB: Implicitly declared variables come before others.
+    • In the data type declaration for ‘T2’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 0f7129020e..2b602fa383 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -28,9 +28,12 @@ test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
 test('T14845_fail1', normal, compile_fail, [''])
 test('T14845_fail2', normal, compile_fail, [''])
-test('InferDependency', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
 test('T15343', normal, compile_fail, [''])
 test('T15380', normal, compile_fail, [''])
+test('T15591b', normal, compile_fail, [''])
+test('T15591c', normal, compile_fail, [''])
+test('T15743c', normal, compile_fail, [''])
+test('T15743d', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci/scripts/T15591.hs b/testsuite/tests/ghci/scripts/T15591.hs
index eccf628eed..f333fe0194 100644
--- a/testsuite/tests/ghci/scripts/T15591.hs
+++ b/testsuite/tests/ghci/scripts/T15591.hs
@@ -1,10 +1,26 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 module Foo where
 
 import Data.Kind
+import Data.Proxy
 
 type family T1 (x :: f (a :: Type))
 
 class C (a :: Type) where
   type T2 (x :: f a)
+
+class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where
+  type T3 (x :: Proxy '(a, c))
+
+-- no CUSK
+class C3 (a :: Type) (b :: Proxy a) (c :: Proxy b) d where
+  type T4 (x :: Proxy '(a, c))
+
+class C4 (a :: Type) b where
+  type T5 (x :: f a)
+
+class C5 a where
+  type T6 (x :: f a)
diff --git a/testsuite/tests/ghci/scripts/T15591.script b/testsuite/tests/ghci/scripts/T15591.script
index 0afd32e1e6..0e181a960e 100644
--- a/testsuite/tests/ghci/scripts/T15591.script
+++ b/testsuite/tests/ghci/scripts/T15591.script
@@ -2,3 +2,7 @@
 :set -fprint-explicit-foralls
 :kind T1
 :kind T2
+:kind T3
+:kind T4
+:kind T5
+:kind T6
diff --git a/testsuite/tests/ghci/scripts/T15591.stdout b/testsuite/tests/ghci/scripts/T15591.stdout
index 28dbd49dc1..b4673d5174 100644
--- a/testsuite/tests/ghci/scripts/T15591.stdout
+++ b/testsuite/tests/ghci/scripts/T15591.stdout
@@ -1,2 +1,6 @@
 T1 :: forall (f :: * -> *) a. f a -> *
 T2 :: forall a (f :: * -> *). f a -> *
+T3 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> *
+T4 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> *
+T5 :: forall a (f :: * -> *). f a -> *
+T6 :: forall {k} (a :: k) (f :: k -> *). f a -> *
diff --git a/testsuite/tests/ghci/scripts/T15743b.hs b/testsuite/tests/ghci/scripts/T15743b.hs
new file mode 100644
index 0000000000..2bd5b6b649
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15743b.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PolyKinds, TypeFamilies #-}
+
+module T15743b where
+
+class C (a :: k) where
+  type F a (b :: k2)
diff --git a/testsuite/tests/ghci/scripts/T15743b.script b/testsuite/tests/ghci/scripts/T15743b.script
new file mode 100644
index 0000000000..cb0f6c4a5b
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15743b.script
@@ -0,0 +1,3 @@
+:load T15743b.hs
+:set -fprint-explicit-foralls
+:k F
diff --git a/testsuite/tests/ghci/scripts/T15743b.stdout b/testsuite/tests/ghci/scripts/T15743b.stdout
new file mode 100644
index 0000000000..03e593e5bd
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15743b.stdout
@@ -0,0 +1 @@
+F :: forall k k2. k -> k2 -> *
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 9765244f1e..6970eb3d7c 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -39,7 +39,7 @@
 
 <interactive>:55:41: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index bb3be803ff..97ae8bb26f 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -287,3 +287,4 @@ test('T15341', normal, ghci_script, ['T15341.script'])
 test('T15568', normal, ghci_script, ['T15568.script'])
 test('T15325', normal, ghci_script, ['T15325.script'])
 test('T15591', normal, ghci_script, ['T15591.script'])
+test('T15743b', normal, ghci_script, ['T15743b.script'])
diff --git a/testsuite/tests/indexed-types/should_fail/T14175.stderr b/testsuite/tests/indexed-types/should_fail/T14175.stderr
index dbadbe1f46..e177036e9e 100644
--- a/testsuite/tests/indexed-types/should_fail/T14175.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14175.stderr
@@ -3,3 +3,4 @@ T14175.hs:7:42: error:
     • Expecting one more argument to ‘k’
       Expected a type, but ‘k’ has kind ‘j -> *’
     • In the kind ‘k’
+      In the type family declaration for ‘PComp’
diff --git a/testsuite/tests/patsyn/should_compile/T14394.stdout b/testsuite/tests/patsyn/should_compile/T14394.stdout
index 557b8f4a74..f59f62cb78 100644
--- a/testsuite/tests/patsyn/should_compile/T14394.stdout
+++ b/testsuite/tests/patsyn/should_compile/T14394.stdout
@@ -1,7 +1,7 @@
 pattern Foo :: () => (b ~ a) => a :~~: b
   	-- Defined at <interactive>:5:1
 pattern Bar
-  :: forall k2 k1 (a :: k1) (b :: k2).
+  :: forall k1 k2 (a :: k1) (b :: k2).
      () =>
      (k2 ~ k1, b ~~ a) =>
      a :~~: b
diff --git a/testsuite/tests/patsyn/should_fail/T14552.hs b/testsuite/tests/patsyn/should_compile/T14552.hs
index a4a7493530..a4a7493530 100644
--- a/testsuite/tests/patsyn/should_fail/T14552.hs
+++ b/testsuite/tests/patsyn/should_compile/T14552.hs
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 19c9eaafae..54775a80a2 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -75,3 +75,4 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])],
                multimod_compile, ['T14058', '-v0'])
 test('T14326', normal, compile, [''])
 test('T14394', normal, ghci_script, ['T14394.script'])
+test('T14552', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
deleted file mode 100644
index 1723b325fa..0000000000
--- a/testsuite/tests/patsyn/should_fail/T14552.stderr
+++ /dev/null
@@ -1,9 +0,0 @@
-
-T14552.hs:22:9: error:
-    • Universal type variable ‘aa’ has existentially bound kind:
-        aa :: k
-      Existentially-bound variables:
-        k :: *
-        w :: k --> *
-      Probable fix: give the pattern synonym a type signature
-    • In the declaration for pattern synonym ‘FOO’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 099e9059d9..7cdef908a6 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -41,7 +41,6 @@ test('T14112', normal, compile_fail, [''])
 test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
 test('T14498', normal, compile_fail, [''])
-test('T14552', normal, compile_fail, [''])
 test('T14507', normal, compile_fail, ['-dsuppress-uniques'])
 test('T15289', normal, compile_fail, [''])
 test('T15685', normal, compile_fail, [''])
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
diff --git a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
index 54a32adafd..f5c06a654a 100644
--- a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
+++ b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
@@ -1,4 +1,14 @@
 
+ExplicitForAllRules1.hs:45:11: warning:
+    Forall'd type variable ‘k’ is not bound in RULE lhs
+      Orig bndrs: [k, a, b, x]
+      Orig lhs: id @ a x
+      optimised lhs: id @ a x
+    Forall'd type variable ‘b’ is not bound in RULE lhs
+      Orig bndrs: [k, a, b, x]
+      Orig lhs: id @ a x
+      optimised lhs: id @ a x
+
 ExplicitForAllRules1.hs:45:31: warning: [-Wunused-foralls (in -Wextra)]
     Unused quantified type variable ‘b’
     in the rule "example7"
diff --git a/testsuite/tests/typecheck/should_fail/T14350.stderr b/testsuite/tests/typecheck/should_fail/T14350.stderr
index cbf67b405f..eb80d3ec80 100644
--- a/testsuite/tests/typecheck/should_fail/T14350.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14350.stderr
@@ -1,6 +1,6 @@
 
 T14350.hs:59:15: error:
-    • Couldn't match expected type ‘Proxy a2
+    • Couldn't match expected type ‘Proxy a1
                                     -> Apply (Apply c 'Proxy) (Apply g 'Proxy)’
                   with actual type ‘Sing (f @@ t0)’
     • The function ‘applySing’ is applied to three arguments,
@@ -8,11 +8,11 @@ T14350.hs:59:15: error:
       In the expression: applySing f Proxy Proxy
       In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
     • Relevant bindings include
-        x :: Sing x3 (bound at T14350.hs:59:11)
+        x :: Sing x (bound at T14350.hs:59:11)
         g :: Sing g (bound at T14350.hs:59:9)
         f :: Sing f (bound at T14350.hs:59:7)
         dcomp :: Sing f
-                 -> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
+                 -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
           (bound at T14350.hs:59:1)
 
 T14350.hs:59:27: error:
@@ -22,9 +22,9 @@ T14350.hs:59:27: error:
       In the expression: applySing f Proxy Proxy
       In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
     • Relevant bindings include
-        x :: Sing x3 (bound at T14350.hs:59:11)
+        x :: Sing x (bound at T14350.hs:59:11)
         g :: Sing g (bound at T14350.hs:59:9)
         f :: Sing f (bound at T14350.hs:59:7)
         dcomp :: Sing f
-                 -> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
+                 -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
           (bound at T14350.hs:59:1)
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 0265250dbe..7f7dadd499 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -59,7 +59,7 @@ T6018fail.hs:53:15: error:
 
 T6018fail.hs:61:10: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVarsF '[] = '[] -- Defined at T6018fail.hs:61:10
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index 9914842013..e90dce0620 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error:
 
 T6018failclosed.hs:25:5: error:
     • Type family equation violates injectivity annotation.
-      Type and kind variables ‘k2’, ‘b’
+      Type and kind variables ‘k1’, ‘b’
       cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
-        forall k1 k2 (b :: k2) (c :: k1).
+        forall k1 k2 (b :: k1) (c :: k2).
           JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
     • In the equations for closed type family ‘JClosed’
       In the type family declaration for ‘JClosed’
diff --git a/testsuite/tests/typecheck/should_fail/T7892.stderr b/testsuite/tests/typecheck/should_fail/T7892.stderr
index d6120f936c..fa332c745e 100644
--- a/testsuite/tests/typecheck/should_fail/T7892.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7892.stderr
@@ -1,2 +1,4 @@
 
-T7892.hs:5:4: error: Expected kind ‘* -> *’, but ‘f’ has kind ‘*’
+T7892.hs:5:4: error:
+    • Expected kind ‘* -> *’, but ‘f’ has kind ‘*’
+    • In the associated type family declaration for ‘F’