implement proposal 106 (Define Kinds Without Promotion) (fixes #6024)

includes corresponding changes to haddock submodule

15 files changed, 271 insertions, 29 deletions

diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index d8b26558aa..e50290a5f8 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -57,7 +57,8 @@ module GHC.Core.DataCon (
         isNullarySrcDataCon, isNullaryRepDataCon,
         isTupleDataCon, isBoxedTupleDataCon, isUnboxedTupleDataCon,
         isUnboxedSumDataCon,
-        isVanillaDataCon, isNewDataCon, classDataCon, dataConCannotMatch,
+        isVanillaDataCon, isNewDataCon, isTypeDataCon,
+        classDataCon, dataConCannotMatch,
         dataConUserTyVarsArePermuted,
         isBanged, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
         specialPromotedDc,
@@ -1634,6 +1635,11 @@ isVanillaDataCon dc = dcVanilla dc
 isNewDataCon :: DataCon -> Bool
 isNewDataCon dc = isNewTyCon (dataConTyCon dc)
 
+-- | Is this data constructor in a "type data" declaration?
+-- See Note [Type data declarations] in GHC.Rename.Module.
+isTypeDataCon :: DataCon -> Bool
+isTypeDataCon dc = isTcClsNameSpace (nameNameSpace (getName dc))
+
 -- | Should this DataCon be allowed in a type even without -XDataKinds?
 -- Currently, only Lifted & Unlifted
 specialPromotedDc :: DataCon -> Bool
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 38bb6598b4..017b8bce20 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -3759,6 +3759,7 @@ xFlagsDeps = [
   flagSpec "TransformListComp"                LangExt.TransformListComp,
   flagSpec "TupleSections"                    LangExt.TupleSections,
   flagSpec "TypeApplications"                 LangExt.TypeApplications,
+  flagSpec "TypeData"                         LangExt.TypeData,
   depFlagSpec' "TypeInType"                   LangExt.TypeInType
     (deprecatedForExtensions ["DataKinds", "PolyKinds"]),
   flagSpec "TypeFamilies"                     LangExt.TypeFamilies,
diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index 1db54bfc4b..c4a79f25a7 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -401,7 +401,7 @@ countTyClDecls decls
     count isNewTy        decls,  -- ...instances
     count isFamilyDecl   decls)
  where
-   isDataTy DataDecl{ tcdDataDefn = HsDataDefn { dd_cons = DataTypeCons _ } } = True
+   isDataTy DataDecl{ tcdDataDefn = HsDataDefn { dd_cons = DataTypeCons _ _ } } = True
    isDataTy _                                                       = False
 
    isNewTy DataDecl{ tcdDataDefn = HsDataDefn { dd_cons = NewTypeCon _ } } = True
@@ -698,8 +698,11 @@ ppDataDefnHeader pp_hdr HsDataDefn
   , dd_cType = mb_ct
   , dd_kindSig = mb_sig
   , dd_cons = condecls }
-  = ppr (dataDefnConsNewOrData condecls) <+> pp_ct <+> pp_hdr context <+> pp_sig
+  = pp_type <+> ppr (dataDefnConsNewOrData condecls) <+> pp_ct <+> pp_hdr context <+> pp_sig
   where
+    pp_type
+      | isTypeDataDefnCons condecls = text "type"
+      | otherwise = empty
     pp_ct = case mb_ct of
                Nothing   -> empty
                Just ct -> ppr ct
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index e6f8ce4c51..c707a29368 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -527,7 +527,7 @@ repDataDefn tc opts
                                    ; ksig' <- repMaybeLTy ksig
                                    ; repNewtype cxt1 tc opts ksig' con'
                                                 derivs1 }
-           DataTypeCons cons -> do { ksig' <- repMaybeLTy ksig
+           DataTypeCons _ cons -> do { ksig' <- repMaybeLTy ksig
                                ; consL <- mapM repC cons
                                ; cons1 <- coreListM conTyConName consL
                                ; repData cxt1 tc opts ksig' cons1
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index e530750745..fd1cd5d3ae 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -1271,22 +1271,22 @@ ty_decl :: { LTyClDecl GhcPs }
                            ++ (fst $ unLoc $5) ++ (fst $ unLoc $6))  }
 
           -- ordinary data type or newtype declaration
