Fix TypeData issues (fixes #22315 and #22332)

There were two bugs here:

1. Treating type-level constructors as PromotedDataCon doesn't always
   work, in particular because constructors promoted via DataKinds are
   called both T and 'T. (Tests T22332a, T22332b, T22315a, T22315b)
   Fix: guard these cases with isDataKindsPromotedDataCon.

2. Type-level constructors were sent to the code generator, producing
   things like constructor wrappers. (Tests T22332a, T22332b)
   Fix: test for them in isDataTyCon.

Other changes:

* changed the marking of "type data" DataCon's as suggested by SPJ.

* added a test TDGADT for a type-level GADT.

* comment tweaks

* change tcIfaceTyCon to ignore IfaceTyConInfo, so that IfaceTyConInfo
  is used only for pretty printing, not for typechecking. (SPJ)

28 files changed, 261 insertions, 74 deletions

diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index e50290a5f8..70aa2b8b75 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -1638,7 +1638,7 @@ 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))
+isTypeDataCon dc = isTypeDataTyCon (dataConTyCon dc)
 
 -- | Should this DataCon be allowed in a type even without -XDataKinds?
 -- Currently, only Lifted & Unlifted
diff --git a/compiler/GHC/Core/DataCon.hs-boot b/compiler/GHC/Core/DataCon.hs-boot
index f8807bf3a6..e5ab19f0db 100644
--- a/compiler/GHC/Core/DataCon.hs-boot
+++ b/compiler/GHC/Core/DataCon.hs-boot
@@ -27,6 +27,7 @@ dataConStupidTheta :: DataCon -> ThetaType
 dataConFullSig :: DataCon
                -> ([TyVar], [TyCoVar], [EqSpec], ThetaType, [Scaled Type], Type)
 isUnboxedSumDataCon :: DataCon -> Bool
