Standalone kind signatures (#16794) wip/top-level-kind-signatures
authorVladislav Zavialov <vlad.z.4096@gmail.com>
Fri, 29 Mar 2019 07:18:03 +0000 (10:18 +0300)
committerVladislav Zavialov <vlad.z.4096@gmail.com>
Wed, 25 Sep 2019 18:06:04 +0000 (21:06 +0300)
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.

244 files changed:
compiler/GHC/Hs/Decls.hs
compiler/GHC/Hs/Extension.hs
compiler/GHC/Hs/Instances.hs
compiler/GHC/Hs/Types.hs
compiler/GHC/ThToHs.hs
compiler/basicTypes/NameEnv.hs
compiler/deSugar/DsMeta.hs
compiler/hieFile/HieAst.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/main/DynFlags.hs
compiler/parser/Parser.y
compiler/parser/RdrHsSyn.hs
compiler/prelude/THNames.hs
compiler/prelude/TysWiredIn.hs
compiler/rename/RnBinds.hs
compiler/rename/RnSource.hs
compiler/rename/RnTypes.hs
compiler/rename/RnUtils.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcEnv.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
compiler/types/TyCon.hs
compiler/types/Type.hs
docs/users_guide/8.10.1-notes.rst
docs/users_guide/glasgow_exts.rst
libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
libraries/template-haskell/Language/Haskell/TH/Lib.hs
libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
libraries/template-haskell/Language/Haskell/TH/Ppr.hs
libraries/template-haskell/Language/Haskell/TH/Syntax.hs
testsuite/tests/backpack/should_fail/bkpfail04.stderr
testsuite/tests/backpack/should_fail/bkpfail06.stderr
testsuite/tests/backpack/should_fail/bkpfail07.stderr
testsuite/tests/backpack/should_fail/bkpfail10.stderr
testsuite/tests/backpack/should_fail/bkpfail17.stderr
testsuite/tests/backpack/should_fail/bkpfail22.stderr
testsuite/tests/backpack/should_fail/bkpfail23.stderr
testsuite/tests/backpack/should_fail/bkpfail25.stderr
testsuite/tests/backpack/should_fail/bkpfail26.stderr
testsuite/tests/backpack/should_fail/bkpfail27.stderr
testsuite/tests/backpack/should_fail/bkpfail41.stderr
testsuite/tests/backpack/should_fail/bkpfail42.stderr
testsuite/tests/backpack/should_fail/bkpfail45.stderr
testsuite/tests/backpack/should_fail/bkpfail46.stderr
testsuite/tests/backpack/should_fail/bkpfail47.stderr
testsuite/tests/dependent/should_compile/Rae31.hs
testsuite/tests/dependent/should_compile/mkGADTVars.hs
testsuite/tests/driver/T4437.hs
testsuite/tests/ghci/prog008/ghci.prog008.stdout
testsuite/tests/ghci/scripts/T10018.stdout
testsuite/tests/ghci/scripts/T10059.stdout
testsuite/tests/ghci/scripts/T11051a.stdout
testsuite/tests/ghci/scripts/T11051b.stdout
testsuite/tests/ghci/scripts/T12005.stdout
testsuite/tests/ghci/scripts/T12550.stdout
testsuite/tests/ghci/scripts/T13407.stdout
testsuite/tests/ghci/scripts/T13420.stdout
testsuite/tests/ghci/scripts/T13699.stdout
testsuite/tests/ghci/scripts/T15341.stdout
testsuite/tests/ghci/scripts/T15546.stdout
testsuite/tests/ghci/scripts/T15827.stdout
testsuite/tests/ghci/scripts/T15872.stdout
testsuite/tests/ghci/scripts/T15941.stdout
testsuite/tests/ghci/scripts/T16030.stdout
testsuite/tests/ghci/scripts/T16527.stdout
testsuite/tests/ghci/scripts/T4015.stdout
testsuite/tests/ghci/scripts/T4087.stdout
testsuite/tests/ghci/scripts/T4175.stdout
testsuite/tests/ghci/scripts/T5417.stdout
testsuite/tests/ghci/scripts/T5820.stdout
testsuite/tests/ghci/scripts/T6027ghci.stdout
testsuite/tests/ghci/scripts/T7627.stdout
testsuite/tests/ghci/scripts/T7730.stdout
testsuite/tests/ghci/scripts/T7872.stdout
testsuite/tests/ghci/scripts/T7873.stdout
testsuite/tests/ghci/scripts/T7939.stdout
testsuite/tests/ghci/scripts/T8469.stdout
testsuite/tests/ghci/scripts/T8535.stdout
testsuite/tests/ghci/scripts/T8579.stdout
testsuite/tests/ghci/scripts/T8674.stdout
testsuite/tests/ghci/scripts/T9181.stdout
testsuite/tests/ghci/scripts/T9881.stdout
testsuite/tests/ghci/scripts/ghci008.stdout
testsuite/tests/ghci/scripts/ghci011.stdout
testsuite/tests/ghci/scripts/ghci019.stdout
testsuite/tests/ghci/scripts/ghci020.stdout
testsuite/tests/ghci/scripts/ghci023.stdout
testsuite/tests/ghci/scripts/ghci025.stdout
testsuite/tests/ghci/scripts/ghci026.stdout
testsuite/tests/ghci/scripts/ghci027.stdout
testsuite/tests/ghci/scripts/ghci030.stdout
testsuite/tests/ghci/scripts/ghci031.stdout
testsuite/tests/ghci/scripts/ghci033.stdout
testsuite/tests/ghci/scripts/ghci040.stdout
testsuite/tests/ghci/scripts/ghci041.stdout
testsuite/tests/ghci/scripts/ghci042.stdout
testsuite/tests/ghci/scripts/ghci051.stdout
testsuite/tests/ghci/scripts/ghci059.stdout
testsuite/tests/ghci/should_run/T10145.stdout
testsuite/tests/ghci/should_run/T11825.stdout
testsuite/tests/ghci/should_run/T12525.stdout
testsuite/tests/ghci/should_run/T9914.stdout
testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr
testsuite/tests/indexed-types/should_fail/T9167.stderr
testsuite/tests/overloadedrecflds/ghci/duplicaterecfldsghci01.stdout
testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
testsuite/tests/parser/should_compile/T14189.stderr
testsuite/tests/polykinds/CuskFam.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T
testsuite/tests/rename/should_fail/rnfail055.stderr
testsuite/tests/roles/should_fail/Roles12.stderr
testsuite/tests/roles/should_fail/T9204.stderr
testsuite/tests/saks/should_compile/T16721.script [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16721.stdout [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16723.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16724.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16724.script [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16724.stdout [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16726.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16731.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16756a.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T16758.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T17164.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/T17164.stderr [new file with mode: 0644]
testsuite/tests/saks/should_compile/all.T [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks001.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks002.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks003.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks004.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks005.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks006.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks007.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks008.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks009.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks010.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks014.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks015.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks016.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks017.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks018.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks019.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks020.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks021.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks023.script [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks023.stdout [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks024.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks025.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks025.script [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks025.stdout [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks026.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks027.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks027.stderr [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks028.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks028.stderr [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks029.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks030.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks031.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks032.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks033.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks034.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks034.script [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks034.stdout [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks035.hs [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks035.script [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks035.stdout [new file with mode: 0644]
testsuite/tests/saks/should_compile/saks036.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16722.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16722.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16725.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16725.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16727a.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16727a.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16727b.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16727b.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16756b.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16756b.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16826.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/T16826.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/all.T [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks007_fail.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks007_fail.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail001.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail001.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail002.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail002.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail003.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail003.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail004.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail004.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail005.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail005.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail006.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail006.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail007.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail007.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail008.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail008.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail009.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail009.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail010.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail010.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail011.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail011.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail012.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail012.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail013.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail013.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail014.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail014.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail015.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail015.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail016.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail016.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail017.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail017.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail018.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail018.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail019.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail019.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail020.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail020.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail021.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail021.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail022.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail022.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail023.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail023.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail024.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail024.stderr [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail025.hs [new file with mode: 0644]
testsuite/tests/saks/should_fail/saks_fail025.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T12035.stderr
testsuite/tests/typecheck/should_fail/T12035j.stderr
testsuite/tests/typecheck/should_fail/T12042.stderr
testsuite/tests/typecheck/should_fail/T3468.stderr
testsuite/tests/typecheck/should_fail/T9201.stderr
testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
testsuite/tests/typecheck/should_fail/tcfail210.stderr

index 701c8b1..c43a27c 100644 (file)
@@ -20,18 +20,20 @@ module GHC.Hs.Decls (
   -- * Toplevel declarations
   HsDecl(..), LHsDecl, HsDataDefn(..), HsDeriving, LHsFunDep,
   HsDerivingClause(..), LHsDerivingClause, NewOrData(..), newOrDataToFlavour,
+  StandaloneKindSig(..), LStandaloneKindSig, standaloneKindSigName,
 
   -- ** Class or type declarations
   TyClDecl(..), LTyClDecl, DataDeclRn(..),
   TyClGroup(..),
   tyClGroupTyClDecls, tyClGroupInstDecls, tyClGroupRoleDecls,
+  tyClGroupKindSigs,
   isClassDecl, isDataDecl, isSynDecl, tcdName,
   isFamilyDecl, isTypeFamilyDecl, isDataFamilyDecl,
   isOpenTypeFamilyInfo, isClosedTypeFamilyInfo,
   tyFamInstDeclName, tyFamInstDeclLName,
   countTyClDecls, pprTyClDeclFlavour,
   tyClDeclLName, tyClDeclTyVars,
-  hsDeclHasCusk, famDeclHasCusk,
+  hsDeclHasCusk, famResultKindSignature,
   FamilyDecl(..), LFamilyDecl,
 
   -- ** Instance declarations
@@ -136,6 +138,7 @@ data HsDecl p
   | DerivD     (XDerivD p)     (DerivDecl p)     -- ^ Deriving declaration
   | ValD       (XValD p)       (HsBind p)        -- ^ Value declaration
   | SigD       (XSigD p)       (Sig p)           -- ^ Signature declaration
+  | KindSigD   (XKindSigD p)   (StandaloneKindSig p) -- ^ Standalone kind signature
   | DefD       (XDefD p)       (DefaultDecl p)   -- ^ 'default' declaration
   | ForD       (XForD p)       (ForeignDecl p)   -- ^ Foreign declaration
   | WarningD   (XWarningD p)   (WarnDecls p)     -- ^ Warning declaration
@@ -152,6 +155,7 @@ type instance XInstD      (GhcPass _) = NoExtField
 type instance XDerivD     (GhcPass _) = NoExtField
 type instance XValD       (GhcPass _) = NoExtField
 type instance XSigD       (GhcPass _) = NoExtField
+type instance XKindSigD   (GhcPass _) = NoExtField
 type instance XDefD       (GhcPass _) = NoExtField
 type instance XForD       (GhcPass _) = NoExtField
 type instance XWarningD   (GhcPass _) = NoExtField
@@ -278,6 +282,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsDecl p) where
     ppr (DerivD _ deriv)          = ppr deriv
     ppr (ForD _ fd)               = ppr fd
     ppr (SigD _ sd)               = ppr sd
+    ppr (KindSigD _ ksd)          = ppr ksd
     ppr (RuleD _ rd)              = ppr rd
     ppr (WarningD _ wd)           = ppr wd
     ppr (AnnD _ ad)               = ppr ad
@@ -304,6 +309,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsGroup p) where
                 then Nothing
                 else Just (ppr val_decls),
              ppr_ds (tyClGroupRoleDecls tycl_decls),
+             ppr_ds (tyClGroupKindSigs  tycl_decls),
              ppr_ds (tyClGroupTyClDecls tycl_decls),
              ppr_ds (tyClGroupInstDecls tycl_decls),
              ppr_ds deriv_decls,
@@ -658,7 +664,7 @@ tyClDeclLName :: TyClDecl pass -> Located (IdP pass)
 tyClDeclLName (FamDecl { tcdFam = FamilyDecl { fdLName = ln } }) = ln
 tyClDeclLName decl = tcdLName decl
 
-tcdName :: TyClDecl pass -> (IdP pass)
+tcdName :: TyClDecl pass -> IdP pass
 tcdName = unLoc . tyClDeclLName
 
 tyClDeclTyVars :: TyClDecl pass -> LHsQTyVars pass
@@ -682,25 +688,21 @@ countTyClDecls decls
 
 -- | Does this declaration have a complete, user-supplied kind signature?
 -- See Note [CUSKs: complete user-supplied kind signatures]
-hsDeclHasCusk
-  :: Bool  -- True <=> the -XCUSKs extension is enabled
-  -> TyClDecl GhcRn
-  -> Bool
-hsDeclHasCusk _cusks_enabled@False _ = False
-hsDeclHasCusk cusks_enabled (FamDecl { tcdFam = fam_decl })
-  = famDeclHasCusk cusks_enabled False fam_decl
-    -- False: this is not: an associated type of a class with no cusk
-hsDeclHasCusk _cusks_enabled@True (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
-  -- NB: Keep this synchronized with 'getInitialKind'
-  = hsTvbAllKinded tyvars && rhs_annotated rhs
-  where
-    rhs_annotated (L _ ty) = case ty of
-      HsParTy _ lty  -> rhs_annotated lty
-      HsKindSig {}   -> True
-      _              -> False
-hsDeclHasCusk _cusks_enabled@True (DataDecl { tcdDExt = DataDeclRn { tcdDataCusk = cusk }}) = cusk
-hsDeclHasCusk _cusks_enabled@True (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars
-hsDeclHasCusk _ (XTyClDecl nec) = noExtCon nec
+hsDeclHasCusk :: TyClDecl GhcRn -> Bool
+hsDeclHasCusk (FamDecl { tcdFam =
+    FamilyDecl { fdInfo      = fam_info
+               , fdTyVars    = tyvars
+               , fdResultSig = L _ resultSig } }) =
+    case fam_info of
+      ClosedTypeFamily {} -> hsTvbAllKinded tyvars
+                          && isJust (famResultKindSignature resultSig)
+      _ -> True -- Un-associated open type/data families have CUSKs
+hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
+  = hsTvbAllKinded tyvars && isJust (hsTyKindSig rhs)
+hsDeclHasCusk (DataDecl { tcdDExt = DataDeclRn { tcdDataCusk = cusk }}) = cusk
+hsDeclHasCusk (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars
+hsDeclHasCusk (FamDecl { tcdFam = XFamilyDecl nec }) = noExtCon nec
+hsDeclHasCusk (XTyClDecl nec) = noExtCon nec
 
 -- Pretty-printing TyClDecl
 -- ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -742,10 +744,13 @@ instance (p ~ GhcPass pass, OutputableBndrId p)
        => Outputable (TyClGroup p) where
   ppr (TyClGroup { group_tyclds = tyclds
                  , group_roles = roles
+                 , group_kisigs = kisigs
                  , group_instds = instds
                  }
       )
-    = ppr tyclds $$
+    = hang (text "TyClGroup") 2 $
+      ppr kisigs $$
+      ppr tyclds $$
       ppr roles $$
       ppr instds
   ppr (XTyClGroup x) = ppr x
@@ -777,8 +782,8 @@ pprTyClDeclFlavour (ClassDecl {})   = text "class"
 pprTyClDeclFlavour (SynDecl {})     = text "type"
 pprTyClDeclFlavour (FamDecl { tcdFam = FamilyDecl { fdInfo = info }})
   = pprFlavour info <+> text "family"
-pprTyClDeclFlavour (FamDecl { tcdFam = XFamilyDecl x})
-  = ppr x
+pprTyClDeclFlavour (FamDecl { tcdFam = XFamilyDecl nec })
+  = noExtCon nec
 pprTyClDeclFlavour (DataDecl { tcdDataDefn = HsDataDefn { dd_ND = nd } })
   = ppr nd
 pprTyClDeclFlavour (DataDecl { tcdDataDefn = XHsDataDefn x })
@@ -910,6 +915,7 @@ data TyClGroup pass  -- See Note [TyClGroups and dependency analysis]
   = TyClGroup { group_ext    :: XCTyClGroup pass
               , group_tyclds :: [LTyClDecl pass]
               , group_roles  :: [LRoleAnnotDecl pass]
+              , group_kisigs :: [LStandaloneKindSig pass]
               , group_instds :: [LInstDecl pass] }
   | XTyClGroup (XXTyClGroup pass)
 
@@ -926,6 +932,8 @@ tyClGroupInstDecls = concatMap group_instds
 tyClGroupRoleDecls :: [TyClGroup pass] -> [LRoleAnnotDecl pass]
 tyClGroupRoleDecls = concatMap group_roles
 
+tyClGroupKindSigs :: [TyClGroup pass] -> [LStandaloneKindSig pass]
+tyClGroupKindSigs = concatMap group_kisigs
 
 
 {- *********************************************************************
@@ -1024,6 +1032,7 @@ data FamilyResultSig pass = -- see Note [FamilyResultSig]
 
 type instance XNoSig            (GhcPass _) = NoExtField
 type instance XCKindSig         (GhcPass _) = NoExtField
+
 type instance XTyVarSig         (GhcPass _) = NoExtField
 type instance XXFamilyResultSig (GhcPass _) = NoExtCon
 
@@ -1081,32 +1090,15 @@ data FamilyInfo pass
      -- said "type family Foo x where .."
   | ClosedTypeFamily (Maybe [LTyFamInstEqn pass])
 
--- | Does this family declaration have a complete, user-supplied kind signature?
--- See Note [CUSKs: complete user-supplied kind signatures]
-famDeclHasCusk :: Bool -- ^ True <=> the -XCUSKs extension is enabled
-               -> Bool -- ^ True <=> this is an associated type family,
-                       --            and the parent class has /no/ CUSK
-               -> FamilyDecl (GhcPass pass)
-               -> Bool
-famDeclHasCusk _cusks_enabled@False _ _ = False
-famDeclHasCusk _cusks_enabled@True assoc_with_no_cusk
-               (FamilyDecl { fdInfo      = fam_info
-                           , fdTyVars    = tyvars
-                           , fdResultSig = L _ resultSig })
-  = case fam_info of
-      ClosedTypeFamily {} -> hsTvbAllKinded tyvars
-                          && hasReturnKindSignature resultSig
-      _ -> not assoc_with_no_cusk
-            -- Un-associated open type/data families have CUSKs
-            -- Associated type families have CUSKs iff the parent class does
-
-famDeclHasCusk _ _ (XFamilyDecl nec) = noExtCon nec
-
--- | Does this family declaration have user-supplied return kind signature?
-hasReturnKindSignature :: FamilyResultSig a -> Bool
-hasReturnKindSignature (NoSig _)                        = False
-hasReturnKindSignature (TyVarSig _ (L _ (UserTyVar{}))) = False
-hasReturnKindSignature _                                = True
+famResultKindSignature :: FamilyResultSig (GhcPass p) -> Maybe (LHsKind (GhcPass p))
+famResultKindSignature (NoSig _) = Nothing
+famResultKindSignature (KindSig _ ki) = Just ki
+famResultKindSignature (TyVarSig _ bndr) =
+  case unLoc bndr of
+    UserTyVar _ _ -> Nothing
+    KindedTyVar _ _ ki -> Just ki
+    XTyVarBndr nec -> noExtCon nec
+famResultKindSignature (XFamilyResultSig nec) = noExtCon nec
 
 -- | Maybe return name of the result type variable
 resultVariableName :: FamilyResultSig (GhcPass a) -> Maybe (IdP (GhcPass a))
@@ -1137,7 +1129,7 @@ pprFamilyDecl top_level (FamilyDecl { fdInfo = info, fdLName = ltycon
                 NoSig    _         -> empty
                 KindSig  _ kind    -> dcolon <+> ppr kind
                 TyVarSig _ tv_bndr -> text "=" <+> ppr tv_bndr
-                XFamilyResultSig x -> ppr x
+                XFamilyResultSig nec -> noExtCon nec
     pp_inj = case mb_inj of
                Just (L _ (InjectivityAnn lhs rhs)) ->
                  hsep [ vbar, ppr lhs, text "->", hsep (map ppr rhs) ]
@@ -1149,7 +1141,7 @@ pprFamilyDecl top_level (FamilyDecl { fdInfo = info, fdLName = ltycon
             Nothing   -> text ".."
             Just eqns -> vcat $ map (ppr_fam_inst_eqn . unLoc) eqns )
       _ -> (empty, empty)
-pprFamilyDecl _ (XFamilyDecl x) = ppr x
+pprFamilyDecl _ (XFamilyDecl nec) = noExtCon nec
 
 pprFlavour :: FamilyInfo pass -> SDoc
 pprFlavour DataFamily            = text "data"
@@ -1203,6 +1195,7 @@ data HsDataDefn pass   -- The payload of a data type defn
   | XHsDataDefn (XXHsDataDefn pass)
 
 type instance XCHsDataDefn    (GhcPass _) = NoExtField
+
 type instance XXHsDataDefn    (GhcPass _) = NoExtCon
 
 -- | Haskell Deriving clause
@@ -1269,6 +1262,37 @@ instance (p ~ GhcPass pass, OutputableBndrId p)
             _                            -> (ppDerivStrategy dcs, empty)
   ppr (XHsDerivingClause x) = ppr x
 
+-- | Located Standalone Kind Signature
+type LStandaloneKindSig pass = Located (StandaloneKindSig pass)
+
+data StandaloneKindSig pass
+  = StandaloneKindSig (XStandaloneKindSig pass)
+      (Located (IdP pass))  -- Why a single binder? See #16754
+      (LHsSigType pass)     -- Why not LHsSigWcType? See Note [Wildcards in standalone kind signatures]
+  | XStandaloneKindSig (XXStandaloneKindSig pass)
+
+type instance XStandaloneKindSig (GhcPass p) = NoExtField
+type instance XXStandaloneKindSig (GhcPass p) = NoExtCon
+
+standaloneKindSigName :: StandaloneKindSig (GhcPass p) -> IdP (GhcPass p)
+standaloneKindSigName (StandaloneKindSig _ lname _) = unLoc lname
+standaloneKindSigName (XStandaloneKindSig nec) = noExtCon nec
+
+{- Note [Wildcards in standalone kind signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Standalone kind signatures enable polymorphic recursion, and it is unclear how
+to reconcile this with partial type signatures, so we disallow wildcards in
+them.
+
+We reject wildcards in 'rnStandaloneKindSignature' by returning False for
+'StandaloneKindSigCtx' in 'wildCardsAllowed'.
+
+The alternative design is to have special treatment for partial standalone kind
+signatures, much like we have special treatment for partial type signatures in
+terms. However, partial standalone kind signatures are not a proper replacement
+for CUSKs, so this would be a separate feature.
+-}
+
 data NewOrData
   = NewType                     -- ^ @newtype Blah ...@
   | DataType                    -- ^ @data Blah ...@
@@ -1279,6 +1303,7 @@ newOrDataToFlavour :: NewOrData -> TyConFlavour
 newOrDataToFlavour NewType  = NewtypeFlavour
 newOrDataToFlavour DataType = DataTypeFlavour
 
+
 -- | Located data Constructor Declaration
 type LConDecl pass = Located (ConDecl pass)
       -- ^ May have 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnSemi' when
@@ -1443,6 +1468,11 @@ instance (p ~ GhcPass pass, OutputableBndrId p)
        => Outputable (HsDataDefn p) where
    ppr d = pp_data_defn (\_ -> text "Naked HsDataDefn") d
 
+instance (p ~ GhcPass pass, OutputableBndrId p)
+       => Outputable (StandaloneKindSig p) where
+  ppr (StandaloneKindSig _ v ki) = text "type" <+> ppr v <+> text "::" <+> ppr ki
+  ppr (XStandaloneKindSig nec) = noExtCon nec
+
 instance Outputable NewOrData where
   ppr NewType  = text "newtype"
   ppr DataType = text "data"
index f360e1c..35afc5f 100644 (file)
@@ -280,6 +280,10 @@ type ForallXFixitySig (c :: * -> Constraint) (x :: *) =
        , c (XXFixitySig        x)
        )
 
+-- StandaloneKindSig type families
+type family XStandaloneKindSig  x
+type family XXStandaloneKindSig x
+
 -- =====================================================================
 -- Type families for the HsDecls extension points
 
@@ -289,6 +293,7 @@ type family XInstD       x
 type family XDerivD      x
 type family XValD        x
 type family XSigD        x
+type family XKindSigD    x
 type family XDefD        x
 type family XForD        x
 type family XWarningD    x
@@ -305,6 +310,7 @@ type ForallXHsDecl (c :: * -> Constraint) (x :: *) =
        , c (XDerivD      x)
        , c (XValD        x)
        , c (XSigD        x)
+       , c (XKindSigD    x)
        , c (XDefD        x)
        , c (XForD        x)
        , c (XWarningD    x)
index d55e20c..b3a33df 100644 (file)
@@ -86,6 +86,11 @@ deriving instance Data (FixitySig GhcPs)
 deriving instance Data (FixitySig GhcRn)
 deriving instance Data (FixitySig GhcTc)
 
+-- deriving instance (DataId p)       => Data (StandaloneKindSig p)
+deriving instance Data (StandaloneKindSig GhcPs)
+deriving instance Data (StandaloneKindSig GhcRn)
+deriving instance Data (StandaloneKindSig GhcTc)
+
 -- deriving instance (DataIdLR p p)   => Data (HsPatSynDir p)
 deriving instance Data (HsPatSynDir GhcPs)
 deriving instance Data (HsPatSynDir GhcRn)
index f14d59b..04fd1ee 100644 (file)
@@ -62,6 +62,7 @@ module GHC.Hs.Types (
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
         ignoreParens, hsSigType, hsSigWcType,
         hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
+        hsTyKindSig,
         hsConDetailsArgs,
 
         -- Printing
@@ -79,7 +80,7 @@ import {-# SOURCE #-} GHC.Hs.Expr ( HsSplice, pprSplice )
 import GHC.Hs.Extension
 
 import Id ( Id )
-import Name( Name )
+import Name( Name, NamedThing(getName) )
 import RdrName ( RdrName )
 import DataCon( HsSrcBang(..), HsImplBang(..),
                 SrcStrictness(..), SrcUnpackedness(..) )
@@ -505,6 +506,7 @@ data HsTyVarBndr pass
 
 type instance XUserTyVar    (GhcPass _) = NoExtField
 type instance XKindedTyVar  (GhcPass _) = NoExtField
+
 type instance XXTyVarBndr   (GhcPass _) = NoExtCon
 
 -- | Does this 'HsTyVarBndr' come with an explicit kind annotation?
@@ -517,6 +519,11 @@ isHsKindedTyVar (XTyVarBndr {})  = False
 hsTvbAllKinded :: LHsQTyVars pass -> Bool
 hsTvbAllKinded = all (isHsKindedTyVar . unLoc) . hsQTvExplicit
 
+instance NamedThing (HsTyVarBndr GhcRn) where
+  getName (UserTyVar _ v) = unLoc v
+  getName (KindedTyVar _ v _) = unLoc v
+  getName (XTyVarBndr nec) = noExtCon nec
+
 -- | Haskell Type
 data HsType pass
   = HsForAllTy   -- See Note [HsType binders]
@@ -1076,6 +1083,24 @@ hsLTyVarBndrsToTypes :: LHsQTyVars (GhcPass p) -> [LHsType (GhcPass p)]
 hsLTyVarBndrsToTypes (HsQTvs { hsq_explicit = tvbs }) = map hsLTyVarBndrToType tvbs
 hsLTyVarBndrsToTypes (XLHsQTyVars nec) = noExtCon nec
 
+-- | Get the kind signature of a type, ignoring parentheses:
+--
+--   hsTyKindSig   `Maybe                    `   =   Nothing
+--   hsTyKindSig   `Maybe ::   Type -> Type  `   =   Just  `Type -> Type`
+--   hsTyKindSig   `Maybe :: ((Type -> Type))`   =   Just  `Type -> Type`
+--
+-- This is used to extract the result kind of type synonyms with a CUSK:
+--
+--  type S = (F :: res_kind)
+--                 ^^^^^^^^
+--
+hsTyKindSig :: LHsType pass -> Maybe (LHsKind pass)
+hsTyKindSig lty =
+  case unLoc lty of
+    HsParTy _ lty'    -> hsTyKindSig lty'
+    HsKindSig _ _ k   -> Just k
+    _                 -> Nothing
+
 ---------------------
 ignoreParens :: LHsType pass -> LHsType pass
 ignoreParens (L _ (HsParTy _ ty)) = ignoreParens ty
@@ -1449,7 +1474,7 @@ instance (p ~ GhcPass pass, OutputableBndrId p)
        => Outputable (HsTyVarBndr p) where
     ppr (UserTyVar _ n)     = ppr n
     ppr (KindedTyVar _ n k) = parens $ hsep [ppr n, dcolon, ppr k]
-    ppr (XTyVarBndr n)      = ppr n
+    ppr (XTyVarBndr nec)    = noExtCon nec
 
 instance (p ~ GhcPass pass,Outputable thing)
        => Outputable (HsImplicitBndrs p thing) where
index ca38d07..f49d6ff 100644 (file)
@@ -180,6 +180,12 @@ cvtDec (TH.SigD nm typ)
         ; returnJustL $ Hs.SigD noExtField
                                     (TypeSig noExtField [nm'] (mkLHsSigWcType ty')) }
 
+cvtDec (TH.KiSigD nm ki)
+  = do  { nm' <- tconNameL nm
+        ; ki' <- cvtType ki
+        ; let sig' = StandaloneKindSig noExtField nm' (mkLHsSigType ki')
+        ; returnJustL $ Hs.KindSigD noExtField sig' }
+
 cvtDec (TH.InfixD fx nm)
   -- Fixity signatures are allowed for variables, constructors, and types
   -- the renamer automatically looks for types during renaming, even when
index 5f6bdc5..03c2150 100644 (file)
@@ -11,7 +11,7 @@ module NameEnv (
         NameEnv,
 
         -- ** Manipulating these environments
-        mkNameEnv,
+        mkNameEnv, mkNameEnvWith,
         emptyNameEnv, isEmptyNameEnv,
         unitNameEnv, nameEnvElts,
         extendNameEnv_C, extendNameEnv_Acc, extendNameEnv,
@@ -92,6 +92,7 @@ type NameEnv a = UniqFM a       -- Domain is Name
 emptyNameEnv       :: NameEnv a
 isEmptyNameEnv     :: NameEnv a -> Bool
 mkNameEnv          :: [(Name,a)] -> NameEnv a
+mkNameEnvWith      :: (a -> Name) -> [a] -> NameEnv a
 nameEnvElts        :: NameEnv a -> [a]
 alterNameEnv       :: (Maybe a-> Maybe a) -> NameEnv a -> Name -> NameEnv a
 extendNameEnv_C    :: (a->a->a) -> NameEnv a -> Name -> a -> NameEnv a
@@ -121,6 +122,7 @@ extendNameEnvList x l = addListToUFM x l
 lookupNameEnv x y     = lookupUFM x y
 alterNameEnv          = alterUFM
 mkNameEnv     l       = listToUFM l
+mkNameEnvWith f       = mkNameEnv . map (\a -> (f a, a))
 elemNameEnv x y          = elemUFM x y
 plusNameEnv x y          = plusUFM x y
 plusNameEnv_C f x y      = plusUFM_C f x y
index c37d366..7baa748 100644 (file)
@@ -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 }
index a1253de..52f8c59 100644 (file)
@@ -1254,8 +1254,13 @@ instance ( a ~ GhcPass p
       XCmd _ -> []
 
 instance ToHie (TyClGroup GhcRn) where
-  toHie (TyClGroup _ classes roles instances) = concatM
+  toHie TyClGroup{ group_tyclds = classes
+                 , group_roles  = roles
+                 , group_kisigs = sigs
+                 , group_instds = instances } =
+    concatM
     [ toHie classes
+    , toHie sigs
     , toHie roles
     , toHie instances
     ]
@@ -1466,6 +1471,17 @@ instance ( HasLoc thing
     where span = loc a
   toHie (TS _ (XHsWildCardBndrs _)) = pure []
 
+instance ToHie (LStandaloneKindSig GhcRn) where
+  toHie (L sp sig) = concatM [makeNode sig sp, toHie sig]
+
+instance ToHie (StandaloneKindSig GhcRn) where
+  toHie sig = concatM $ case sig of
+    StandaloneKindSig _ name typ ->
+      [ toHie $ C TyDecl name
+      , toHie $ TS (ResolvedScopes []) typ
+      ]
+    XStandaloneKindSig _ -> []
+
 instance ToHie (SigContext (LSig GhcRn)) where
   toHie (SC (SI styp msp) (L sp sig)) = concatM $ makeNode sig sp : case sig of
       TypeSig _ names typ ->
index 688998f..f86ca45 100644 (file)
@@ -69,6 +69,7 @@ import TyCon ( Role (..), Injectivity(..), tyConBndrVisArgFlag )
 import Util( dropList, filterByList, notNull, unzipWith )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
 import Lexeme (isLexSym)
+import TysWiredIn ( constraintKindTyConName )
 
 import Control.Monad
 import System.IO.Unsafe
@@ -730,6 +731,14 @@ pprClassRoles ss clas binders roles =
              binders
              roles
 
+pprClassStandaloneKindSig :: ShowSub -> IfaceTopBndr -> IfaceKind -> SDoc
+pprClassStandaloneKindSig ss clas =
+  pprStandaloneKindSig (pprPrefixIfDeclBndr (ss_how_much ss) (occName clas))
+
+constraintIfaceKind :: IfaceKind
+constraintIfaceKind =
+  IfaceTyConApp (IfaceTyCon constraintKindTyConName (IfaceTyConInfo NotPromoted IfaceNormalTyCon)) IA_Nil
+
 pprIfaceDecl :: ShowSub -> IfaceDecl -> SDoc
 -- NB: pprIfaceDecl is also used for pretty-printing TyThings in GHCi
 --     See Note [Pretty-printing TyThings] in PprTyThing
@@ -741,10 +750,12 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
                              ifBinders = binders })
 
   | gadt      = vcat [ pp_roles
+                     , pp_ki_sig
                      , pp_nd <+> pp_lhs <+> pp_kind <+> pp_where
                      , nest 2 (vcat pp_cons)
                      , nest 2 $ ppShowIface ss pp_extra ]
   | otherwise = vcat [ pp_roles
+                     , pp_ki_sig
                      , hang (pp_nd <+> pp_lhs) 2 (add_bars pp_cons)
                      , nest 2 $ ppShowIface ss pp_extra ]
   where
@@ -759,26 +770,45 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     cons       = visibleIfConDecls condecls
     pp_where   = ppWhen (gadt && not (null cons)) $ text "where"
     pp_cons    = ppr_trim (map show_con cons) :: [SDoc]
-    pp_kind
-      | isIfaceLiftedTypeKind kind = empty
-      | otherwise = dcolon <+> ppr kind
+    pp_kind    = ppUnless (if ki_sig_printable
+                              then isIfaceTauType kind
+                                      -- Even in the presence of a standalone kind signature, a non-tau
+                                      -- result kind annotation cannot be discarded as it determines the arity.
+                                      -- See Note [Arity inference in kcDeclHeader_sig] in TcHsType
+                              else isIfaceLiftedTypeKind kind)
+                          (dcolon <+> ppr kind)
 
     pp_lhs = case parent of
-               IfNoParent -> pprIfaceDeclHead context ss tycon binders Nothing
+               IfNoParent -> pprIfaceDeclHead suppress_bndr_sig context ss tycon binders
                IfDataInstance{}
                           -> text "instance" <+> pp_data_inst_forall
                                              <+> pprIfaceTyConParent parent
 
     pp_roles
       | is_data_instance = empty
-      | otherwise        = pprRoles (== Representational)
-                                    (pprPrefixIfDeclBndr
-                                        (ss_how_much ss)
-                                        (occName tycon))
-                                    binders roles
+      | otherwise        = pprRoles (== Representational) name_doc binders roles
             -- Don't display roles for data family instances (yet)
             -- See discussion on #8672.
 
+    ki_sig_printable =
+      -- If we print a standalone kind signature for a data instance, we leak
+      -- the internal constructor name:
+      --
+      --    type T15827.R:Dka :: forall k. k -> *
+      --    data instance forall k (a :: k). D a = MkD (Proxy a)
+      --
+      -- This T15827.R:Dka is a compiler-generated type constructor for the
+      -- data instance.
+      not is_data_instance
+
+    pp_ki_sig = ppWhen ki_sig_printable $
+                pprStandaloneKindSig name_doc (mkIfaceTyConKind binders kind)
+
+    -- See Note [Suppressing binder signatures] in IfaceType
+    suppress_bndr_sig = SuppressBndrSig ki_sig_printable
+
+    name_doc = pprPrefixIfDeclBndr (ss_how_much ss) (occName tycon)
+
     add_bars []     = Outputable.empty
     add_bars (c:cs) = sep ((equals <+> c) : map (vbar <+>) cs)
 
@@ -801,8 +831,11 @@ pprIfaceDecl ss (IfaceClass { ifName  = clas
                             , ifBinders = binders
                             , ifBody = IfAbstractClass })
   = vcat [ pprClassRoles ss clas binders roles
-         , text "class" <+> pprIfaceDeclHead [] ss clas binders Nothing
-                                <+> pprFundeps fds ]
+         , pprClassStandaloneKindSig ss clas (mkIfaceTyConKind binders constraintIfaceKind)
+         , text "class" <+> pprIfaceDeclHead suppress_bndr_sig [] ss clas binders <+> pprFundeps fds ]
+  where
+    -- See Note [Suppressing binder signatures] in IfaceType
+    suppress_bndr_sig = SuppressBndrSig True
 
 pprIfaceDecl ss (IfaceClass { ifName  = clas
                             , ifRoles = roles
@@ -815,8 +848,8 @@ pprIfaceDecl ss (IfaceClass { ifName  = clas
                                 ifMinDef = minDef
                               }})
   = vcat [ pprClassRoles ss clas binders roles
-         , text "class" <+> pprIfaceDeclHead context ss clas binders Nothing
-                                <+> pprFundeps fds <+> pp_where
+         , pprClassStandaloneKindSig ss clas (mkIfaceTyConKind binders constraintIfaceKind)
+         , text "class" <+> pprIfaceDeclHead suppress_bndr_sig context ss clas binders <+> pprFundeps fds <+> pp_where
          , nest 2 (vcat [ vcat asocs, vcat dsigs
                         , ppShowAllSubs ss (pprMinDef minDef)])]
     where
@@ -842,31 +875,46 @@ pprIfaceDecl ss (IfaceClass { ifName  = clas
           (\_ def -> cparen (isLexSym def) (ppr def)) 0 minDef <+>
         text "#-}"
 
+      -- See Note [Suppressing binder signatures] in IfaceType
+      suppress_bndr_sig = SuppressBndrSig True
+
 pprIfaceDecl ss (IfaceSynonym { ifName    = tc
                               , ifBinders = binders
                               , ifSynRhs  = mono_ty
                               , ifResKind = res_kind})
-  = hang (text "type" <+> pprIfaceDeclHead [] ss tc binders Nothing <+> equals)
-       2 (sep [ pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau
-              , ppUnless (isIfaceLiftedTypeKind res_kind) (dcolon <+> ppr res_kind) ])
+  = vcat [ pprStandaloneKindSig name_doc (mkIfaceTyConKind binders res_kind)
+         , hang (text "type" <+> pprIfaceDeclHead suppress_bndr_sig [] ss tc binders <+> equals)
+           2 (sep [ pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau
+                  , ppUnless (isIfaceLiftedTypeKind res_kind) (dcolon <+> ppr res_kind) ])
+         ]
   where
     (tvs, theta, tau) = splitIfaceSigmaTy mono_ty
+    name_doc = pprPrefixIfDeclBndr (ss_how_much ss) (occName tc)
+
+    -- See Note [Suppressing binder signatures] in IfaceType
+    suppress_bndr_sig = SuppressBndrSig True
 
 pprIfaceDecl ss (IfaceFamily { ifName = tycon
                              , ifFamFlav = rhs, ifBinders = binders
                              , ifResKind = res_kind
                              , ifResVar = res_var, ifFamInj = inj })
   | IfaceDataFamilyTyCon <- rhs
-  = text "data family" <+> pprIfaceDeclHead [] ss tycon binders Nothing
+  = vcat [ pprStandaloneKindSig name_doc (mkIfaceTyConKind binders res_kind)
+         , text "data family" <+> pprIfaceDeclHead suppress_bndr_sig [] ss tycon binders
+         ]
 
   | otherwise
-  = hang (text "type family"
-            <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind)
-            <+> ppShowRhs ss (pp_where rhs))
-       2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs))
-    $$
-    nest 2 (ppShowRhs ss (pp_branches rhs))
+  = vcat [ pprStandaloneKindSig name_doc (mkIfaceTyConKind binders res_kind)
+         , hang (text "type family"
+                   <+> pprIfaceDeclHead suppress_bndr_sig [] ss tycon binders
+                   <+> ppShowRhs ss (pp_where rhs))
+              2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs))
+           $$
+           nest 2 (ppShowRhs ss (pp_branches rhs))
+         ]
   where
+    name_doc = pprPrefixIfDeclBndr (ss_how_much ss) (occName tycon)
+
     pp_where (IfaceClosedSynFamilyTyCon {}) = text "where"
     pp_where _                              = empty
 
@@ -900,6 +948,9 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon
         $$ ppShowIface ss (text "axiom" <+> ppr ax)
     pp_branches _ = Outputable.empty
 
+    -- See Note [Suppressing binder signatures] in IfaceType
+    suppress_bndr_sig = SuppressBndrSig True
+
 pprIfaceDecl _ (IfacePatSyn { ifName = name,
                               ifPatUnivBndrs = univ_bndrs, ifPatExBndrs = ex_bndrs,
                               ifPatProvCtxt = prov_ctxt, ifPatReqCtxt = req_ctxt,
@@ -948,6 +999,9 @@ pprRoles suppress_if tyCon bndrs roles
       in ppUnless (all suppress_if froles || null froles) $
          text "type role" <+> tyCon <+> hsep (map ppr froles)
 
+pprStandaloneKindSig :: SDoc -> IfaceType -> SDoc
+pprStandaloneKindSig tyCon ty = text "type" <+> tyCon <+> text "::" <+> ppr ty
+
 pprInfixIfDeclBndr :: ShowHowMuch -> OccName -> SDoc
 pprInfixIfDeclBndr (ShowSome _ (AltPpr (Just ppr_bndr))) name
   = pprInfixVar (isSymOcc name) (ppr_bndr name)
@@ -998,16 +1052,16 @@ pprIfaceTyConParent IfNoParent
 pprIfaceTyConParent (IfDataInstance _ tc tys)
   = pprIfaceTypeApp topPrec tc tys
 
-pprIfaceDeclHead :: IfaceContext -> ShowSub -> Name
+pprIfaceDeclHead :: SuppressBndrSig
+                 -> IfaceContext -> ShowSub -> Name
                  -> [IfaceTyConBinder]   -- of the tycon, for invisible-suppression
-                 -> Maybe IfaceKind
                  -> SDoc
-pprIfaceDeclHead context ss tc_occ bndrs m_res_kind
+pprIfaceDeclHead suppress_sig context ss tc_occ bndrs
   = sdocWithDynFlags $ \ dflags ->
     sep [ pprIfaceContextArr context
         , pprPrefixIfDeclBndr (ss_how_much ss) (occName tc_occ)
-          <+> pprIfaceTyConBinders (suppressIfaceInvisibles dflags bndrs bndrs)
-        , maybe empty (\res_kind -> dcolon <+> pprIfaceType res_kind) m_res_kind ]
+          <+> pprIfaceTyConBinders suppress_sig
+                (suppressIfaceInvisibles dflags bndrs bndrs) ]
 
 pprIfaceConDecl :: ShowSub -> Bool
                 -> IfaceTopBndr
index 9e7021b..e3362b7 100644 (file)
@@ -24,6 +24,7 @@ module IfaceType (
         IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..),
         ForallVisFlag(..), ShowForAllFlag(..),
         mkIfaceForAllTvBndr,
+        mkIfaceTyConKind,
 
         ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
         ifTyConBinderVar, ifTyConBinderName,
@@ -35,6 +36,8 @@ module IfaceType (
         appArgsIfaceTypes, appArgsIfaceTypesArgFlags,
 
         -- Printing
+        SuppressBndrSig(..),
+        UseBndrParens(..),
         pprIfaceType, pprParendIfaceType, pprPrecIfaceType,
         pprIfaceContext, pprIfaceContextArr,
         pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
@@ -44,6 +47,7 @@ module IfaceType (
         pprIfaceCoercion, pprParendIfaceCoercion,
         splitIfaceSigmaTy, pprIfaceTypeApp, pprUserIfaceForAll,
         pprIfaceCoTcApp, pprTyTcApp, pprIfacePrefixApp,
+        isIfaceTauType,
 
         suppressIfaceInvisibles,
         stripIfaceInvisVars,
@@ -106,6 +110,10 @@ ifaceBndrName :: IfaceBndr -> IfLclName
 ifaceBndrName (IfaceTvBndr bndr) = ifaceTvBndrName bndr
 ifaceBndrName (IfaceIdBndr bndr) = ifaceIdBndrName bndr
 
+ifaceBndrType :: IfaceBndr -> IfaceType
+ifaceBndrType (IfaceIdBndr (_, t)) = t
+ifaceBndrType (IfaceTvBndr (_, t)) = t
+
 type IfaceLamBndr = (IfaceBndr, IfaceOneShot)
 
 data IfaceOneShot    -- See Note [Preserve OneShotInfo] in CoreTicy
@@ -164,6 +172,15 @@ type IfaceForAllBndr  = VarBndr IfaceBndr ArgFlag
 mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr
 mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis
 
+-- | Build the 'tyConKind' from the binders and the result kind.
+-- Keep in sync with 'mkTyConKind' in types/TyCon.
+mkIfaceTyConKind :: [IfaceTyConBinder] -> IfaceKind -> IfaceKind
+mkIfaceTyConKind bndrs res_kind = foldr mk res_kind bndrs
+  where
+    mk :: IfaceTyConBinder -> IfaceKind -> IfaceKind
+    mk (Bndr tv (AnonTCB af))   k = IfaceFunTy af (ifaceBndrType tv) k
+    mk (Bndr tv (NamedTCB vis)) k = IfaceForAllTy (Bndr tv vis) k
+
 -- | Stores the arguments in a type application as a list.
 -- See @Note [Suppressing invisible arguments]@.
 data IfaceAppArgs
@@ -686,11 +703,17 @@ pprIfacePrefixApp ctxt_prec pp_fun pp_tys
   | otherwise   = maybeParen ctxt_prec appPrec $
                   hang pp_fun 2 (sep pp_tys)
 
+isIfaceTauType :: IfaceType -> Bool
+isIfaceTauType (IfaceForAllTy _ _) = False
+isIfaceTauType (IfaceFunTy InvisArg _ _) = False
+isIfaceTauType _ = True
+
 -- ----------------------------- Printing binders ------------------------------------
 
 instance Outputable IfaceBndr where
     ppr (IfaceIdBndr bndr) = pprIfaceIdBndr bndr
-    ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr False bndr
+    ppr (IfaceTvBndr bndr) = char '@' <+> pprIfaceTvBndr bndr (SuppressBndrSig False)
+                                                              (UseBndrParens False)
 
 pprIfaceBndrs :: [IfaceBndr] -> SDoc
 pprIfaceBndrs bs = sep (map ppr bs)
@@ -702,31 +725,60 @@ pprIfaceLamBndr (b, IfaceOneShot)   = ppr b <> text "[OneShot]"
 pprIfaceIdBndr :: IfaceIdBndr -> SDoc
 pprIfaceIdBndr (name, ty) = parens (ppr name <+> dcolon <+> ppr ty)
 
-pprIfaceTvBndr :: Bool -> IfaceTvBndr -> SDoc
-pprIfaceTvBndr use_parens (tv, ki)
+{- Note [Suppressing binder signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When printing the binders in a 'forall', we want to keep the kind annotations:
+
+    forall (a :: k). blah
+              ^^^^
+              good
+
+On the other hand, when we print the binders of a data declaration in :info,
+the kind information would be redundant due to the standalone kind signature:
+
+   type F :: Symbol -> Type
+   type F (s :: Symbol) = blah
+             ^^^^^^^^^
+             redundant
+
+Here we'd like to omit the kind annotation:
+
+   type F :: Symbol -> Type
+   type F s = blah
+-}
+
+-- | Do we want to suppress kind annotations on binders?
+-- See Note [Suppressing binder signatures]
+newtype SuppressBndrSig = SuppressBndrSig Bool
+
+newtype UseBndrParens = UseBndrParens Bool
+
+pprIfaceTvBndr :: IfaceTvBndr -> SuppressBndrSig -> UseBndrParens -> SDoc
+pprIfaceTvBndr (tv, ki) (SuppressBndrSig suppress_sig) (UseBndrParens use_parens)
+  | suppress_sig             = ppr tv
   | isIfaceLiftedTypeKind ki = ppr tv
   | otherwise                = maybe_parens (ppr tv <+> dcolon <+> ppr ki)
   where
     maybe_parens | use_parens = parens
                  | otherwise  = id
 
-pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
-pprIfaceTyConBinders = sep . map go
+pprIfaceTyConBinders :: SuppressBndrSig -> [IfaceTyConBinder] -> SDoc
+pprIfaceTyConBinders suppress_sig = sep . map go
   where
     go :: IfaceTyConBinder -> SDoc
     go (Bndr (IfaceIdBndr bndr) _) = pprIfaceIdBndr bndr
     go (Bndr (IfaceTvBndr bndr) vis) =
       -- See Note [Pretty-printing invisible arguments]
       case vis of
-        AnonTCB  VisArg    -> ppr_bndr True
-        AnonTCB  InvisArg  -> char '@' <> braces (ppr_bndr False)
+        AnonTCB  VisArg    -> ppr_bndr (UseBndrParens True)
+        AnonTCB  InvisArg  -> char '@' <> braces (ppr_bndr (UseBndrParens False))
           -- The above case is rare. (See Note [AnonTCB InvisArg] in TyCon.)
           -- Should we print these differently?
-        NamedTCB Required  -> ppr_bndr True
-        NamedTCB Specified -> char '@' <> ppr_bndr True
-        NamedTCB Inferred  -> char '@' <> braces (ppr_bndr False)
+        NamedTCB Required  -> ppr_bndr (UseBndrParens True)
+        NamedTCB Specified -> char '@' <> ppr_bndr (UseBndrParens True)
+        NamedTCB Inferred  -> char '@' <> braces (ppr_bndr (UseBndrParens False))
       where
-        ppr_bndr use_parens = pprIfaceTvBndr use_parens bndr
+        ppr_bndr = pprIfaceTvBndr bndr suppress_sig
 
 instance Binary IfaceBndr where
     put_ bh (IfaceIdBndr aa) = do
@@ -1045,13 +1097,19 @@ pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
 pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
 
 pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
-pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) Inferred)
-  = sdocWithDynFlags $ \dflags ->
-                          if gopt Opt_PrintExplicitForalls dflags
-                          then braces $ pprIfaceTvBndr False tv
-                          else pprIfaceTvBndr True tv
-pprIfaceForAllBndr (Bndr (IfaceTvBndr tv) _)  = pprIfaceTvBndr True tv
-pprIfaceForAllBndr (Bndr (IfaceIdBndr idv) _) = pprIfaceIdBndr idv
+pprIfaceForAllBndr bndr =
+  case bndr of
+    Bndr (IfaceTvBndr tv) Inferred ->
+      sdocWithDynFlags $ \dflags ->
+        if gopt Opt_PrintExplicitForalls dflags
+        then braces $ pprIfaceTvBndr tv suppress_sig (UseBndrParens False)
+        else pprIfaceTvBndr tv suppress_sig (UseBndrParens True)
+    Bndr (IfaceTvBndr tv) _ ->
+      pprIfaceTvBndr tv suppress_sig (UseBndrParens True)
+    Bndr (IfaceIdBndr idv) _ -> pprIfaceIdBndr idv
+  where
+    -- See Note [Suppressing binder signatures] in IfaceType
+    suppress_sig = SuppressBndrSig False
 
 pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
 pprIfaceForAllCoBndr (tv, kind_co)
index 02499d2..07b266d 100644 (file)
@@ -4526,6 +4526,7 @@ xFlagsDeps = [
   flagSpec' "TemplateHaskell"                 LangExt.TemplateHaskell
                                               checkTemplateHaskellOk,
   flagSpec "TemplateHaskellQuotes"            LangExt.TemplateHaskellQuotes,
+  flagSpec "StandaloneKindSignatures"         LangExt.StandaloneKindSignatures,
   flagSpec "TraditionalRecordSyntax"          LangExt.TraditionalRecordSyntax,
   flagSpec "TransformListComp"                LangExt.TransformListComp,
   flagSpec "TupleSections"                    LangExt.TupleSections,
@@ -4653,6 +4654,9 @@ impliedXFlags
     , (LangExt.TypeInType,       turnOn, LangExt.PolyKinds)
     , (LangExt.TypeInType,       turnOn, LangExt.KindSignatures)
 
+    -- Standalone kind signatures are a replacement for CUSKs.
+    , (LangExt.StandaloneKindSignatures, turnOff, LangExt.CUSKs)
+
     -- AutoDeriveTypeable is not very useful without DeriveDataTypeable
     , (LangExt.AutoDeriveTypeable, turnOn, LangExt.DeriveDataTypeable)
 
index 276fcb1..f32ce4a 100644 (file)
@@ -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)
index 538c20c..0686f66 100644 (file)
@@ -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
index 58f9af7..0eedeee 100644 (file)
@@ -68,7 +68,7 @@ templateHaskellNames = [
     -- Dec
     funDName, valDName, dataDName, newtypeDName, tySynDName,
     classDName, instanceWithOverlapDName,
-    standaloneDerivWithStrategyDName, sigDName, forImpDName,
+    standaloneDerivWithStrategyDName, sigDName, kiSigDName, forImpDName,
     pragInlDName, pragSpecDName, pragSpecInlDName, pragSpecInstDName,
     pragRuleDName, pragCompleteDName, pragAnnDName, defaultSigDName,
     dataFamilyDName, openTypeFamilyDName, closedTypeFamilyDName,
@@ -341,7 +341,7 @@ recSName    = libFun (fsLit "recS")    recSIdKey
 
 -- data Dec = ...
 funDName, valDName, dataDName, newtypeDName, tySynDName, classDName,
-    instanceWithOverlapDName, sigDName, forImpDName, pragInlDName,
+    instanceWithOverlapDName, sigDName, kiSigDName, forImpDName, pragInlDName,
     pragSpecDName, pragSpecInlDName, pragSpecInstDName, pragRuleDName,
     pragAnnDName, standaloneDerivWithStrategyDName, defaultSigDName,
     dataInstDName, newtypeInstDName, tySynInstDName, dataFamilyDName,
@@ -357,6 +357,7 @@ classDName                       = libFun (fsLit "classD")
 instanceWithOverlapDName         = libFun (fsLit "instanceWithOverlapD")         instanceWithOverlapDIdKey
 standaloneDerivWithStrategyDName = libFun (fsLit "standaloneDerivWithStrategyD") standaloneDerivWithStrategyDIdKey
 sigDName                         = libFun (fsLit "sigD")                         sigDIdKey
+kiSigDName                       = libFun (fsLit "kiSigD")                       kiSigDIdKey
 defaultSigDName                  = libFun (fsLit "defaultSigD")                  defaultSigDIdKey
 forImpDName                      = libFun (fsLit "forImpD")                      forImpDIdKey
 pragInlDName                     = libFun (fsLit "pragInlD")                     pragInlDIdKey
@@ -868,7 +869,8 @@ funDIdKey, valDIdKey, dataDIdKey, newtypeDIdKey, tySynDIdKey, classDIdKey,
     openTypeFamilyDIdKey, closedTypeFamilyDIdKey, dataInstDIdKey,
     newtypeInstDIdKey, tySynInstDIdKey, standaloneDerivWithStrategyDIdKey,
     infixLDIdKey, infixRDIdKey, infixNDIdKey, roleAnnotDIdKey, patSynDIdKey,
-    patSynSigDIdKey, pragCompleteDIdKey, implicitParamBindDIdKey :: Unique
+    patSynSigDIdKey, pragCompleteDIdKey, implicitParamBindDIdKey,
+    kiSigDIdKey :: Unique
 funDIdKey                         = mkPreludeMiscIdUnique 320
 valDIdKey                         = mkPreludeMiscIdUnique 321
 dataDIdKey                        = mkPreludeMiscIdUnique 322
@@ -901,6 +903,7 @@ patSynDIdKey                      = mkPreludeMiscIdUnique 348
 patSynSigDIdKey                   = mkPreludeMiscIdUnique 349
 pragCompleteDIdKey                = mkPreludeMiscIdUnique 350
 implicitParamBindDIdKey           = mkPreludeMiscIdUnique 351
+kiSigDIdKey                       = mkPreludeMiscIdUnique 352
 
 -- type Cxt = ...
 cxtIdKey :: Unique
index 4b0141a..be4bfe1 100644 (file)
@@ -93,7 +93,7 @@ module TysWiredIn (
         -- * Kinds
         typeNatKindCon, typeNatKind, typeSymbolKindCon, typeSymbolKind,
         isLiftedTypeKindTyConName, liftedTypeKind, constraintKind,
-        liftedTypeKindTyCon, constraintKindTyCon,
+        liftedTypeKindTyCon, constraintKindTyCon,  constraintKindTyConName,
         liftedTypeKindTyConName,
 
         -- * Equality predicates
@@ -406,7 +406,7 @@ makeRecoveryTyCon :: TyCon -> TyCon
 makeRecoveryTyCon tc
   = mkTcTyCon (tyConName tc)
               bndrs res_kind
-              []               -- No scoped vars
+              noTcTyConScopedTyVars
               True             -- Fully generalised
               flavour          -- Keep old flavour
   where
index 811a81b..56caee1 100644 (file)
@@ -973,7 +973,7 @@ renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
         ; when (is_deflt && not defaultSigs_on) $
           addErr (defaultSigErr sig)
         ; new_v <- mapM (lookupSigOccRn ctxt sig) vs
-        ; (new_ty, fvs) <- rnHsSigType ty_ctxt ty
+        ; (new_ty, fvs) <- rnHsSigType ty_ctxt TypeLevel ty
         ; return (ClassOpSig noExtField is_deflt new_v new_ty, fvs) }
   where
     (v1:_) = vs
@@ -981,7 +981,7 @@ renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
                           <+> quotes (ppr v1))
 
 renameSig _ (SpecInstSig _ src ty)
-  = do  { (new_ty, fvs) <- rnHsSigType SpecInstSigCtx ty
+  = do  { (new_ty, fvs) <- rnHsSigType SpecInstSigCtx TypeLevel ty
         ; return (SpecInstSig noExtField src new_ty,fvs) }
 
 -- {-# SPECIALISE #-} pragmas can refer to imported Ids
@@ -998,7 +998,7 @@ renameSig ctxt sig@(SpecSig _ v tys inl)
     ty_ctxt = GenericCtx (text "a SPECIALISE signature for"
                           <+> quotes (ppr v))
     do_one (tys,fvs) ty
-      = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt ty
+      = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel ty
            ; return ( new_ty:tys, fvs_ty `plusFV` fvs) }
 
 renameSig ctxt sig@(InlineSig _ v s)
@@ -1015,7 +1015,7 @@ renameSig ctxt sig@(MinimalSig _ s (L l bf))
 
 renameSig ctxt sig@(PatSynSig _ vs ty)
   = do  { new_vs <- mapM (lookupSigOccRn ctxt sig) vs
-        ; (ty', fvs) <- rnHsSigType ty_ctxt ty
+        ; (ty', fvs) <- rnHsSigType ty_ctxt TypeLevel ty
         ; return (PatSynSig noExtField new_vs ty', fvs) }
   where
     ty_ctxt = GenericCtx (text "a pattern synonym signature for"
index 229c66f..1ab80e7 100644 (file)
@@ -70,8 +70,9 @@ import Control.Arrow ( first )
 import Data.List ( mapAccumL )
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
-import Data.Maybe ( isNothing, isJust, fromMaybe )
+import Data.Maybe ( isNothing, fromMaybe, mapMaybe )
 import qualified Data.Set as Set ( difference, fromList, toList, null )
+import Data.Function ( on )
 
 {- | @rnSourceDecl@ "renames" declarations.
 It simultaneously performs dependency analysis and precedence parsing.
@@ -370,7 +371,7 @@ rnHsForeignDecl :: ForeignDecl GhcPs -> RnM (ForeignDecl GhcRn, FreeVars)
 rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec })
   = do { topEnv :: HscEnv <- getTopEnv
        ; name' <- lookupLocatedTopBndrRn name
-       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) ty
+       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty
 
         -- Mark any PackageTarget style imports as coming from the current package
        ; let unitId = thisPackage $ hsc_dflags topEnv
@@ -382,7 +383,7 @@ rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec })
 
 rnHsForeignDecl (ForeignExport { fd_name = name, fd_sig_ty = ty, fd_fe = spec })
   = do { name' <- lookupLocatedOccRn name
-       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) ty
+       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty
        ; return (ForeignExport { fd_e_ext = noExtField
                                , fd_name = name', fd_sig_ty = ty'
                                , fd_fe = spec }
@@ -607,7 +608,7 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
                            , cid_overlap_mode = oflag
                            , cid_datafam_insts = adts })
   = do { (inst_ty', inst_fvs)
-           <- rnHsSigType (GenericCtx $ text "an instance declaration") inst_ty
+           <- rnHsSigType (GenericCtx $ text "an instance declaration") TypeLevel inst_ty
        ; let (ktv_names, _, head_ty') = splitLHsInstDeclTy inst_ty'
        ; cls <-
            case hsTyGetAppHead_maybe head_ty' of
@@ -1288,17 +1289,17 @@ rnTyClDecls :: [TyClGroup GhcPs]
 -- Rename the declarations and do dependency analysis on them
 rnTyClDecls tycl_ds
   = do { -- Rename the type/class, instance, and role declaraations
-         tycls_w_fvs <- mapM (wrapLocFstM rnTyClDecl)
-                             (tyClGroupTyClDecls tycl_ds)
+       ; tycls_w_fvs <- mapM (wrapLocFstM rnTyClDecl) (tyClGroupTyClDecls tycl_ds)
        ; let tc_names = mkNameSet (map (tcdName . unLoc . fst) tycls_w_fvs)
-
+       ; kisigs_w_fvs <- rnStandaloneKindSignatures tc_names (tyClGroupKindSigs tycl_ds)
        ; instds_w_fvs <- mapM (wrapLocFstM rnSrcInstDecl) (tyClGroupInstDecls tycl_ds)
        ; role_annots  <- rnRoleAnnots tc_names (tyClGroupRoleDecls tycl_ds)
 
        -- Do SCC analysis on the type/class decls
        ; rdr_env <- getGlobalRdrEnv
-       ; let tycl_sccs = depAnalTyClDecls rdr_env tycls_w_fvs
+       ; let tycl_sccs = depAnalTyClDecls rdr_env kisig_fv_env tycls_w_fvs
              role_annot_env = mkRoleAnnotEnv role_annots
+             (kisig_env, kisig_fv_env) = mkKindSig_fv_env kisigs_w_fvs
 
              inst_ds_map = mkInstDeclFreeVarsMap rdr_env tc_names instds_w_fvs
              (init_inst_ds, rest_inst_ds) = getInsts [] inst_ds_map
@@ -1307,15 +1308,16 @@ rnTyClDecls tycl_ds
                | null init_inst_ds = []
                | otherwise = [TyClGroup { group_ext    = noExtField
                                         , group_tyclds = []
+                                        , group_kisigs = []
                                         , group_roles  = []
                                         , group_instds = init_inst_ds }]
 
              (final_inst_ds, groups)
-                = mapAccumL (mk_group role_annot_env) rest_inst_ds tycl_sccs
-
+                = mapAccumL (mk_group role_annot_env kisig_env) rest_inst_ds tycl_sccs
 
-             all_fvs = plusFV (foldr (plusFV . snd) emptyFVs tycls_w_fvs)
-                              (foldr (plusFV . snd) emptyFVs instds_w_fvs)
+             all_fvs = foldr (plusFV . snd) emptyFVs tycls_w_fvs  `plusFV`
+                       foldr (plusFV . snd) emptyFVs instds_w_fvs `plusFV`
+                       foldr (plusFV . snd) emptyFVs kisigs_w_fvs
 
              all_groups = first_group ++ groups
 
@@ -1326,32 +1328,91 @@ rnTyClDecls tycl_ds
        ; return (all_groups, all_fvs) }
   where
     mk_group :: RoleAnnotEnv
+             -> KindSigEnv
              -> InstDeclFreeVarsMap
              -> SCC (LTyClDecl GhcRn)
              -> (InstDeclFreeVarsMap, TyClGroup GhcRn)
-    mk_group role_env inst_map scc
+    mk_group role_env kisig_env inst_map scc
       = (inst_map', group)
       where
         tycl_ds              = flattenSCC scc
         bndrs                = map (tcdName . unLoc) tycl_ds
         roles                = getRoleAnnots bndrs role_env
+        kisigs               = getKindSigs   bndrs kisig_env
         (inst_ds, inst_map') = getInsts      bndrs inst_map
         group = TyClGroup { group_ext    = noExtField
                           , group_tyclds = tycl_ds
+                          , group_kisigs = kisigs
                           , group_roles  = roles
                           , group_instds = inst_ds }
 
+-- | Free variables of standalone kind signatures.
+newtype KindSig_FV_Env = KindSig_FV_Env (NameEnv FreeVars)
+
+lookupKindSig_FV_Env :: KindSig_FV_Env -> Name -> FreeVars
+lookupKindSig_FV_Env (KindSig_FV_Env e) name
+  = fromMaybe emptyFVs (lookupNameEnv e name)
+
+-- | Standalone kind signatures.
+type KindSigEnv = NameEnv (LStandaloneKindSig GhcRn)
+
+mkKindSig_fv_env :: [(LStandaloneKindSig GhcRn, FreeVars)] -> (KindSigEnv, KindSig_FV_Env)
+mkKindSig_fv_env kisigs_w_fvs = (kisig_env, kisig_fv_env)
+  where
+    kisig_env = mapNameEnv fst compound_env
+    kisig_fv_env = KindSig_FV_Env (mapNameEnv snd compound_env)
+    compound_env :: NameEnv (LStandaloneKindSig GhcRn, FreeVars)
+      = mkNameEnvWith (standaloneKindSigName . unLoc . fst) kisigs_w_fvs
+
+getKindSigs :: [Name] -> KindSigEnv -> [LStandaloneKindSig GhcRn]
+getKindSigs bndrs kisig_env = mapMaybe (lookupNameEnv kisig_env) bndrs
+
+rnStandaloneKindSignatures
+  :: NameSet  -- names of types and classes in the current TyClGroup
+  -> [LStandaloneKindSig GhcPs]
+  -> RnM [(LStandaloneKindSig GhcRn, FreeVars)]
+rnStandaloneKindSignatures tc_names kisigs
+  = do { let (no_dups, dup_kisigs) = removeDups (compare `on` get_name) kisigs
+             get_name = standaloneKindSigName . unLoc
+       ; mapM_ dupKindSig_Err dup_kisigs
+       ; mapM (wrapLocFstM (rnStandaloneKindSignature tc_names)) no_dups
+       }
+
+rnStandaloneKindSignature
+  :: NameSet  -- names of types and classes in the current TyClGroup
+  -> StandaloneKindSig GhcPs
+  -> RnM (StandaloneKindSig GhcRn, FreeVars)
+rnStandaloneKindSignature tc_names (StandaloneKindSig _ v ki)
+  = do  { standalone_ki_sig_ok <- xoptM LangExt.StandaloneKindSignatures
+        ; unless standalone_ki_sig_ok $ addErr standaloneKiSigErr
+        ; new_v <- lookupSigCtxtOccRn (TopSigCtxt tc_names) (text "standalone kind signature") v
+        ; let doc = StandaloneKindSigCtx (ppr v)
+        ; (new_ki, fvs) <- rnHsSigType doc KindLevel ki
+        ; return (StandaloneKindSig noExtField new_v new_ki, fvs)
+        }
+  where
+    standaloneKiSigErr :: SDoc
+    standaloneKiSigErr =
+      hang (text "Illegal standalone kind signature")
+         2 (text "Did you mean to enable StandaloneKindSignatures?")
+rnStandaloneKindSignature _ (XStandaloneKindSig nec) = noExtCon nec
 
 depAnalTyClDecls :: GlobalRdrEnv
+                 -> KindSig_FV_Env
                  -> [(LTyClDecl GhcRn, FreeVars)]
                  -> [SCC (LTyClDecl GhcRn)]
 -- See Note [Dependency analysis of type, class, and instance decls]
-depAnalTyClDecls rdr_env ds_w_fvs
+depAnalTyClDecls rdr_env kisig_fv_env ds_w_fvs
   = stronglyConnCompFromEdgedVerticesUniq edges
   where
     edges :: [ Node Name (LTyClDecl GhcRn) ]
-    edges = [ DigraphNode d (tcdName (unLoc d)) (map (getParent rdr_env) (nonDetEltsUniqSet fvs))
-            | (d, fvs) <- ds_w_fvs ]
+    edges = [ DigraphNode d name (map (getParent rdr_env) (nonDetEltsUniqSet deps))
+            | (d, fvs) <- ds_w_fvs,
+              let { name = tcdName (unLoc d)
+                  ; kisig_fvs = lookupKindSig_FV_Env kisig_fv_env name
+                  ; deps = fvs `plusFV` kisig_fvs
+                  }
+            ]
             -- It's OK to use nonDetEltsUFM here as
             -- stronglyConnCompFromEdgedVertices is still deterministic
             -- even if the edges are in nondeterministic order as explained
@@ -1391,9 +1452,8 @@ rnRoleAnnots :: NameSet
 rnRoleAnnots tc_names role_annots
   = do {  -- Check for duplicates *before* renaming, to avoid
           -- lumping together all the unboundNames
-         let (no_dups, dup_annots) = removeDups role_annots_cmp role_annots
-             role_annots_cmp (dL->L _ annot1) (dL->L _ annot2)
-               = roleAnnotDeclName annot1 `compare` roleAnnotDeclName annot2
+         let (no_dups, dup_annots) = removeDups (compare `on` get_name) role_annots
+             get_name = roleAnnotDeclName . unLoc
        ; mapM_ dupRoleAnnotErr dup_annots
        ; mapM (wrapLocM rn_role_annot1) no_dups }
   where
@@ -1421,6 +1481,20 @@ dupRoleAnnotErr list
 
       cmp_annot (dL->L loc1 _) (dL->L loc2 _) = loc1 `compare` loc2
 
+dupKindSig_Err :: NonEmpty (LStandaloneKindSig GhcPs) -> RnM ()
+dupKindSig_Err list
+  = addErrAt loc $
+    hang (text "Duplicate standalone kind signatures for" <+>
+          quotes (ppr $ standaloneKindSigName first_decl) <> colon)
+       2 (vcat $ map pp_kisig $ NE.toList sorted_list)
+    where
+      sorted_list = NE.sortBy cmp_loc list
+      ((dL->L loc first_decl) :| _) = sorted_list
+
+      pp_kisig (dL->L loc decl) =
+        hang (ppr decl) 4 (text "-- written at" <+> ppr loc)
+
+      cmp_loc (dL->L loc1 _) (dL->L loc2 _) = loc1 `compare` loc2
 
 {- Note [Role annotations in the renamer]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1495,12 +1569,11 @@ getInsts bndrs inst_decl_map
 rnTyClDecl :: TyClDecl GhcPs
            -> RnM (TyClDecl GhcRn, FreeVars)
 
--- All flavours of type family declarations ("type family", "newtype family",
--- and "data family"), both top level and (for an associated type)
--- in a class decl
-rnTyClDecl (FamDecl { tcdFam = decl })
-  = do { (decl', fvs) <- rnFamDecl Nothing decl
-       ; return (FamDecl noExtField decl', fvs) }
+-- All flavours of top-level type family declarations ("type family", "newtype
+-- family", and "data family")
+rnTyClDecl (FamDecl { tcdFam = fam })
+  = do { (fam', fvs) <- rnFamDecl Nothing fam
+       ; return (FamDecl noExtField fam', fvs) }
 
 rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars,
                       tcdFixity = fixity, tcdRhs = rhs })
@@ -1515,9 +1588,7 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars,
                          , tcdRhs = rhs', tcdSExt = fvs }, fvs) } }
 
 -- "data", "newtype" declarations
--- both top level and (for an associated type) in an instance decl
-rnTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) =
-  panic "rnTyClDecl: DataDecl with XHsDataDefn"
+rnTyClDecl (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec
 rnTyClDecl (DataDecl
     { tcdLName = tycon, tcdTyVars = tyvars,
       tcdFixity = fixity,
@@ -1529,8 +1600,7 @@ rnTyClDecl (DataDecl
        ; traceRn "rntycl-data" (ppr tycon <+> ppr kvs)
        ; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' no_rhs_kvs ->
     do { (defn', fvs) <- rnDataDefn doc defn
-       ; cusk <- dataDeclHasCUSK
-           tyvars' new_or_data no_rhs_kvs (isJust kind_sig)
+       ; cusk <- data_decl_has_cusk tyvars' new_or_data no_rhs_kvs kind_sig
        ; let rn_info = DataDeclRn { tcdDataCusk = cusk
                                   , tcdFVs      = fvs }
        ; traceRn "rndata" (ppr tycon <+> ppr cusk <+> ppr no_rhs_kvs)
@@ -1608,19 +1678,17 @@ rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls,
 rnTyClDecl (XTyClDecl nec) = noExtCon nec
 
 -- Does the data type declaration include a CUSK?
-dataDeclHasCUSK :: LHsQTyVars pass -> NewOrData -> Bool -> Bool -> RnM Bool
-dataDeclHasCUSK tyvars new_or_data no_rhs_kvs has_kind_sig = do
+data_decl_has_cusk :: LHsQTyVars pass -> NewOrData -> Bool -> Maybe (LHsKind pass') -> RnM Bool
+data_decl_has_cusk tyvars new_or_data no_rhs_kvs kind_sig = do
   { -- See Note [Unlifted Newtypes and CUSKs], and for a broader
     -- picture, see Note [Implementation of UnliftedNewtypes].
   ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
   ; let non_cusk_newtype
           | NewType <- new_or_data =
-              unlifted_newtypes && not has_kind_sig
+              unlifted_newtypes && isNothing kind_sig
           | otherwise = False
     -- See Note [CUSKs: complete user-supplied kind signatures] in GHC.Hs.Decls
-  ; cusks_enabled <- xoptM LangExt.CUSKs
-  ; return $ cusks_enabled && hsTvbAllKinded tyvars &&
-             no_rhs_kvs && not non_cusk_newtype
+  ; return $ hsTvbAllKinded tyvars && no_rhs_kvs && not non_cusk_newtype
   }
 
 {- Note [Unlifted Newtypes and CUSKs]
@@ -1724,7 +1792,7 @@ rnLHsDerivingClause doc
                               , deriv_clause_strategy = dcs
                               , deriv_clause_tys = (dL->L loc' dct) }))
   = do { (dcs', dct', fvs)
-           <- rnLDerivStrategy doc dcs $ mapFvRn (rnHsSigType doc) dct
+           <- rnLDerivStrategy doc dcs $ mapFvRn (rnHsSigType doc TypeLevel) dct
        ; warnNoDerivStrat dcs' loc
        ; pure ( cL loc (HsDerivingClause { deriv_clause_ext = noExtField
                                          , deriv_clause_strategy = dcs'
@@ -1766,7 +1834,7 @@ rnLDerivStrategy doc mds thing_inside
         AnyclassStrategy -> boring_case AnyclassStrategy
         NewtypeStrategy  -> boring_case NewtypeStrategy
         ViaStrategy via_ty ->
-          do (via_ty', fvs1) <- rnHsSigType doc via_ty
+          do (via_ty', fvs1) <- rnHsSigType doc TypeLevel via_ty
              let HsIB { hsib_ext  = via_imp_tvs
                       , hsib_body = via_body } = via_ty'
                  (via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body
@@ -2249,6 +2317,11 @@ add gp@(HsGroup {hs_tyclds = ts, hs_fixds = fs}) l (TyClD _ d) ds
 -- Signatures: fixity sigs go a different place than all others
 add gp@(HsGroup {hs_fixds = ts}) l (SigD _ (FixSig _ f)) ds
   = addl (gp {hs_fixds = cL l f : ts}) ds
+
+-- Standalone kind signatures: added to the TyClGroup
+add gp@(HsGroup {hs_tyclds = ts}) l (KindSigD _ s) ds
+  = addl (gp {hs_tyclds = add_kisig (cL l s) ts}) ds
+
 add gp@(HsGroup {hs_valds = ts}) l (SigD _ d) ds
   = addl (gp {hs_valds = add_sig (cL l d) ts}) ds
 
@@ -2289,6 +2362,7 @@ add_tycld :: LTyClDecl (GhcPass p) -> [TyClGroup (GhcPass p)]
           -> [TyClGroup (GhcPass p)]
 add_tycld d []       = [TyClGroup { group_ext    = noExtField
                                   , group_tyclds = [d]
+                                  , group_kisigs = []
                                   , group_roles  = []
                                   , group_instds = []
                                   }
@@ -2301,6 +2375,7 @@ add_instd :: LInstDecl (GhcPass p) -> [TyClGroup (GhcPass p)]
           -> [TyClGroup (GhcPass p)]
 add_instd d []       = [TyClGroup { group_ext    = noExtField
                                   , group_tyclds = []
+                                  , group_kisigs = []
                                   , group_roles  = []
                                   , group_instds = [d]
                                   }
@@ -2313,6 +2388,7 @@ add_role_annot :: LRoleAnnotDecl (GhcPass p) -> [TyClGroup (GhcPass p)]
                -> [TyClGroup (GhcPass p)]
 add_role_annot d [] = [TyClGroup { group_ext    = noExtField
                                  , group_tyclds = []
+                                 , group_kisigs = []
                                  , group_roles  = [d]
                                  , group_instds = []
                                  }
@@ -2321,6 +2397,19 @@ add_role_annot d (tycls@(TyClGroup { group_roles = roles }) : rest)
   = tycls { group_roles = d : roles } : rest
 add_role_annot _ (XTyClGroup nec: _) = noExtCon nec
 
+add_kisig :: LStandaloneKindSig (GhcPass p)
+         -> [TyClGroup (GhcPass p)] -> [TyClGroup (GhcPass p)]
+add_kisig d [] = [TyClGroup { group_ext    = noExtField
+                            , group_tyclds = []
+                            , group_kisigs = [d]
+                            , group_roles  = []
+                            , group_instds = []
+                            }
+                 ]
+add_kisig d (tycls@(TyClGroup { group_kisigs = kisigs }) : rest)
+  = tycls { group_kisigs = d : kisigs } : rest
+add_kisig _ (XTyClGroup nec : _) = noExtCon nec
+
 add_bind :: LHsBind a -> HsValBinds a -> HsValBinds a
 add_bind b (ValBinds x bs sigs) = ValBinds x (bs `snocBag` b) sigs
 add_bind _ (XValBindsLR {})     = panic "RdrHsSyn:add_bind"
index e982e72..5f0a1c6 100644 (file)
@@ -242,6 +242,7 @@ extraConstraintWildCardsAllowed env
       TypeSigCtx {}       -> True
       ExprWithTySigCtx {} -> True
       DerivDeclCtx {}     -> True
+      StandaloneKindSigCtx {} -> False  -- See Note [Wildcards in standalone kind signatures] in GHC/Hs/Decls
       _                   -> False
 
 -- | Finds free type and kind variables in a type,
@@ -295,19 +296,22 @@ of the HsWildCardBndrs structure, and we are done.
 *                                                       *
 ****************************************************** -}
 
-rnHsSigType :: HsDocContext -> LHsSigType GhcPs
+rnHsSigType :: HsDocContext
+            -> TypeOrKind
+            -> LHsSigType GhcPs
             -> RnM (LHsSigType GhcRn, FreeVars)
 -- Used for source-language type signatures
 -- that cannot have wildcards
-rnHsSigType ctx (HsIB { hsib_body = hs_ty })
+rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
        ; vars <- extractFilteredRdrTyVarsDups hs_ty
        ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars ->
-    do { (body', fvs) <- rnLHsType ctx hs_ty
+    do { (body', fvs) <- rnLHsTyKi (mkTyKiEnv ctx level RnTypeBody) hs_ty
+
        ; return ( HsIB { hsib_ext = vars
                        , hsib_body = body' }
                 , fvs ) } }
-rnHsSigType _ (XHsImplicitBndrs nec) = noExtCon nec
+rnHsSigType _ (XHsImplicitBndrs nec) = noExtCon nec
 
 rnImplicitBndrs :: Bool    -- True <=> bring into scope any free type variables
                            -- E.g.  f :: forall a. a->b
@@ -563,9 +567,9 @@ rnHsTyKi env t@(HsKindSig _ ty k)
   = do { checkPolyKinds env t
        ; kind_sigs_ok <- xoptM LangExt.KindSignatures
        ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
-       ; (ty', fvs1) <- rnLHsTyKi env ty
-       ; (k', fvs2)  <- rnLHsTyKi (env { rtke_level = KindLevel }) k
-       ; return (HsKindSig noExtField ty' k', fvs1 `plusFV` fvs2) }
+       ; (ty', lhs_fvs) <- rnLHsTyKi env ty
+       ; (k', sig_fvs)  <- rnLHsTyKi (env { rtke_level = KindLevel }) k
+       ; return (HsKindSig noExtField ty' k', lhs_fvs `plusFV` sig_fvs) }
 
 -- Unboxed tuples are allowed to have poly-typed arguments.  These
 -- sometimes crop up as a result of CPR worker-wrappering dictionaries.
@@ -734,6 +738,7 @@ wildCardsAllowed env
        FamPatCtx {}        -> True   -- Not named wildcards though
        GHCiCtx {}          -> True
        HsTypeCtx {}        -> True
+       StandaloneKindSigCtx {} -> False  -- See Note [Wildcards in standalone kind signatures] in GHC/Hs/Decls
        _                   -> False
 
 
index 6678ad6..0da8e30 100644 (file)
@@ -458,6 +458,7 @@ checkTupSize tup_size
 --          Merge TcType.UserTypeContext in to it.
 data HsDocContext
   = TypeSigCtx SDoc
+  | StandaloneKindSigCtx SDoc
   | PatCtx
   | SpecInstSigCtx
   | DefaultDeclCtx
@@ -487,6 +488,7 @@ inHsDocContext ctxt = text "In" <+> pprHsDocContext ctxt
 pprHsDocContext :: HsDocContext -> SDoc
 pprHsDocContext (GenericCtx doc)      = doc
 pprHsDocContext (TypeSigCtx doc)      = text "the type signature for" <+> doc
+pprHsDocContext (StandaloneKindSigCtx doc) = text "the standalone kind signature for" <+> doc
 pprHsDocContext PatCtx                = text "a pattern type-signature"
 pprHsDocContext SpecInstSigCtx        = text "a SPECIALISE instance pragma"
 pprHsDocContext DefaultDeclCtx        = text "a `default' declaration"
index d2b32e7..d74b38c 100644 (file)
@@ -195,6 +195,8 @@ both of them.  So we gather defs/uses from deriving just like anything else.
 data DerivInfo = DerivInfo { di_rep_tc  :: TyCon
                              -- ^ The data tycon for normal datatypes,
                              -- or the *representation* tycon for data families
+                           , di_scoped_tvs :: ![(Name,TyVar)]
+                             -- ^ Variables that scope over the deriving clause.
                            , di_clauses :: [LHsDerivingClause GhcRn]
                            , di_ctxt    :: SDoc -- ^ error context
                            }
@@ -493,8 +495,10 @@ makeDerivSpecs :: Bool
                -> TcM [EarlyDerivSpec]
 makeDerivSpecs is_boot deriv_infos deriv_decls
   = do  { eqns1 <- sequenceA
-                     [ deriveClause rep_tc dcs preds err_ctxt
-                     | DerivInfo { di_rep_tc = rep_tc, di_clauses = clauses
+                     [ deriveClause rep_tc scoped_tvs dcs preds err_ctxt
+                     | DerivInfo { di_rep_tc = rep_tc
+                                 , di_scoped_tvs = scoped_tvs
+                                 , di_clauses = clauses
                                  , di_ctxt = err_ctxt } <- deriv_infos
                      , L _ (HsDerivingClause { deriv_clause_strategy = dcs
                                              , deriv_clause_tys = L _ preds })
@@ -515,17 +519,21 @@ makeDerivSpecs is_boot deriv_infos deriv_decls
 
 ------------------------------------------------------------------
 -- | Process the derived classes in a single @deriving@ clause.
-deriveClause :: TyCon -> Maybe (LDerivStrategy GhcRn)
+deriveClause :: TyCon
+             -> [(Name, TcTyVar)]  -- Scoped type variables taken from tcTyConScopedTyVars
+                                   -- See Note [Scoped tyvars in a TcTyCon] in types/TyCon
+             -> Maybe (LDerivStrategy GhcRn)
              -> [LHsSigType GhcRn] -> SDoc
              -> TcM [EarlyDerivSpec]
-deriveClause rep_tc mb_lderiv_strat deriv_preds err_ctxt
+deriveClause rep_tc scoped_tvs mb_lderiv_strat deriv_preds err_ctxt
   = addErrCtxt err_ctxt $ do
       traceTc "deriveClause" $ vcat
         [ text "tvs"             <+> ppr tvs
+        , text "scoped_tvs"      <+> ppr scoped_tvs
         , text "tc"              <+> ppr tc
         , text "tys"             <+> ppr tys
         , text "mb_lderiv_strat" <+> ppr mb_lderiv_strat ]
-      tcExtendTyVarEnv tvs $ do
+      tcExtendNameTyVarEnv scoped_tvs $ do
         (mb_lderiv_strat', via_tvs) <- tcDerivStrategy mb_lderiv_strat
         tcExtendTyVarEnv via_tvs $
         -- Moreover, when using DerivingVia one can bind type variables in
index 3cc1994..2d59dc1 100644 (file)
@@ -36,6 +36,7 @@ module TcEnv(
 
         tcLookup, tcLookupLocated, tcLookupLocalIds,
         tcLookupId, tcLookupIdMaybe, tcLookupTyVar,
+        tcLookupTcTyCon,
         tcLookupLcl_maybe,
         getInLocalScope,
         wrongThingErr, pprBinders,
@@ -106,6 +107,7 @@ import ListSetOps
 import ErrUtils
 import Maybes( MaybeErr(..), orElse )
 import qualified GHC.LanguageExtensions as LangExt
+import Util ( HasDebugCallStack )
 
 import Data.IORef
 import Data.List
@@ -443,6 +445,13 @@ tcLookupLocalIds ns
                 Just (ATcId { tct_id = id }) ->  id
                 _ -> pprPanic "tcLookupLocalIds" (ppr name)
 
+tcLookupTcTyCon :: HasDebugCallStack => Name -> TcM TcTyCon
+tcLookupTcTyCon name = do
+    thing <- tcLookup name
+    case thing of
+        ATcTyCon tc -> return tc
+        _           -> pprPanic "tcLookupTcTyCon" (ppr name)
+
 getInLocalScope :: TcM (Name -> Bool)
 getInLocalScope = do { lcl_env <- getLclTypeEnv
                      ; return (`elemNameEnv` lcl_env) }
index 37cc83e..cd65fc0 100644 (file)
@@ -7,6 +7,7 @@
 
 {-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ViewPatterns #-}
 
@@ -15,6 +16,7 @@ module TcHsType (
         kcClassSigType, tcClassSigType,
         tcHsSigType, tcHsSigWcType,
         tcHsPartialSigType,
+        tcStandaloneKindSig,
         funsSigCtxt, addSigCtxt, pprSigCtxt,
 
         tcHsClsInstType,
@@ -36,7 +38,9 @@ module TcHsType (
 
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
-        kcLHsQTyVars,
+        InitialKindStrategy(..),
+        SAKS_or_CUSK(..),
+        kcDeclHeader,
         tcNamedWildCardBinders,
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
@@ -52,6 +56,7 @@ module TcHsType (
 
         -- Sort-checking kinds
         tcLHsKindSig, checkDataKindSig, DataSort(..),
+        checkClassKindSig,
 
         -- Pattern type signatures
         tcHsPatSigType, tcPatSig,
@@ -74,11 +79,10 @@ import TcUnify
 import TcIface
 import TcSimplify
 import TcHsSyn
-import TyCoRep  ( Type(..) )
+import TyCoRep
 import TcErrors ( reportAllUnsolved )
 import TcType
 import Inst   ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
-import TyCoRep( TyCoBinder(..) )  -- Used in etaExpandAlgTyCon
 import Type
 import TysPrim
 import RdrName( lookupLocalRdrOcc )
@@ -241,6 +245,17 @@ tcHsSigType ctxt sig_ty
   where
     skol_info = SigTypeSkol ctxt
 
+-- Does validity checking and zonking.
+tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
+tcStandaloneKindSig (L _ kisig) = case kisig of
+  StandaloneKindSig _ (L _ name) ksig ->
+    let ctxt = StandaloneKindSigCtxt name in
+    addSigCtxt ctxt (hsSigType ksig) $
+    do { kind <- tcTopLHsType kindLevelMode ksig (expectedKindInCtxt ctxt)
+       ; checkValidType ctxt kind
+       ; return (name, kind) }
+  XStandaloneKindSig nec -> noExtCon nec
+
 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
                -> ContextKind -> TcM (Bool, TcType)
 -- Kind-checks/desugars an 'LHsSigType',
@@ -279,13 +294,13 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
 
 tc_hs_sig_type _ (XHsImplicitBndrs nec) _ = noExtCon nec
 
-tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
+tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
 -- tcTopLHsType is used for kind-checking top-level HsType where
 --   we want to fully solve /all/ equalities, and report errors
 -- Does zonking, but not validity checking because it's used
 --   for things (like deriving and instances) that aren't
 --   ordinary types
-tcTopLHsType hs_sig_type ctxt_kind
+tcTopLHsType mode hs_sig_type ctxt_kind
   | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
   = do { traceTc "tcTopLHsType {" (ppr hs_ty)
        ; (spec_tkvs, ty)
@@ -293,7 +308,7 @@ tcTopLHsType hs_sig_type ctxt_kind
                  solveEqualities                   $
                  bindImplicitTKBndrs_Skol sig_vars $
                  do { kind <- newExpectedKind ctxt_kind
-                    ; tc_lhs_type typeLevelMode hs_ty kind }
+                    ; tc_lhs_type mode hs_ty kind }
 
        ; spec_tkvs <- zonkAndScopedSort spec_tkvs
        ; let ty1 = mkSpecForAllTys spec_tkvs ty
@@ -302,7 +317,7 @@ tcTopLHsType hs_sig_type ctxt_kind
        ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
        ; return final_ty}
 
-tcTopLHsType (XHsImplicitBndrs nec) _ = noExtCon nec
+tcTopLHsType (XHsImplicitBndrs nec) _ = noExtCon nec
 
 -----------------
 tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
@@ -315,7 +330,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
 tcHsDeriv hs_ty
   = do { ty <- checkNoErrs $  -- Avoid redundant error report
                               -- with "illegal deriving", below
-               tcTopLHsType hs_ty AnyKind
+               tcTopLHsType typeLevelMode hs_ty AnyKind
        ; let (tvs, pred)    = splitForAllTys ty
              (kind_args, _) = splitFunTys (tcTypeKind pred)
        ; case getClassPredTys_maybe pred of
@@ -344,7 +359,7 @@ tcDerivStrategy mb_lds
     tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
     tc_deriv_strategy NewtypeStrategy  = boring_case NewtypeStrategy
     tc_deriv_strategy (ViaStrategy ty) = do
-      ty' <- checkNoErrs $ tcTopLHsType ty AnyKind
+      ty' <- checkNoErrs $ tcTopLHsType typeLevelMode ty AnyKind
       let (via_tvs, via_pred) = splitForAllTys ty'
       pure (ViaStrategy via_pred, via_tvs)
 
@@ -362,7 +377,7 @@ tcHsClsInstType user_ctxt hs_inst_ty
          -- eagerly avoids follow-on errors when checkValidInstance
          -- sees an unsolved coercion hole
          inst_ty <- checkNoErrs $
-                    tcTopLHsType hs_inst_ty (TheKind constraintKind)
+                    tcTopLHsType typeLevelMode hs_inst_ty (TheKind constraintKind)
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty
        ; return inst_ty }
 
@@ -1776,57 +1791,68 @@ newWildTyVar
 *                                                                      *
 ********************************************************************* -}
 
-{- Note [The initial kind of a type constructor]
+-- See Note [kcCheckDeclHeader vs kcInferDeclHeader]
+data InitialKindStrategy
+  = InitialKindCheck SAKS_or_CUSK
+  | InitialKindInfer
+
+-- Does the declaration have a standalone kind signature (SAKS) or a complete
+-- user-specified kind (CUSK)?
+data SAKS_or_CUSK
+  = SAKS Kind  -- Standalone kind signature, fully zonked! (zonkTcTypeToType)
+  | CUSK       -- Complete user-specified kind (CUSK)
+
+instance Outputable SAKS_or_CUSK where
+  ppr (SAKS k) = text "SAKS" <+> ppr k
+  ppr CUSK = text "CUSK"
+
+-- See Note [kcCheckDeclHeader vs kcInferDeclHeader]
+kcDeclHeader
+  :: InitialKindStrategy
+  -> Name              -- ^ of the thing being checked
+  -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+  -> LHsQTyVars GhcRn  -- ^ Binders in the header
+  -> TcM ContextKind   -- ^ The result kind
+  -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
+kcDeclHeader (InitialKindCheck msig) = kcCheckDeclHeader msig
+kcDeclHeader InitialKindInfer = kcInferDeclHeader
+
+{- Note [kcCheckDeclHeader vs kcInferDeclHeader]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-kcLHsQTyVars is responsible for getting the initial kind of
-a type constructor.
-
-It has two cases:
-
- * The TyCon has a CUSK.  In that case, find the full, final,
-   poly-kinded kind of the TyCon.  It's very like a term-level
-   binding where we have a complete type signature for the
-   function.
-
- * It does not have a CUSK.  Find a monomorphic kind, with
-   unification variables in it; they will be generalised later.
-   It's very like a term-level binding where we do not have
-   a type signature (or, more accurately, where we have a
-   partial type signature), so we infer the type and generalise.
+kcCheckDeclHeader and kcInferDeclHeader are responsible for getting the initial kind
+of a type constructor.
+
+* kcCheckDeclHeader: the TyCon has a standalone kind signature or a CUSK. In that
+  case, find the full, final, poly-kinded kind of the TyCon.  It's very like a
+  term-level binding where we have a complete type signature for the function.
+
+* kcInferDeclHeader: the TyCon has neither a standalone kind signature nor a
+  CUSK. Find a monomorphic kind, with unification variables in it; they will be
+  generalised later.  It's very like a term-level binding where we do not have a
+  type signature (or, more accurately, where we have a partial type signature),
+  so we infer the type and generalise.
 -}
 
-
-------------------------------
--- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
--- user-supplied kind signature (CUSK), generalise the result.
--- Used in 'getInitialKind' (for tycon kinds and other kinds)
--- and in kind-checking (but not for tycon kinds, which are checked with
--- tcTyClDecls). See Note [CUSKs: complete user-supplied kind signatures]
--- in GHC.Hs.Decls.
---
--- This function does not do telescope checking.
-kcLHsQTyVars :: Name              -- ^ of the thing being checked
-             -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
-             -> Bool              -- ^ True <=> the decl being checked has a CUSK
-             -> LHsQTyVars GhcRn
-             -> TcM Kind          -- ^ The result kind
-             -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
-kcLHsQTyVars name flav cusk tvs thing_inside
-  | cusk      = kcLHsQTyVars_Cusk    name flav tvs thing_inside
-  | otherwise = kcLHsQTyVars_NonCusk name flav tvs thing_inside
-
-
-kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk
-    :: Name              -- ^ of the thing being checked
-    -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
-    -> LHsQTyVars GhcRn
-    -> TcM Kind          -- ^ The result kind
-    -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
-
 ------------------------------
-kcLHsQTyVars_Cusk name flav
+kcCheckDeclHeader
+  :: SAKS_or_CUSK
+  -> Name              -- ^ of the thing being checked
+  -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+  -> LHsQTyVars GhcRn  -- ^ Binders in the header
+  -> TcM ContextKind   -- ^ The result kind. AnyKind == no result signature
+  -> TcM TcTyCon       -- ^ A suitably-kinded generalized TcTyCon
+kcCheckDeclHeader (SAKS sig) = kcCheckDeclHeader_sig sig
+kcCheckDeclHeader CUSK       = kcCheckDeclHeader_cusk
+
+kcCheckDeclHeader_cusk
+  :: Name              -- ^ of the thing being checked
+  -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+  -> LHsQTyVars GhcRn  -- ^ Binders in the header
+  -> TcM ContextKind   -- ^ The result kind
+  -> TcM TcTyCon       -- ^ A suitably-kinded generalized TcTyCon
+kcCheckDeclHeader_cusk name flav
               (HsQTvs { hsq_ext = kv_ns
-                      , hsq_explicit = hs_tvs }) thing_inside
+                      , hsq_explicit = hs_tvs }) kc_res_ki
   -- CUSK case
   -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
   = addTyConFlavCtxt name flav $
@@ -1835,19 +1861,21 @@ kcLHsQTyVars_Cusk name flav
               solveEqualities                             $
               bindImplicitTKBndrs_Q_Skol kv_ns            $
               bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $
-              thing_inside
+              newExpectedKind =<< kc_res_ki
 
            -- Now, because we're in a CUSK,
            -- we quantify over the mentioned kind vars
        ; let spec_req_tkvs = scoped_kvs ++ tc_tvs
              all_kinds     = res_kind : map tyVarKind spec_req_tkvs
 
-       ; candidates <- candidateQTyVarsOfKinds all_kinds
+       ; candidates' <- candidateQTyVarsOfKinds all_kinds
              -- 'candidates' are all the variables that we are going to
              -- skolemise and then quantify over.  We do not include spec_req_tvs
              -- because they are /already/ skolems
 
-       ; let inf_candidates = candidates `delCandidates` spec_req_tkvs
+       ; let non_tc_candidates = filter (not . isTcTyVar) (nonDetEltsUniqSet (tyCoVarsOfTypes all_kinds))
+             candidates = candidates' { dv_kvs = dv_kvs candidates' `extendDVarSetList` non_tc_candidates }
+             inf_candidates = candidates `delCandidates` spec_req_tkvs
 
        ; inferred <- quantifyTyVars inf_candidates
                      -- NB: 'inferred' comes back sorted in dependency order
@@ -1866,13 +1894,14 @@ kcLHsQTyVars_Cusk name flav
 
              all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
              tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs
-                               True {- it is generalised -} flav
+                               True -- it is generalised
+                               flav
          -- If the ordering from
          -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls
          -- doesn't work, we catch it here, before an error cascade
        ; checkTyConTelescope tycon
 
-       ; traceTc "kcLHsQTyVars: cusk" $
+       ; traceTc "kcCheckDeclHeader_cusk " $
          vcat [ text "name" <+> ppr name
               , text "kv_ns" <+> ppr kv_ns
               , text "hs_tvs" <+> ppr hs_tvs
@@ -1891,21 +1920,29 @@ kcLHsQTyVars_Cusk name flav
   where
     ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
               | otherwise            = AnyKind
+kcCheckDeclHeader_cusk _ _ (XLHsQTyVars nec) _ = noExtCon nec
 
-kcLHsQTyVars_Cusk _ _ (XLHsQTyVars nec) _ = noExtCon nec
-
-------------------------------
-kcLHsQTyVars_NonCusk name flav
+-- | Kind-check a 'LHsQTyVars'. Used in 'inferInitialKind' (for tycon kinds and
+-- other kinds).
+--
+-- This function does not do telescope checking.
+kcInferDeclHeader
+  :: Name              -- ^ of the thing being checked
+  -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+  -> LHsQTyVars GhcRn
+  -> TcM ContextKind   -- ^ The result kind
+  -> TcM TcTyCon       -- ^ A suitably-kinded non-generalized TcTyCon
+kcInferDeclHeader name flav
               (HsQTvs { hsq_ext = kv_ns
-                      , hsq_explicit = hs_tvs }) thing_inside
-  -- Non_CUSK case
+                      , hsq_explicit = hs_tvs }) kc_res_ki
+  -- No standalane kind signature and no CUSK.
   -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
   = do { (scoped_kvs, (tc_tvs, res_kind))
            -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
            -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
            <- bindImplicitTKBndrs_Q_Tv kv_ns            $
               bindExplicitTKBndrs_Q_Tv ctxt_kind hs_tvs $
-              thing_inside
+              newExpectedKind =<< kc_res_ki
               -- Why "_Tv" not "_Skol"? See third wrinkle in
               -- Note [Inferring kinds for type declarations] in TcTyClsDecls,
 
@@ -1931,7 +1968,7 @@ kcLHsQTyVars_NonCusk name flav
                                False -- not yet generalised
                                flav
 
-       ; traceTc "kcLHsQTyVars: not-cusk" $
+       ; traceTc "kcInferDeclHeader: not-cusk" $
          vcat [ ppr name, ppr kv_ns, ppr hs_tvs
               , ppr scoped_kvs
               , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
@@ -1940,8 +1977,414 @@ kcLHsQTyVars_NonCusk name flav
     ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
               | otherwise            = AnyKind
 
-kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars nec) _ = noExtCon nec
+kcInferDeclHeader _ _ (XLHsQTyVars nec) _ = noExtCon nec
+
+-- | Kind-check a declaration header against a standalone kind signature.
+-- See Note [Arity inference in kcCheckDeclHeader_sig]
+kcCheckDeclHeader_sig
+  :: Kind              -- ^ Standalone kind signature, fully zonked! (zonkTcTypeToType)
+  -> Name              -- ^ of the thing being checked
+  -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+  -> LHsQTyVars GhcRn  -- ^ Binders in the header
+  -> TcM ContextKind   -- ^ The result kind. AnyKind == no result signature
+  -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
+kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki =
+  addTyConFlavCtxt name flav $
+    pushTcLevelM_ $
+    solveEqualities $  -- #16687
+    bind_implicit (hsq_ext ktvs) $ \implicit_tcv_prs -> do
+
+      -- Step 1: zip user-written binders with quantifiers from the kind signature.
+      -- For example:
+      --
+      --   type F :: forall k -> k -> forall j. j -> Type
+      --   data F i a b = ...
+      --
+      -- Results in the following 'zipped_binders':
+      --
+      --                   TyBinder      LHsTyVarBndr
+      --    ---------------------------------------
+      --    ZippedBinder   forall k ->   i
+      --    ZippedBinder   k ->          a
+      --    ZippedBinder   forall j.
+      --    ZippedBinder   j ->          b
+      --
+      let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig (hsq_explicit ktvs)
+
+      -- Report binders that don't have a corresponding quantifier.
+      -- For example:
+      --
+      --   type T :: Type -> Type
+      --   data T b1 b2 b3 = ...
+      --
+      -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders.
+      --
+      unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs)
+
+      -- Convert each ZippedBinder to TyConBinder        for  tyConBinders
+      --                       and to [(Name, TcTyVar)]  for  tcTyConScopedTyVars
+      (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders
+
+      tcExtendNameTyVarEnv explicit_tv_prs $ do
+
+        -- Check that inline kind annotations on binders are valid.
+        -- For example:
+        --
+        --   type T :: Maybe k -> Type
+        --   data T (a :: Maybe j) = ...
+        --
+        -- Here we unify   Maybe k ~ Maybe j
+        mapM_ check_zipped_binder zipped_binders
+
+        -- Kind-check the result kind annotation, if present:
+        --
+        --    data T a b :: res_ki where
+        --               ^^^^^^^^^
+        -- We do it here because at this point the environment has been
+        -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
+        m_res_ki <- kc_res_ki >>= \ctx_k ->
+          case ctx_k of
+            AnyKind -> return Nothing
+            _ -> Just <$> newExpectedKind ctx_k
+
+        -- Step 2: split off invisible binders.
+        -- For example:
+        --
+        --   type F :: forall k1 k2. (k1, k2) -> Type
+        --   type family F
+        --
+        -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'?
+        -- See Note [Arity inference in kcCheckDeclHeader_sig]
+        let (invis_binders, r_ki) = split_invis kisig' m_res_ki
+
+        -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders.
+        invis_tcbs <- mapM invis_to_tcb invis_binders
+
+        -- Check that the inline result kind annotation is valid.
+        -- For example:
+        --
+        --   type T :: Type -> Maybe k
+        --   type family T a :: Maybe j where
+        --
+        -- Here we unify   Maybe k ~ Maybe j
+        whenIsJust m_res_ki $ \res_ki ->
+          discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
+          unifyKind Nothing r_ki res_ki
+
+        -- Zonk the implicitly quantified variables.
+        implicit_tv_prs <- mapSndM zonkTcTyVarToTyVar implicit_tcv_prs
+
+        -- Build the final, generalized TcTyCon
+        let tcbs       = vis_tcbs ++ invis_tcbs
+            all_tv_prs = implicit_tv_prs ++ explicit_tv_prs
+            tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
+
+        traceTc "kcCheckDeclHeader_sig done:" $ vcat
+          [ text "tyConName = " <+> ppr (tyConName tc)
+          , text "kisig =" <+> debugPprType kisig
+          , text "tyConKind =" <+> debugPprType (tyConKind tc)
+          , text "tyConBinders = " <+> ppr (tyConBinders tc)
+          , text "tcTyConScopedTyVars" <+> ppr (tcTyConScopedTyVars tc)
+          , text "tyConResKind" <+> debugPprType (tyConResKind tc)
+          ]
+        return tc
+  where
+    -- Consider this declaration:
+    --
+    --    type T :: forall a. forall b -> (a~b) => Proxy a -> Type
+    --    data T x p = MkT
+    --
+    -- Here, we have every possible variant of ZippedBinder:
+    --
+    --                   TyBinder           LHsTyVarBndr
+    --    ----------------------------------------------
+    --    ZippedBinder   forall {k}.
+    --    ZippedBinder   forall (a::k).
+    --    ZippedBinder   forall (b::k) ->   x
+    --    ZippedBinder   (a~b) =>
+    --    ZippedBinder   Proxy a ->         p
+    --
+    -- Given a ZippedBinder zipped_to_tcb produces:
+    --
+    --  * TyConBinder      for  tyConBinders
+    --  * (Name, TcTyVar)  for  tcTyConScopedTyVars, if there's a user-written LHsTyVarBndr
+    --
+    zipped_to_tcb :: ZippedBinder -> TcM (TyConBinder, [(Name, TcTyVar)])
+    zipped_to_tcb zb = case zb of
+
+      -- Inferred variable, no user-written binder.
+      -- Example:   forall {k}.
+      ZippedBinder (Named (Bndr v Specified)) Nothing ->
+        return (mkNamedTyConBinder Specified v, [])
+
+      -- Specified variable, no user-written binder.
+      -- Example:   forall (a::k).
+      ZippedBinder (Named (Bndr v Inferred)) Nothing ->
+        return (mkNamedTyConBinder Inferred v, [])
+
+      -- Constraint, no user-written binder.
+      -- Example:   (a~b) =>
+      ZippedBinder (Anon InvisArg bndr_ki) Nothing -> do
+        name <- newSysName (mkTyVarOccFS (fsLit "ev"))
+        let tv = mkTyVar name bndr_ki
+        return (mkAnonTyConBinder InvisArg tv, [])
+
+      -- Non-dependent visible argument with a user-written binder.
+      -- Example:   Proxy a ->
+      ZippedBinder (Anon VisArg bndr_ki) (Just b) ->
+        return $
+          let v_name = getName b
+              tv = mkTyVar v_name bndr_ki
+              tcb = mkAnonTyConBinder VisArg tv
+          in (tcb, [(v_name, tv)])
+
+      -- Dependent visible argument with a user-written binder.
+      -- Example:   forall (b::k) ->
+      ZippedBinder (Named (Bndr v Required)) (Just b) ->
+        return $
+          let v_name = getName b
+              tcb = mkNamedTyConBinder Required v
+          in (tcb, [(v_name, v)])
+
+      -- 'zipBinders' does not produce any other variants of ZippedBinder.
+      _ -> panic "goVis: invalid ZippedBinder"
+
+    -- Given an invisible binder that comes from 'split_invis',
+    -- convert it to TyConBinder.
+    invis_to_tcb :: TyCoBinder -> TcM TyConBinder
+    invis_to_tcb tb = do
+      (tcb, stv) <- zipped_to_tcb (ZippedBinder tb Nothing)
+      MASSERT(null stv)
+      return tcb
+
+    -- similar to:  bindImplicitTKBndrs_Tv
+    bind_implicit :: [Name] -> ([(Name,TcTyVar)] -> TcM a) -> TcM a
+    bind_implicit tv_names thing_inside =
+      do { let new_tv name = do { tcv <- newFlexiKindedTyVarTyVar name
+                                ; return (name, tcv) }
+         ; tcvs <- mapM new_tv tv_names
+         ; tcExtendNameTyVarEnv tcvs (thing_inside tcvs) }
+
+    -- Check that the inline kind annotation on a binder is valid
+    -- by unifying it with the kind of the quantifier.
+    check_zipped_binder :: ZippedBinder -> TcM ()
+    check_zipped_binder (ZippedBinder _ Nothing) = return ()
+    check_zipped_binder (ZippedBinder tb (Just b)) =
+      case unLoc b of
+        UserTyVar _ _ -> return ()
+        KindedTyVar _ v v_hs_ki -> do
+          v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki
+          discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
+            unifyKind (Just (HsTyVar noExtField NotPromoted v))
+                      (tyBinderType tb)
+                      v_ki
+        XTyVarBndr nec -> noExtCon nec
+
+    -- Split the invisible binders that should become a part of 'tyConBinders'
+    -- rather than 'tyConResKind'.
+    -- See Note [Arity inference in kcCheckDeclHeader_sig]
+    split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind)
+    split_invis sig_ki Nothing =
+      -- instantiate all invisible binders
+      splitPiTysInvisible sig_ki
+    split_invis sig_ki (Just res_ki) =
+      -- subtraction a la checkExpectedKind
+      let n_res_invis_bndrs = invisibleTyBndrCount res_ki
+          n_sig_invis_bndrs = invisibleTyBndrCount sig_ki
+          n_inst = n_sig_invis_bndrs - n_res_invis_bndrs
+      in splitPiTysInvisibleN n_inst sig_ki
+
+-- A quantifier from a kind signature zipped with a user-written binder for it.
+data ZippedBinder =
+  ZippedBinder TyBinder (Maybe (LHsTyVarBndr GhcRn))
+
+-- See Note [Arity inference in kcCheckDeclHeader_sig]
+zipBinders
+  :: Kind                      -- kind signature
+  -> [LHsTyVarBndr GhcRn]      -- user-written binders
+  -> ([ZippedBinder],          -- zipped binders
+      [LHsTyVarBndr GhcRn],    -- remaining user-written binders
+      Kind)                    -- remainder of the kind signature
+zipBinders = zip_binders []
+  where
+    zip_binders acc ki [] = (reverse acc, [], ki)
+    zip_binders acc ki (b:bs) =
+      case tcSplitPiTy_maybe ki of
+        Nothing -> (reverse acc, b:bs, ki)
+        Just (tb, ki') ->
+          let
+            (zb, bs') | zippable  = (ZippedBinder tb (Just b),  bs)
+                      | otherwise = (ZippedBinder tb Nothing, b:bs)
+            zippable =
+              case tb of
+                Named (Bndr _ Specified) -> False
+                Named (Bndr _ Inferred)  -> False
+                Named (Bndr _ Required)  -> True
+                Anon InvisArg _ -> False
+                Anon VisArg   _ -> True
+          in
+            zip_binders (zb:acc) ki' bs'
+
+tooManyBindersErr :: Kind -> [LHsTyVarBndr GhcRn] -> SDoc
+tooManyBindersErr ki bndrs =
+   hang (text "Not a function kind:")
+      4 (ppr ki) $$
+   hang (text "but extra binders found:")
+      4 (fsep (map ppr bndrs))
+
+{- Note [Arity inference in kcCheckDeclHeader_sig]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given a kind signature 'kisig' and a declaration header, kcCheckDeclHeader_sig
+verifies that the declaration conforms to the signature. The end result is a
+TcTyCon 'tc' such that:
+
+  tyConKind tc == kisig
+
+This TcTyCon would be rather easy to produce if we didn't have to worry about
+arity. Consider these declarations:
+
+  type family S1 :: forall k. k -> Type
+  type family S2 (a :: k) :: Type
+
+Both S1 and S2 can be given the same standalone kind signature:
+
+  type S2 :: forall k. k -> Type
+
+And, indeed, tyConKind S1 == tyConKind S2. However, tyConKind is built from
+tyConBinders and tyConResKind, such that
+
+  tyConKind tc == mkTyConKind (tyConBinders tc) (tyConResKind tc)
+
+For S1 and S2, tyConBinders and tyConResKind are different:
+
+  tyConBinders S1  ==  []
+  tyConResKind S1  ==  forall k. k -> Type
+  tyConKind    S1  ==  forall k. k -> Type
+
+  tyConBinders S2  ==  [spec k, anon-vis (a :: k)]
+  tyConResKind S2  ==  Type
+  tyConKind    S1  ==  forall k. k -> Type
+
+This difference determines the arity:
+
+  tyConArity tc == length (tyConBinders tc)
+
+That is, the arity of S1 is 0, while the arity of S2 is 2.
+
+'kcCheckDeclHeader_sig' needs to infer the desired arity to split the standalone
+kind signature into binders and the result kind. It does so in two rounds:
 
+1. zip user-written binders (vis_tcbs)
+2. split off invisible binders (invis_tcbs)
+
+Consider the following declarations:
+
+    type F :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
+    type family F a b
+
+    type G :: Type -> forall j. j -> forall k1 k2. (k1, k2) -> Type
+    type family G a b :: forall r2. (r1, r2) -> Type
+
+In step 1 (zip user-written binders), we zip the quantifiers in the signature
+with the binders in the header using 'zipBinders'. In both F and G, this results in
+the following zipped binders:
+
+                   TyBinder     LHsTyVarBndr
+    ---------------------------------------
+    ZippedBinder   Type ->      a
+    ZippedBinder   forall j.
+    ZippedBinder   j ->         b
+
+
+At this point, we have accumulated three zipped binders which correspond to a
+prefix of the standalone kind signature:
+
+  Type -> forall j. j -> ...
+
+In step 2 (split off invisible binders), we have to decide how much remaining
+invisible binders of the standalone kind signature to split off:
+
+    forall k1 k2. (k1, k2) -> Type
+    ^^^^^^^^^^^^^
+    split off or not?
+
+This decision is made in 'split_invis':
+
+* If a user-written result kind signature is not provided, as in F,
+  then split off all invisible binders. This is why we need special treatment
+  for AnyKind.
+* If a user-written result kind signature is provided, as in G,
+  then do as checkExpectedKind does and split off (n_sig - n_res) binders.
+  That is, split off such an amount of binders that the remainder of the
+  standalone kind signature and the user-written result kind signature have the
+  same amount of invisible quantifiers.
+
+For F, split_invis splits away all invisible binders, and we have 2:
+
+    forall k1 k2. (k1, k2) -> Type
+    ^^^^^^^^^^^^^
+    split away both binders
+
+The resulting arity of F is 3+2=5.  (length vis_tcbs = 3,
+                                     length invis_tcbs = 2,
+                                     length tcbs = 5)
+
+For G, split_invis decides to split off 1 invisible binder, so that we have the
+same amount of invisible quantifiers left:
+
+    res_ki  =  forall    r2. (r1, r2) -> Type
+    kisig   =  forall k1 k2. (k1, k2) -> Type
+                     ^^^
+                     split off this one.
+
+The resulting arity of G is 3+1=4. (length vis_tcbs = 3,
+                                    length invis_tcbs = 1,
+                                    length tcbs = 4)
+
+-}
+
+{- Note [discardResult in kcCheckDeclHeader_sig]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We use 'unifyKind' to check inline kind annotations in declaration headers
+against the signature.
+
+  type T :: [i] -> Maybe j -> Type
+  data T (a :: [k1]) (b :: Maybe k2) :: Type where ...
+
+Here, we will unify:
+
+       [k1] ~ [i]
+  Maybe k2  ~ Maybe j
+      Type  ~ Type
+
+The end result is that we fill in unification variables k1, k2:
+
+    k1  :=  i
+    k2  :=  j
+
+We also validate that the user isn't confused:
+
+  type T :: Type -> Type
+  data T (a :: Bool) = ...
+
+This will report that (Type ~ Bool) failed to unify.
+
+Now, consider the following example:
+
+  type family Id a where Id x = x
+  type T :: Bool -> Type
+  type T (a :: Id Bool) = ...
+
+We will unify (Bool ~ Id Bool), and this will produce a non-reflexive coercion.
+However, we are free to discard it, as the kind of 'T' is determined by the
+signature, not by the inline kind annotation:
+
+      we have   T ::    Bool -> Type
+  rather than   T :: Id Bool -> Type
+
+This (Id Bool) will not show up anywhere after we're done validating it, so we
+have no use for the produced coercion.
+-}
 
 {- Note [No polymorphic recursion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1956,11 +2399,11 @@ be a tough nut.
 Previously, we laboriously (with help from the renamer)
 tried to give T the polymoprhic kind
    T :: forall ka -> ka -> kappa -> Type
-where kappa is a unification variable, even in the getInitialKinds
-phase (which is what kcLHsQTyVars_NonCusk is all about).  But
+where kappa is a unification variable, even in the inferInitialKinds
+phase (which is what kcInferDeclHeader is all about).  But
 that is dangerously fragile (see the ticket).
 
-Solution: make kcLHsQTyVars_NonCusk give T a straightforward
+Solution: make kcInferDeclHeader give T a straightforward
 monomorphic kind, with no quantification whatsoever. That's why
 we use mkAnonTyConBinder for all arguments when figuring out
 tc_binders.
@@ -1970,7 +2413,7 @@ But notice that (#16322 comment:3)
 * The algorithm successfully kind-checks this declaration:
     data T2 ka (a::ka) = MkT2 (T2 Type a)
 
-  Starting with (getInitialKinds)
+  Starting with (inferInitialKinds)
     T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> *
   we get
     kappa4 := kappa1   -- from the (a:ka) kind signature
@@ -2037,7 +2480,7 @@ Then `a` first appears /after/ `f`, so the kind of `T2` should be:
 
   T2 :: forall f a. f a -> Type
 
-In order to make this distinction, we need to know (in kcLHsQTyVars) which
+In order to make this distinction, we need to know (in kcCheckDeclHeader) which
 type variables have been bound by the parent class (if there is one). With
 the class-bound variables in hand, we can ensure that we always quantify
 these first.
@@ -2218,7 +2661,6 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
 
 tcHsQTyVarBndr _ _ (XTyVarBndr nec) = noExtCon nec
 
-
 --------------------------------------
 -- Binding type/class variables in the
 -- kind-checking and typechecking phases
@@ -2238,7 +2680,7 @@ bindTyClTyVars tycon_name thing_inside
        ; tcExtendNameTyVarEnv scoped_prs $
          thing_inside binders res_kind }
 
--- getInitialKind has made a suitably-shaped kind for the type or class
+-- inferInitialKind has made a suitably-shaped kind for the type or class
 -- Look it up in the local environment. This is used only for tycons
 -- that we're currently type-checking, so we're sure to find a TcTyCon.
 kcLookupTcTyCon :: Name -> TcM TcTyCon
@@ -2539,6 +2981,16 @@ checkDataKindSig data_sort kind = do
             then text "Perhaps you intended to use UnliftedNewtypes"
             else empty ]
 
+-- | Checks that the result kind of a class is exactly `Constraint`, rejecting
+-- type synonyms and type families that reduce to `Constraint`. See #16826.
+checkClassKindSig :: Kind -> TcM ()
+checkClassKindSig kind = checkTc (tcIsConstraintKind kind) err_msg
+  where
+    err_msg :: SDoc
+    err_msg =
+      text "Kind signature on a class must end with" <+> ppr constraintKind $$
+      text "unobscured by type families"
+
 tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
 -- Result is in 1-1 correpondence with orig_args
 tcbVisibilities tc orig_args
index e9d75fb..c047d13 100644 (file)
@@ -746,6 +746,7 @@ tcDataFamInstDecl mb_clsinfo
                L _ []    -> Nothing
                L _ preds ->
                  Just $ DerivInfo { di_rep_tc  = rep_tc
+                                  , di_scoped_tvs = mkTyVarNamePairs (tyConTyVars rep_tc)
                                   , di_clauses = preds
                                   , di_ctxt    = tcMkDataFamInstCtxt decl }
 
index a0297c6..8a15d9c 100644 (file)
@@ -1587,11 +1587,10 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
       = return Nothing   -- this can happen for a covar that's associated with
                          -- a coercion hole. Test case: typecheck/should_compile/T2494
 
-      | not (isTcTyVar tkv)  -- I don't think this can ever happen.
-                             -- Hence the assert
-      = ASSERT2( False, text "quantifying over a TyVar" <+> ppr tkv)
-        return (Just tkv)
-
+      | not (isTcTyVar tkv)
+      = return (Just tkv)  -- For associated types in a class with a standalone
+                           -- kind signature, we have the class variables in
+                           -- scope, and they are TyVars not TcTyVars
       | otherwise
       = do { deflt_done <- defaultTyVar default_kind tkv
            ; case deflt_done of
index 69c909f..904f808 100644 (file)
@@ -154,13 +154,17 @@ tcTyClGroup :: TyClGroup GhcRn
 -- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls
 tcTyClGroup (TyClGroup { group_tyclds = tyclds
                        , group_roles  = roles
+                       , group_kisigs = kisigs
                        , group_instds = instds })
   = do { let role_annots = mkRoleAnnotEnv roles
 
-           -- Step 1: Typecheck the type/class declarations
+           -- Step 1: Typecheck the standalone kind signatures and type/class declarations
        ; traceTc "---- tcTyClGroup ---- {" empty
        ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
-       ; (tyclss, data_deriv_info) <- tcTyClDecls tyclds role_annots
+       ; (tyclss, data_deriv_info) <-
+           tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution]
+           do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs
+              ; tcTyClDecls tyclds kisig_env role_annots }
 
            -- Step 1.5: Make sure we don't have any type synonym cycles
        ; traceTc "Starting synonym cycle check" (ppr tyclss)
@@ -196,16 +200,19 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds
 
 tcTyClGroup (XTyClGroup nec) = noExtCon nec
 
+-- Gives the kind for every TyCon that has a standalone kind signature
+type KindSigEnv = NameEnv Kind
+
 tcTyClDecls
   :: [LTyClDecl GhcRn]
+  -> KindSigEnv
   -> RoleAnnotEnv
   -> TcM ([TyCon], [DerivInfo])
-tcTyClDecls tyclds role_annots
-  = tcExtendKindEnv promotion_err_env $   --- See Note [Type environment evolution]
-    do {    -- Step 1: kind-check this group and returns the final
+tcTyClDecls tyclds kisig_env role_annots
+  = do {    -- Step 1: kind-check this group and returns the final
             -- (possibly-polymorphic) kind of each TyCon and Class
             -- See Note [Kind checking for type and class decls]
-         tc_tycons <- kcTyClGroup tyclds
+         tc_tycons <- kcTyClGroup kisig_env tyclds
        ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
 
             -- Step 2: type-check all groups together, returning
@@ -236,7 +243,6 @@ tcTyClDecls tyclds role_annots
            ; return (tycons, concat data_deriv_infos)
            } }
   where
-    promotion_err_env = mkPromotionErrorEnv tyclds
     ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                   , ppr (tyConBinders tc) <> comma
                                   , ppr (tyConResKind tc)
@@ -315,7 +321,7 @@ Consider
     data T (a :: *) = MkT (S a)   -- Has CUSK
     data S a = MkS (T Int) (S a)  -- No CUSK
 
-Via getInitialKinds we get
+Via inferInitialKinds we get
   T :: * -> *
   S :: kappa -> *
 
@@ -352,7 +358,7 @@ General type functions can be recursive, and hence, appear in `alg_decls'.
 
 The kind of an open type family is solely determinded by its kind signature;
 hence, only kind signatures participate in the construction of the initial
-kind environment (as constructed by `getInitialKind'). In fact, we ignore
+kind environment (as constructed by `inferInitialKind'). In fact, we ignore
 instances of families altogether in the following. However, we need to include
 the kinds of *associated* families into the construction of the initial kind
 environment. (This is handled by `allDecls').
@@ -371,7 +377,7 @@ TcTyCons are used for two distinct purposes
 2.  When checking a type/class declaration (in module TcTyClsDecls), we come
     upon knowledge of the eventual tycon in bits and pieces.
 
-      S1) First, we use getInitialKinds to look over the user-provided
+      S1) First, we use inferInitialKinds to look over the user-provided
           kind signature of a tycon (including, for example, the number
           of parameters written to the tycon) to get an initial shape of
           the tycon's kind.  We record that shape in a TcTyCon.
@@ -397,7 +403,7 @@ TcTyCons are used for two distinct purposes
 
 4.  tyConScopedTyVars.  A challenging piece in all of this is that we
     end up taking three separate passes over every declaration:
-      - one in getInitialKind (this pass look only at the head, not the body)
+      - one in inferInitialKind (this pass look only at the head, not the body)
       - one in kcTyClDecls (to kind-check the body)
       - a final one in tcTyClDecls (to desugar)
 
@@ -437,7 +443,7 @@ We do the following steps:
             MkB :-> DataConPE
 
   2. kcTyCLGroup
-      - Do getInitialKinds, which will signal a promotion
+      - Do inferInitialKinds, which will signal a promotion
         error if B is used in any of the kinds needed to initialise
         B's kind (e.g. (a :: Type)) here
 
@@ -481,9 +487,9 @@ to Note [Single function non-recursive binding special-case]:
 Unfortunately this requires reworking a bit of the code in
 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
 
-Note [Don't process associated types in kcLHsQTyVars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Previously, we processed associated types in the thing_inside in kcLHsQTyVars,
+Note [Don't process associated types in getInitialKind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Previously, we processed associated types in the thing_inside in getInitialKind,
 but this was wrong -- we want to do ATs sepearately.
 The consequence for not doing it this way is #15142:
 
@@ -496,7 +502,7 @@ kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring
 unified with Type. And then, when we generalize the kind of ListToTuple (which
 indeed has a CUSK, according to the rules), we skolemize the free metavariable
 kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple,
-because the solveEqualities in kcLHsQTyVars is at TcLevel 1 and so kappa[1]
+because the solveEqualities in kcInferDeclHeader is at TcLevel 1 and so kappa[1]
 will unify with Type.
 
 Bottom line: as associated types should have no effect on a CUSK enclosing class,
@@ -505,13 +511,13 @@ been generalized.
 
 -}
 
-kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
+kcTyClGroup :: KindSigEnv -> [LTyClDecl GhcRn] -> TcM [TcTyCon]
 
 -- Kind check this group, kind generalize, and return the resulting local env
 -- This binds the TyCons and Classes of the group, but not the DataCons
 -- See Note [Kind checking for type and class decls]
 -- and Note [Inferring kinds for type declarations]
-kcTyClGroup decls
+kcTyClGroup kisig_env decls
   = do  { mod <- getModule
         ; traceTc "---- kcTyClGroup ---- {"
                   (text "module" <+> ppr mod $$ vcat (map ppr decls))
@@ -523,19 +529,26 @@ kcTyClGroup decls
           -- See Note [Kind checking for type and class decls]
 
         ; cusks_enabled <- xoptM LangExt.CUSKs
-        ; let (cusk_decls, no_cusk_decls)
-                 = partition (hsDeclHasCusk cusks_enabled . unLoc) decls
+        ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls
+
+              get_kind d
+                | Just ki <- lookupNameEnv kisig_env (tcdName (unLoc d))
+                = Right (d, SAKS ki)
+
+                | cusks_enabled && hsDeclHasCusk (unLoc d)
+                = Right (d, CUSK)
 
-        ; poly_cusk_tcs <- getInitialKinds True cusk_decls
+                | otherwise = Left d
 
-        ; mono_tcs
-            <- tcExtendKindEnvWithTyCons poly_cusk_tcs $
+        ; checked_tcs <- checkInitialKinds kinded_decls
+        ; inferred_tcs
+            <- tcExtendKindEnvWithTyCons checked_tcs $
                pushTcLevelM_   $  -- We are going to kind-generalise, so
                                   -- unification variables in here must
                                   -- be one level in
                solveEqualities $
                do {  -- Step 1: Bind kind variables for all decls
-                    mono_tcs <- getInitialKinds False no_cusk_decls
+                    mono_tcs <- inferInitialKinds kindless_decls
 
                   ; traceTc "kcTyClGroup: initial kinds" $
                     ppr_tc_kinds mono_tcs
@@ -546,7 +559,7 @@ kcTyClGroup decls
                     --     See Note [Type environment evolution]
                   ; poly_kinds  <- xoptM LangExt.PolyKinds
                   ; tcExtendKindEnvWithTyCons mono_tcs $
-                    mapM_ kcLTyClDecl (if poly_kinds then no_cusk_decls else decls)
+                    mapM_ kcLTyClDecl (if poly_kinds then kindless_decls else decls)
                     -- See Note [Skip decls with CUSKs in kcLTyClDecl]
 
                   ; return mono_tcs }
@@ -555,9 +568,9 @@ kcTyClGroup decls
         -- Finally, go through each tycon and give it its final kind,
         -- with all the required, specified, and inferred variables
         -- in order.
-        ; poly_no_cusk_tcs <- mapAndReportM generaliseTcTyCon mono_tcs
+        ; generalized_tcs <- mapAndReportM generaliseTcTyCon inferred_tcs
 
-        ; let poly_tcs = poly_cusk_tcs ++ poly_no_cusk_tcs
+        ; let poly_tcs = checked_tcs ++ generalized_tcs
         ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
         ; return poly_tcs }
 
@@ -772,11 +785,11 @@ How it works
 These design choices are implemented by two completely different code
 paths for
 
-  * Declarations with a complete user-specified kind signature (CUSK)
-    Handed by the CUSK case of kcLHsQTyVars.
+  * Declarations with a standalone kind signature or a complete user-specified
+    kind signature (CUSK). Handled by the kcCheckDeclHeader.
 
-  * Declarations without a CUSK are handled by kcTyClDecl; see
-    Note [Inferring kinds for type declarations].
+  * Declarations without a kind signature (standalone or CUSK) are handled by
+    kcInferDeclHeader; see Note [Inferring kinds for type declarations].
 
 Note that neither code path worries about point (4) above, as this
 is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
@@ -821,7 +834,7 @@ that do not have a CUSK.  Consider
 
 We do kind inference as follows:
 
-* Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk.
+* Step 1: inferInitialKinds, and in particular kcInferDeclHeader.
   Make a unification variable for each of the Required and Specified
   type varialbes in the header.
 
@@ -997,17 +1010,34 @@ mk_prom_err_env decl
     -- Works for family declarations too
 
 --------------
-getInitialKinds :: Bool -> [LTyClDecl GhcRn] -> TcM [TcTyCon]
+inferInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
 -- Returns a TcTyCon for each TyCon bound by the decls,
 -- each with its initial kind
 
-getInitialKinds cusk decls
-  = do { traceTc "getInitialKinds {" empty
-       ; tcs <- concatMapM (addLocM (getInitialKind cusk)) decls
-       ; traceTc "getInitialKinds done }" empty
+inferInitialKinds decls
+  = do { traceTc "inferInitialKinds {" $ ppr (map (tcdName . unLoc) decls)
+       ; tcs <- concatMapM infer_initial_kind decls
+       ; traceTc "inferInitialKinds done }" empty
        ; return tcs }
+  where
+    infer_initial_kind = addLocM (getInitialKind InitialKindInfer)
+
+-- Check type/class declarations against their standalone kind signatures or
+-- CUSKs, producing a generalized TcTyCon for each.
+checkInitialKinds :: [(LTyClDecl GhcRn, SAKS_or_CUSK)] -> TcM [TcTyCon]
+checkInitialKinds decls
+  = do { traceTc "checkInitialKinds {" $ ppr (mapFst (tcdName . unLoc) decls)
+       ; tcs <- concatMapM check_initial_kind decls
+       ; traceTc "checkInitialKinds done }" empty
+       ; return tcs }
+  where
+    check_initial_kind (ldecl, msig) =
+      addLocM (getInitialKind (InitialKindCheck msig)) ldecl
+
+-- | Get the initial kind of a TyClDecl, either generalized or non-generalized,
+-- depending on the 'InitialKindStrategy'.
+getInitialKind :: InitialKindStrategy -> TyClDecl GhcRn -> TcM [TcTyCon]
 
-getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon]
 -- Allocate a fresh kind variable for each TyCon and Class
 -- For each tycon, return a TcTyCon with kind k
 -- where k is the kind of tc, derived from the LHS
@@ -1020,108 +1050,208 @@ getInitialKind :: Bool -> TyClDecl GhcRn -> TcM [TcTyCon]
 --   * The kind signatures on type-variable binders
 --   * The result kinds signature on a TyClDecl
 --
--- No family instances are passed to getInitialKinds
-
-getInitialKind cusk
+-- No family instances are passed to checkInitialKinds/inferInitialKinds
+getInitialKind strategy
     (ClassDecl { tcdLName = dL->L _ name
                , tcdTyVars = ktvs
                , tcdATs = ats })
-  = do { tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $
-                  return constraintKind
-       ; let parent_tv_prs = tcTyConScopedTyVars tycon
-            -- See Note [Don't process associated types in kcLHsQTyVars]
-       ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $
-                      getFamDeclInitialKinds cusk (Just tycon) ats
-       ; return (tycon : inner_tcs) }
-
-getInitialKind cusk
+  = do { cls <- kcDeclHeader strategy name ClassFlavour ktvs $
+                return (TheKind constraintKind)
+       ; let parent_tv_prs = tcTyConScopedTyVars cls
+            -- See Note [Don't process associated types in getInitialKind]
+       ; inner_tcs <-
+           tcExtendNameTyVarEnv parent_tv_prs $
+           mapM (addLocM (getAssocFamInitialKind cls)) ats
+       ; return (cls : inner_tcs) }
+  where
+    getAssocFamInitialKind cls =
+      case strategy of
+        InitialKindInfer -> get_fam_decl_initial_kind (Just cls)
+        InitialKindCheck _ -> check_initial_kind_assoc_fam cls
+
+getInitialKind strategy
     (DataDecl { tcdLName = dL->L _ name
               , tcdTyVars = ktvs
               , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                          , dd_ND = new_or_data } })
   = do  { let flav = newOrDataToFlavour new_or_data
-        ; tc <- kcLHsQTyVars name flav cusk ktvs $
-                -- See Note [Implementation of UnliftedNewtypes]
-                do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
-                   ; case m_sig of
-                       Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
-                       Nothing
-                         |  NewType <- new_or_data
-                         ,  unlifted_newtypes -> newOpenTypeKind
-                         |  otherwise -> pure liftedTypeKind
-                   }
+              ctxt = DataKindCtxt name
+        ; tc <- kcDeclHeader strategy name flav ktvs $
+                case m_sig of
+                  Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
+                  Nothing -> dataDeclDefaultResultKind new_or_data
         ; return [tc] }
 
-getInitialKind cusk (FamDecl { tcdFam = decl })
-  = do { tc <- getFamDeclInitialKind cusk Nothing decl
+getInitialKind InitialKindInfer (FamDecl { tcdFam = decl })
+  = do { tc <- get_fam_decl_initial_kind Nothing decl
        ; return [tc] }
 
-getInitialKind cusk (SynDecl { tcdLName = dL->L _ name
-                             , tcdTyVars = ktvs
-                             , tcdRhs = rhs })
-  = do  { cusks_enabled <- xoptM LangExt.CUSKs
-        ; tycon <- kcLHsQTyVars name TypeSynonymFlavour cusk ktvs $
-                   case kind_annotation cusks_enabled rhs of
-                     Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
-                     Nothing -> newMetaKindVar
-        ; return [tycon] }
-  where
-    -- Keep this synchronized with 'hsDeclHasCusk'.
-    kind_annotation
-      :: Bool           --  cusks_enabled?
-      -> LHsType GhcRn  --  rhs
-      -> Maybe (LHsKind GhcRn)
-    kind_annotation False = const Nothing
-    kind_annotation True = go
-      where
-        go (dL->L _ ty) = case ty of
-          HsParTy _ lty     -> go lty
-          HsKindSig _ _ k   -> Just k
-          _                 -> Nothing
+getInitialKind (InitialKindCheck msig) (FamDecl { tcdFam =
+  FamilyDecl { fdLName     = unLoc -> name
+             , fdTyVars    = ktvs
+             , fdResultSig = unLoc -> resultSig
+             , fdInfo      = info } } )
+  = do { let flav = getFamFlav Nothing info
+             ctxt = TyFamResKindCtxt name
+       ; tc <- kcDeclHeader (InitialKindCheck msig) name flav ktvs $
+               case famResultKindSignature resultSig of
+                 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
+                 Nothing ->
+                   case msig of
+                     CUSK -> return (TheKind liftedTypeKind)
+                     SAKS _ -> return AnyKind
+       ; return [tc] }
+
+getInitialKind strategy
+    (SynDecl { tcdLName = dL->L _ name
+             , tcdTyVars = ktvs
+             , tcdRhs = rhs })
+  = do { let ctxt = TySynKindCtxt name
+       ; tc <- kcDeclHeader strategy name TypeSynonymFlavour ktvs $
+               case hsTyKindSig rhs of
+                 Just rhs_sig -> TheKind <$> tcLHsKindSig ctxt rhs_sig
+                 Nothing -> return AnyKind
+       ; return [tc] }
 
 getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec
+getInitialKind _ (FamDecl {tcdFam = XFamilyDecl nec}) = noExtCon nec
 getInitialKind _ (XTyClDecl nec) = noExtCon nec
 
----------------------------------
-getFamDeclInitialKinds
-  :: Bool        -- ^ True <=> cusk
-  -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls
-  -> [LFamilyDecl GhcRn]
-  -> TcM [TcTyCon]
-getFamDeclInitialKinds cusk mb_parent_tycon decls
-  = mapM (addLocM (getFamDeclInitialKind cusk mb_parent_tycon)) decls
-
-getFamDeclInitialKind
-  :: Bool        -- ^ True <=> cusk
-  -> Maybe TyCon -- ^ Just cls <=> this is an associated family of class cls
+get_fam_decl_initial_kind
+  :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls
   -> FamilyDecl GhcRn
   -> TcM TcTyCon
-getFamDeclInitialKind parent_cusk mb_parent_tycon
-    decl@(FamilyDecl { fdLName     = (dL->L _ name)
-                     , fdTyVars    = ktvs
-                     , fdResultSig = (dL->L _ resultSig)
-                     , fdInfo      = info })
-  = do { cusks_enabled <- xoptM LangExt.CUSKs
-       ; kcLHsQTyVars name flav (fam_cusk cusks_enabled) ktvs $
-         case resultSig of
-           KindSig _ ki                              -> tcLHsKindSig ctxt ki
-           TyVarSig _ (dL->L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
-           _ -- open type families have * return kind by default
-             | tcFlavourIsOpen flav              -> return liftedTypeKind
-                    -- closed type families have their return kind inferred
-                    -- by default
-             | otherwise                         -> newMetaKindVar
-       }
+get_fam_decl_initial_kind mb_parent_tycon
+    FamilyDecl { fdLName     = (dL->L _ name)
+               , fdTyVars    = ktvs
+               , fdResultSig = (dL->L _ resultSig)
+               , fdInfo      = info }
+  = kcDeclHeader InitialKindInfer name flav ktvs $
+    case resultSig of
+      KindSig _ ki                              -> TheKind <$> tcLHsKindSig ctxt ki
+      TyVarSig _ (dL->L _ (KindedTyVar _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki
+      _ -- open type families have * return kind by default
+        | tcFlavourIsOpen flav              -> return (TheKind liftedTypeKind)
+               -- closed type families have their return kind inferred
+               -- by default
+        | otherwise                         -> return AnyKind
   where
-    assoc_with_no_cusk = isJust mb_parent_tycon && not parent_cusk
-    fam_cusk cusks_enabled = famDeclHasCusk cusks_enabled assoc_with_no_cusk decl
-    flav = case info of
-      DataFamily         -> DataFamilyFlavour mb_parent_tycon
-      OpenTypeFamily     -> OpenTypeFamilyFlavour mb_parent_tycon
-      ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon )
-                            ClosedTypeFamilyFlavour
-    ctxt  = TyFamResKindCtxt name
-getFamDeclInitialKind _ _ (XFamilyDecl nec) = noExtCon nec
+    flav = getFamFlav mb_parent_tycon info
+    ctxt = TyFamResKindCtxt name
+get_fam_decl_initial_kind _ (XFamilyDecl nec) = noExtCon nec
+
+-- See Note [Standalone kind signatures for associated types]
+check_initial_kind_assoc_fam
+  :: TcTyCon -- parent class
+  -> FamilyDecl GhcRn
+  -> TcM TcTyCon
+check_initial_kind_assoc_fam cls
+  FamilyDecl
+    { fdLName     = unLoc -> name
+    , fdTyVars    = ktvs
+    , fdResultSig = unLoc -> resultSig
+    , fdInfo      = info }
+  = kcDeclHeader (InitialKindCheck CUSK) name flav ktvs $
+    case famResultKindSignature resultSig of
+      Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
+      Nothing -> return (TheKind liftedTypeKind)
+  where
+    ctxt = TyFamResKindCtxt name
+    flav = getFamFlav (Just cls) info
+check_initial_kind_assoc_fam _ (XFamilyDecl nec) = noExtCon nec
+
+{- Note [Standalone kind signatures for associated types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+If associated types had standalone kind signatures, would they wear them
+
+---------------------------+------------------------------
+  like this? (OUT)         |   or like this? (IN)
+---------------------------+------------------------------
+  type T :: Type -> Type   |   class C a where
+  class C a where          |     type T :: Type -> Type
+    type T a               |     type T a
+
+The (IN) variant is syntactically ambiguous:
+
+  class C a where
+    type T :: a   -- standalone kind signature?
+    type T :: a   -- declaration header?
+
+The (OUT) variant does not suffer from this issue, but it might not be the
+direction in which we want to take Haskell: we seek to unify type families and
+functions, and, by extension, associated types with class methods. And yet we
+give class methods their signatures inside the class, not outside. Neither do
+we have the counterpart of InstanceSigs for StandaloneKindSignatures.
+
+For now, we dodge the question by using CUSKs for associated types instead of
+standalone kind signatures. This is a simple addition to the rule we used to
+have before standalone kind signatures:
+
+  old rule:  associated type has a CUSK iff its parent class has a CUSK
+  new rule:  associated type has a CUSK iff its parent class has a CUSK or a standalone kind signature
+
+-}
+
+-- See Note [Data declaration default result kind]
+dataDeclDefaultResultKind :: NewOrData -> TcM ContextKind
+dataDeclDefaultResultKind new_or_data = do
+  -- See Note [Implementation of UnliftedNewtypes]
+  unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+  return $ case new_or_data of
+    NewType | unlifted_newtypes -> OpenKind
+    _ -> TheKind liftedTypeKind
+
+{- Note [Data declaration default result kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When the user has not written an inline result kind annotation on a data
+declaration, we assume it to be 'Type'. That is, the following declarations
+D1 and D2 are considered equivalent:
+
+  data D1         where ...
+  data D2 :: Type where ...
+
+The consequence of this assumption is that we reject D3 even though we
+accept D4:
+
+  data D3 where
+    MkD3 :: ... -> D3 param
+
+  data D4 :: Type -> Type where
+    MkD4 :: ... -> D4 param
+
+However, there's a twist: when -XUnliftedNewtypes are enabled, we must relax
+the assumed result kind to (TYPE r) for newtypes:
+
+  newtype D5 where
+    MkD5 :: Int# -> D5
+
+dataDeclDefaultResultKind takes care to produce the appropriate result kind.
+-}
+
+---------------------------------
+getFamFlav
+  :: Maybe TcTyCon    -- ^ Just cls <=> this is an associated family of class cls
+  -> FamilyInfo pass
+  -> TyConFlavour
+getFamFlav mb_parent_tycon info =
+  case info of
+    DataFamily         -> DataFamilyFlavour mb_parent_tycon
+    OpenTypeFamily     -> OpenTypeFamilyFlavour mb_parent_tycon
+    ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) -- See Note [Closed type family mb_parent_tycon]
+                          ClosedTypeFamilyFlavour
+
+{- Note [Closed type family mb_parent_tycon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There's no way to write a closed type family inside a class declaration:
+
+  class C a where
+    type family F a where  -- error: parse error on input ‘where’
+
+In fact, it is not clear what the meaning of such a declaration would be.
+Therefore, 'mb_parent_tycon' of any closed type family has to be Nothing.
+-}
 
 ------------------------------------------------------------------------
 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
@@ -1139,7 +1269,7 @@ kcTyClDecl :: TyClDecl GhcRn -> TcM ()
 -- This function is used solely for its side effect on kind variables
 -- NB kind signatures on the type variables and
 --    result kind signature have already been dealt with
---    by getInitialKind, so we can ignore them here.
+--    by inferInitialKind, so we can ignore them here.
 
 kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
                      , tcdDataDefn = defn })
@@ -1150,7 +1280,7 @@ kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
          -- See Note [Implementation of UnliftedNewtypes] STEP 2
        ; kcConDecls new_or_data (tyConResKind tyCon) cons
        }
-    -- hs_tvs and dd_kindSig already dealt with in getInitialKind
+    -- hs_tvs and dd_kindSig already dealt with in inferInitialKind
     -- This must be a GADT-style decl,
     --        (see invariants of DataDefn declaration)
     -- so (a) we don't need to bring the hs_tvs into scope, because the
@@ -1170,7 +1300,7 @@ kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs })
   = bindTyClTyVars name $ \ _ res_kind ->
     discardResult $ tcCheckLHsType rhs res_kind
         -- NB: check against the result kind that we allocated
-        -- in getInitialKinds.
+        -- in inferInitialKinds.
 
 kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name)
                       , tcdCtxt = ctxt, tcdSigs = sigs })
@@ -1304,7 +1434,7 @@ corner, to pass to kcConDecl c.f. #16828. Hence the splitPiTys here.
 I am a bit concerned about tycons with a declaration like
    data T a :: Type -> forall k. k -> Type  where ...
 
-It does not have a CUSK, so kcLHsQTyVars_NonCusk will make a TcTyCon
+It does not have a CUSK, so kcInferDeclHeader will make a TcTyCon
 with tyConResKind of Type -> forall k. k -> Type.  Even that is fine:
 the splitPiTys will look past the forall.  But I'm bothered about
 what if the type "in the corner" metions k?  This is incredibly
@@ -1468,7 +1598,7 @@ Expected behavior of UnliftedNewtypes:
 What follows is a high-level overview of the implementation of the
 proposal.
 
-STEP 1: Getting the initial kind, as done by getInitialKind. We have
+STEP 1: Getting the initial kind, as done by inferInitialKind. We have
 two sub-cases (assuming we have a newtype and -XUnliftedNewtypes is enabled):
 
 * With a CUSK: no change in kind-checking; the tycon is given the kind
@@ -1489,7 +1619,7 @@ enabled (we use r0 to denote a unification variable):
 
 newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
 + kcConDecl unifies (TYPE r0) with (TYPE rep), where (TYPE r0)
-  is the kind that getInitialKind invented for (Foo rep).
+  is the kind that inferInitialKind invented for (Foo rep).
 
 data Color = Red | Blue
 type family Interpret (x :: Color) :: RuntimeRep where
@@ -1587,6 +1717,10 @@ wiredInDerivInfo tycon decl
   | DataDecl { tcdDataDefn = dataDefn } <- decl
   , HsDataDefn { dd_derivs = derivs } <- dataDefn
   = [ DerivInfo { di_rep_tc = tycon
+                , di_scoped_tvs =
+                    if isFunTyCon tycon || isPrimTyCon tycon
+                       then []  -- no tyConTyVars
+                       else mkTyVarNamePairs (tyConTyVars tycon)
                 , di_clauses = unLoc derivs
                 , di_ctxt = tcMkDeclCtxt decl } ]
 wiredInDerivInfo _ _ = []
@@ -1645,8 +1779,7 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
   = fixM $ \ clas ->
     -- We need the knot because 'clas' is passed into tcClassATs
     bindTyClTyVars class_name $ \ binders res_kind ->
-    do { MASSERT2( tcIsConstraintKind res_kind
-                 , ppr class_name $$ ppr res_kind )
+    do { checkClassKindSig res_kind
        ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
        ; let tycon_name = class_name        -- We use the same name
              roles = roles_info tycon_name  -- for TyCon and Class
@@ -1983,7 +2116,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
 
          -- Process the equations, creating CoAxBranches
        ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind
-                                   [] False {- this doesn't matter here -}
+                                   noTcTyConScopedTyVars
+                                   False {- this doesn't matter here -}
                                    ClosedTypeFamilyFlavour
 
        ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc NotAssociated) eqns
@@ -2082,7 +2216,7 @@ tcDataDefn err_ctxt
            (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                        , dd_ctxt = ctxt
                        , dd_kindSig = mb_ksig  -- Already in tc's kind
-                                               -- via getInitialKinds
+                                               -- via inferInitialKinds
                        , dd_cons = cons
                        , dd_derivs = derivs })
  =  do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons
@@ -2122,7 +2256,11 @@ tcDataDefn err_ctxt
                                   stupid_theta tc_rhs
                                   (VanillaAlgTyCon tc_rep_nm)
                                   gadt_syntax) }
+       ; tctc <- tcLookupTcTyCon tc_name
+            -- 'tctc' is a 'TcTyCon' and has the 'tcTyConScopedTyVars' that we need
+            -- unlike the finalized 'tycon' defined above which is an 'AlgTyCon'
        ; let deriv_info = DerivInfo { di_rep_tc = tycon
+                                    , di_scoped_tvs = tcTyConScopedTyVars tctc
                                     , di_clauses = unLoc derivs
                                     , di_ctxt = err_ctxt }
        ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
@@ -2299,7 +2437,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
        -- have checked that the number of patterns matches tyConArity
 
        -- This code is closely related to the code
-       -- in TcHsType.kcLHsQTyVars_Cusk
+       -- in TcHsType.kcCheckDeclHeader_cusk
        ; (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty)))
                <- pushTcLevelM_                                $
                   solveEqualities                              $
@@ -4098,7 +4236,7 @@ badMethPred sel_id pred
 
 noClassTyVarErr :: Class -> TyCon -> SDoc
 noClassTyVarErr clas fam_tc
-  = sep [ text "The associated type" <+> quotes (ppr fam_tc)
+  = sep [ text "The associated type" <+> quotes (ppr fam_tc <+> hsep (map ppr (tyConTyVars fam_tc)))
         , text "mentions none of the type or kind variables of the class" <+>
                 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
 
index 7fe9476..7fa45ae 100644 (file)
@@ -596,6 +596,8 @@ data UserTypeCtxt
   | InfSigCtxt Name     -- Inferred type for function
   | ExprSigCtxt         -- Expression type signature
   | KindSigCtxt         -- Kind signature
+  | StandaloneKindSigCtxt  -- Standalone kind signature
+       Name                -- Name of the type/class
   | TypeAppCtxt         -- Visible type application
   | ConArgCtxt Name     -- Data constructor argument
   | TySynCtxt Name      -- RHS of a type synonym decl
@@ -653,6 +655,7 @@ pprUserTypeCtxt (InfSigCtxt n)    = text "the inferred type for" <+> quotes (ppr
 pprUserTypeCtxt (RuleSigCtxt n)   = text "a RULE for" <+> quotes (ppr n)
 pprUserTypeCtxt ExprSigCtxt       = text "an expression type signature"
 pprUserTypeCtxt KindSigCtxt       = text "a kind signature"
+pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n)
 pprUserTypeCtxt TypeAppCtxt       = text "a type argument"
 pprUserTypeCtxt (ConArgCtxt c)    = text "the type of the constructor" <+> quotes (ppr c)
 pprUserTypeCtxt (TySynCtxt c)     = text "the RHS of the type synonym" <+> quotes (ppr c)
index eaec2db..307ec6d 100644 (file)
@@ -232,6 +232,7 @@ wantAmbiguityCheck ctxt
       GhciCtxt {}  -> False
       TySynCtxt {} -> False
       TypeAppCtxt  -> False
+      StandaloneKindSigCtxt{} -> False
       _            -> True
 
 checkUserTypeError :: Type -> TcM ()
@@ -280,6 +281,10 @@ In a few places we do not want to check a user-specified type for ambiguity
      f @ty
   No need to check ty for ambiguity
 
+* StandaloneKindSigCtxt: type T :: ksig
+  Kinds need a different ambiguity check than types, and the currently
+  implemented check is only good for types. See #14419, in particular
+  https://gitlab.haskell.org/ghc/ghc/issues/14419#note_160844
 
 ************************************************************************
 *                                                                      *
@@ -343,6 +348,7 @@ checkValidType ctxt ty
 
                  ExprSigCtxt    -> rank1
                  KindSigCtxt    -> rank1
+                 StandaloneKindSigCtxt{} -> rank1
                  TypeAppCtxt | impred_flag -> ArbitraryRank
                              | otherwise   -> tyConArgMonoType
                     -- Normally, ImpredicativeTypes is handled in check_arg_type,
@@ -463,6 +469,7 @@ allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
 allConstraintsAllowed (DataKindCtxt {})      = False
 allConstraintsAllowed (TySynKindCtxt {})     = False
 allConstraintsAllowed (TyFamResKindCtxt {})  = False
+allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
 allConstraintsAllowed _ = True
 
 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
@@ -482,6 +489,7 @@ allConstraintsAllowed _ = True
 vdqAllowed :: UserTypeCtxt -> Bool
 -- Currently allowed in the kinds of types...
 vdqAllowed (KindSigCtxt {}) = True
+vdqAllowed (StandaloneKindSigCtxt {}) = True
 vdqAllowed (TySynCtxt {}) = True
 vdqAllowed (ThBrackCtxt {}) = True
 vdqAllowed (GhciCtxt {}) = True
@@ -1329,6 +1337,7 @@ okIPCtxt (TySynCtxt {})         = True   -- e.g.   type Blah = ?x::Int
                                          -- #11466
 
 okIPCtxt (KindSigCtxt {})       = False
+okIPCtxt (StandaloneKindSigCtxt {}) = False
 okIPCtxt (ClassSCCtxt {})       = False
 okIPCtxt (InstDeclCtxt {})      = False
 okIPCtxt (SpecInstCtxt {})      = False
@@ -2149,7 +2158,7 @@ checkFamPatBinders fam_tc qtvs pats rhs
          --    data T            = MkT (forall (a::k). blah)
          --    data family D Int = MkD (forall (a::k). blah)
          -- In both cases, 'k' is not bound on the LHS, but is used on the RHS
-         -- We catch the former in kcLHsQTyVars, and the latter right here
+         -- We catch the former in kcDeclHeader, and the latter right here
          -- See Note [Check type-family instance binders]
        ; check_tvs bad_rhs_tvs (text "mentioned in the RHS")
                                (text "bound on the LHS of")
index 19f3f0e..7af2bc0 100644 (file)
@@ -41,6 +41,7 @@ module TyCon(
         mkFamilyTyCon,
         mkPromotedDataCon,
         mkTcTyCon,
+        noTcTyConScopedTyVars,
 
         -- ** Predicates on TyCons
         isAlgTyCon, isVanillaAlgTyCon,
@@ -477,6 +478,8 @@ isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
 -- Works for IfaceTyConBinder too
 isInvisibleTyConBinder tcb = not (isVisibleTyConBinder tcb)
 
+-- Build the 'tyConKind' from the binders and the result kind.
+-- Keep in sync with 'mkTyConKind' in iface/IfaceType.
 mkTyConKind :: [TyConBinder] -> Kind -> Kind
 mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
   where
@@ -1702,6 +1705,10 @@ mkTcTyCon name binders res_kind scoped_tvs poly flav
             , tcTyConIsPoly       = poly
             , tcTyConFlavour      = flav }
 
+-- | No scoped type variables (to be used with mkTcTyCon).
+noTcTyConScopedTyVars :: [(Name, TcTyVar)]
+noTcTyConScopedTyVars = []
+
 -- | Create an unlifted primitive 'TyCon', such as @Int#@.
 mkPrimTyCon :: Name -> [TyConBinder]
             -> Kind   -- ^ /result/ kind, never levity-polymorphic
index d8664eb..f8cd1da 100644 (file)
@@ -42,7 +42,8 @@ module Type (
         mkSpecForAllTy, mkSpecForAllTys,
         mkVisForAllTys, mkTyCoInvForAllTy,
         mkInvForAllTy, mkInvForAllTys,
-        splitForAllTys, splitForAllTysSameVis, splitForAllVarBndrs,
+        splitForAllTys, splitForAllTysSameVis,
+        splitForAllVarBndrs,
         splitForAllTy_maybe, splitForAllTy,
         splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
         splitPiTy_maybe, splitPiTy, splitPiTys,
index e8316d7..907f7e2 100644 (file)
@@ -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>`__),
index 8ec105f..de0aabb 100644 (file)
@@ -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
 --------------------------------------
index ef1d5c9..3f22518 100644 (file)
@@ -142,4 +142,5 @@ data Extension
    | StarIsType
    | ImportQualifiedPost
    | CUSKs
+   | StandaloneKindSignatures
    deriving (Eq, Enum, Show, Generic, Bounded)
index 8631176..7bb4eb5 100644 (file)
@@ -85,7 +85,7 @@ module Language.Haskell.TH.Lib (
     viaStrategy, DerivStrategy(..),
     -- **** Class
     classD, instanceD, instanceWithOverlapD, Overlap(..),
-    sigD, standaloneDerivD, standaloneDerivWithStrategyD, defaultSigD,
+    sigD, kiSigD, standaloneDerivD, standaloneDerivWithStrategyD, defaultSigD,
 
     -- **** Role annotations
     roleAnnotD,
index 5ec59b3..4d3887b 100644 (file)
@@ -435,6 +435,9 @@ instanceWithOverlapD o ctxt ty decs =
 sigD :: Name -> TypeQ -> DecQ
 sigD fun ty = liftM (SigD fun) $ ty
 
+kiSigD :: Name -> KindQ -> DecQ
+kiSigD fun ki = liftM (KiSigD fun) $ ki
+
 forImpD :: Callconv -> Safety -> String -> Name -> TypeQ -> DecQ
 forImpD cc s str n ty
  = do ty' <- ty
index 792a78b..98ddd1c 100644 (file)
@@ -341,6 +341,7 @@ ppr_dec _ (InstanceD o ctxt i ds) =
         text "instance" <+> maybe empty ppr_overlap o <+> pprCxt ctxt <+> ppr i
                                   $$ where_clause ds
 ppr_dec _ (SigD f t)    = pprPrefixOcc f <+> dcolon <+> ppr t
+ppr_dec _ (KiSigD f k)  = text "type" <+> pprPrefixOcc f <+> dcolon <+> ppr k
 ppr_dec _ (ForeignD f)  = ppr f
 ppr_dec _ (InfixD fx n) = pprFixity n fx
 ppr_dec _ (PragmaD p)   = ppr p
index 72eadbf..59cc5dc 100644 (file)
@@ -2029,6 +2029,7 @@ data Dec
                                   -- ^ @{ instance {\-\# OVERLAPS \#-\}
                                   --        Show w => Show [w] where ds }@
   | SigD Name Type                -- ^ @{ length :: [a] -> Int }@
+  | KiSigD Name Kind              -- ^ @{ type TypeRep :: k -> Type }@
   | ForeignD Foreign              -- ^ @{ foreign import ... }
                                   --{ foreign export ... }@
 
index 07159cf..0cb8d9c 100644 (file)
@@ -8,8 +8,10 @@
 bkpfail04.bkp:7:9: error:
     • Type constructor ‘A’ has conflicting definitions in the module
       and its hsig file
-      Main module: data A = A {foo :: Int}
-      Hsig file:  data A = A {bar :: Bool}
+      Main module: type A :: *
+                   data A = A {foo :: Int}
+      Hsig file:  type A :: *
+                  data A = A {bar :: Bool}
       The constructors do not match:
         The record label lists for ‘A’ differ
         The types for ‘A’ differ
index 27e0ddf..a707bf0 100644 (file)
@@ -14,7 +14,9 @@
 bkpfail06.bkp:10:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
-      Main module: data T = T GHC.Types.Bool
-      Hsig file:  data T = T GHC.Types.Int
+      Main module: type T :: *
+                   data T = T GHC.Types.Bool
+      Hsig file:  type T :: *
+                  data T = T GHC.Types.Int
       The constructors do not match: The types for ‘T’ differ
     • while checking that qimpl:H implements signature H in p[H=qimpl:H]
index f8cf6b0..0527703 100644 (file)
@@ -10,7 +10,9 @@
 bkpfail07.bkp:6:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
-      Main module: data T = T GHC.Types.Bool
-      Hsig file:  data T = T GHC.Types.Int
+      Main module: type T :: *
+                   data T = T GHC.Types.Bool
+      Hsig file:  type T :: *
+                  data T = T GHC.Types.Int
       The constructors do not match: The types for ‘T’ differ
     • while checking that h[A=<A>]:H implements signature H in p[H=h[A=<A>]:H]
index 70b0853..78ceaff 100644 (file)
 bkpfail10.bkp:8:9: error:
     • Type constructor ‘H’ has conflicting definitions in the module
       and its hsig file
-      Main module: data H a = H a
-      Hsig file:  data H
+      Main module: type H :: * -> *
+                   data H a = H a
+      Hsig file:  type H :: *
+                  data H
       The types have different kinds
     • while checking that q:H implements signature H in p[H=q:H]
 
index 7bd5c57..81e47ec 100644 (file)
@@ -9,8 +9,10 @@
 <no location info>: error:
     • Type constructor ‘Either’ has conflicting definitions in the module
       and its hsig file
-      Main module: data Either a b = Left a | Right b
+      Main module: type Either :: * -> * -> *
+                   data Either a b = Left a | Right b
       Hsig file:  type role Either representational phantom phantom
+                  type Either :: * -> * -> * -> *
                   data Either a b c = Left a
       The types have different kinds
     • while checking that Prelude implements signature ShouldFail in p[ShouldFail=Prelude]
index fe066bd..cb0a0e2 100644 (file)
@@ -16,6 +16,8 @@
 bkpfail22.bkp:16:9: error:
     • Type constructor ‘S’ has conflicting definitions in the module
       and its hsig file
-      Main module: type S = ()
-      Hsig file:  type S = GHC.Types.Bool
+      Main module: type S :: *
+                   type S = ()
+      Hsig file:  type S :: *
+                  type S = GHC.Types.Bool
     • while checking that badimpl:H2 implements signature H2 in q[H2=badimpl:H2]
index 00a19e2..6a2eb8c 100644 (file)
 bkpfail23.bkp:14:9: error:
     • Type constructor ‘F’ has conflicting definitions in the module
       and its hsig file
-      Main module: type F a = ()
+      Main module: type F :: * -> *
+                   type F a = ()
       Hsig file:  type role F phantom
+                  type F :: * -> *
                   data F a
       Illegal parameterized type synonym in implementation of abstract data.
       (Try eta reducing your type synonym so that it is nullary.)
index 1a9c573..cedcd30 100644 (file)
@@ -18,7 +18,9 @@ bkpfail25.bkp:7:18: warning: [-Wmissing-methods (in -Wdefault)]
 bkpfail25.bkp:12:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
-      Main module: type T a = a
+      Main module: type T :: * -> *
+                   type T a = a
       Hsig file:  type role T nominal
+                  type T :: * -> *
                   data T a
     • while checking that q:H implements signature H in p[H=q:H]
index 3de59a2..09410ce 100644 (file)
 bkpfail26.bkp:15:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
-      Main module: type T a = [a]
+      Main module: type T :: * -> *
+                   type T a = [a]
       Hsig file:  type role T nominal
+                  type T :: * -> *
                   data T a
       Illegal parameterized type synonym in implementation of abstract data.
       (Try eta reducing your type synonym so that it is nullary.)
index dfadb40..bc5a8c6 100644 (file)
@@ -13,7 +13,9 @@
 bkpfail27.bkp:15:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
-      Main module: type T = F
-      Hsig file:  data T
+      Main module: type T :: *
+                   type T = F
+      Hsig file:  type T :: *
+                  data T
       Illegal type family application in implementation of abstract data.
     • while checking that q:H implements signature H in p[H=q:H]
index 9a1b421..6cd72dc 100644 (file)
 bkpfail41.bkp:10:9: error:
     • Class ‘C’ has conflicting definitions in the module
       and its hsig file
-      Main module: class C a where
+      Main module: type C :: * -> Constraint
+                   class C a where
                      f :: a -> a
                      {-# MINIMAL f #-}
-      Hsig file:  class C a where
+      Hsig file:  type C :: * -> Constraint
+                  class C a where
                     f :: a -> a
                     default f :: a -> a
       The methods do not match:
index 467ab71..5b07891 100644 (file)
@@ -6,10 +6,12 @@
 bkpfail42.bkp:9:9: error:
     • Type constructor ‘F’ has conflicting definitions in the module
       and its hsig file
-      Main module: type family F a :: *
-                     where F a = Int
-      Hsig file:  type family F a :: *
-                    where F a = Bool
+      Main module: type F :: * -> *
+                   type family F a where
+                       F a = Int
+      Hsig file:  type F :: * -> *
+                  type family F a where
+                      F a = Bool
     • while merging the signatures from:
         • p[A=<A>]:A
         • ...and the local signature for A
index 7377693..f28f183 100644 (file)
@@ -14,8 +14,10 @@ bkpfail45.bkp:13:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
       Main module: type role T phantom
+                   type T :: * -> *
                    data T a = T
       Hsig file:  type role T nominal
+                  type T :: * -> *
                   data T a = T
       The roles do not match.
       Roles on abstract types default to ‘representational’ in boot files.
index 9aeaccb..908866f 100644 (file)
 bkpfail46.bkp:15:9: error:
     • Type constructor ‘K’ has conflicting definitions in the module
       and its hsig file
-      Main module: type K a = GHC.Classes.Eq a :: Constraint
-      Hsig file:  class K a
+      Main module: type K :: * -> Constraint
+                   type K a = GHC.Classes.Eq a :: Constraint
+      Hsig file:  type K :: * -> Constraint
+                  class K a
       Illegal parameterized type synonym in implementation of abstract data.
       (Try eta reducing your type synonym so that it is nullary.)
     • while checking that q:A implements signature A in p[A=q:A]
index b2bc08b..0eb58d8 100644 (file)
@@ -9,8 +9,10 @@ bkpfail47.bkp:9:9: error:
     • Type constructor ‘T’ has conflicting definitions in the module
       and its hsig file
       Main module: type role T representational nominal
+                   type T :: * -> * -> *
                    data T a b = MkT
       Hsig file:  type role T nominal representational
+                  type T :: * -> * -> *
                   data T a b
       The roles are not compatible:
       Main module: [representational, nominal]
index 7a50b60..5bc41b9 100644 (file)
@@ -1,5 +1,5 @@
 {-# LANGUAGE TemplateHaskell, TypeOperators, PolyKinds, DataKinds,
-             TypeFamilies #-}
+             TypeFamilies, RankNTypes #-}
 
 module A where
 
index 7075325..13ac024 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, PolyKinds #-}
+{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
 
 module GADTVars where
 
index c432e4b..fd70fcc 100644 (file)
@@ -41,6 +41,7 @@ expectedGhcOnlyExtensions = ["RelaxedLayout",
                              "AlternativeLayoutRuleTransitional",
                              "UnliftedNewtypes",
                              "CUSKs",
+                             "StandaloneKindSignatures",
                              "ImportQualifiedPost"]
 
 expectedCabalOnlyExtensions :: [String]
index 5601247..41efe82 100644 (file)
@@ -1,8 +1,10 @@
+type C :: * -> * -> Constraint
 class C a b where
   c1 :: Num b => a -> b
   c2 :: (Num b, Show b) => a -> b
   c3 :: a1 -> b
   {-# MINIMAL c1, c2, c3 #-}
+type C :: * -> * -> Constraint
 class C a b where
   c1 :: Num b => a -> b
   c2 :: (Num b, Show b) => a -> b
index 4f7d480..069ea31 100644 (file)
@@ -1,2 +1,4 @@
-data Infix a b = a :@: b       -- Defined at <interactive>:2:18
+type Infix :: * -> * -> *
+data Infix a b = a :@: b
+       -- Defined at <interactive>:2:18
 infixl 4 :@:
index 955c95a..3832719 100644 (file)
@@ -1,4 +1,7 @@
-class (a ~ b) => (~) (a :: k) (b :: k)         -- Defined in ‘GHC.Types’
+type (~) :: forall k. k -> k -> Constraint
+class (a ~ b) => (~) a b
+       -- Defined in ‘GHC.Types’
 (~) :: k -> k -> Constraint
-class (a GHC.Prim.~# b) => (~) (a :: k) (b :: k)
+type (~) :: forall k. k -> k -> Constraint
+class (a GHC.Prim.~# b) => (~) a b
        -- Defined in ‘GHC.Types’
index 34cde4a..5e4b70c 100644 (file)
@@ -1,4 +1,5 @@
-class Defer (p :: Constraint) where
+type Defer :: Constraint -> Constraint
+class Defer p where
   defer :: (p => r) -> r
   {-# MINIMAL defer #-}
        -- Defined at <interactive>:5:1
index c7173fc..81be552 100644 (file)
@@ -11,12 +11,14 @@ f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
 f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
 f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
 fmap ∷ ∀ {f ∷ ★ → ★} {a} {b}. Functor f ⇒ (a → b) → f a → f b
-class Functor (f ∷ ★ → ★) where
+type Functor :: (★ → ★) → Constraint
+class Functor f where
   fmap ∷ ∀ a b. (a → b) → f a → f b
   ...
        -- Defined in ‘GHC.Base’
 Functor ∷ (★ → ★) → Constraint
-class Functor (f ∷ ★ → ★) where
+type Functor :: (★ → ★) → Constraint
+class Functor f where
   fmap ∷ ∀ a b. (a → b) → f a → f b
   (<$) ∷ ∀ a b. a → f b → f a
   {-# MINIMAL fmap #-}
@@ -56,7 +58,8 @@ datatypeName
   ∷ ∀ {d} {t ∷ ★ → (★ → ★) → ★ → ★} {f ∷ ★ → ★} {a}.
     Datatype d ⇒
     t d f a → [Char]
-class Datatype (d ∷ k) where
+type Datatype :: ∀ {k}. k → Constraint
+class Datatype d where
   datatypeName ∷ ∀ k1 (t ∷ k → (k1 → ★) → k1 → ★) (f ∷ k1 → ★)
                    (a ∷ k1).
                  t d f a → [Char]
index 083f3a8..85d73d9 100644 (file)
@@ -1,3 +1,4 @@
 type role Foo phantom phantom
-data Foo (a :: * -> *) (b :: k)
+type Foo :: (* -> *) -> forall k. k -> *
+data Foo a b
        -- Defined at <interactive>:3:1
index c6dbaf2..030b902 100644 (file)
@@ -1,4 +1,5 @@
-type family F a :: * where
+type F :: * -> *
+type family F a where
     F [Int] = Bool
     F [a] = Double
     F (a b) = Char
index b5950a7..7c30448 100644 (file)
@@ -1,8 +1,10 @@
+type Foo :: *
 data Foo
   = Foo {foo1 :: Int,
          foo2 :: !Int,
          foo3 :: Maybe Int,
          foo4 :: !(Maybe Int)}
        -- Defined at T13699.hs:3:1
+type Bar :: *
 data Bar = Bar Int !Int (Maybe Int) !(Maybe Int)
        -- Defined at T13699.hs:10:1
index e2555f9..403b504 100644 (file)
@@ -1,6 +1,8 @@
-type family Foo (a :: k) :: k where
+type Foo :: forall k. k -> k
+type family Foo a where
   forall k (a :: k). Foo a = a
        -- Defined at T15341.hs:5:1
-type family Foo @k (a :: k) :: k where
+type Foo :: forall k. k -> k
+type family Foo @k a where
   forall k (a :: k). Foo @k a = a
        -- Defined at T15341.hs:5:1
index 5dc8cf3..d14b442 100644 (file)
@@ -1,8 +1,10 @@
-type family E a b :: * where
+type E :: * -> * -> *
+type family E a b where
     E a a = ()
     E a b = Bool
        -- Defined at <interactive>:2:1
-type family E a b :: * where
+type E :: * -> * -> *
+type family E a b where
   {- #0 -} E a a = ()
   {- #1 -} E a b = Bool
       -- incompatible with: #0
index 50df504..8b403d4 100644 (file)
@@ -1,9 +1,14 @@
-type family F1 (a :: k) :: *   -- Defined at T15827.hs:9:1
+type F1 :: forall k. k -> *
+type family F1 a
+       -- Defined at T15827.hs:9:1
 type instance forall k (a :: k). F1 a = Proxy a
        -- Defined at T15827.hs:10:34
-type family F2 (a :: k) :: * where
+type F2 :: forall k. k -> *
+type family F2 a where
   forall k (a :: k). F2 a = Proxy a
        -- Defined at T15827.hs:12:1
-data family D (a :: k)         -- Defined at T15827.hs:15:1
+type D :: forall k. k -> *
+data family D a
+       -- Defined at T15827.hs:15:1
 data instance forall k (a :: k). D a = MkD (Proxy a)
        -- Defined at T15827.hs:16:34
index 6236311..e1aa200 100644 (file)
@@ -1,5 +1,6 @@
 MkFun :: (a -> b) -> Fun a b
 Fun :: (a ~ 'OP) => * -> * -> *
+type Fun :: forall (a :: WHICH). (a ~ 'OP) => * -> * -> *
 data Fun b c where
   MkFun :: (b -> c) -> Fun b c
        -- Defined at T15872.hs:11:1
@@ -7,10 +8,10 @@ MkFun
   :: (a -> b) -> Fun @'OP @{'GHC.Types.Eq# @WHICH @'OP @'OP <>} a b
 Fun :: ((a :: WHICH) ~ ('OP :: WHICH)) => * -> * -> *
 type role Fun nominal nominal representational representational
-data Fun @(a :: WHICH)
-         @{a1 :: (a :: WHICH) ~ ('OP :: WHICH)}
-         b
-         c where
+type Fun :: forall (a :: WHICH).
+            ((a :: WHICH) ~ ('OP :: WHICH)) =>
+            * -> * -> *
+data Fun @a @{a1} b c where
   MkFun :: (b -> c)
            -> Fun @'OP @{'GHC.Types.Eq# @WHICH @'OP @'OP <>} b c
        -- Defined at T15872.hs:11:1
index c6f31a7..f9e6d33 100644 (file)
@@ -1,3 +1,4 @@
+type T :: * -> * -> *
 type T =
   (->) @{'GHC.Types.LiftedRep} @{'GHC.Types.LiftedRep} :: * -> * -> *
        -- Defined at <interactive>:2:1
index d1691a6..4efa27c 100644 (file)
@@ -1,20 +1,26 @@
 type role Foo1 phantom
-data Foo1 (a :: k) where
+type Foo1 :: forall k. k -> *
+data Foo1 a where
   MkFoo1a :: forall k (a :: k). Proxy a -> Int -> Foo1 a
   MkFoo1b :: forall k (a :: k). {a :: Proxy a, b :: Int} -> Foo1 a
        -- Defined at T16030.hs:8:1
-data family Foo2 (a :: k)      -- Defined at T16030.hs:12:1
+type Foo2 :: forall k. k -> *
+data family Foo2 a
+       -- Defined at T16030.hs:12:1
 data instance forall k (a :: k). Foo2 a where
   MkFoo2a :: forall k (a :: k). Proxy a -> Int -> Foo2 a
   MkFoo2b :: forall k (a :: k). {c :: Proxy a, d :: Int} -> Foo2 a
        -- Defined at T16030.hs:13:15
 type role Foo1 nominal phantom
-data Foo1 @k (a :: k) where
+type Foo1 :: forall k. k -> *
+data Foo1 @k a where
   MkFoo1a :: forall k (a :: k). Proxy @{k} a -> Int -> Foo1 @k a
   MkFoo1b :: forall k (a :: k).
              {a :: Proxy @{k} a, b :: Int} -> Foo1 @k a
        -- Defined at T16030.hs:8:1
-data family Foo2 @k (a :: k)   -- Defined at T16030.hs:12:1
+type Foo2 :: forall k. k -> *
+data family Foo2 @k a
+       -- Defined at T16030.hs:12:1
 data instance forall k (a :: k). Foo2 @k a where
   MkFoo2a :: forall k (a :: k). Proxy @{k} a -> Int -> Foo2 @k a
   MkFoo2b :: forall k (a :: k).
index fd4e0ef..40688b5 100644 (file)
@@ -1,3 +1,4 @@
+type T :: *
 data T where
   MkT1 :: (Int -> Int) -> T
   MkT2 :: (forall a. Maybe a) -> T
index 4ce312c..cd88672 100644 (file)
@@ -1,20 +1,31 @@
+type R :: *
 data R
   = R {x :: Char, y :: Int, z :: Float}
   | S {x :: Char}
   | T {y :: Int, z :: Float}
   | W
+type R :: *
 data R
   = R {x :: Char, y :: Int, z :: Float}
   | S {x :: Char}
   | T {y :: Int, z :: Float}
   | W
        -- Defined at T4015.hs:3:1
-data R = ... | S {...} | ...   -- Defined at T4015.hs:4:10
-data R = ... | T {...} | ...   -- Defined at T4015.hs:5:10
-data R = ... | W       -- Defined at T4015.hs:6:10
+type R :: *
+data R = ... | S {...} | ...
+       -- Defined at T4015.hs:4:10
+type R :: *
+data R = ... | T {...} | ...
+       -- Defined at T4015.hs:5:10
+type R :: *
+data R = ... | W
+       -- Defined at T4015.hs:6:10
+type R :: *
 data R = R {x :: Char, ...} | S {x :: Char} | ...
        -- Defined at T4015.hs:3:14
+type R :: *
 data R = R {..., y :: Int, ...} | ... | T {y :: Int, ...} | ...
        -- Defined at T4015.hs:3:25
+type R :: *
 data R = R {..., z :: Float} | ... | T {..., z :: Float} | ...
        -- Defined at T4015.hs:3:35
index 3f600bd..8dafaa8 100644 (file)
@@ -1,4 +1,5 @@
 type role Equal nominal nominal
+type Equal :: * -> * -> *
 data Equal a b where
   Equal :: Equal a a
        -- Defined at T4087.hs:5:1
index 9dfcd6c..52d8a68 100644 (file)
@@ -1,21 +1,30 @@
-type family A a b :: *         -- Defined at T4175.hs:7:1
+type A :: * -> * -> *
+type family A a b
+       -- Defined at T4175.hs:7:1
 type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15
 type instance A Int Int = ()   -- Defined at T4175.hs:8:15
 type instance A (B a) b = ()   -- Defined at T4175.hs:10:15
-data family B a        -- Defined at T4175.hs:12:1
+type B :: * -> *
+data family B a
+       -- Defined at T4175.hs:12:1
 instance [safe] G B -- Defined at T4175.hs:34:10
 type instance A (B a) b = ()   -- Defined at T4175.hs:10:15
 data instance B () = MkB       -- Defined at T4175.hs:13:15
+type C :: * -> Constraint
 class C a where
-  type family D a b :: *
+  type D :: * -> * -> *
+  type family D a b
        -- Defined at T4175.hs:16:5
 type instance D () () = Bool   -- Defined at T4175.hs:22:10
 type instance D Int () = String        -- Defined at T4175.hs:19:10
-type family E a :: * where
+type E :: * -> *
+type family E a where
     E () = Bool
     E Int = String
        -- Defined at T4175.hs:24:1
-data () = ()   -- Defined in ‘GHC.Tuple’
+type () :: *
+data () = ()
+       -- Defined in ‘GHC.Tuple’
 instance [safe] C () -- Defined at T4175.hs:21:10
 instance Eq () -- Defined in ‘GHC.Classes’
 instance Monoid () -- Defined in ‘GHC.Base’
@@ -28,7 +37,9 @@ instance Bounded () -- Defined in ‘GHC.Enum’
 type instance D () () = Bool   -- Defined at T4175.hs:22:10
 type instance D Int () = String        -- Defined at T4175.hs:19:10
 data instance B () = MkB       -- Defined at T4175.hs:13:15
-data Maybe a = Nothing | Just a        -- Defined in ‘GHC.Maybe’
+type Maybe :: * -> *
+data Maybe a = Nothing | Just a
+       -- Defined in ‘GHC.Maybe’
 instance Applicative Maybe -- Defined in ‘GHC.Base’
 instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Maybe’
 instance Functor Maybe -- Defined in ‘GHC.Base’
@@ -43,7 +54,9 @@ instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’
 instance Foldable Maybe -- Defined in ‘Data.Foldable’
 instance Traversable Maybe -- Defined in ‘Data.Traversable’
 type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15
-data Int = GHC.Types.I# GHC.Prim.Int#  -- Defined in ‘GHC.Types’
+type Int :: *
+data Int = GHC.Types.I# GHC.Prim.Int#
+       -- Defined in ‘GHC.Types’
 instance [safe] C Int -- Defined at T4175.hs:18:10
 instance Eq Int -- Defined in ‘GHC.Classes’
 instance Ord Int -- Defined in ‘GHC.Classes’
@@ -56,5 +69,7 @@ instance Bounded Int -- Defined in ‘GHC.Enum’
 instance Integral Int -- Defined in ‘GHC.Real’
 type instance D Int () = String        -- Defined at T4175.hs:19:10
 type instance A Int Int = ()   -- Defined at T4175.hs:8:15
-class Z a      -- Defined at T4175.hs:28:1
+type Z :: * -> Constraint
+class Z a
+       -- Defined at T4175.hs:28:1
 instance [safe] F (Z a) -- Defined at T4175.hs:31:10
index ab28277..163a923 100644 (file)
@@ -1,9 +1,15 @@
+type B1 :: * -> *
 data B1 a = B1 a
 data instance C.F (B1 a) = B2 a
+type D :: * -> *
 data family D a
+type C.C1 :: * -> Constraint
 class C.C1 a where
+  type C.F :: * -> *
   data family C.F a
+type C.C1 :: * -> Constraint
 class C.C1 a where
+  type C.F :: * -> *
   data family C.F a
        -- Defined at T5417a.hs:7:5
 data instance C.F (B1 a) = B2 a        -- Defined at T5417.hs:8:10
index a8dddd3..faa5f6f 100644 (file)
@@ -1,4 +1,8 @@
-data Foo = Foo         -- Defined at T5820.hs:2:1
+type Foo :: *
+data Foo = Foo
+       -- Defined at T5820.hs:2:1
 instance [safe] Eq Foo -- Defined at T5820.hs:3:10
-data Foo = Foo         -- Defined at T5820.hs:2:1
+type Foo :: *
+data Foo = Foo
+       -- Defined at T5820.hs:2:1
 instance [safe] Eq Foo -- Defined at T5820.hs:3:10
index be1034b..7711a30 100644 (file)
@@ -1 +1,3 @@
-data (?)       -- Defined at <interactive>:2:1
+type (?) :: *
+data (?)
+       -- Defined at <interactive>:2:1
index ea9aaaf..b86ea43 100644 (file)
@@ -1,4 +1,6 @@
-data () = ()   -- Defined in ‘GHC.Tuple’
+type () :: *
+data () = ()
+       -- Defined in ‘GHC.Tuple’
 instance Eq () -- Defined in ‘GHC.Classes’
 instance Monoid () -- Defined in ‘GHC.Base’
 instance Ord () -- Defined in ‘GHC.Classes’
@@ -7,12 +9,16 @@ instance Enum () -- Defined in ‘GHC.Enum’
 instance Show () -- Defined in ‘GHC.Show’
 instance Read () -- Defined in ‘GHC.Read’
 instance Bounded () -- Defined in ‘GHC.Enum’
-data (##) = (##)       -- Defined in ‘GHC.Prim’
+type (##) :: TYPE ('GHC.Types.TupleRep '[])
+data (##) = (##)
+       -- Defined in ‘GHC.Prim’
 () :: ()
 (##) :: (# #)
 (   ) :: ()
 (#   #) :: (# #)
-data (,) a b = (,) a b         -- Defined in ‘GHC.Tuple’
+type (,) :: * -> * -> *
+data (,) a b = (,) a b
+       -- Defined in ‘GHC.Tuple’
 instance Monoid a => Applicative ((,) a) -- Defined in ‘GHC.Base’
 instance (Eq a, Eq b) => Eq (a, b) -- Defined in ‘GHC.Classes’
 instance Functor ((,) a) -- Defined in ‘GHC.Base’
@@ -28,7 +34,12 @@ instance Foldable ((,) a) -- Defined in ‘Data.Foldable’
 instance Traversable ((,) a) -- Defined in ‘Data.Traversable’
 instance (Bounded a, Bounded b) => Bounded (a, b)
   -- Defined in ‘GHC.Enum’
-data (#,#) (a :: TYPE k0) (b :: TYPE k1) = (#,#) a b
+type (#,#) :: *
+              -> *
+              -> TYPE
+                   ('GHC.Types.TupleRep
+                      '[ 'GHC.Types.LiftedRep, 'GHC.Types.LiftedRep])
+data (#,#) a b = (#,#) a b
        -- Defined in ‘GHC.Prim’
 (,) :: a -> b -> (a, b)
 (#,#) :: a -> b -> (# a, b #)
index bf9c1d0..9c3e385 100644 (file)
@@ -1,7 +1,9 @@
 type role A phantom phantom
-data A (x :: k) (y :: k1)
+type A :: forall k k1. k -> k1 -> *
+data A x y
        -- Defined at <interactive>:2:1
 A :: k1 -> k2 -> *
 type role T phantom
-data T (a :: k) = forall a1. MkT a1
+type T :: forall k. k -> *
+data T a = forall a1. MkT a1
        -- Defined at <interactive>:6:1
index 4c577ce..4c8c1dd 100644 (file)
@@ -1,2 +1,6 @@
-type T = forall a. a -> a      -- Defined at <interactive>:2:1
-data D = MkT (forall b. b -> b)        -- Defined at <interactive>:3:1
+type T :: *
+type T = forall a. a -> a
+       -- Defined at <interactive>:2:1
+type D :: *
+data D = MkT (forall b. b -> b)
+       -- Defined at <interactive>:3:1
index bcdebe7..4abcab8 100644 (file)
@@ -1,5 +1,7 @@
+type D2 :: *
 data D2
   = forall k. MkD2 (forall (p :: k -> *) (a :: k). p a -> Int)
        -- Defined at <interactive>:3:1
+type D3 :: *
 data D3 = MkD3 (forall k (p :: k -> *) (a :: k). p a -> Int)
        -- Defined at <interactive>:4:1
index 4c2a602..1b6b04e 100644 (file)
@@ -1,24 +1,32 @@
-class Foo (a :: k) where
-  type family Bar (a :: k) b :: *
+type Foo :: forall k. k -> Constraint
+class Foo a where
+  type Bar :: forall k. k -> * -> *
+  type family Bar a b
        -- Defined at T7939.hs:6:4
 Bar :: k -> * -> *
-type family F a :: *   -- Defined at T7939.hs:8:1
+type F :: * -> *
+type family F a
+       -- Defined at T7939.hs:8:1
 type instance F Int = Bool     -- Defined at T7939.hs:9:15
 F :: * -> *
-type family G a :: * where
+type G :: * -> *
+type family G a where
     G Int = Bool
        -- Defined at T7939.hs:11:1
 G :: * -> *
-type family H (a :: Bool) :: Bool where
+type H :: Bool -> Bool
+type family H a where
     H 'False = 'True
        -- Defined at T7939.hs:14:1
 H :: Bool -> Bool
-type family J (a :: [k]) :: Bool where
+type J :: forall k. [k] -> Bool
+type family J a where
     J '[] = 'False
   forall k (h :: k) (t :: [k]). J (h : t) = 'True
        -- Defined at T7939.hs:17:1
 J :: [k] -> Bool
-type family K (a1 :: [a]) :: Maybe a where
+type K :: forall a. [a] -> Maybe a
+type family K a1 where
     K '[] = 'Nothing
   forall a (h :: a) (t :: [a]). K (h : t) = 'Just h
        -- Defined at T7939.hs:21:1
index 1a511e6..7cad316 100644 (file)
@@ -1,4 +1,6 @@
-data Int = GHC.Types.I# GHC.Prim.Int#  -- Defined in ‘GHC.Types’
+type Int :: *
+data Int = GHC.Types.I# GHC.Prim.Int#
+       -- Defined in ‘GHC.Types’
 instance Eq Int -- Defined in ‘GHC.Classes’
 instance Ord Int -- Defined in ‘GHC.Classes’
 instance Enum Int -- Defined in ‘GHC.Enum’
index 4effb90..7a949cd 100644 (file)
@@ -1,4 +1,6 @@
-data (->) (a :: TYPE q) (b :: TYPE r)  -- Defined in ‘GHC.Prim’
+type (->) :: * -> * -> *
+data (->) a b
+       -- Defined in ‘GHC.Prim’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
index 2db09d7..b9f7c74 100644 (file)
@@ -1,2 +1,6 @@
-data A = Y     -- Defined at <interactive>:2:1
-data A = Y     -- Defined at <interactive>:2:1
+type A :: *
+data A = Y
+       -- Defined at <interactive>:2:1
+type A :: *
+data A = Y
+       -- Defined at <interactive>:2:1
index d938f95..7d7beeb 100644 (file)
@@ -1,4 +1,6 @@
-data family Sing (a :: k)      -- Defined at T8674.hs:4:1
+type Sing :: forall k. k -> *
+data family Sing a
+       -- Defined at T8674.hs:4:1
 data instance Sing Bool = SBool        -- Defined at T8674.hs:6:15
 data instance forall k (a :: [k]). Sing a = SNil
        -- Defined at T8674.hs:5:15
index a30879c..388681e 100644 (file)
@@ -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
index 68acea7..57bc625 100644 (file)
@@ -1,3 +1,4 @@
+type Data.ByteString.Lazy.ByteString :: *
 data Data.ByteString.Lazy.ByteString
   = Data.ByteString.Lazy.Internal.Empty
   | Data.ByteString.Lazy.Internal.Chunk {-# UNPACK #-}Data.ByteString.ByteString
@@ -16,6 +17,7 @@ instance Show Data.ByteString.Lazy.ByteString
 instance Read Data.ByteString.Lazy.ByteString
   -- Defined in ‘Data.ByteString.Lazy.Internal’
 
+type Data.ByteString.ByteString :: *
 data Data.ByteString.ByteString
   = Data.ByteString.Internal.PS {-# UNPACK #-}(GHC.ForeignPtr.ForeignPtr
                                                  GHC.Word.Word8)
index abed6d2..3f62f3f 100644 (file)
@@ -1,19 +1,24 @@
+type Num :: * -> Constraint
 class Num a where
   (+) :: a -> a -> a
   ...
        -- Defined in ‘GHC.Num’
 infixl 6 +
+type Num :: * -> Constraint
 class Num a where
   (+) :: a -> a -> a
   ...
        -- Defined in ‘GHC.Num’
 infixl 6 +
+type Data.Complex.Complex :: * -> *
 data Data.Complex.Complex a = !a Data.Complex.:+ !a
        -- Defined in ‘Data.Complex’
 infix 6 Data.Complex.:+
+type Data.Complex.Complex :: * -> *
 data Data.Complex.Complex a = !a Data.Complex.:+ !a
        -- Defined in ‘Data.Complex’
 infix 6 Data.Complex.:+
+type RealFloat :: * -> Constraint
 class (RealFrac a, Floating a) => RealFloat a where
   floatRadix :: a -> Integer
   floatDigits :: a -> Int
index 6dd5782..35f4b9f 100644 (file)
@@ -1,4 +1,6 @@
-data [] a = [] | a : [a]       -- Defined in ‘GHC.Types’
+type [] :: * -> *
+data [] a = [] | a : [a]
+       -- Defined in ‘GHC.Types’
 instance Applicative [] -- Defined in ‘GHC.Base’
 instance Eq a => Eq [a] -- Defined in ‘GHC.Classes’
 instance Functor [] -- Defined in ‘GHC.Base’
@@ -11,7 +13,9 @@ instance MonadFail [] -- Defined in ‘Control.Monad.Fail’
 instance Read a => Read [a] -- Defined in ‘GHC.Read’
 instance Foldable [] -- Defined in ‘Data.Foldable’
 instance Traversable [] -- Defined in ‘Data.Traversable’
-data () = ()   -- Defined in ‘GHC.Tuple’
+type () :: *
+data () = ()
+       -- Defined in ‘GHC.Tuple’
 instance Eq () -- Defined in ‘GHC.Classes’
 instance Monoid () -- Defined in ‘GHC.Base’
 instance Ord () -- Defined in ‘GHC.Classes’
@@ -20,7 +24,9 @@ instance Enum () -- Defined in ‘GHC.Enum’
 instance Show () -- Defined in ‘GHC.Show’
 instance Read () -- Defined in ‘GHC.Read’
 instance Bounded () -- Defined in ‘GHC.Enum’
-data (,) a b = (,) a b         -- Defined in ‘GHC.Tuple’
+type (,) :: * -> * -> *
+data (,) a b = (,) a b
+       -- Defined in ‘GHC.Tuple’
 instance Monoid a => Applicative ((,) a) -- Defined in ‘GHC.Base’
 instance (Eq a, Eq b) => Eq (a, b) -- Defined in ‘GHC.Classes’
 instance Functor ((,) a) -- Defined in ‘GHC.Base’
index d03720d..0a9fefb 100644 (file)
@@ -1,2 +1,4 @@
-data Foo = Foo         -- Defined at ghci019.hs:8:1
+type Foo :: *
+data Foo = Foo
+       -- Defined at ghci019.hs:8:1
 instance [safe] Prelude.Eq Foo -- Defined at ghci019.hs:9:10
index 4effb90..7a949cd 100644 (file)
@@ -1,4 +1,6 @@
-data (->) (a :: TYPE q) (b :: TYPE r)  -- Defined in ‘GHC.Prim’
+type (->) :: * -> * -> *
+data (->) a b
+       -- Defined in ‘GHC.Prim’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
index 9403102..70c64c4 100644 (file)
@@ -12,6 +12,7 @@ Data.Maybe.listToMaybe :: [a] -> Maybe a
 Data.Maybe.mapMaybe :: (a -> Maybe b) -> [a] -> [b]
 maybe :: b -> (a -> b) -> Maybe a -> b
 Data.Maybe.maybeToList :: Maybe a -> [a]
+type Maybe :: * -> *
 data Maybe a = Nothing | Just a
 -- via readFile
 (True,False)
index 9c862d3..3531825 100644 (file)
@@ -2,8 +2,11 @@
 :browse! *T
 -- defined locally
 T.length :: T.Integer
+type N :: * -> Constraint
 class N a
+type S :: * -> Constraint
 class S a
+type C :: * -> * -> Constraint
 class C a b
   ...
 c1 :: (C a b, N b) => a -> b
@@ -11,7 +14,8 @@ c2 :: (C a b, N b, S b) => a -> b
 c3 :: C a b => a -> b
 c4 :: C a b => a1 -> b
 -- imported via Control.Monad
-class (GHC.Base.Alternative m, Monad m) => MonadPlus (m :: * -> *)
+type MonadPlus :: (* -> *) -> Constraint
+class (GHC.Base.Alternative m, Monad m) => MonadPlus m
   ...
 mplus :: MonadPlus m => m a -> m a -> m a
 mzero :: MonadPlus m => m a
@@ -20,7 +24,8 @@ mzero :: MonadPlus m => m a
 (>>=) :: Monad m => m a -> (a -> m b) -> m b
 return :: Monad m => a -> m a
 -- imported via Control.Monad, Prelude, T
-class GHC.Base.Applicative m => Monad (m :: * -> *)
+type Monad :: (* -> *) -> Constraint
+class GHC.Base.Applicative m => Monad m
   ...
 -- imported via Data.Maybe
 catMaybes :: [Maybe a] -> [a]
@@ -34,23 +39,29 @@ maybe :: b -> (a -> b) -> Maybe a -> b
 maybeToList :: Maybe a -> [a]
 -- imported via Data.Maybe, Prelude
 Just :: a -> Maybe a
+type Maybe :: * -> *
 data Maybe a = ...
 Nothing :: Maybe a
 -- imported via Prelude
 (+) :: GHC.Num.Num a => a -> a -> a
 (=<<) :: Monad m => (a -> m b) -> m a -> m b
+type Eq :: * -> Constraint
 class Eq a
   ...
 -- imported via Prelude, T
 Prelude.length :: Data.Foldable.Foldable t => t a -> GHC.Types.Int
 -- imported via T
+type T.Integer :: *
 data T.Integer = ...
 T.length :: Data.ByteString.Internal.ByteString -> GHC.Types.Int
 :browse! T
 -- defined locally
 T.length :: T.Integer
+type N :: * -> Constraint
 class N a
+type S :: * -> Constraint
 class S a
+type C :: * -> * -> Constraint
 class C a b
   ...
 c1 :: (C a b, N b) => a -> b
@@ -60,8 +71,11 @@ c4 :: C a b => a1 -> b
 :browse! T -- with -fprint-explicit-foralls
 -- defined locally
 T.length :: T.Integer
+type N :: * -> Constraint
 class N a
+type S :: * -> Constraint
 class S a
+type C :: * -> * -> Constraint
 class C a b
   ...
 c1 :: forall a b. (C a b, N b) => a -> b
index 24049ee..d8e282a 100644 (file)
@@ -7,7 +7,9 @@ listToMaybe :: [a] -> Maybe a
 mapMaybe :: (a -> Maybe b) -> [a] -> [b]
 maybe :: b -> (a -> b) -> Maybe a -> b
 maybeToList :: Maybe a -> [a]
+type Maybe :: * -> *
 data Maybe a = Nothing | Just a
+type T :: *
 data T = A Int | B Float
 f :: Double -> Double
 g :: Double -> Double
index bbe355c..e152e74 100644 (file)
@@ -1,8 +1,10 @@
+type GHC.Base.MonadPlus :: (* -> *) -> Constraint
 class (GHC.Base.Alternative m, GHC.Base.Monad m) =>
-      GHC.Base.MonadPlus (m :: * -> *) where
+      GHC.Base.MonadPlus m where
   ...
   mplus :: m a -> m a -> m a
+type GHC.Base.MonadPlus :: (* -> *) -> Constraint
 class (GHC.Base.Alternative m, GHC.Base.Monad m) =>
-      GHC.Base.MonadPlus (m :: * -> *) where
+      GHC.Base.MonadPlus m where
   ...
   Control.Monad.mplus :: m a -> m a -> m a
index 49ce606..1195afc 100644 (file)
@@ -1,2 +1,6 @@
-data D = forall a. C (Int -> a) Char   -- Defined at ghci030.hs:8:1
-data D = forall a. C (Int -> a) Char   -- Defined at ghci030.hs:8:10
+type D :: *
+data D = forall a. C (Int -> a) Char
+       -- Defined at ghci030.hs:8:1
+type D :: *
+data D = forall a. C (Int -> a) Char
+       -- Defined at ghci030.hs:8:10
index 796433e..6ed9770 100644 (file)
@@ -1,3 +1,4 @@
 type role D nominal
+type D :: * -> *
 data Eq a => D a = C a
        -- Defined at ghci031.hs:7:1
index e4bfebe..4deea62 100644 (file)
@@ -1,2 +1,3 @@
+type Foo :: *
 data Foo = Foo1 Int | Int `InfixCon` Bool
        -- Defined at ghci033.hs:4:1
index d9ebd9c..bfd7897 100644 (file)
@@ -1 +1,3 @@
-data Ghci1.T = A | ...         -- Defined at <interactive>:2:10
+type Ghci1.T :: *
+data Ghci1.T = A | ...
+       -- Defined at <interactive>:2:10
index 14b8726..67a68f0 100644 (file)
@@ -1 +1,3 @@
-data R = A | ...       -- Defined at <interactive>:3:10
+type R :: *
+data R = A | ...
+       -- Defined at <interactive>:3:10
index 5cb84f6..d68caeb 100644 (file)
@@ -1,6 +1,14 @@
-data T = A {...}       -- Defined at <interactive>:2:10
-data T = A {a :: Int}  -- Defined at <interactive>:2:13
+type T :: *
+data T = A {...}
+       -- Defined at <interactive>:2:10
+type T :: *
+data T = A {a :: Int}
+       -- Defined at <interactive>:2:13
 a :: Integer   -- Defined at <interactive>:5:5
 3
-data R = B {a :: Int}  -- Defined at <interactive>:8:13
-data T = A {Ghci1.a :: Int}    -- Defined at <interactive>:2:1
+type R :: *
+data R = B {a :: Int}
+       -- Defined at <interactive>:8:13
+type T :: *
+data T = A {Ghci1.a :: Int}
+       -- Defined at <interactive>:2:1
index a354286..9e77b01 100644 (file)
@@ -1,9 +1,21 @@
-data T = C | D         -- Defined at <interactive>:8:1
-type T' = Ghci1.T      -- Defined at <interactive>:3:1
-data Ghci1.T = A | ...         -- Defined at <interactive>:2:10
-data Ghci4.T = B | ...         -- Defined at <interactive>:5:12
-data T = C | ...       -- Defined at <interactive>:8:14
-data T = ... | D       -- Defined at <interactive>:8:18
+type T :: *
+data T = C | D
+       -- Defined at <interactive>:8:1
+type T' :: *
+type T' = Ghci1.T
+       -- Defined at <interactive>:3:1
+type Ghci1.T :: *
+data Ghci1.T = A | ...
+       -- Defined at <interactive>:2:10
+type Ghci4.T :: *
+data Ghci4.T = B | ...
+       -- Defined at <interactive>:5:12
+type T :: *
+data T = C | ...
+       -- Defined at <interactive>:8:14
+type T :: *
+data T = ... | D
+       -- Defined at <interactive>:8:18
 b :: T'        -- Defined at <interactive>:4:5
 c :: Ghci4.T   -- Defined at <interactive>:7:5
 d :: T         -- Defined at <interactive>:9:5
index 2fc93e6..e5cdb3d 100644 (file)
@@ -5,6 +5,7 @@ Please see section `The Coercible constraint`
 of the user's guide for details.
 -}
 type role Coercible representational representational
-class Coercible a b => Coercible (a :: k) (b :: k)
+type Coercible :: forall k. k -> k -> Constraint
+class Coercible a b => Coercible a b
        -- Defined in ‘GHC.Types’
 coerce :: Coercible a b => a -> b      -- Defined in ‘GHC.Prim’
index 4effb90..7a949cd 100644 (file)
@@ -1,4 +1,6 @@
-data (->) (a :: TYPE q) (b :: TYPE r)  -- Defined in ‘GHC.Prim’
+type (->) :: * -> * -> *
+data (->) a b
+       -- Defined in ‘GHC.Prim’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
index 9ab7b1b..6ff7d89 100644 (file)
@@ -1,3 +1,4 @@
+type X :: ★ → ★ → Constraint
 class X a b | a → b where
   to ∷ a → b
   {-# MINIMAL to #-}
index 652a5cd..a00ffea 100644 (file)
@@ -1,3 +1,4 @@
 x :: () = ()
 y :: () = ()
+type Foo :: * -> Constraint
 class Foo a
index d9407d3..5187084 100644 (file)
@@ -1,5 +1,9 @@
 1
 2
 2
-data T1 = MkT1         -- Defined at <interactive>:6:1
-data T2 = MkT2         -- Defined at <interactive>:8:2
+type T1 :: *
+data T1 = MkT1
+       -- Defined at <interactive>:6:1
+type T2 :: *
+data T2 = MkT2
+       -- Defined at <interactive>:8:2
index 28e7179..f0a5614 100644 (file)
@@ -2,30 +2,33 @@
 ClosedFam3.hs-boot:7:1: error:
     Type constructor ‘Foo’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type family Foo a :: *
-                   where
-                       Foo Int = Bool
-                       Foo Double = Char
-    Boot file:   type family Foo a :: *
-                   where Foo Int = Bool
+    Main module: type Foo :: * -> *
+                 type family Foo a where
+                     Foo Int = Bool
+                     Foo Double = Char
+    Boot file:   type Foo :: * -> *
+                 type family Foo a where
+                     Foo Int = Bool
 
 ClosedFam3.hs-boot:10:1: error:
     Type constructor ‘Bar’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type family Bar a :: *
-                   where
-                       Bar Int = Bool
-                       Bar Double = Double
-    Boot file:   type family Bar a :: *
-                   where
-                       Bar Int = Bool
-                       Bar Double = Char
+    Main module: type Bar :: * -> *
+                 type family Bar a where
+                     Bar Int = Bool
+                     Bar Double = Double
+    Boot file:   type Bar :: * -> *
+                 type family Bar a where
+                     Bar Int = Bool
+                     Bar Double = Char
 
 ClosedFam3.hs-boot:14:1: error:
     Type constructor ‘Baz’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type family Baz a :: *
-                   where Baz Int = Bool
-    Boot file:   type family Baz (a :: k) :: *
-                   where Baz Int = Bool
+    Main module: type Baz :: * -> *
+                 type family Baz a where
+                     Baz Int = Bool
+    Boot file:   type Baz :: forall k. k -> *
+                 type family Baz a where
+                     Baz Int = Bool
     The types have different kinds
index 1bd21ae..2c29679 100644 (file)
@@ -1,5 +1,5 @@
 
-T9167.hs:5:1:
-    The associated type ‘F
-    mentions none of the type or kind variables of the class ‘C a’
-    In the class declaration for ‘C’
+T9167.hs:5:1: error:
+    • The associated type ‘F b
+      mentions none of the type or kind variables of the class ‘C a’
+    • In the class declaration for ‘C’
index cfed45f..ff758c1 100644 (file)
@@ -1,6 +1,9 @@
 True
-data S = MkS {Ghci1.foo :: Int}        -- Defined at <interactive>:3:16
+type S :: *
+data S = MkS {Ghci1.foo :: Int}
+       -- Defined at <interactive>:3:16
 
+type T :: * -> *
 data T a = MkT {Ghci2.foo :: Bool, ...}
        -- Defined at <interactive>:4:18
 
index 49ec1d1..53d4f37 100644 (file)
          ({ <no location info> }
           []))))]
      []
+     []
      [])
    ,(TyClGroup
      (NoExtField)
               {Name: DumpRenamedAst.Peano})))))
          (Nothing))))]
      []
+     []
      [])
    ,(TyClGroup
      (NoExtField)
                   {Name: GHC.Types.Type})))))))))
          (Nothing))))]
      []
+     []
      [({ DumpRenamedAst.hs:(18,1)-(19,45) }
        (DataFamInstD
         (NoExtField)
          ({ <no location info> }
           []))))]
      []
+     []
      [])
    ,(TyClGroup
      (NoExtField)
               {Name: GHC.Types.Type})))))
          (Nothing))))]
      []
+     []
      [])]
    []
    []
index 9e6b981..29518e5 100644 (file)
@@ -91,6 +91,7 @@
          ({ <no location info> }
           []))))]
      []
+     []
      [])]
    []
    []
diff --git a/testsuite/tests/polykinds/CuskFam.hs b/testsuite/tests/polykinds/CuskFam.hs
new file mode 100644 (file)
index 0000000..c339dbc
--- /dev/null
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds #-}
+-- {-# LANGUAGE CUSKs #-}    -- enabled by default
+
+module CuskFam where
+
+type family F a   -- non-injective
+
+type family X :: F a
+    -- Used to fail with:
+    --
+    --    • Couldn't match expected kind ‘F a1’ with actual kind ‘F a’
+    --      NB: ‘F’ is a non-injective type family
+    --      The type variable ‘a1’ is ambiguous
+    --    • In the type family declaration for ‘X’
+    --
+    -- See Note [Unifying implicit CUSK variables] in TcHsType
index 6345b22..74ab266 100644 (file)
@@ -214,3 +214,4 @@ test('T16221a', normal, compile_fail, [''])
 test('T16342', normal, compile, [''])
 test('T16263', normal, compile_fail, [''])
 test('T16902', normal, compile_fail, [''])
+test('CuskFam', normal, compile, [''])
index b9ba174..ef4b09f 100644 (file)
@@ -15,31 +15,39 @@ RnFail055.hs-boot:4:1: error:
 RnFail055.hs-boot:6:1: error:
     Type constructor ‘S1’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type S1 a b = (a, b)
-    Boot file:   type S1 a b c = (a, b)
+    Main module: type S1 :: * -> * -> *
+                 type S1 a b = (a, b)
+    Boot file:   type S1 :: * -> * -> * -> *
+                 type S1 a b c = (a, b)
     The types have different kinds
 
 RnFail055.hs-boot:8:1: error:
     Type constructor ‘S2’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type S2 a b = forall a1. (a1, b)
-    Boot file:   type S2 a b = forall b1. (a, b1)
+    Main module: type S2 :: * -> * -> *
+                 type S2 a b = forall a1. (a1, b)
+    Boot file:   type S2 :: * -> * -> *
+                 type S2 a b = forall b1. (a, b1)
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
 
 RnFail055.hs-boot:12:1: error:
     Type constructor ‘T1’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: data T1 a b = T1 [b] [a]
-    Boot file:   data T1 a b = T1 [a] [b]
+    Main module: type T1 :: * -> * -> *
+                 data T1 a b = T1 [b] [a]
+    Boot file:   type T1 :: * -> * -> *
+                 data T1 a b = T1 [a] [b]
     The constructors do not match: The types for ‘T1’ differ
 
 RnFail055.hs-boot:14:1: error:
     Type constructor ‘T2’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role T2 representational nominal
+                 type T2 :: * -> * -> *
                  data Eq b => T2 a b = T2 a
     Boot file:   type role T2 nominal phantom
+                 type T2 :: * -> * -> *
                  data Eq a => T2 a b = T2 a
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
@@ -54,16 +62,20 @@ RnFail055.hs-boot:17:12: error:
 RnFail055.hs-boot:21:1: error:
     Type constructor ‘T5’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: data T5 a = T5 {field5 :: a}
-    Boot file:   data T5 a = T5 a
+    Main module: type T5 :: * -> *
+                 data T5 a = T5 {field5 :: a}
+    Boot file:   type T5 :: * -> *
+                 data T5 a = T5 a
     The constructors do not match:
       The record label lists for ‘T5’ differ
 
 RnFail055.hs-boot:23:1: error:
     Type constructor ‘T6’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: data T6 = T6 Int
-    Boot file:   data T6 = T6 !Int
+    Main module: type T6 :: *
+                 data T6 = T6 Int
+    Boot file:   type T6 :: *
+                 data T6 = T6 !Int
     The constructors do not match:
       The strictness annotations for ‘T6’ differ
 
@@ -71,8 +83,10 @@ RnFail055.hs-boot:25:1: error:
     Type constructor ‘T7’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role T7 phantom
+                 type T7 :: * -> *
                  data T7 a = forall a1. T7 a1
-    Boot file:   data T7 a = forall b. T7 a
+    Boot file:   type T7 :: * -> *
+                 data T7 a = forall b. T7 a
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
     The constructors do not match: The types for ‘T7’ differ
@@ -83,11 +97,13 @@ RnFail055.hs-boot:27:22: error:
 RnFail055.hs-boot:28:1: error:
     Class ‘C2’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: class C2 a b where
+    Main module: type C2 :: * -> * -> Constraint
+                 class C2 a b where
                    m2 :: a -> b
                    m2' :: a -> b
                    {-# MINIMAL m2, m2' #-}
-    Boot file:   class C2 a b where
+    Boot file:   type C2 :: * -> * -> Constraint
+                 class C2 a b where
                    m2 :: a -> b
                    {-# MINIMAL m2 #-}
     The methods do not match: There are different numbers of methods
@@ -96,6 +112,8 @@ RnFail055.hs-boot:28:1: error:
 RnFail055.hs-boot:29:1: error:
     Class ‘C3’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: class (Eq a, Ord a) => C3 a
-    Boot file:   class (Ord a, Eq a) => C3 a
+    Main module: type C3 :: * -> Constraint
+                 class (Eq a, Ord a) => C3 a
+    Boot file:   type C3 :: * -> Constraint
+                 class (Ord a, Eq a) => C3 a
     The class constraints do not match
index d1872f3..ec3bff4 100644 (file)
@@ -3,7 +3,9 @@ Roles12.hs:5:1: error:
     Type constructor ‘T’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role T phantom
+                 type T :: * -> *
+                 data T a
+    Boot file:   type T :: * -> *
                  data T a
-    Boot file:   data T a
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
index 998f17c..0e8cbf4 100644 (file)
@@ -3,7 +3,9 @@ T9204.hs:6:1: error:
     Type constructor ‘D’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type role D phantom
+                 type D :: * -> *
+                 data D a
+    Boot file:   type D :: * -> *
                  data D a
-    Boot file:   data D a
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
diff --git a/testsuite/tests/saks/should_compile/T16721.script b/testsuite/tests/saks/should_compile/T16721.script
new file mode 100644 (file)
index 0000000..1e747be
--- /dev/null
@@ -0,0 +1,4 @@
+:set -XStandaloneKindSignatures -XNoStarIsType
+import Data.Kind (Type)
+type T :: (Type -> Type) -> Type; data T a
+:info T
diff --git a/testsuite/tests/saks/should_compile/T16721.stdout b/testsuite/tests/saks/should_compile/T16721.stdout
new file mode 100644 (file)
index 0000000..8dce9ca
--- /dev/null
@@ -0,0 +1,4 @@
+type role T phantom
+type T :: (Type -> Type) -> Type
+data T a
+       -- Defined at <interactive>:3:35
diff --git a/testsuite/tests/saks/should_compile/T16723.hs b/testsuite/tests/saks/should_compile/T16723.hs
new file mode 100644 (file)
index 0000000..2ba216a
--- /dev/null
@@ -0,0 +1,10 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T16723 where
+
+import Data.Kind
+
+type D :: forall a. Type
+data D
diff --git a/testsuite/tests/saks/should_compile/T16724.hs b/testsuite/tests/saks/should_compile/T16724.hs
new file mode 100644 (file)
index 0000000..3ab5d07
--- /dev/null
@@ -0,0 +1,15 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T16724 where
+
+import Data.Kind
+
+type T1 :: forall k (a :: k). Type
+type family T1
+
+-- type T2 :: forall {k} (a :: k). Type
+type T2 :: forall a. Type
+type family T2
diff --git a/testsuite/tests/saks/should_compile/T16724.script b/testsuite/tests/saks/should_compile/T16724.script
new file mode 100644 (file)
index 0000000..f5681b8
--- /dev/null
@@ -0,0 +1,5 @@
+:set -fprint-explicit-kinds -fprint-explicit-foralls -XNoStarIsType
+:load T16724.hs
+:info T1
+:info T2
+   -- must have the same arity!
diff --git a/testsuite/tests/saks/should_compile/T16724.stdout b/testsuite/tests/saks/should_compile/T16724.stdout
new file mode 100644 (file)
index 0000000..099371c
--- /dev/null
@@ -0,0 +1,6 @@
+type T1 :: forall k (a :: k). Type
+type family T1 @k @a
+       -- Defined at T16724.hs:11:1
+type T2 :: forall {k} (a :: k). Type
+type family T2 @{k} @a
+       -- Defined at T16724.hs:15:1
diff --git a/testsuite/tests/saks/should_compile/T16726.hs b/testsuite/tests/saks/should_compile/T16726.hs
new file mode 100644 (file)
index 0000000..e1a748d
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T16726 where
+
+import Data.Kind
+
+type D :: forall k. k -> Type
+data D :: forall j. j -> Type
+
+type DF :: forall k. k -> Type
+data family DF :: forall j. j -> Type
+
+type T :: forall k. k -> Type
+type family T :: forall j. j -> Type
diff --git a/testsuite/tests/saks/should_compile/T16731.hs b/testsuite/tests/saks/should_compile/T16731.hs
new file mode 100644 (file)
index 0000000..c2051f6
--- /dev/null
@@ -0,0 +1,14 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T16731 where
+
+import Data.Kind
+
+class C (a :: Type) (b :: Type)
+
+type T :: forall a. a -> Type
+data T (x :: z) deriving (C z)
diff --git a/testsuite/tests/saks/should_compile/T16756a.hs b/testsuite/tests/saks/should_compile/T16756a.hs
new file mode 100644 (file)
index 0000000..f85c2ec
--- /dev/null
@@ -0,0 +1,12 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T16756a where
+
+import Data.Kind (Type)
+
+type T :: Type -> Type
+data family T
+  -- We do /not/ need to write:
+  --   data family T a
+  -- See https://gitlab.haskell.org/ghc/ghc/issues/16756#note_203567
diff --git a/testsuite/tests/saks/should_compile/T16758.hs b/testsuite/tests/saks/should_compile/T16758.hs
new file mode 100644 (file)
index 0000000..2798156
--- /dev/null
@@ -0,0 +1,14 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE ConstrainedClassMethods #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+
+module T16758 where
+
+import Data.Kind
+
+type C :: forall (a :: Type) -> a ~ Int => Constraint
+class C a where
+  f :: C a => a -> Int
diff --git a/testsuite/tests/saks/should_compile/T17164.hs b/testsuite/tests/saks/should_compile/T17164.hs
new file mode 100644 (file)
index 0000000..0f9d9e4
--- /dev/null
@@ -0,0 +1,14 @@
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -ddump-splices #-}
+
+module T17164 where
+
+import Data.Kind
+
+$([d| type T :: forall k -> k -> Type
+      type family T :: forall k -> k -> Type
+    |])
diff --git a/testsuite/tests/saks/should_compile/T17164.stderr b/testsuite/tests/saks/should_compile/T17164.stderr
new file mode 100644 (file)
index 0000000..5b1fdbf
--- /dev/null
@@ -0,0 +1,7 @@
+T17164.hs:(12,3)-(14,6): Splicing declarations
+    [d| type T :: forall k -> k -> Type
+        
+        type family T :: forall k -> k -> Type |]
+  ======>
+    type T :: forall k -> k -> Type
+    type family T :: forall k -> k -> Type
diff --git a/testsuite/tests/saks/should_compile/all.T b/testsuite/tests/saks/should_compile/all.T
new file mode 10064