-        | data_or_newtype capi_ctype tycl_hdr constrs maybe_derivings
-                {% mkTyData (comb4 $1 $3 $4 $5) (snd $ unLoc $1) $2 $3
+        | type_data_or_newtype capi_ctype tycl_hdr constrs maybe_derivings
+                {% mkTyData (comb4 $1 $3 $4 $5) (sndOf3 $ unLoc $1) (thdOf3 $ unLoc $1) $2 $3
                            Nothing (reverse (snd $ unLoc $4))
                                    (fmap reverse $5)
-                           ((fst $ unLoc $1):(fst $ unLoc $4)) }
+                           ((fstOf3 $ unLoc $1):(fst $ unLoc $4)) }
                                    -- We need the location on tycl_hdr in case
                                    -- constrs and deriving are both empty
 
           -- ordinary GADT declaration
-        | data_or_newtype capi_ctype tycl_hdr opt_kind_sig
+        | type_data_or_newtype capi_ctype tycl_hdr opt_kind_sig
                  gadt_constrlist
                  maybe_derivings
-            {% mkTyData (comb4 $1 $3 $5 $6) (snd $ unLoc $1) $2 $3
+            {% mkTyData (comb4 $1 $3 $5 $6) (sndOf3 $ unLoc $1) (thdOf3 $ unLoc $1) $2 $3
                             (snd $ unLoc $4) (snd $ unLoc $5)
                             (fmap reverse $6)
-                            ((fst $ unLoc $1):(fst $ unLoc $4)++(fst $ unLoc $5)) }
+                            ((fstOf3 $ unLoc $1):(fst $ unLoc $4)++(fst $ unLoc $5)) }
                                    -- We need the location on tycl_hdr in case
                                    -- constrs and deriving are both empty
 
@@ -1510,6 +1510,11 @@ at_decl_inst :: { LInstDecl GhcPs }
                                 (fmap reverse $7)
                         ((fst $ unLoc $1):$2++(fst $ unLoc $5)++(fst $ unLoc $6)) }
 
+type_data_or_newtype :: { Located (AddEpAnn, Bool, NewOrData) }
+        : 'data'        { sL1 $1 (mj AnnData    $1,False,DataType) }
+        | 'newtype'     { sL1 $1 (mj AnnNewtype $1,False,NewType) }
+        | 'type' 'data' { sL1 $1 (mj AnnData    $1,True ,DataType) }
+
 data_or_newtype :: { Located (AddEpAnn, NewOrData) }
         : 'data'        { sL1 $1 (mj AnnData    $1,DataType) }
         | 'newtype'     { sL1 $1 (mj AnnNewtype $1,NewType) }
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index 928e7ce4aa..ced580d743 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -215,6 +215,7 @@ mkClassDecl loc' (L _ (mcxt, tycl_hdr)) fds where_cls layoutInfo annsIn
                                   , tcdDocs  = docs })) }
 
 mkTyData :: SrcSpan
+         -> Bool
          -> NewOrData
          -> Maybe (LocatedP CType)
          -> Located (Maybe (LHsContext GhcPs), LHsType GhcPs)
@@ -223,14 +224,14 @@ mkTyData :: SrcSpan
          -> Located (HsDeriving GhcPs)
          -> [AddEpAnn]
          -> P (LTyClDecl GhcPs)
