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, 10 insertions, 1 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index c37d366d5e..7baa748faa 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -140,6 +140,7 @@ repTopDs group@(HsGroup { hs_valds   = valds
                      ; _        <- mapM no_splice splcds
                      ; tycl_ds  <- mapM repTyClD (tyClGroupTyClDecls tyclds)
                      ; role_ds  <- mapM repRoleD (concatMap group_roles tyclds)
+                     ; kisig_ds <- mapM repKiSigD (concatMap group_kisigs tyclds)
                      ; inst_ds  <- mapM repInstD instds
                      ; deriv_ds <- mapM repStandaloneDerivD derivds
                      ; fix_ds   <- mapM repFixD fixds
@@ -155,6 +156,7 @@ repTopDs group@(HsGroup { hs_valds   = valds
                         -- more needed
                      ;  return (de_loc $ sort_by_loc $
                                 val_ds ++ catMaybes tycl_ds ++ role_ds
+                                       ++ kisig_ds
                                        ++ (concat fix_ds)
                                        ++ inst_ds ++ rule_ds ++ for_ds
                                        ++ ann_ds ++ deriv_ds) }) ;
@@ -348,6 +350,13 @@ repRoleD (dL->L loc (RoleAnnotDecl _ tycon roles))
 repRoleD _ = panic "repRoleD"
 
 -------------------------
+repKiSigD :: LStandaloneKindSig GhcRn -> DsM (SrcSpan, Core TH.DecQ)
+repKiSigD (dL->L loc kisig) =
+  case kisig of
+    StandaloneKindSig _ v ki -> rep_ty_sig kiSigDName loc ki v
+    XStandaloneKindSig nec -> noExtCon nec
+
+-------------------------
 repDataDefn :: Core TH.Name
             -> Either (Core [TH.TyVarBndrQ])
                         -- the repTyClD case
@@ -870,7 +879,7 @@ rep_ty_sig :: Name -> SrcSpan -> LHsSigType GhcRn -> Located Name
 -- and Note [Don't quantify implicit type variables in quotes]
 rep_ty_sig mk_sig loc sig_ty nm
   | HsIB { hsib_body = hs_ty } <- sig_ty
-  , (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy hs_ty
+  , (explicit_tvs, ctxt, ty) <- splitLHsSigmaTyInvis hs_ty
   = do { nm1 <- lookupLOcc nm
        ; let rep_in_scope_tv tv = do { name <- lookupBinder (hsLTyVarName tv)
                                      ; repTyVarBndrWithKind tv name }