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, 39 insertions, 0 deletions

diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index 276fcb1c5b..f32ce4a5e0 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -1049,6 +1049,7 @@ topdecls_semi :: { OrdList (LHsDecl GhcPs) }
 topdecl :: { LHsDecl GhcPs }
         : cl_decl                               { sL1 $1 (TyClD noExtField (unLoc $1)) }
         | ty_decl                               { sL1 $1 (TyClD noExtField (unLoc $1)) }
+        | standalone_kind_sig                   { sL1 $1 (KindSigD noExtField (unLoc $1)) }
         | inst_decl                             { sL1 $1 (InstD noExtField (unLoc $1)) }
         | stand_alone_deriving                  { sLL $1 $> (DerivD noExtField (unLoc $1)) }
         | role_annot                            { sL1 $1 (RoleAnnotD noExtField (unLoc $1)) }
@@ -1131,6 +1132,19 @@ ty_decl :: { LTyClDecl GhcPs }
                                    (snd $ unLoc $4) Nothing)
                         (mj AnnData $1:mj AnnFamily $2:(fst $ unLoc $4)) }
 
+-- standalone kind signature
+standalone_kind_sig :: { LStandaloneKindSig GhcPs }
+  : 'type' sks_vars '::' ktypedoc
+      {% amms (mkStandaloneKindSig (comb2 $1 $4) $2 $4)
+              [mj AnnType $1,mu AnnDcolon $3] }
+
+-- See also: sig_vars
+sks_vars :: { Located [Located RdrName] }  -- Returned in reverse order
+  : sks_vars ',' oqtycon
+      {% addAnnotation (gl $ head $ unLoc $1) AnnComma (gl $2) >>
+         return (sLL $1 $> ($3 : unLoc $1)) }
+  | oqtycon { sL1 $1 [$1] }
+
 inst_decl :: { LInstDecl GhcPs }
         : 'instance' overlap_pragma inst_type where_inst
        {% do { (binds, sigs, _, ats, adts, _) <- cvBindsAndSigs (snd $ unLoc $4)
diff --git a/compiler/parser/RdrHsSyn.hs b/compiler/parser/RdrHsSyn.hs
index 538c20cc8a..0686f669d3 100644
--- a/compiler/parser/RdrHsSyn.hs
+++ b/compiler/parser/RdrHsSyn.hs
@@ -23,6 +23,7 @@ module   RdrHsSyn (
         mkClassDecl,
         mkTyData, mkDataFamInst,
         mkTySynonym, mkTyFamInstEqn,
+        mkStandaloneKindSig,
         mkTyFamInst,
         mkFamDecl, mkLHsSigType,
         mkInlinePragma,
@@ -239,6 +240,30 @@ mkTySynonym loc lhs rhs
                                  , tcdFixity = fixity
                                  , tcdRhs = rhs })) }
 
+mkStandaloneKindSig
+  :: SrcSpan
+  -> Located [Located RdrName] -- LHS
+  -> LHsKind GhcPs             -- RHS
+  -> P (LStandaloneKindSig GhcPs)
+mkStandaloneKindSig loc lhs rhs =
+  do { vs <- mapM check_lhs_name (unLoc lhs)
+     ; v <- check_singular_lhs (reverse vs)
+     ; return $ cL loc $ StandaloneKindSig noExtField v (mkLHsSigType rhs) }
+  where
+    check_lhs_name v@(unLoc->name) =
+      if isUnqual name && isTcOcc (rdrNameOcc name)
+      then return v
+      else addFatalError (getLoc v) $
+           hang (text "Expected an unqualified type constructor:") 2 (ppr v)
+    check_singular_lhs vs =
+      case vs of
+        [] -> panic "mkStandaloneKindSig: empty left-hand side"
+        [v] -> return v
+        _ -> addFatalError (getLoc lhs) $
+             vcat [ hang (text "Standalone kind signatures do not support multiple names at the moment:")
+                       2 (pprWithCommas ppr vs)
+                  , text "See https://gitlab.haskell.org/ghc/ghc/issues/16754 for details." ]
+
 mkTyFamInstEqn :: Maybe [LHsTyVarBndr GhcPs]
                -> LHsType GhcPs
                -> LHsType GhcPs