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.

2 files changed, 211 insertions, 5 deletions

diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst
index e8316d7059..907f7e288b 100644
--- a/docs/users_guide/8.10.1-notes.rst
+++ b/docs/users_guide/8.10.1-notes.rst
@@ -46,6 +46,20 @@ Language
     type T = Just (Nothing :: Maybe a)         -- no longer accepted
     type T = Just Nothing :: Maybe (Maybe a)   -- still accepted
 
+- A new extension :extension:`StandaloneKindSignatures` allows one to explicitly
+  specify the kind of a type constructor, as proposed in `GHC proposal #54
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0054-kind-signatures.rst>`__: ::
+
+    type TypeRep :: forall k. k -> Type
+    data TypeRep a where
+      TyInt   :: TypeRep Int
+      TyMaybe :: TypeRep Maybe
+      TyApp   :: TypeRep a -> TypeRep b -> TypeRep (a b)
+
+  Analogous to function type signatures, a :ref:`standalone kind signature
+  <standalone-kind-signatures>` enables polymorphic recursion. This feature is
+  a replacement for :extension:`CUSKs`.
+
 - GHC now parses visible, dependent quantifiers (as proposed in
   `GHC proposal 35
   <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst>`__),
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 8ec105f3a0..de0aabbbbb 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7856,6 +7856,42 @@ using a parameter in the kind annotation: ::
 In this case the kind parameter ``k`` is actually an implicit parameter
 of the type family.
 
+At definition site, the arity determines what inputs can be matched on: ::
+
+    data PT (a :: Type)
+
+    type family F1 :: k -> Type
+    type instance F1 = PT
+      -- OK, 'k' can be matched on.
+
+    type family F0 :: forall k. k -> Type
+    type instance F0 = PT
+      -- Error:
+      --   • Expected kind ‘forall k. k -> Type’,
+      --       but ‘PT’ has kind ‘Type -> Type’
+      --   • In the type ‘PT’
+      --     In the type instance declaration for ‘F0’
+
+Both ``F1`` and ``F0`` have kind ``forall k. k -> Type``, but their arity
+differs.
+
+At use sites, the arity determines if the definition can be used in a
+higher-rank scenario: ::
+
+    type HRK (f :: forall k. k -> Type) = (f Int, f Maybe, f True)
+
+    type H1 = HRK F0  -- OK
+    type H2 = HRK F1
+      -- Error:
+      --   • Expected kind ‘forall k. k -> Type’,
+      --       but ‘F1’ has kind ‘k0 -> Type’
+      --   • In the first argument of ‘HRK’, namely ‘F1’
+      --     In the type ‘HRK F1’
+      --     In the type declaration for ‘H2’
+
+This is a consequence of the requirement that all applications of a type family
+must be fully saturated with respect to their arity.
+
 .. _type-instance-declarations:
 
 Type instance declarations
@@ -9148,6 +9184,9 @@ Complete user-supplied kind signatures and polymorphic recursion
 
     :since: 8.10.1
 
+NB! This is a legacy feature, see :extension:`StandaloneKindSignatures` for the
+modern replacement.
+
 Just as in type inference, kind inference for recursive types can only
 use *monomorphic* recursion. Consider this (contrived) example: ::
 
@@ -9261,11 +9300,164 @@ According to the rules above ``X`` has a CUSK. Yet, the kind of ``k`` is undeter
 It is thus quantified over, giving ``X`` the kind ``forall k1 (k :: k1). Proxy k -> Type``.
 
 The detection of CUSKs is enabled by the :extension:`CUSKs` flag, which is
