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.

1 files changed, 46 insertions, 36 deletions

diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index a30879c316..388681ed63 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -1,9 +1,10 @@
-type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol)
-                                      (b :: GHC.Types.Symbol)
-            :: GHC.Types.Symbol
-type family GHC.TypeLits.CmpSymbol (a :: GHC.Types.Symbol)
-                                   (b :: GHC.Types.Symbol)
-            :: Ordering
+type GHC.TypeLits.AppendSymbol :: GHC.Types.Symbol
+                                  -> GHC.Types.Symbol -> GHC.Types.Symbol
+type family GHC.TypeLits.AppendSymbol a b
+type GHC.TypeLits.CmpSymbol :: GHC.Types.Symbol
+                               -> GHC.Types.Symbol -> Ordering
+type family GHC.TypeLits.CmpSymbol a b
+type GHC.TypeLits.ErrorMessage :: *
 data GHC.TypeLits.ErrorMessage
   = GHC.TypeLits.Text GHC.Types.Symbol
   | forall t. GHC.TypeLits.ShowType t
@@ -13,15 +14,18 @@ data GHC.TypeLits.ErrorMessage
   | GHC.TypeLits.ErrorMessage
     GHC.TypeLits.:$$:
     GHC.TypeLits.ErrorMessage
-class GHC.TypeLits.KnownSymbol (n :: GHC.Types.Symbol) where
+type GHC.TypeLits.KnownSymbol :: GHC.Types.Symbol -> Constraint
+class GHC.TypeLits.KnownSymbol n where
   GHC.TypeLits.symbolSing :: GHC.TypeLits.SSymbol n
   {-# MINIMAL symbolSing #-}
+type GHC.TypeLits.SomeSymbol :: *
 data GHC.TypeLits.SomeSymbol
   = forall (n :: GHC.Types.Symbol).
     GHC.TypeLits.KnownSymbol n =>
     GHC.TypeLits.SomeSymbol (Data.Proxy.Proxy n)
-type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
-            :: b where
+type GHC.TypeLits.TypeError :: forall b.
+                               GHC.TypeLits.ErrorMessage -> b
+type family GHC.TypeLits.TypeError a where
 GHC.TypeLits.natVal ::
   GHC.TypeNats.KnownNat n => proxy n -> Integer
 GHC.TypeLits.natVal' ::
@@ -36,42 +40,48 @@ GHC.TypeLits.symbolVal ::
   GHC.TypeLits.KnownSymbol n => proxy n -> String
 GHC.TypeLits.symbolVal' ::
   GHC.TypeLits.KnownSymbol n => GHC.Prim.Proxy# n -> String
-type family (GHC.TypeNats.*) (a :: GHC.Types.Nat)
-                             (b :: GHC.Types.Nat)
-            :: GHC.Types.Nat
-type family (GHC.TypeNats.+) (a :: GHC.Types.Nat)
-                             (b :: GHC.Types.Nat)
-            :: GHC.Types.Nat
-type family (GHC.TypeNats.-) (a :: GHC.Types.Nat)
-                             (b :: GHC.Types.Nat)
-            :: GHC.Types.Nat
-type (GHC.TypeNats.<=) (x :: GHC.Types.Nat) (y :: GHC.Types.Nat) =
+type (GHC.TypeNats.*) :: GHC.Types.Nat
+                         -> GHC.Types.Nat -> GHC.Types.Nat
+type family (GHC.TypeNats.*) a b
+type (GHC.TypeNats.+) :: GHC.Types.Nat
+                         -> GHC.Types.Nat -> GHC.Types.Nat
+type family (GHC.TypeNats.+) a b
+type (GHC.TypeNats.-) :: GHC.Types.Nat
+                         -> GHC.Types.Nat -> GHC.Types.Nat
+type family (GHC.TypeNats.-) a b
+type (GHC.TypeNats.<=) :: GHC.Types.Nat
+                          -> GHC.Types.Nat -> Constraint
+type (GHC.TypeNats.<=) x y =
   (x GHC.TypeNats.<=? y) ~ 'True :: Constraint
-type family (GHC.TypeNats.<=?) (a :: GHC.Types.Nat)
-                               (b :: GHC.Types.Nat)
-            :: Bool
-type family GHC.TypeNats.CmpNat (a :: GHC.Types.Nat)
-                                (b :: GHC.Types.Nat)
-            :: Ordering
-type family GHC.TypeNats.Div (a :: GHC.Types.Nat)
-                             (b :: GHC.Types.Nat)
-            :: GHC.Types.Nat
-class GHC.TypeNats.KnownNat (n :: GHC.Types.Nat) where
+type (GHC.TypeNats.<=?) :: GHC.Types.Nat -> GHC.Types.Nat -> Bool
+type family (GHC.TypeNats.<=?) a b
+type GHC.TypeNats.CmpNat :: GHC.Types.Nat
+                            -> GHC.Types.Nat -> Ordering
+type family GHC.TypeNats.CmpNat a b
+type GHC.TypeNats.Div :: GHC.Types.Nat
+                         -> GHC.Types.Nat -> GHC.Types.Nat
+type family GHC.TypeNats.Div a b
+type GHC.TypeNats.KnownNat :: GHC.Types.Nat -> Constraint
+class GHC.TypeNats.KnownNat n where
   GHC.TypeNats.natSing :: GHC.TypeNats.SNat n
   {-# MINIMAL natSing #-}
-type family GHC.TypeNats.Log2 (a :: GHC.Types.Nat) :: GHC.Types.Nat
-type family GHC.TypeNats.Mod (a :: GHC.Types.Nat)
-                             (b :: GHC.Types.Nat)
-            :: GHC.Types.Nat
+type GHC.TypeNats.Log2 :: GHC.Types.Nat -> GHC.Types.Nat
+type family GHC.TypeNats.Log2 a
+type GHC.TypeNats.Mod :: GHC.Types.Nat
+                         -> GHC.Types.Nat -> GHC.Types.Nat
+type family GHC.TypeNats.Mod a b
+type GHC.Types.Nat :: *
 data GHC.Types.Nat
+type GHC.TypeNats.SomeNat :: *
 data GHC.TypeNats.SomeNat
   = forall (n :: GHC.Types.Nat).
     GHC.TypeNats.KnownNat n =>
     GHC.TypeNats.SomeNat (Data.Proxy.Proxy n)
+type GHC.Types.Symbol :: *
 data GHC.Types.Symbol
-type family (GHC.TypeNats.^) (a :: GHC.Types.Nat)
-                             (b :: GHC.Types.Nat)
-            :: GHC.Types.Nat
+type (GHC.TypeNats.^) :: GHC.Types.Nat
+                         -> GHC.Types.Nat -> GHC.Types.Nat
+type family (GHC.TypeNats.^) a b
 GHC.TypeNats.sameNat ::
   (GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
   Data.Proxy.Proxy a