[Git][ghc/ghc][master] Fix TypeData issues (fixes #22315 and #22332)
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Tue Nov 8 17:55:07 UTC 2022
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
ce726cd2 by Ross Paterson at 2022-11-08T12:54:34-05:00
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 changed files:
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/DataCon.hs-boot
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Iface/Make.hs
- compiler/GHC/Iface/Rename.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Instance/Typeable.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Types/TyThing.hs
- + testsuite/tests/type-data/should_compile/T22315a/Lib.hs
- + testsuite/tests/type-data/should_compile/T22315a/Main.hs
- + testsuite/tests/type-data/should_compile/TDGADT.hs
- testsuite/tests/type-data/should_compile/all.T
- + testsuite/tests/type-data/should_fail/T22332b.hs
- + testsuite/tests/type-data/should_fail/T22332b.stderr
- testsuite/tests/type-data/should_fail/all.T
- + testsuite/tests/type-data/should_run/Makefile
- + testsuite/tests/type-data/should_run/T22315b.hs
- + testsuite/tests/type-data/should_run/T22315b.script
- + testsuite/tests/type-data/should_run/T22315b.stdout
- + testsuite/tests/type-data/should_run/T22332a.hs
- + testsuite/tests/type-data/should_run/T22332a.stderr
- + testsuite/tests/type-data/should_run/all.T
Changes:
=====================================
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
=====================================
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
=====================================
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
=====================================
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
=====================================
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.
=====================================
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
=====================================
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
=====================================
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)
=====================================
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
=====================================
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.
-}
=====================================
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
=====================================
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
=====================================
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
=====================================
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]
=====================================
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 _ = ()
=====================================
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
=====================================
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)
=====================================
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'])
=====================================
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
=====================================
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
=====================================
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, [''])
=====================================
testsuite/tests/type-data/should_run/Makefile
=====================================
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
=====================================
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
=====================================
testsuite/tests/type-data/should_run/T22315b.script
=====================================
@@ -0,0 +1,5 @@
+:load T22315b.hs
+:type Mk
+:kind Mk
+:type mk
+:kind Mk2
=====================================
testsuite/tests/type-data/should_run/T22315b.stdout
=====================================
@@ -0,0 +1,4 @@
+Mk :: TermLevel
+Mk :: TypeLevel
+mk :: TermLevel
+Mk2 :: TypeLevel
=====================================
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)
=====================================
testsuite/tests/type-data/should_run/T22332a.stderr
=====================================
@@ -0,0 +1 @@
+T22332a: T22332a.hs:18:1-35: Non-exhaustive patterns in Just eq
=====================================
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'])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce726cd2a3182006999c57eff73368ab9a4f7c60
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ce726cd2a3182006999c57eff73368ab9a4f7c60
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221108/1aa7d286/attachment-0001.html>
More information about the ghc-commits
mailing list