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.

48 files changed, 89 insertions, 113 deletions

diff --git a/testsuite/tests/codeGen/should_fail/T13233.hs b/testsuite/tests/codeGen/should_fail/T13233.hs
index 1facb77914..f24fc03bfb 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.hs
+++ b/testsuite/tests/codeGen/should_fail/T13233.hs
@@ -8,9 +8,9 @@ module Bug where
 import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
 
 class Foo (a :: TYPE rep) where
-  bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
+  bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
 
-baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
+baz :: forall rep (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
 baz = bar (#,#)
 
 obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
diff --git a/testsuite/tests/dependent/should_compile/T15264.stderr b/testsuite/tests/dependent/should_compile/T15264.stderr
deleted file mode 100644
index 222d686513..0000000000
--- a/testsuite/tests/dependent/should_compile/T15264.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-T15264.hs:8:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
-    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k’
-    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
-    Suggested fix: add ‘forall k.’
-
-T15264.hs:11:22: warning: [-Wimplicit-kind-vars (in -Wcompat)]
-    An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k1’, ‘k2’
-    Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future.
-    Suggested fix: add ‘forall k1 k2.’
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index fa39c9a69a..ca5f436174 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -48,7 +48,6 @@ test('T14066a', normal, compile, [''])
 test('T14749', normal, compile, [''])
 test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
-test('T15264', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
 test('T15419', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
index b12adbd8e3..e33fdf110e 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -10,5 +10,5 @@ data SameKind :: k -> k -> *
 foo :: forall a k (b :: k). SameKind a b
 foo = undefined
 
-bar :: forall a (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
+bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
 bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 55a484910c..a8c4b689ae 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -5,9 +5,9 @@ BadTelescope2.hs:10:8: error:
         k (a :: k) (b :: k)
     • In the type signature: foo :: forall a k (b :: k). SameKind a b
 
-BadTelescope2.hs:13:70: error:
-    • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+BadTelescope2.hs:13:81: error:
+    • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
     • In the second argument of ‘SameKind’, namely ‘d’
       In the type signature:
-        bar :: forall a (c :: Proxy b) (d :: Proxy a).
+        bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
                Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_compile/T15264.hs b/testsuite/tests/dependent/should_fail/T15264.hs
index f3dec42564..394c53a013 100644
--- a/testsuite/tests/dependent/should_compile/T15264.hs
+++ b/testsuite/tests/dependent/should_fail/T15264.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE ExplicitForAll, PolyKinds #-}
-{-# OPTIONS -Wcompat -Wno-error=implicit-kind-vars #-}
 
 module T15264 where
 
diff --git a/testsuite/tests/dependent/should_fail/T15264.stderr b/testsuite/tests/dependent/should_fail/T15264.stderr
new file mode 100644
index 0000000000..6d5f597823
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15264.stderr
@@ -0,0 +1,6 @@
+
+T15264.hs:7:22: error: Not in scope: type variable ‘k’
+
+T15264.hs:10:22: error: Not in scope: type variable ‘k1’
+
+T15264.hs:10:32: error: Not in scope: type variable ‘k2’
diff --git a/testsuite/tests/dependent/should_fail/T15825.hs b/testsuite/tests/dependent/should_fail/T15825.hs
index 01227a8696..651525b21d 100644
--- a/testsuite/tests/dependent/should_fail/T15825.hs
+++ b/testsuite/tests/dependent/should_fail/T15825.hs
@@ -10,5 +10,5 @@ module T15825 where
 
 type C k = (forall (x::k). *)
 
-class                       X (a :: *)
-instance forall (a :: C k). X (a :: *)
+class                         X (a :: *)
+instance forall k (a :: C k). X (a :: *)
diff --git a/testsuite/tests/dependent/should_fail/T15825.stderr b/testsuite/tests/dependent/should_fail/T15825.stderr
index d64cab0494..97582ba952 100644
--- a/testsuite/tests/dependent/should_fail/T15825.stderr
+++ b/testsuite/tests/dependent/should_fail/T15825.stderr
@@ -1,5 +1,5 @@
 
-T15825.hs:14:29: error:
+T15825.hs:14:31: error:
     • Illegal type synonym family application ‘GHC.Types.Any
                                                  @k’ in instance:
         X (a @(GHC.Types.Any @k))
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index f1272200ba..4b258cc065 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -39,3 +39,4 @@ test('T15743c', normal, compile_fail, [''])
 test('T15743d', normal, compile_fail, [''])
 test('T15825', normal, compile_fail, [''])
 test('T15859', normal, compile_fail, [''])
+test('T15264', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr
index b4759714c2..8ec10322c8 100644
--- a/testsuite/tests/ghci/scripts/T7873.stderr
+++ b/testsuite/tests/ghci/scripts/T7873.stderr
@@ -1,8 +1,2 @@
 
-<interactive>:2:1: error:
-    • Kind variable ‘k’ is implicitly bound in data type
-      ‘D1’, but does not appear as the kind of any
-      of its type variables. Perhaps you meant
-      to bind it explicitly somewhere?
-      Type variables with inferred kinds: (k :: *)
-    • In the data type declaration for ‘D1’
+<interactive>:2:32: error: Not in scope: type variable ‘k’
diff --git a/testsuite/tests/ghci/scripts/T9293.stdout b/testsuite/tests/ghci/scripts/T9293.stdout
index 6d140bc9f7..87b950654d 100644
--- a/testsuite/tests/ghci/scripts/T9293.stdout
+++ b/testsuite/tests/ghci/scripts/T9293.stdout
@@ -13,7 +13,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -37,7 +36,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -60,7 +58,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -85,7 +82,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
diff --git a/testsuite/tests/ghci/scripts/ghci024.stdout b/testsuite/tests/ghci/scripts/ghci024.stdout
index 863184ad49..138da30075 100644
--- a/testsuite/tests/ghci/scripts/ghci024.stdout
+++ b/testsuite/tests/ghci/scripts/ghci024.stdout
@@ -14,7 +14,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
diff --git a/testsuite/tests/ghci/scripts/ghci057.stdout b/testsuite/tests/ghci/scripts/ghci057.stdout
index 6d140bc9f7..87b950654d 100644
--- a/testsuite/tests/ghci/scripts/ghci057.stdout
+++ b/testsuite/tests/ghci/scripts/ghci057.stdout
@@ -13,7 +13,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -37,7 +36,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -60,7 +58,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
@@ -85,7 +82,6 @@ other dynamic, non-language, flag settings:
   -fimplicit-import-qualified
   -fshow-warning-groups
 warning settings:
-  -Wimplicit-kind-vars
   -Wmissing-monadfail-instances
   -Wsemigroup
   -Wnoncanonical-monoid-instances
diff --git a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
index 067127cf8a..c16e4e0156 100644
--- a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
+++ b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs
@@ -26,6 +26,6 @@ type family H a b where
 -- More tests
 
 type family D a b where
-  forall (a :: Type -> Type) (b :: a Int) (c :: k). D (Proxy b) (Proxy c) = ()
+  forall (a :: Type -> Type) (b :: a Int) k (c :: k). D (Proxy b) (Proxy c) = ()
   forall (a :: Bool) (b :: Proxy a). D (Proxy b) () = Int
   forall (a :: Type). D a a = Maybe a
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index d6cfe26b40..9a0c6b8e6e 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -287,8 +287,8 @@
         (NoExt)
         (DataFamInstDecl
          (HsIB
-          [{Name: k}
-          ,{Name: a}]
+          [{Name: a}
+          ,{Name: k}]
           (FamEqn
            (NoExt)
            ({ DumpRenamedAst.hs:18:18-20 }
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
index 1563a2eb23..d07ce73230 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr
@@ -27,7 +27,7 @@ T15039a.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict (a ~~ b) -> ()
+                 ex3 :: forall a k (b :: k). Dict (a ~~ b) -> ()
                at T15039a.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
index c28b94879b..8f9c2c8a45 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr
@@ -28,7 +28,7 @@ T15039b.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         standing for ‘Dict ((a :: *) ~~ (b :: k))’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
+                 ex3 :: forall a k (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
                at T15039b.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
index 40c126f061..261a82e91a 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr
@@ -27,7 +27,7 @@ T15039c.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict (a ~~ b) -> ()
+                 ex3 :: forall a k (b :: k). Dict (a ~~ b) -> ()
                at T15039c.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
index cca94416b8..8548356001 100644
--- a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr
@@ -29,7 +29,7 @@ T15039d.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
         standing for ‘Dict ((a :: *) ~~ (b :: k))’
       Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by
                the type signature for:
-                 ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
+                 ex3 :: forall a k (b :: k). Dict ((a :: *) ~~ (b :: k)) -> ()
                at T15039d.hs:24:1-43
     • In a pattern type signature: _
       In the pattern: Dict :: _
diff --git a/testsuite/tests/partial-sigs/should_compile/T16334.hs b/testsuite/tests/partial-sigs/should_compile/T16334.hs
new file mode 100644
index 0000000000..c01ef5cc16
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16334.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE NamedWildCards, PartialTypeSignatures, PolyKinds, NoStarIsType #-}
+
+module T16334 where
+
+k :: (Int :: _t)
+k = 42
diff --git a/testsuite/tests/partial-sigs/should_compile/T16334.stderr b/testsuite/tests/partial-sigs/should_compile/T16334.stderr
new file mode 100644
index 0000000000..83429e0d33
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16334.stderr
@@ -0,0 +1,4 @@
+
+T16334.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_t’ standing for ‘Type’
+    • In the type signature: k :: (Int :: _t)
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index d6eaa7727a..3e62552a20 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -89,3 +89,4 @@ test('T15039b', normal, compile, ['-fprint-explicit-kinds'])
 test('T15039c', normal, compile, ['-fprint-equality-relations'])
 test('T15039d', normal, compile,
                 ['-fprint-explicit-kinds -fprint-equality-relations'])
+test('T16334', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T14498.hs b/testsuite/tests/patsyn/should_compile/T14498.hs
index 0744310aee..b7f7db4d8a 100644
--- a/testsuite/tests/patsyn/should_fail/T14498.hs
+++ b/testsuite/tests/patsyn/should_compile/T14498.hs
@@ -23,9 +23,9 @@ type SN = (TypeRep :: N -> Type)
 pattern SO = (Typeable :: TypeRep (O::N))
 
 pattern SS ::
-     forall (t :: k').
+     forall k' (t :: k').
      ()
-  => forall (a :: kk -> k') (n :: kk).
+  => forall kk (a :: kk -> k') (n :: kk).
      (t ~ a n)
   =>
   TypeRep n -> TypeRep t
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 54775a80a2..6eb9e2db8a 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -76,3 +76,4 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])],
 test('T14326', normal, compile, [''])
 test('T14394', normal, ghci_script, ['T14394.script'])
 test('T14552', normal, compile, [''])
+test('T14498', normal, compile, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T14507.hs b/testsuite/tests/patsyn/should_fail/T14507.hs
index b36425ced6..9599b73c77 100644
--- a/testsuite/tests/patsyn/should_fail/T14507.hs
+++ b/testsuite/tests/patsyn/should_fail/T14507.hs
@@ -13,7 +13,7 @@ foo rep = error "urk"
 type family SING :: k -> Type where
   SING = (TypeRep :: Bool -> Type)
 
-pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
+pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
 pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
                            , tr :: TypeRep (a::Bool)))
 
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 7cdef908a6..5431e8b76a 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -40,7 +40,6 @@ test('T13470', normal, compile_fail, [''])
 test('T14112', normal, compile_fail, [''])
 test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
-test('T14498', 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/BadKindVar.hs b/testsuite/tests/polykinds/BadKindVar.hs
index c24657f3d2..9275d453c5 100644
--- a/testsuite/tests/polykinds/BadKindVar.hs
+++ b/testsuite/tests/polykinds/BadKindVar.hs
@@ -5,5 +5,5 @@ module Foo where
 import Data.Proxy
 
 -- Should be illegal without PolyKinds
-f :: forall (a :: k). Proxy a
+f :: forall k (a :: k). Proxy a
 f = f
diff --git a/testsuite/tests/polykinds/BadKindVar.stderr b/testsuite/tests/polykinds/BadKindVar.stderr
index beeed2b3c8..3312350602 100644
--- a/testsuite/tests/polykinds/BadKindVar.stderr
+++ b/testsuite/tests/polykinds/BadKindVar.stderr
@@ -1,5 +1,5 @@
 
-BadKindVar.hs:8:19: error:
+BadKindVar.hs:8:21: error:
     Unexpected kind variable ‘k’
     Perhaps you intended to use PolyKinds
     In the type signature for ‘f’
diff --git a/testsuite/tests/polykinds/KindVarOrder.script b/testsuite/tests/polykinds/KindVarOrder.script
new file mode 100644
index 0000000000..c4b4165dcf
--- /dev/null
+++ b/testsuite/tests/polykinds/KindVarOrder.script
@@ -0,0 +1,9 @@
+:set -XPolyKinds -XDataKinds
+import Data.Kind (Type)
+data Proxy (a :: k)
+f :: Proxy (a :: k) -> Proxy (b :: j) -> (); f = f
+g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> (); g = g
+h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> (); h = h
+:t +v f
+:t +v g
+:t +v h
diff --git a/testsuite/tests/polykinds/KindVarOrder.stdout b/testsuite/tests/polykinds/KindVarOrder.stdout
new file mode 100644
index 0000000000..66a950dc23
--- /dev/null
+++ b/testsuite/tests/polykinds/KindVarOrder.stdout
@@ -0,0 +1,5 @@
+f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -> ()
+g :: forall j (b :: j) k (a :: Proxy Proxy).
+     Proxy b -> Proxy a -> ()
+h :: forall j k (a :: (j, k)) (b :: Proxy a).
+     Proxy a -> Proxy b -> ()
diff --git a/testsuite/tests/polykinds/T10503.hs b/testsuite/tests/polykinds/T10503.hs
index 2cc1ee717e..2b9900652f 100644
--- a/testsuite/tests/polykinds/T10503.hs
+++ b/testsuite/tests/polykinds/T10503.hs
@@ -5,5 +5,5 @@ data Proxy p = Proxy
 
 data KProxy (a :: *) = KProxy
 
-h :: forall r . (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r
+h :: forall k r . (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r
 h = undefined
diff --git a/testsuite/tests/polykinds/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr
index 9fb87e9be7..a47a872253 100644
--- a/testsuite/tests/polykinds/T10503.stderr
+++ b/testsuite/tests/polykinds/T10503.stderr
@@ -4,14 +4,14 @@ T10503.hs:8:6: error:
       from the context: Proxy 'KProxy ~ Proxy 'KProxy
         bound by a type expected by the context:
                    (Proxy 'KProxy ~ Proxy 'KProxy) => r
-        at T10503.hs:8:6-85
+        at T10503.hs:8:6-87
       ‘k’ is a rigid type variable bound by
         the type signature for:
           h :: forall k r. ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r
-        at T10503.hs:8:6-85
+        at T10503.hs:8:6-87
     • In the ambiguity check for ‘h’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
-        h :: forall r.
+        h :: forall k r.
              (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r)
              -> r
diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr
index 2df92c34da..ba07f3cda1 100644
--- a/testsuite/tests/polykinds/T13985.stderr
+++ b/testsuite/tests/polykinds/T13985.stderr
@@ -1,28 +1,10 @@
 
-T13985.hs:13:41: error:
-    • Type variable ‘k’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the data instance declaration for ‘Fam’
+T13985.hs:13:41: error: Not in scope: type variable ‘k’
 
-T13985.hs:16:43: error:
-    • Type variable ‘a’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the type instance declaration for ‘T’
+T13985.hs:16:43: error: Not in scope: type variable ‘a’
 
-T13985.hs:23:26: error:
-    • Type variable ‘k’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the data instance declaration for ‘CD’
-      In the instance declaration for ‘C Type’
+T13985.hs:23:26: error: Not in scope: type variable ‘k’
 
-T13985.hs:24:37: error:
-    • Type variable ‘a’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the type instance declaration for ‘CT’
-      In the instance declaration for ‘C Type’
+T13985.hs:24:37: error: Not in scope: type variable ‘a’
 
-T13985.hs:28:39: error:
-    • Type variable ‘x’ is mentioned in the RHS,
-        but not bound on the LHS of the family instance
-    • In the default type instance declaration for ‘ZT’
-      In the class declaration for ‘Z’
+T13985.hs:28:39: error: Not in scope: type variable ‘x’
diff --git a/testsuite/tests/polykinds/T14561.hs b/testsuite/tests/polykinds/T14561.hs
index 7b1f17e08e..8c74ab4740 100644
--- a/testsuite/tests/polykinds/T14561.hs
+++ b/testsuite/tests/polykinds/T14561.hs
@@ -8,7 +8,7 @@ module T14561 where
 import GHC.Types
 import GHC.Prim
 
-badId :: forall (a :: TYPE r). a -> a
+badId :: forall r (a :: TYPE r). a -> a
 badId = unsafeCoerce#
 -- Un-saturated application of a levity-polymorphic
 -- function that must be eta-expanded
diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs
index bdc05dd6df..aefa12b59e 100644
--- a/testsuite/tests/polykinds/T14563.hs
+++ b/testsuite/tests/polykinds/T14563.hs
@@ -5,5 +5,5 @@ import GHC.Types (TYPE)
 import Data.Kind
 
 data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where
-  Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a.
+  Lan :: forall rep rep' xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a.
          (g xx -> a) -> h xx -> Lan g h a
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 43d81c5e1e..6e8384542f 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -23,13 +23,13 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:12: error:
-    • Couldn't match kind ‘k3’ with ‘Struct cls2’
-      ‘k3’ is a rigid type variable bound by
+    • Couldn't match kind ‘k4’ with ‘Struct cls2’
+      ‘k4’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
         cls0 :: Struct cls -> Constraint
-        cls1 :: k3 -> Constraint
+        cls1 :: k4 -> Constraint
     • In the expression: struct :: AStruct (Structured a cls)
       In the expression: case struct :: AStruct (Structured a cls) of
       In an equation for ‘i’:
@@ -38,12 +38,12 @@ T14846.hs:39:12: error:
         i :: Hom riki a a (bound at T14846.hs:39:3)
 
 T14846.hs:39:31: error:
-    • Couldn't match kind ‘k3’ with ‘Struct cls2’
-      ‘k3’ is a rigid type variable bound by
+    • Couldn't match kind ‘k4’ with ‘Struct cls2’
+      ‘k4’ is a rigid type variable bound by
         the instance declaration
         at T14846.hs:37:10-65
       When matching kinds
-        cls1 :: k3 -> Constraint
+        cls1 :: k4 -> Constraint
         cls0 :: Struct cls -> Constraint
       Expected kind ‘Struct cls0’,
         but ‘Structured a cls’ has kind ‘Struct cls1’
diff --git a/testsuite/tests/polykinds/T14887a.hs b/testsuite/tests/polykinds/T14887a.hs
index 2e5cf02212..4179862cad 100644
--- a/testsuite/tests/polykinds/T14887a.hs
+++ b/testsuite/tests/polykinds/T14887a.hs
@@ -1,16 +1,10 @@
 {-# LANGUAGE PartialTypeSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-implicit-kind-vars #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 module Bug where
 
 import Data.Proxy
 
-f1 :: forall (x :: a). Proxy (x :: _)
--- This one has an implicitly-quantified kind var 'a', which
--- we will stop accepting in the future, under the forall-or-nothing
--- rule.  Hence -Wno-implicit-kind-vars
-f1 = Proxy
-
 f2 :: forall a (x :: a). Proxy (x :: _)
 f2 = Proxy
diff --git a/testsuite/tests/polykinds/T8616.hs b/testsuite/tests/polykinds/T8616.hs
index 47e31bcc94..e8f4c682bf 100644
--- a/testsuite/tests/polykinds/T8616.hs
+++ b/testsuite/tests/polykinds/T8616.hs
@@ -4,11 +4,11 @@ module T8616 where
 import Data.Proxy
 import GHC.Exts
 
-withSomeSing :: forall (kproxy :: k). Proxy kproxy
+withSomeSing :: forall k (kproxy :: k). Proxy kproxy
 withSomeSing = undefined :: (Any :: k)
   -- The 'k' is bought into scope by the type signature
   -- This is a type error, but should not crash GHC
 
-foo = (undefined :: Proxy (a :: k)) :: forall (a :: k). Proxy a
+foo = (undefined :: Proxy (a :: k)) :: forall k (a :: k). Proxy a
   -- Again, the 'k' is bought into scope by the type signature
-  -- No type error though
\ No newline at end of file
+  -- No type error though
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index f9e5132a34..4341b3051a 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -4,7 +4,7 @@ T8616.hs:8:16: error:
       ‘k’ is a rigid type variable bound by
         the type signature for:
           withSomeSing :: forall k (kproxy :: k). Proxy kproxy
-        at T8616.hs:7:1-50
+        at T8616.hs:7:1-52
       When matching types
         a0 :: *
         Any :: k
diff --git a/testsuite/tests/polykinds/T9144.hs b/testsuite/tests/polykinds/T9144.hs
index 0a9ef08afa..85e1b24dbe 100644
--- a/testsuite/tests/polykinds/T9144.hs
+++ b/testsuite/tests/polykinds/T9144.hs
@@ -8,7 +8,7 @@ import GHC.TypeLits
 data family Sing (a :: k)
 
 data SomeSing :: KProxy k -> * where
-  SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
+  SomeSing :: forall k (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k)
 
 class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where
   fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k)
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 8a885b39a5..1cfb2aa424 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -206,3 +206,4 @@ test('T14887a', normal, compile, [''])
 test('T14847', normal, compile, [''])
 test('T15795', normal, compile, [''])
 test('T15795a', normal, compile, [''])
+test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script'])
diff --git a/testsuite/tests/typecheck/should_compile/T13343.hs b/testsuite/tests/typecheck/should_compile/T13343.hs
index fcff9db1a4..2f3f120c72 100644
--- a/testsuite/tests/typecheck/should_compile/T13343.hs
+++ b/testsuite/tests/typecheck/should_compile/T13343.hs
@@ -4,6 +4,6 @@ module Bug where
 
 import GHC.Exts
 
-type Bad = forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1
+type Bad = (forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1) :: TYPE v
 
 -- should be accepted because GHC will generalize over v. Note v /= v1.
diff --git a/testsuite/tests/typecheck/should_fail/T12973.hs b/testsuite/tests/typecheck/should_fail/T12973.hs
index b0a33a8213..765e02f34b 100644
--- a/testsuite/tests/typecheck/should_fail/T12973.hs
+++ b/testsuite/tests/typecheck/should_fail/T12973.hs
@@ -9,7 +9,7 @@ class Num (a :: TYPE r) where
   (+) :: a -> a -> a
   fromInteger :: P.Integer -> a
 
-foo :: forall (a :: TYPE r). Num a => a
+foo :: forall r (a :: TYPE r). Num a => a
 foo = 3 + 4
 
 
diff --git a/testsuite/tests/typecheck/should_fail/T13983.stderr b/testsuite/tests/typecheck/should_fail/T13983.stderr
index d1b2fe067b..aba88bc9f2 100644
--- a/testsuite/tests/typecheck/should_fail/T13983.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13983.stderr
@@ -1,8 +1,2 @@
 
-T13983.hs:7:1: error:
-    • Kind variable ‘k’ is implicitly bound in type synonym
-      ‘Wat’, but does not appear as the kind of any
-      of its type variables. Perhaps you meant
-      to bind it explicitly somewhere?
-      Type variables with inferred kinds: (k :: *)
-    • In the type synonym declaration for ‘Wat’
+T13983.hs:7:25: error: Not in scope: type variable ‘k’
diff --git a/testsuite/tests/typecheck/should_fail/T15629.hs b/testsuite/tests/typecheck/should_fail/T15629.hs
index fdbba60ccc..6d1d0b8897 100644
--- a/testsuite/tests/typecheck/should_fail/T15629.hs
+++ b/testsuite/tests/typecheck/should_fail/T15629.hs
@@ -23,5 +23,5 @@ sg _ _ = Proxy
 f :: forall (x :: Type). Proxy x -> ()
 f _ = ()
   where
-    g :: forall ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+    g :: forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
     g = sg Proxy Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr
index ce77bb04a3..a0e0f42286 100644
--- a/testsuite/tests/typecheck/should_fail/T15629.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15629.stderr
@@ -1,12 +1,12 @@
 
-T15629.hs:26:35: error:
+T15629.hs:26:37: error:
     • Expected kind ‘x1 ~> F x1 ab1’,
         but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z’
     • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’
       In the first argument of ‘Proxy’, namely
         ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’
       In the type signature:
-        g :: forall ab.
+        g :: forall z ab.
              Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
 
 T15629.hs:27:9: error:
@@ -14,11 +14,11 @@ T15629.hs:27:9: error:
       ‘ab1’ is a rigid type variable bound by
         the type signature for:
           g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym)
-        at T15629.hs:26:5-82
+        at T15629.hs:26:5-84
       ‘z’ is a rigid type variable bound by
         the type signature for:
           g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym)
-        at T15629.hs:26:5-82
+        at T15629.hs:26:5-84
       When matching types
         f0 :: x ~> F x ab
         F1Sym :: TyFun x1 (F x1 z) -> *
@@ -31,7 +31,7 @@ T15629.hs:27:9: error:
             = ()
             where
                 g ::
-                  forall ab.
+                  forall z ab.
                   Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
                 g = sg Proxy Proxy
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/T15797.hs b/testsuite/tests/typecheck/should_fail/T15797.hs
index eadd8cb972..925674fecf 100644
--- a/testsuite/tests/typecheck/should_fail/T15797.hs
+++ b/testsuite/tests/typecheck/should_fail/T15797.hs
@@ -13,7 +13,7 @@ import Data.Kind
 
 class Ríki (obj :: Type) where
   type Obj :: obj -> Constraint
-  type Obj = Bæ @obj
+  type Obj = Bæ @k :: k -> Constraint
 
 class    Bæ    (a :: k)
 instance Bæ @k (a :: k)