+isTypeDataCon :: DataCon -> Bool
 
 instance Eq DataCon
 instance Uniquable DataCon
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index 5ae1e2bf6b..9ecf34c6a5 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -56,10 +56,12 @@ module GHC.Core.TyCon(
         isTypeSynonymTyCon,
         mustBeSaturated,
         isPromotedDataCon, isPromotedDataCon_maybe,
+        isDataKindsPromotedDataCon,
         isKindTyCon, isLiftedTypeKindTyConName,
         isTauTyCon, isFamFreeTyCon, isForgetfulSynTyCon,
 
         isDataTyCon,
+        isTypeDataTyCon,
         isEnumerationTyCon,
         isNewTyCon, isAbstractTyCon,
         isFamilyTyCon, isOpenFamilyTyCon,
@@ -147,7 +149,7 @@ import {-# SOURCE #-} GHC.Builtin.Types
 import {-# SOURCE #-} GHC.Core.DataCon
    ( DataCon, dataConFieldLabels
    , dataConTyCon, dataConFullSig
-   , isUnboxedSumDataCon )
+   , isUnboxedSumDataCon, isTypeDataCon )
 import {-# SOURCE #-} GHC.Core.Type
    ( isLiftedTypeKind )
 import GHC.Builtin.Uniques
@@ -1138,6 +1140,9 @@ data AlgTyConRhs
                           -- ^ Cached value: length data_cons
         is_enum :: Bool,  -- ^ Cached value: is this an enumeration type?
                           --   See Note [Enumeration types]
+        is_type_data :: Bool,
+                        -- from a "type data" declaration
+                        -- See Note [Type data declarations] in GHC.Rename.Module
         data_fixed_lev :: Bool
                         -- ^ 'True' if the data type constructor has
                         -- a known, fixed levity when fully applied
@@ -1218,14 +1223,18 @@ mkSumTyConRhs data_cons = SumTyCon data_cons (length data_cons)
 -- | Create an 'AlgTyConRhs' from the data constructors,
 -- for a potentially levity-polymorphic datatype (with `UnliftedDatatypes`).
 mkLevPolyDataTyConRhs :: Bool -- ^ whether the 'DataCon' has a fixed levity
+                      -> Bool -- ^ True if this is a "type data" declaration
+                              -- See Note [Type data declarations]
+                              -- in GHC.Rename.Module
                       -> [DataCon]
                       -> AlgTyConRhs
-mkLevPolyDataTyConRhs fixed_lev cons
+mkLevPolyDataTyConRhs fixed_lev type_data cons
   = DataTyCon {
         data_cons = cons,
         data_cons_size = length cons,
         is_enum = not (null cons) && all is_enum_con cons,
                   -- See Note [Enumeration types] in GHC.Core.TyCon
+        is_type_data = type_data,
         data_fixed_lev = fixed_lev
     }
   where
@@ -1236,9 +1245,10 @@ mkLevPolyDataTyConRhs fixed_lev cons
 
 -- | Create an 'AlgTyConRhs' from the data constructors.
 --
--- Use 'mkLevPolyDataConRhs' if the datatype can be levity-polymorphic.
+-- Use 'mkLevPolyDataConRhs' if the datatype can be levity-polymorphic
+-- or if it comes from a "data type" declaration
 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
-mkDataTyConRhs = mkLevPolyDataTyConRhs True
+mkDataTyConRhs = mkLevPolyDataTyConRhs True False
 
 -- | Some promoted datacons signify extra info relevant to GHC. For example,
 -- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
@@ -2133,11 +2143,21 @@ isDataTyCon (AlgTyCon {algTcRhs = rhs})
         TupleTyCon { tup_sort = sort }
                            -> isBoxed (tupleSortBoxity sort)
         SumTyCon {}        -> False
-        DataTyCon {}       -> True
+            -- Constructors from "type data" declarations exist only at
+            -- the type level.
+            -- See Note [Type data declarations] in GHC.Rename.Module.
+        DataTyCon { is_type_data = type_data } -> not type_data
         NewTyCon {}        -> False
         AbstractTyCon {}   -> False      -- We don't know, so return False
 isDataTyCon _ = False
 
+-- | Was this 'TyCon' declared as "type data"?
+-- See Note [Type data declarations] in GHC.Rename.Module.
+isTypeDataTyCon :: TyCon -> Bool
+isTypeDataTyCon (AlgTyCon {algTcRhs = DataTyCon {is_type_data = type_data }})
+  = type_data
+isTypeDataTyCon _              = False
+
 -- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
 -- (where X is the role passed in):
 --   If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
@@ -2385,6 +2405,19 @@ isPromotedDataCon :: TyCon -> Bool
 isPromotedDataCon (PromotedDataCon {}) = True
 isPromotedDataCon _                    = False
 
+-- | This function identifies PromotedDataCon's from data constructors in
+-- `data T = K1 | K2`, promoted by -XDataKinds.  These type constructors
+-- are printed with a tick mark 'K1 and 'K2, and similarly have a tick
+-- mark added to their OccName's.
+--
+-- In contrast, constructors in `type data T = K1 | K2` are printed and
+-- represented with their original undecorated names.
+-- See Note [Type data declarations] in GHC.Rename.Module
+isDataKindsPromotedDataCon :: TyCon -> Bool
+isDataKindsPromotedDataCon (PromotedDataCon { dataCon = dc })
+  = not (isTypeDataCon dc)
+isDataKindsPromotedDataCon _ = False
+
 -- | Retrieves the promoted DataCon if this is a PromotedDataCon;
 isPromotedDataCon_maybe :: TyCon -> Maybe DataCon
 isPromotedDataCon_maybe (PromotedDataCon { dataCon = dc }) = Just dc
@@ -2921,9 +2954,10 @@ tcFlavourIsOpen TypeSynonymFlavour      = False
 pprPromotionQuote :: TyCon -> SDoc
 -- Promoted data constructors already have a tick in their OccName
 pprPromotionQuote tc
-  = case tc of
-      PromotedDataCon {} -> char '\'' -- Always quote promoted DataCons in types
-      _                  -> empty
+        -- Always quote promoted DataCons in types, unless they come
+        -- from "type data" declarations.
+  | isDataKindsPromotedDataCon tc = char '\''
+  | otherwise = empty
 
 instance NamedThing TyCon where
     getName = tyConName
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index ad2d8497ff..c8471039e7 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -230,7 +230,7 @@ toIfaceTyCon tc
   where
     tc_name = tyConName tc
     info    = mkIfaceTyConInfo promoted sort
-    promoted | isPromotedDataCon tc = IsPromoted
+    promoted | isDataKindsPromotedDataCon tc = IsPromoted
              | otherwise            = NotPromoted
 
     tupleSort :: TyCon -> Maybe IfaceTyConSort
diff --git a/compiler/GHC/Iface/Make.hs b/compiler/GHC/Iface/Make.hs
index e84d342324..6dd7f75509 100644
--- a/compiler/GHC/Iface/Make.hs
+++ b/compiler/GHC/Iface/Make.hs
@@ -550,7 +550,7 @@ tyConToIfaceDecl env tycon
                   ifCType      = Nothing,
                   ifRoles      = tyConRoles tycon,
                   ifCtxt       = [],
-                  ifCons       = IfDataTyCon [],
+                  ifCons       = IfDataTyCon False [],
                   ifGadtSyntax = False,
                   ifParent     = IfNoParent })
   where
@@ -584,9 +584,10 @@ tyConToIfaceDecl env tycon
             axn  = coAxiomName ax
 
     ifaceConDecls (NewTyCon { data_con = con })    = IfNewTyCon  (ifaceConDecl con)
-    ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
-    ifaceConDecls (TupleTyCon { data_con = con })  = IfDataTyCon [ifaceConDecl con]
-    ifaceConDecls (SumTyCon { data_cons = cons })  = IfDataTyCon (map ifaceConDecl cons)
+    ifaceConDecls (DataTyCon { data_cons = cons, is_type_data = type_data })
+      = IfDataTyCon type_data (map ifaceConDecl cons)
+    ifaceConDecls (TupleTyCon { data_con = con })  = IfDataTyCon False [ifaceConDecl con]
+    ifaceConDecls (SumTyCon { data_cons = cons })  = IfDataTyCon False (map ifaceConDecl cons)
     ifaceConDecls AbstractTyCon                    = IfAbstractTyCon
         -- The AbstractTyCon case happens when a TyCon has been trimmed
         -- during tidying.
diff --git a/compiler/GHC/Iface/Rename.hs b/compiler/GHC/Iface/Rename.hs
index 1a7acea25f..8cbbb0e247 100644
--- a/compiler/GHC/Iface/Rename.hs
+++ b/compiler/GHC/Iface/Rename.hs
@@ -543,8 +543,8 @@ rnIfaceTyConParent (IfDataInstance n tc args)
 rnIfaceTyConParent IfNoParent = pure IfNoParent
 
 rnIfaceConDecls :: Rename IfaceConDecls
-rnIfaceConDecls (IfDataTyCon ds)
-    = IfDataTyCon <$> mapM rnIfaceConDecl ds
+rnIfaceConDecls (IfDataTyCon type_data ds)
+    = IfDataTyCon type_data <$> mapM rnIfaceConDecl ds
 rnIfaceConDecls (IfNewTyCon d) = IfNewTyCon <$> rnIfaceConDecl d
 rnIfaceConDecls IfAbstractTyCon = pure IfAbstractTyCon
 
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index 299dfe553b..c209a70123 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -236,7 +236,9 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars    :: [IfaceTvBndr]
 
 data IfaceConDecls
   = IfAbstractTyCon -- c.f TyCon.AbstractTyCon
-  | IfDataTyCon [IfaceConDecl] -- Data type decls
+  | IfDataTyCon !Bool [IfaceConDecl] -- Data type decls
+        -- The Bool is True for "type data" declarations.
+        -- see Note [Type data declarations] in GHC.Rename.Module
   | IfNewTyCon  IfaceConDecl   -- Newtype decls
 
 -- For IfDataTyCon and IfNewTyCon we store:
@@ -450,7 +452,7 @@ See [https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/recompilation-
 
 visibleIfConDecls :: IfaceConDecls -> [IfaceConDecl]
 visibleIfConDecls (IfAbstractTyCon {}) = []
-visibleIfConDecls (IfDataTyCon cs)     = cs
+visibleIfConDecls (IfDataTyCon _ cs)   = cs
 visibleIfConDecls (IfNewTyCon c)       = [c]
 
 ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName]
@@ -459,18 +461,23 @@ ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName]
 -- especially the question of whether there's a wrapper for a datacon
 -- See Note [Implicit TyThings] in GHC.Driver.Env
 