-mkTyData loc' new_or_data cType (L _ (mcxt, tycl_hdr))
+mkTyData loc' is_type_data new_or_data cType (L _ (mcxt, tycl_hdr))
          ksig data_cons (L _ maybe_deriv) annsIn
   = do { let loc = noAnnSrcSpan loc'
        ; (tc, tparams, fixity, ann) <- checkTyClHdr False tycl_hdr
        ; tyvars <- checkTyVars (ppr new_or_data) equalsDots tc tparams
        ; cs <- getCommentsFor (locA loc) -- Get any remaining comments
        ; let anns' = addAnns (EpAnn (spanAsAnchor $ locA loc) annsIn emptyComments) ann cs
-       ; data_cons <- checkNewOrData (locA loc) (unLoc tc) new_or_data data_cons
+       ; data_cons <- checkNewOrData (locA loc) (unLoc tc) is_type_data new_or_data data_cons
        ; defn <- mkDataDefn cType mcxt ksig data_cons maybe_deriv
        ; return (L loc (DataDecl { tcdDExt = anns',
                                    tcdLName = tc, tcdTyVars = tyvars,
@@ -252,7 +253,6 @@ mkDataDefn cType mcxt ksig data_cons maybe_deriv
                             , dd_kindSig = ksig
                             , dd_derivs = maybe_deriv }) }
 
-
 mkTySynonym :: SrcSpan
             -> LHsType GhcPs  -- LHS
             -> LHsType GhcPs  -- RHS
@@ -327,7 +327,7 @@ mkDataFamInst loc new_or_data cType (mcxt, bndrs, tycl_hdr)
   = do { (tc, tparams, fixity, ann) <- checkTyClHdr False tycl_hdr
        ; cs <- getCommentsFor loc -- Add any API Annotations to the top SrcSpan
        ; let fam_eqn_ans = addAnns (EpAnn (spanAsAnchor loc) ann cs) anns emptyComments
-       ; data_cons <- checkNewOrData loc (unLoc tc) new_or_data data_cons
+       ; data_cons <- checkNewOrData loc (unLoc tc) False new_or_data data_cons
        ; defn <- mkDataDefn cType mcxt ksig data_cons maybe_deriv
        ; return (L (noAnnSrcSpan loc) (DataFamInstD noExtField (DataFamInstDecl
                   (FamEqn { feqn_ext    = fam_eqn_ans
@@ -2622,11 +2622,27 @@ mkOpaquePragma src
                  , inl_rule   = FunLike
                  }
 
-checkNewOrData :: SrcSpan -> RdrName -> NewOrData -> [a] -> P (DataDefnCons a)
-checkNewOrData span name = curry $ \ case
+checkNewOrData :: SrcSpan -> RdrName -> Bool -> NewOrData -> [LConDecl GhcPs]
+               -> P (DataDefnCons (LConDecl GhcPs))
+checkNewOrData span name is_type_data = curry $ \ case
     (NewType, [a]) -> pure $ NewTypeCon a
-    (DataType, as) -> pure $ DataTypeCons as
+    (DataType, as) -> pure $ DataTypeCons is_type_data (handle_type_data as)
     (NewType, as) -> addFatalError $ mkPlainErrorMsgEnvelope span $ PsErrMultipleConForNewtype name (length as)
+  where
+    -- In a "type data" declaration, the constructors are in the type/class
+    -- namespace rather than the data constructor namespace.
+    -- See Note [Type data declarations] in GHC.Rename.Module.
+    handle_type_data
+      | is_type_data = map (fmap promote_constructor)
+      | otherwise = id
+
+    promote_constructor (dc@ConDeclGADT { con_names = cons })
+      = dc { con_names = fmap (fmap promote_name) cons }
+    promote_constructor (dc@ConDeclH98 { con_name = con })
+      = dc { con_name = fmap promote_name con }
+    promote_constructor dc = dc
+
+    promote_name name = fromMaybe name (promoteRdrName name)
 
 -----------------------------------------------------------------------------
 -- utilities for foreign declarations
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 7e2c4a0388..6748d60a56 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -69,6 +69,7 @@ import GHC.Data.Graph.Directed ( SCC, flattenSCC, flattenSCCs, Node(..)
 import GHC.Types.Unique.Set
 import GHC.Data.OrdList
 import qualified GHC.LanguageExtensions as LangExt
+import GHC.Core.DataCon ( isSrcStrict )
 
 import Control.Monad
 import Control.Arrow ( first )
@@ -1948,6 +1949,10 @@ rnDataDefn doc (HsDataDefn { dd_cType = cType, dd_ctxt = context, dd_cons = cond
           checkTc (h98_style || null (fromMaybeContext context))
                   (badGadtStupidTheta doc)
 
+        -- Check restrictions on "type data" declarations.
+        -- See Note [Type data declarations].
+        ; when (isTypeDataDefnCons condecls) check_type_data
+
         ; (m_sig', sig_fvs) <- case m_sig of
              Just sig -> first Just <$> rnLHsKind doc sig
              Nothing  -> return (Nothing, emptyFVs)
@@ -1982,6 +1987,121 @@ rnDataDefn doc (HsDataDefn { dd_cType = cType, dd_ctxt = context, dd_cons = cond
            ; (ds', fvs) <- mapFvRn (rnLHsDerivingClause doc) ds
            ; return (ds', fvs) }
 
+    -- Given a "type data" declaration, check that the TypeData extension
+    -- is enabled and check restrictions (R1), (R2), (R3) and (R5)
+    -- on the declaration.  See Note [Type data declarations].
+    check_type_data
+      = do { unlessXOptM LangExt.TypeData $ failWith TcRnIllegalTypeData
+           ; unless (null (fromMaybeContext context)) $
+               failWith $ TcRnTypeDataForbids TypeDataForbidsDatatypeContexts
+           ; mapM_ (addLocMA check_type_data_condecl) condecls
+           ; unless (null derivs) $
+               failWith $ TcRnTypeDataForbids TypeDataForbidsDerivingClauses
+           }
+
+    -- Check restrictions (R2) and (R3) on a "type data" constructor.
+    -- See Note [Type data declarations].
+    check_type_data_condecl :: ConDecl GhcPs -> RnM ()
+    check_type_data_condecl condecl
+      = do {
+           ; when (has_labelled_fields condecl) $
+               failWith $ TcRnTypeDataForbids TypeDataForbidsLabelledFields
+           ; when (has_strictness_flags condecl) $
+               failWith $ TcRnTypeDataForbids TypeDataForbidsStrictnessAnnotations
+           }
+
+    has_labelled_fields (ConDeclGADT { con_g_args = RecConGADT _ _ }) = True
+    has_labelled_fields (ConDeclH98 { con_args = RecCon rec })
+      = not (null (unLoc rec))
+    has_labelled_fields _ = False
+
+    has_strictness_flags condecl
+      = any (is_strict . getBangStrictness . hsScaledThing) (con_args condecl)
+
+    is_strict (HsSrcBang _ _ s) = isSrcStrict s
+
+    con_args (ConDeclGADT { con_g_args = PrefixConGADT args }) = args
+    con_args (ConDeclH98 { con_args = PrefixCon _ args }) = args
+    con_args (ConDeclH98 { con_args = InfixCon arg1 arg2 }) = [arg1, arg2]
+    con_args _ = []
+
+{-
+Note [Type data declarations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With the TypeData extension (GHC proposal #106), one can write "type data"
+declarations, like
+
+    type data Nat = Zero | Succ Nat
+
+or equivalently in GADT style:
+
+    type data Nat where
+        Zero :: Nat
+        Succ :: Nat -> Nat
+
+This defines the constructors Zero and Succ in the TcCls namespace
+(type constructors and classes) instead of the Data namespace (data
+constructors).  This contrasts with the DataKinds extension, which allows
+constructors defined in the Data namespace to be promoted to the TcCls
+namespace at the point of use in a type.
+
+Type data declarations have the syntax of data declarations, either
+ordinary algebraic data types or GADTs, preceded by "type", with the
+following restrictions:
+
+(R1) There are data type contexts (even with the DatatypeContexts extension).
+
+(R2) There are no labelled fields.  Perhaps these could be supported
+     using type families, but they are omitted for now.
+
+(R3) There are no strictness flags, because they don't make sense at
+     the type level.
+
+(R4) The types of the constructors contain no constraints other than
+     equality constraints.  (This is the same restriction imposed
+     on constructors to be promoted with the DataKinds extension in
+     dc_theta_illegal_constraint called from GHC.Tc.Gen.HsType.tcTyVar,
+     but in that case the restriction is imposed if and when a data
+     constructor is used in a type, whereas here it is imposed at
+     the point of definition.  See also Note [Constraints in kinds]
+     in GHC.Core.TyCo.Rep.)
+
+(R5) There are no deriving clauses.
+
+The main parts of the implementation are:
+
+* The Bool argument to DataTypeCons (in Language.Haskell.Syntax.Decls)
+  distinguishes "type data" declarations from ordinary "data" declarations.
+
+* This flag is set, and the constructor names placed in the
+  TcCls namespace, during the initial construction of the AST in
+  GHC.Parser.PostProcess.checkNewOrData.
+
+* GHC.Rename.Module.rnDataDefn calls check_type_data on these
+  declarations, which checks that the TypeData extension is enabled and
+  checks restrictions (R1), (R2), (R3) and (R5).  They could equally
+  well be checked in the typechecker, but we err on the side of catching
+  imposters early.
+
+* GHC.Tc.TyCl.checkValidDataCon checks restriction (R4) on these declarations.
+
+* When beginning to type check a mutually recursive group of declarations,
+  the "type data" constructors are added to the type-checker environment
+  as APromotionErr TyConPE by GHC.Tc.TyCl.mkPromotionErrorEnv, so they
+  cannot be used within the recursive group.  This mirrors the DataKinds
+  behaviour described at Note [Recursion and promoting data constructors]
+  in GHC.Tc.TyCl.  For example, this is rejected:
+
+    type data T f = K (f (K Int))
+
+* After a "type data" declaration has been type-checked, the type-checker
+  environment entry for each constructor (which can be recognized
+  by being in the TcCls namespace) is just the promoted type
+  constructor, not the bundle required for a data constructor.
+  (GHC.Types.TyThing.implicitTyConThings)
+
+-}
+
 warnNoDerivStrat :: Maybe (LDerivStrategy GhcRn)
                  -> SrcSpan
                  -> RnM ()
diff --git a/compiler/GHC/Rename/Names.hs b/compiler/GHC/Rename/Names.hs
index e4f11fa3fd..edc0af5f52 100644
--- a/compiler/GHC/Rename/Names.hs
+++ b/compiler/GHC/Rename/Names.hs
@@ -2198,9 +2198,13 @@ packageImportErr
 -- We can get an operator as the constructor, even in the prefix form:
 --      data T = :% Int Int
 -- from interface files, which always print in prefix form
+--
+-- We also allow type constructor names, which are defined by "type data"
+-- declarations.  See Note [Type data declarations] in GHC.Rename.Module.
 
 checkConName :: RdrName -> TcRn ()
-checkConName name = checkErr (isRdrDataCon name) (badDataCon name)
+checkConName name
+  = checkErr (isRdrDataCon name || isRdrTc name) (badDataCon name)
 
 badDataCon :: RdrName -> TcRnMessage
 badDataCon name
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index ab338cf452..3f6989e9f9 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -994,6 +994,13 @@ instance Diagnostic TcRnMessage where
         text "No explicit" <+> text "associated type"
           <+> text "or default declaration for"
           <+> quotes (ppr name)
+    TcRnIllegalTypeData
+      -> mkSimpleDecorated $
+        text "Illegal type-level data declaration"
+    TcRnTypeDataForbids feature
+      -> mkSimpleDecorated $
+        ppr feature <+> text "are not allowed in type data declarations."
+
   diagnosticReason = \case
     TcRnUnknownMessage m
       -> diagnosticReason m
@@ -1323,6 +1330,10 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnNoExplicitAssocTypeOrDefaultDeclaration{}
       -> WarningWithFlag (Opt_WarnMissingMethods)
+    TcRnIllegalTypeData
+      -> ErrorWithoutFlag
+    TcRnTypeDataForbids{}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -1655,6 +1666,10 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnNoExplicitAssocTypeOrDefaultDeclaration{}
       -> noHints
+    TcRnIllegalTypeData
+      -> [suggestExtension LangExt.TypeData]
+    TcRnTypeDataForbids{}
+      -> noHints
 
   diagnosticCode = constructorCode
 
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 16d91f1c44..a2daa7d900 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -7,6 +7,7 @@ module GHC.Tc.Errors.Types (
     TcRnMessage(..)
   , mkTcRnUnknownMessage
   , TcRnMessageDetailed(..)
+  , TypeDataForbids(..)
   , ErrInfo(..)
   , FixedRuntimeRepProvenance(..)
   , pprFixedRuntimeRepProvenance
@@ -2288,8 +2289,48 @@ data TcRnMessage where
             :: Name
             -> TcRnMessage
 
+  {-| TcRnIllegalTypeData is an error that occurs when a @type data@
+      declaration occurs without the TypeOperators extension.
+
+      See Note [Type data declarations]
+
+     Test case:
+       testsuite/tests/type-data/should_fail/TDNoPragma
+  -}
+  TcRnIllegalTypeData :: TcRnMessage
+
+  {-| TcRnTypeDataForbids is an error that occurs when a @type data@
+      declaration contains @data@ declaration features that are
+      forbidden in a @type data@ declaration.
+
+      See Note [Type data declarations]
+
+     Test cases:
+       testsuite/tests/type-data/should_fail/TDDeriving
+       testsuite/tests/type-data/should_fail/TDRecordsGADT
+       testsuite/tests/type-data/should_fail/TDRecordsH98
+       testsuite/tests/type-data/should_fail/TDStrictnessGADT
+       testsuite/tests/type-data/should_fail/TDStrictnessH98
+  -}
+  TcRnTypeDataForbids :: !TypeDataForbids -> TcRnMessage
+
   deriving Generic
 
+-- | Things forbidden in @type data@ declarations.
+-- See Note [Type data declarations]
+data TypeDataForbids
+  = TypeDataForbidsDatatypeContexts
+  | TypeDataForbidsLabelledFields
+  | TypeDataForbidsStrictnessAnnotations
+  | TypeDataForbidsDerivingClauses
+  deriving Generic
+
+instance Outputable TypeDataForbids where
+  ppr TypeDataForbidsDatatypeContexts      = text "Data type contexts"
+  ppr TypeDataForbidsLabelledFields        = text "Labelled fields"
+  ppr TypeDataForbidsStrictnessAnnotations = text "Strictness flags"
+  ppr TypeDataForbidsDerivingClauses       = text "Deriving clauses"
+
 -- | Specifies which back ends can handle a requested foreign import or export
 type ExpectedBackends = [Backend]
 -- | Specifies which calling convention is unsupported on the current platform
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index d0eb6337ef..3539b6e0e5 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -1287,9 +1287,15 @@ mk_prom_err_env (DataDecl { tcdLName = L _ name
                           , tcdDataDefn = HsDataDefn { dd_cons = cons } })
   = unitNameEnv name (APromotionErr TyConPE)
     `plusNameEnv`
-    mkNameEnv [ (con, APromotionErr RecDataConPE)
+    mkNameEnv [ (con, APromotionErr conPE)
               | L _ con' <- toList cons
               , L _ con  <- getConNames con' ]
+  where
+    -- In a "type data" declaration, the constructors are at the type level.
+    -- See Note [Type data declarations] in GHC.Rename.Module.
+    conPE
+      | isTypeDataDefnCons cons = TyConPE
+      | otherwise = RecDataConPE
 
 mk_prom_err_env decl
   = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
@@ -1788,6 +1794,9 @@ mappings:
 APromotionErr is only used for DataCons, and only used during type checking
 in tcTyClGroup.
 
+The same restriction applies constructors in to "type data" declarations.
+See Note [Type data declarations] in GHC.Rename.Module.
+
 
 ************************************************************************
 *                                                                      *
@@ -2952,17 +2961,17 @@ tcDataDefn err_ctxt roles_info tc_name
     -- so one could not have, say, a data family instance in an hsig file that
     -- has kind `Bool`. Therefore, this check need only occur in the code that
     -- typechecks data type declarations.
-    mk_permissive_kind HsigFile (DataTypeCons []) = True
+    mk_permissive_kind HsigFile (DataTypeCons _ []) = True
     mk_permissive_kind _ _ = False
 
     -- In an hs-boot or a signature file,
     -- a 'data' declaration with no constructors
     -- indicates a nominally distinct abstract data type.
-    mk_tc_rhs (isHsBootOrSig -> True) _ (DataTypeCons [])
+    mk_tc_rhs (isHsBootOrSig -> True) _ (DataTypeCons _ [])
       = return AbstractTyCon
 
     mk_tc_rhs _ tycon data_cons = case data_cons of
-          DataTypeCons data_cons -> return $
+          DataTypeCons _ data_cons -> return $
                         mkLevPolyDataTyConRhs
                           (isFixedRuntimeRepKind (tyConResKind tycon))
                           data_cons
@@ -3367,7 +3376,7 @@ concatMapDataDefnConsTcM name f = \ case
     NewTypeCon a -> f NewType a >>= \ case
         b:|[] -> pure (NewTypeCon b)
         bs -> failWithTc $ newtypeConError name (length bs)
-    DataTypeCons as -> DataTypeCons <$> concatMapM (fmap toList . f DataType) as
+    DataTypeCons is_type_data as -> DataTypeCons is_type_data <$> concatMapM (fmap toList . f DataType) as
 
 tcConDecl :: NewOrData
           -> DataDeclInfo
@@ -4415,6 +4424,14 @@ checkValidDataCon dflags existential_ok tc con
         ; checkTc (existential_ok || isVanillaDataCon con)
                   (badExistential con)
 
+          -- Check that the only constraints in signatures of constructors
+          -- in a "type data" declaration are equality constraints.
+          -- See Note [Type data declarations] in GHC.Rename.Module,
+          -- restriction (R4).
+        ; when (isTypeDataCon con) $
+          checkTc (all isEqPred (dataConOtherTheta con))
+                  (TcRnConstraintInKind (dataConRepType con))
+
           -- Check that UNPACK pragmas and bangs work out
           -- E.g.  reject   data T = MkT {-# UNPACK #-} Int     -- No "!"
           --                data T = MkT {-# UNPACK #-} !a      -- Can't unpack
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 32d710dec7..e1b7fc0f0f 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -772,7 +772,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
               ; rep_tc_name <- newFamInstTyConName lfam_name pats
               ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
               ; tc_rhs <- case data_cons of
-                     DataTypeCons data_cons -> return $
+                     DataTypeCons _ data_cons -> return $
                         mkLevPolyDataTyConRhs
                           (isFixedRuntimeRepKind res_kind)
                           data_cons
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index f7ba81db6b..47e8b5758c 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -294,7 +294,8 @@ cvtDec (DataD ctxt tc tvs ksig constrs derivs)
                                 , dd_cType = Nothing
                                 , dd_ctxt = mkHsContextMaybe ctxt'
                                 , dd_kindSig = ksig'
-                                , dd_cons = DataTypeCons cons', dd_derivs = derivs' }
+                                , dd_cons = DataTypeCons False cons'
+                                , dd_derivs = derivs' }
         ; returnJustLA $ TyClD noExtField $
           DataDecl { tcdDExt = noAnn
                    , tcdLName = tc', tcdTyVars = tvs'
@@ -381,7 +382,8 @@ cvtDec (DataInstD ctxt bndrs tys ksig constrs derivs)
                                , dd_cType = Nothing
                                , dd_ctxt = mkHsContextMaybe ctxt'
                                , dd_kindSig = ksig'
-                               , dd_cons = DataTypeCons cons', dd_derivs = derivs' }
+                               , dd_cons = DataTypeCons False cons'
+                               , dd_derivs = derivs' }
 
        ; returnJustLA $ InstD noExtField $ DataFamInstD
            { dfid_ext = noExtField
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 639863c630..58353483dc 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -466,6 +466,8 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnIgnoreSpecialisePragmaOnDefMethod"         = 72520
   GhcDiagnosticCode "TcRnBadMethodErr"                              = 46284
   GhcDiagnosticCode "TcRnNoExplicitAssocTypeOrDefaultDeclaration"   = 08585
+  GhcDiagnosticCode "TcRnIllegalTypeData"                           = 15013
+  GhcDiagnosticCode "TcRnTypeDataForbids"                           = 67297
 
   -- TcRnPragmaWarning
   GhcDiagnosticCode "WarningTxt"                                    = 63394
diff --git a/compiler/GHC/Types/TyThing.hs b/compiler/GHC/Types/TyThing.hs
index 8a12506a63..628d8da801 100644
--- a/compiler/GHC/Types/TyThing.hs
+++ b/compiler/GHC/Types/TyThing.hs
@@ -183,9 +183,8 @@ implicitTyConThings tc
     implicitCoTyCon tc ++
 
       -- for each data constructor in order,
-      --   the constructor, worker, and (possibly) wrapper
-    [ thing | dc    <- tyConDataCons tc
-            , thing <- AConLike (RealDataCon dc) : dataConImplicitTyThings dc ]
+      --   the constructor and associated implicit 'Id's
+    concatMap datacon_stuff (tyConDataCons tc)
       -- NB. record selectors are *not* implicit, they have fully-fledged
       -- bindings that pass through the compilation pipeline as normal.
   where
@@ -193,6 +192,17 @@ implicitTyConThings tc
         Nothing -> []
         Just cl -> implicitClassThings cl
 
+    -- For each data constructor,
+    --   the constructor, worker, and (possibly) wrapper
+    --
+    -- If the data constructor is in a "type data" declaration,
+    -- promote it to the type level now.
+    -- See Note [Type data declarations] in GHC.Rename.Module.
+    datacon_stuff dc
+      | isTypeDataCon dc = [ATyCon (promoteDataCon dc)]
+      | otherwise
+        = AConLike (RealDataCon dc) : dataConImplicitTyThings dc
+
 -- For newtypes and closed type families (only) add the implicit coercion tycon
 implicitCoTyCon :: TyCon -> [TyThing]
 implicitCoTyCon tc