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.

5 files changed, 9 insertions, 15 deletions

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)