--- N.B. the set of names returned here *must* match the set of
--- TyThings returned by GHC.Driver.Env.implicitTyThings, in the sense that
+-- N.B. the set of names returned here *must* match the set of TyThings
+-- returned by GHC.Types.TyThing.implicitTyThings, in the sense that
 -- TyThing.getOccName should define a bijection between the two lists.
--- This invariant is used in GHC.IfaceToCore.tc_iface_decl_fingerprint (see note
--- [Tricky iface loop])
+-- This invariant is used in GHC.IfaceToCore.tc_iface_decl_fingerprint
+-- (see Note [Tricky iface loop] in GHC.Types.TyThing.)
 -- The order of the list does not matter.
 
 ifaceDeclImplicitBndrs (IfaceData {ifName = tc_name, ifCons = cons })
   = case cons of
       IfAbstractTyCon {} -> []
       IfNewTyCon  cd     -> mkNewTyCoOcc (occName tc_name) : ifaceConDeclImplicitBndrs cd
-      IfDataTyCon cds    -> concatMap ifaceConDeclImplicitBndrs cds
+      IfDataTyCon type_data cds
+        | type_data ->
+          -- Constructors in "type data" declarations have no implicits.
+          -- see Note [Type data declarations] in GHC.Rename.Module
+          [occName con_name | IfCon { ifConName = con_name } <- cds]
+        | otherwise -> concatMap ifaceConDeclImplicitBndrs cds
 
 ifaceDeclImplicitBndrs (IfaceClass { ifBody = IfAbstractClass })
   = []
