Standalone kind signatures (#16794)wip/top-level-kind-signatures

Implements GHC Proposal #54: .../ghc-proposals/blob/master/proposals/0054-kind-signatures.rst

With this patch, a type constructor can now be given an explicit
standalone kind signature:

  {-# LANGUAGE StandaloneKindSignatures #-}
  type Functor :: (Type -> Type) -> Constraint
  class Functor f where
    fmap :: (a -> b) -> f a -> f b

This is a replacement for CUSKs (complete user-specified
kind signatures), which are now scheduled for deprecation.

User-facing changes
-------------------

* A new extension flag has been added, -XStandaloneKindSignatures, which
  implies -XNoCUSKs.

* There is a new syntactic construct, a standalone kind signature:

    type <name> :: <kind>

  Declarations of data types, classes, data families, type families, and
  type synonyms may be accompanied by a standalone kind signature.

* A standalone kind signature enables polymorphic recursion in types,
  just like a function type signature enables polymorphic recursion in
  terms. This obviates the need for CUSKs.

* TemplateHaskell AST has been extended with 'KiSigD' to represent
  standalone kind signatures.

* GHCi :info command now prints the kind signature of type constructors:

    ghci> :info Functor
    type Functor :: (Type -> Type) -> Constraint
    ...

Limitations
-----------

* 'forall'-bound type variables of a standalone kind signature do not
  scope over the declaration body, even if the -XScopedTypeVariables is
  enabled. See #16635 and #16734.

* Wildcards are not allowed in standalone kind signatures, as partial
  signatures do not allow for polymorphic recursion.

* Associated types may not be given an explicit standalone kind
  signature. Instead, they are assumed to have a CUSK if the parent class
  has a standalone kind signature and regardless of the -XCUSKs flag.

* Standalone kind signatures do not support multiple names at the moment:

    type T1, T2 :: Type -> Type   -- rejected
    type T1 = Maybe
    type T2 = Either String

  See #16754.

* Creative use of equality constraints in standalone kind signatures may
  lead to GHC panics:

    type C :: forall (a :: Type) -> a ~ Int => Constraint
    class C a where
      f :: C a => a -> Int

  See #16758.

Implementation notes
--------------------

* The heart of this patch is the 'kcDeclHeader' function, which is used to
  kind-check a declaration header against its standalone kind signature.
  It does so in two rounds:

    1. check user-written binders
    2. instantiate invisible binders a la 'checkExpectedKind'

* 'kcTyClGroup' now partitions declarations into declarations with a
  standalone kind signature or a CUSK (kinded_decls) and declarations
  without either (kindless_decls):

    * 'kinded_decls' are kind-checked with 'checkInitialKinds'
    * 'kindless_decls' are kind-checked with 'getInitialKinds'

* DerivInfo has been extended with a new field:

    di_scoped_tvs :: ![(Name,TyVar)]

  These variables must be added to the context in case the deriving clause
  references tcTyConScopedTyVars. See #16731.

7 files changed, 21 insertions, 13 deletions

diff --git a/testsuite/tests/typecheck/should_fail/T12035.stderr b/testsuite/tests/typecheck/should_fail/T12035.stderr
index c6113ea207..375b94c95a 100644
--- a/testsuite/tests/typecheck/should_fail/T12035.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12035.stderr
@@ -2,5 +2,7 @@
 T12035.hs-boot:2:1: error:
     Type constructor ‘T’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type T = Bool
-    Boot file:   data T
+    Main module: type T :: *
+                 type T = Bool
+    Boot file:   type T :: *
+                 data T
diff --git a/testsuite/tests/typecheck/should_fail/T12035j.stderr b/testsuite/tests/typecheck/should_fail/T12035j.stderr
index c6113ea207..375b94c95a 100644
--- a/testsuite/tests/typecheck/should_fail/T12035j.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12035j.stderr
@@ -2,5 +2,7 @@
 T12035.hs-boot:2:1: error:
     Type constructor ‘T’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type T = Bool
-    Boot file:   data T
+    Main module: type T :: *
+                 type T = Bool
+    Boot file:   type T :: *
+                 data T
diff --git a/testsuite/tests/typecheck/should_fail/T12042.stderr b/testsuite/tests/typecheck/should_fail/T12042.stderr
index 3266a1fe11..ae3cf33ea7 100644
--- a/testsuite/tests/typecheck/should_fail/T12042.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12042.stderr
@@ -5,5 +5,7 @@
 T12042.hs-boot:2:1: error:
     Type constructor ‘S’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type S = R
-    Boot file:   data S
+    Main module: type S :: *
+                 type S = R
+    Boot file:   type S :: *
+                 data S
diff --git a/testsuite/tests/typecheck/should_fail/T3468.stderr b/testsuite/tests/typecheck/should_fail/T3468.stderr
index 0a0fec223b..c8aa7622f8 100644
--- a/testsuite/tests/typecheck/should_fail/T3468.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3468.stderr
@@ -3,6 +3,8 @@ T3468.hs-boot:3:1: error:
     Type constructor ‘Tool’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role Tool phantom
+                 type Tool :: * -> *
                  data Tool d = forall a r. F a
-    Boot file:   data Tool
+    Boot file:   type Tool :: *
+                 data Tool
     The types have different kinds
diff --git a/testsuite/tests/typecheck/should_fail/T9201.stderr b/testsuite/tests/typecheck/should_fail/T9201.stderr
index 28f2f1d391..5e8f0173c5 100644
--- a/testsuite/tests/typecheck/should_fail/T9201.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9201.stderr
@@ -3,5 +3,4 @@ T9201.hs:6:17: error:
     • Expected kind ‘x’, but ‘a’ has kind ‘y’
     • In the first argument of ‘f’, namely ‘a’
       In the second argument of ‘d’, namely ‘(f a)’
-      In the type signature:
-        ret :: d a (f a)
+      In the type signature: ret :: d a (f a)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
index 13c9836c43..c868a1321e 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
@@ -1,4 +1,5 @@
-UnliftedNewtypesFamilyKindFail1.hs:11:31:
-     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
-     In the kind ‘5’
+
+UnliftedNewtypesFamilyKindFail1.hs:11:31: error:
+    • Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+    • In the kind ‘5’
       In the data family declaration for ‘DF’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail210.stderr b/testsuite/tests/typecheck/should_fail/tcfail210.stderr
index 9df9b7ef8f..819a9524fb 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail210.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail210.stderr
@@ -1,3 +1,3 @@
 
-tcfail210.hs:4:31:
+tcfail210.hs:4:31: error:
     Not in scope: type constructor or class ‘Constraint’