-switched on by default. When :extension:`CUSKs` is switched off, there is
-currently no way to enable polymorphic recursion in types. In the future, the
-notion of a CUSK will be replaced by top-level kind signatures
-(`GHC Proposal #36 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0036-kind-signatures.rst>`__),
-then, after a transition period, this extension will be turned off by default, and eventually removed.
+switched on by default. This extension is scheduled for deprecation to be
+replaced with :extension:`StandaloneKindSignatures`.
+
+.. index::
+   single: standalone kind signature
+
+.. _standalone-kind-signatures:
+
+Standalone kind signatures and polymorphic recursion
+----------------------------------------------------
+
+.. extension:: StandaloneKindSignatures
+    :shortdesc: Allow the use of standalone kind signatures.
+
+    :implies: :extension:`NoCUSKs`
+    :since: 8.10.1
+
+Just as in type inference, kind inference for recursive types can only
+use *monomorphic* recursion. Consider this (contrived) example: ::
+
+    data T m a = MkT (m a) (T Maybe (m a))
+    -- GHC infers kind  T :: (Type -> Type) -> Type -> Type
+
+The recursive use of ``T`` forced the second argument to have kind
+``Type``. However, just as in type inference, you can achieve polymorphic
+recursion by giving a *standalone kind signature* for ``T``: ::
+
+    type T :: (k -> Type) -> k -> Type
+    data T m a = MkT (m a) (T Maybe (m a))
+
+The standalone kind signature specifies the polymorphic kind
+for ``T``, and this signature is used for all the calls to ``T``
+including the recursive ones. In particular, the recursive use of ``T``
+is at kind ``Type``.
+
+While a standalone kind signature determines the kind of a type constructor, it
+does not determine its arity. This is of particular importance for type
+families and type synonyms, as they cannot be partially applied. See
+:ref:`type-family-declarations` for more information about arity.
+
+The arity can be specified using explicit binders and inline kind annotations::
+
+    -- arity F0 = 0
+    type F0 :: forall k. k -> Type
+    type family F0 :: forall k. k -> Type
+
+    -- arity F1 = 1
+    type F1 :: forall k. k -> Type
+    type family F1 :: k -> Type
+
+    -- arity F2 = 2
+    type F2 :: forall k. k -> Type
+    type family F2 a :: Type
+
+In absence of an inline kind annotation, the inferred arity includes all
+explicitly bound parameters and all immediately following invisible
+parameters::
+
+    -- arity FD1 = 1
+    type FD1 :: forall k. k -> Type
+    type FD1
+
+    -- arity FD2 = 2
+    type FD2 :: forall k. k -> Type
+    type FD2 a
+
+Note that ``F0``, ``F1``, ``F2``, ``FD1``, and ``FD2`` all have identical
+standalone kind signatures. The arity is inferred from the type family header.
+
+Standalone kind signatures and declaration headers
+--------------------------------------------------
+
+GHC requires that in the presence of a standalone kind signature, data
+declarations must bind all their inputs. For example: ::
+
+    type Prox1 :: k -> Type
+    data Prox1 a = MkProx1
+      -- OK.
+
+    type Prox2 :: k -> Type
+    data Prox2 = MkProx2
+      -- Error:
+      --   • Expected a type, but found something with kind ‘k -> Type’
+      --   • In the data type declaration for ‘Prox2’
+
+
+GADT-style data declarations may either bind their inputs or use an inline
+signature in addition to the standalone kind signature: ::
+
+    type GProx1 :: k -> Type
+    data GProx1 a where MkGProx1 :: GProx1 a
+      -- OK.
+
+    type GProx2 :: k -> Type
+    data GProx2 where MkGProx2 :: GProx2 a
+      -- Error:
+      --   • Expected a type, but found something with kind ‘k -> Type’
+      --   • In the data type declaration for ‘GProx2’
+
+    type GProx3 :: k -> Type
+    data GProx3 :: k -> Type where MkGProx3 :: GProx3 a
+      -- OK.
+
+    type GProx4 :: k -> Type
+    data GProx4 :: w where MkGProx4 :: GProx4 a
+      -- OK, w ~ (k -> Type)
+
+Classes are subject to the same rules: ::
+
+    type C1 :: Type -> Constraint
+    class C1 a
+      -- OK.
+
+    type C2 :: Type -> Constraint
+    class C2
+      -- Error:
+      --   • Couldn't match expected kind ‘Constraint’
+      --                 with actual kind ‘Type -> Constraint’
+      --   • In the class declaration for ‘C2’
+
+On the other hand, type families are exempt from this rule: ::
+
+    type F :: Type -> Type
+    type family F
+      -- OK.
+
+Data families are tricky territory. Their headers are exempt from this rule,
+but their instances are not: ::
+
+    type T :: k -> Type
+    data family T
+      -- OK.
+
+    data instance T Int = MkT1
+      -- OK.
+
+    data instance T = MkT3
+      -- Error:
+      --   • Expecting one more argument to ‘T’
+      --     Expected a type, but ‘T’ has kind ‘k0 -> Type’
+      --   • In the data instance declaration for ‘T’
+
+This also applies to GADT-style data instances: ::
+
+    data instance T (a :: Nat) where MkN4 :: T 4
+                                     MKN9 :: T 9
+      -- OK.
+
+    data instance T :: Symbol -> Type where MkSN :: T "Neptune"
+                                            MkSJ :: T "Jupiter"
+      -- OK.
+
+    data instance T where MkT4 :: T x
+      -- Error:
+      --   • Expecting one more argument to ‘T’
+      --     Expected a type, but ‘T’ has kind ‘k0 -> Type’
+      --   • In the data instance declaration for ‘T’
+
 
 Kind inference in closed type families
 --------------------------------------