@@ -907,6 +914,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
 
     pp_nd = case condecls of
               IfAbstractTyCon{} -> text "data"
+              IfDataTyCon True _ -> text "type data"
               IfDataTyCon{}     -> text "data"
               IfNewTyCon{}      -> text "newtype"
 
@@ -1633,8 +1641,8 @@ freeNamesDM (Just (GenericDM ty)) = freeNamesIfType ty
 freeNamesDM _                     = emptyNameSet
 
 freeNamesIfConDecls :: IfaceConDecls -> NameSet
-freeNamesIfConDecls (IfDataTyCon c) = fnList freeNamesIfConDecl c
-freeNamesIfConDecls (IfNewTyCon  c) = freeNamesIfConDecl c
+freeNamesIfConDecls (IfDataTyCon _ cs) = fnList freeNamesIfConDecl cs
+freeNamesIfConDecls (IfNewTyCon    c)  = freeNamesIfConDecl c
 freeNamesIfConDecls _                   = emptyNameSet
 
 freeNamesIfConDecl :: IfaceConDecl -> NameSet
@@ -2118,14 +2126,16 @@ instance Binary IfaceAxBranch where
 
 instance Binary IfaceConDecls where
     put_ bh IfAbstractTyCon  = putByte bh 0
-    put_ bh (IfDataTyCon cs) = putByte bh 1 >> put_ bh cs
-    put_ bh (IfNewTyCon c)   = putByte bh 2 >> put_ bh c
+    put_ bh (IfDataTyCon False cs) = putByte bh 1 >> put_ bh cs
+    put_ bh (IfDataTyCon True cs) = putByte bh 2 >> put_ bh cs
+    put_ bh (IfNewTyCon c)   = putByte bh 3 >> put_ bh c
     get bh = do
         h <- getByte bh
         case h of
             0 -> return IfAbstractTyCon
-            1 -> liftM IfDataTyCon (get bh)
-            2 -> liftM IfNewTyCon (get bh)
+            1 -> liftM (IfDataTyCon False) (get bh)
+            2 -> liftM (IfDataTyCon True) (get bh)
+            3 -> liftM IfNewTyCon (get bh)
             _ -> error "Binary(IfaceConDecls).get: Invalid IfaceConDecls"
 
 instance Binary IfaceConDecl where
@@ -2624,7 +2634,7 @@ instance NFData IfaceTyConParent where
 instance NFData IfaceConDecls where
   rnf = \case
     IfAbstractTyCon -> ()
-    IfDataTyCon f1 -> rnf f1
+    IfDataTyCon _ f1 -> rnf f1
     IfNewTyCon f1 -> rnf f1
 
 instance NFData IfaceConDecl where
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index cb50003fe4..831380c03b 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -352,9 +352,13 @@ for the purposes of pretty-printing.
 See Note [The equality types story] in GHC.Builtin.Types.Prim.
 -}
 
-data IfaceTyConInfo   -- Used to guide pretty-printing
-                      -- and to disambiguate D from 'D (they share a name)
+data IfaceTyConInfo   -- Used only to guide pretty-printing
   = IfaceTyConInfo { ifaceTyConIsPromoted :: PromotionFlag
+                      -- A PromotionFlag value of IsPromoted indicates
+                      -- that the type constructor came from a data
+                      -- constructor promoted by -XDataKinds, and thus
+                      -- should be printed as 'D to distinguish it from
+                      -- an existing type constructor D.
                    , ifaceTyConSort       :: IfaceTyConSort }
     deriving (Eq)
 
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 0999f419b6..0df2dec9bc 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -338,7 +338,7 @@ d1 `withRolesFrom` d2
     mergeRoles roles1 roles2 = zipWithEqual "mergeRoles" max roles1 roles2
 
 isRepInjectiveIfaceDecl :: IfaceDecl -> Bool
-isRepInjectiveIfaceDecl IfaceData{ ifCons = IfDataTyCon _ } = True
+isRepInjectiveIfaceDecl IfaceData{ ifCons = IfDataTyCon{} } = True
 isRepInjectiveIfaceDecl IfaceFamily{ ifFamFlav = IfaceDataFamilyTyCon } = True
 isRepInjectiveIfaceDecl _ = False
 
@@ -1083,11 +1083,12 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
   = case if_cons of
         IfAbstractTyCon
           -> return AbstractTyCon
-        IfDataTyCon cons
+        IfDataTyCon type_data cons
           -> do  { data_cons  <- mapM tc_con_decl cons
                  ; return $
                      mkLevPolyDataTyConRhs
                        (isFixedRuntimeRepKind $ tyConResKind tycon)
+                       type_data
                        data_cons }
         IfNewTyCon con
           -> do  { data_con  <- tc_con_decl con
@@ -1957,11 +1958,12 @@ tcIfaceGlobal name
 -- this expression *after* typechecking T.
 
 tcIfaceTyCon :: IfaceTyCon -> IfL TyCon
-tcIfaceTyCon (IfaceTyCon name info)
+tcIfaceTyCon (IfaceTyCon name _info)
   = do { thing <- tcIfaceGlobal name
-       ; return $ case ifaceTyConIsPromoted info of
-           NotPromoted -> tyThingTyCon thing
-           IsPromoted  -> promoteDataCon $ tyThingDataCon thing }
+       ; case thing of
+              ATyCon tc -> return tc
+              AConLike (RealDataCon dc) -> return (promoteDataCon dc)
+              _ -> pprPanic "tcIfaceTyCon" (ppr thing) }
 
 tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
 tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 922e0f7a8e..74058503ca 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2036,7 +2036,7 @@ rnDataDefn doc (HsDataDefn { dd_cType = cType, dd_ctxt = context, dd_cons = cond
 {-
 Note [Type data declarations]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-With the TypeData extension (GHC proposal #106), one can write "type data"
+With the TypeData extension (GHC proposal #106), one can write `type data`
 declarations, like
 
     type data Nat = Zero | Succ Nat
@@ -2047,17 +2047,18 @@ or equivalently in GADT style:
         Zero :: Nat
         Succ :: Nat -> Nat
 
-This defines the constructors Zero and Succ in the TcCls namespace
+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.
+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:
+Type data declarations have the syntax of `data` declarations (but not
+`newtype` 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).
+(R1) There are no 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.
@@ -2078,14 +2079,15 @@ following restrictions:
 
 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.
+* The parser recognizes `type data` (but not `type newtype`).
 
-* 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.
+* During the initial construction of the AST,
+  GHC.Parser.PostProcess.checkNewOrData sets the `Bool` argument of the
+  `DataTypeCons` inside a `HsDataDefn` to mark a `type data` declaration.
+  It also puts the the constructor names (`Zero` and `Succ` in our
+  example) in the TcCls namespace.
 
-* GHC.Rename.Module.rnDataDefn calls check_type_data on these
+* 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
@@ -2094,19 +2096,40 @@ The main parts of the implementation are:
 * 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)
+  the `type data` constructors (`Zero` and `Succ` in our example) 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)) -- illegal: tycon K is recursively defined
+
+* The `type data` data type, such as `Nat` in our example, is represented
+  by a `TyCon` that is an `AlgTyCon`, but its `AlgTyConRhs` has the
+  `is_type_data` field set.
+
+* The constructors of the data type, `Zero` and `Succ` in our example,
+  are each represented by a `DataCon` as usual.  That `DataCon`'s
+  `dcPromotedField` is a `TyCon` (for `Zero`, say) that you can use
+  in a type.
+
+* After a `type data` declaration has been type-checked, the type-checker
+  environment entry for each constructor (`Zero` and `Succ` in our
+  example) is just the promoted type constructor, not the bundle required
+  for a data constructor.  (GHC.Types.TyThing.implicitTyConThings)
+
+* GHC.Core.TyCon.isDataKindsPromotedDataCon ignores promoted constructors
+  from `type data`, which do not use the distinguishing quote mark added
+  to constructors promoted by DataKinds.
+
+* GHC.Core.TyCon.isDataTyCon ignores types coming from a `type data`
+  declaration (by checking the `is_type_data` field), so that these do
+  not contribute executable code such as constructor wrappers.
+
+* The `is_type_data` field is copied into a Boolean argument
+  of the `IfDataTyCon` constructor of `IfaceConDecls` by
+  GHC.Iface.Make.tyConToIfaceDecl.
 
 -}
 
diff --git a/compiler/GHC/Tc/Instance/Typeable.hs b/compiler/GHC/Tc/Instance/Typeable.hs
index e0bcfa8428..d5ad9b5186 100644
--- a/compiler/GHC/Tc/Instance/Typeable.hs
+++ b/compiler/GHC/Tc/Instance/Typeable.hs
@@ -649,7 +649,7 @@ mkTyConRepTyConRHS (Stuff {..}) todo tycon kind_rep
   where
     n_kind_vars = length $ filter isNamedTyConBinder (tyConBinders tycon)
     tycon_str = add_tick (occNameString (getOccName tycon))
-    add_tick s | isPromotedDataCon tycon = '\'' : s
+    add_tick s | isDataKindsPromotedDataCon tycon = '\'' : s
                | otherwise               = s
 
     -- This must match the computation done in
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 225e53d83e..605d004834 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -2981,9 +2981,10 @@ tcDataDefn err_ctxt roles_info tc_name
       = return AbstractTyCon
 
     mk_tc_rhs _ tycon data_cons = case data_cons of
-          DataTypeCons _ data_cons -> return $
+          DataTypeCons is_type_data data_cons -> return $
                         mkLevPolyDataTyConRhs
                           (isFixedRuntimeRepKind (tyConResKind tycon))
+                          is_type_data
                           data_cons
           NewTypeCon data_con -> mkNewTyConRhs tc_name tycon data_con
 
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 8b3c34aa83..2eccaa22fc 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -772,9 +772,10 @@ 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 type_data data_cons -> return $
                         mkLevPolyDataTyConRhs
                           (isFixedRuntimeRepKind res_kind)
+                          type_data
                           data_cons
                      NewTypeCon data_con -> mkNewTyConRhs rep_tc_name rec_rep_tc data_con
 
diff --git a/compiler/GHC/Types/TyThing.hs b/compiler/GHC/Types/TyThing.hs
index 628d8da801..15fff48509 100644
--- a/compiler/GHC/Types/TyThing.hs
+++ b/compiler/GHC/Types/TyThing.hs
@@ -184,7 +184,7 @@ implicitTyConThings tc
 
       -- for each data constructor in order,
       --   the constructor and associated implicit 'Id's
-    concatMap datacon_stuff (tyConDataCons tc)
+    datacon_stuff
       -- NB. record selectors are *not* implicit, they have fully-fledged
       -- bindings that pass through the compilation pipeline as normal.
   where
@@ -192,16 +192,22 @@ implicitTyConThings tc
         Nothing -> []
         Just cl -> implicitClassThings cl
 
-    -- For each data constructor,
+    -- For each data constructor in order,
     --   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)]
+    datacon_stuff :: [TyThing]
+    datacon_stuff
+      | isTypeDataTyCon tc = [ATyCon (promoteDataCon dc) | dc <- cons]
       | otherwise
-        = AConLike (RealDataCon dc) : dataConImplicitTyThings dc
+      = [ty_thing | dc <- cons,
+                    ty_thing <- AConLike (RealDataCon dc) :
+                                dataConImplicitTyThings dc]
+
+    cons :: [DataCon]
+    cons = tyConDataCons tc
 
 -- For newtypes and closed type families (only) add the implicit coercion tycon
 implicitCoTyCon :: TyCon -> [TyThing]
diff --git a/testsuite/tests/type-data/should_compile/T22315a/Lib.hs b/testsuite/tests/type-data/should_compile/T22315a/Lib.hs
new file mode 100644
index 0000000000..a705db82f7
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/T22315a/Lib.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE DataKinds, TypeData #-}
+module T22315a.Lib where
+
+data TermLevel = Mk
+type data TypeLevel = Mk
+
+class C (a :: TypeLevel)
+instance C Mk where
+
+foo :: C a => proxy a -> ()
+foo _ = ()
diff --git a/testsuite/tests/type-data/should_compile/T22315a/Main.hs b/testsuite/tests/type-data/should_compile/T22315a/Main.hs
new file mode 100644
index 0000000000..6089f788d6
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/T22315a/Main.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+module T22315a.Main where
+
+import T22315a.Lib
+
+data Proxy (a :: TypeLevel)
+
+bar :: Proxy Mk -> ()
+bar = foo
diff --git a/testsuite/tests/type-data/should_compile/TDGADT.hs b/testsuite/tests/type-data/should_compile/TDGADT.hs
new file mode 100644
index 0000000000..a286e60680
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/TDGADT.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeData #-}
+module TDGADT where
+
+import Data.Kind (Type)
+
+type data Nat = Zero | Succ Nat
+
+-- type level GADT
+type data Vec :: Nat -> Type -> Type where
+    VNil :: Vec Zero a
+    VCons :: a -> Vec n a -> Vec (Succ n) a
+
+type X = VCons Bool (VCons Int VNil)
diff --git a/testsuite/tests/type-data/should_compile/all.T b/testsuite/tests/type-data/should_compile/all.T
index 0f8294bee7..b5e9810b00 100644
--- a/testsuite/tests/type-data/should_compile/all.T
+++ b/testsuite/tests/type-data/should_compile/all.T
@@ -1,4 +1,6 @@
 test('TDDataConstructor', normal, compile, [''])
 test('TDExistential', normal, compile, [''])
+test('TDGADT', normal, compile, [''])
 test('TDGoodConsConstraints', normal, compile, [''])
 test('TDVector', normal, compile, [''])
+test('T22315a', [extra_files(['T22315a/'])], multimod_compile, ['T22315a.Lib T22315a.Main', '-v0'])
diff --git a/testsuite/tests/type-data/should_fail/T22332b.hs b/testsuite/tests/type-data/should_fail/T22332b.hs
new file mode 100644
index 0000000000..f13e15ba9c
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/T22332b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeData, DataKinds #-}
+module T22332b where
+
+type data X1 = T
+data X2 = T
+data Proxy a
+
+f :: Proxy T
+f = f :: Proxy 'T
diff --git a/testsuite/tests/type-data/should_fail/T22332b.stderr b/testsuite/tests/type-data/should_fail/T22332b.stderr
new file mode 100644
index 0000000000..26fd44a45f
--- /dev/null
+++ b/testsuite/tests/type-data/should_fail/T22332b.stderr
@@ -0,0 +1,7 @@
+
+T22332b.hs:9:5: error: [GHC-83865]
+    • Couldn't match type ‘T’ with ‘'T’
+      Expected: Proxy 'T
+        Actual: Proxy T
+    • In the expression: f :: Proxy 'T
+      In an equation for ‘f’: f = f :: Proxy 'T
diff --git a/testsuite/tests/type-data/should_fail/all.T b/testsuite/tests/type-data/should_fail/all.T
index ddf7bd86bd..82b257df22 100644
--- a/testsuite/tests/type-data/should_fail/all.T
+++ b/testsuite/tests/type-data/should_fail/all.T
@@ -11,3 +11,4 @@ test('TDRecordsH98', normal, compile_fail, [''])
 test('TDRecursive', normal, compile_fail, [''])
 test('TDStrictnessGADT', normal, compile_fail, [''])
 test('TDStrictnessH98', normal, compile_fail, [''])
+test('T22332b', normal, compile_fail, [''])
diff --git a/testsuite/tests/type-data/should_run/Makefile b/testsuite/tests/type-data/should_run/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/type-data/should_run/T22315b.hs b/testsuite/tests/type-data/should_run/T22315b.hs
new file mode 100644
index 0000000000..ce58e8ae1c
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22315b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeData #-}
+module T22315b where
+
+data TermLevel = Mk
+type data TypeLevel = Mk
+
+mk = Mk
+
+type Mk2 = Mk
diff --git a/testsuite/tests/type-data/should_run/T22315b.script b/testsuite/tests/type-data/should_run/T22315b.script
new file mode 100644
index 0000000000..fff5aa2d98
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22315b.script
@@ -0,0 +1,5 @@
+:load T22315b.hs
+:type Mk
+:kind Mk
+:type mk
+:kind Mk2
diff --git a/testsuite/tests/type-data/should_run/T22315b.stdout b/testsuite/tests/type-data/should_run/T22315b.stdout
new file mode 100644
index 0000000000..f071fb1724
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22315b.stdout
@@ -0,0 +1,4 @@
+Mk :: TermLevel
+Mk :: TypeLevel
+mk :: TermLevel
+Mk2 :: TypeLevel
diff --git a/testsuite/tests/type-data/should_run/T22332a.hs b/testsuite/tests/type-data/should_run/T22332a.hs
new file mode 100644
index 0000000000..bddb9065c5
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22332a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE TypeData, DataKinds, TypeFamilies #-}
+module Main where
+
+import Type.Reflection
+import Data.Type.Equality
+
+data Proxy a
+type data X1 = T -- defines type constructor T
+data X2 = T      -- defines type constructor 'T
+
+data family F p
+
+newtype instance F (Proxy T) = ID (forall a. a -> a)
+newtype instance F (Proxy 'T) = UC (forall a b. a -> b)
+
+-- This should fail at runtime because these are different types
+eq :: T :~~: 'T
+Just eq = eqTypeRep typeRep typeRep
+
+p :: a :~~: b -> F (Proxy a) :~: F (Proxy b)
+p HRefl = Refl
+
+uc :: a -> b
+uc = case castWith (p eq) (ID id) of UC a -> a
+
+main :: IO ()
+main = print (uc 'a' :: Int)
diff --git a/testsuite/tests/type-data/should_run/T22332a.stderr b/testsuite/tests/type-data/should_run/T22332a.stderr
new file mode 100644
index 0000000000..693ad69986
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/T22332a.stderr
@@ -0,0 +1 @@
+T22332a: T22332a.hs:18:1-35: Non-exhaustive patterns in Just eq
diff --git a/testsuite/tests/type-data/should_run/all.T b/testsuite/tests/type-data/should_run/all.T
new file mode 100644
index 0000000000..f1faf7796e
--- /dev/null
+++ b/testsuite/tests/type-data/should_run/all.T
@@ -0,0 +1,2 @@
+test('T22332a', exit_code(1), compile_and_run, [''])
+test('T22315b', extra_files(['T22315b.hs']), ghci_script, ['T22315b.script'])