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 (but not
`newtype` declarations), either ordinary algebraic data types or GADTs,
preceded by `type`, with the following restrictions:
(R0) 'data' decls only, not 'newtype' decls. This is checked by
the parser.
(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.
(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.
(R5) There are no deriving clauses.
The data constructors of a `type data` declaration obey the following
Core invariant:
(I1) The data constructors of a `type data` declaration may be mentioned in
/types/, but never in /terms/ or the /pattern of a case alternative/.
Wrinkles:
(W0) Wrappers. The data constructor of a `type data` declaration has a worker
(like every data constructor) but does /not/ have a wrapper. Wrappers
only make sense for value-level data constructors. Indeed, the worker Id
is never used (invariant (I1)), so it barely makes sense to talk about
the worker. A `type data` constructor only shows up in types, where it
appears as a TyCon, specifically a PromotedDataCon -- no Id in sight.
See #24620 for an example of what happens if you accidentally include
a wrapper.
See `wrapped_reqd` in GHC.Types.Id.Make.mkDataConRep` for the place where
this check is implemented.
This specifically includes `type data` declarations implemented as GADTs,
such as this example from #22948:
type data T a where
A :: T Int
B :: T a
If `T` were an ordinary `data` declaration, then `A` would have a wrapper
to account for the GADT-like equality in its return type. Because `T` is
declared as a `type data` declaration, however, the wrapper is omitted.
(W1) To prevent users from conjuring up `type data` values at the term level,
we disallow using the tagToEnum# function on a type headed by a `type
data` type. For instance, GHC will reject this code:
type data Letter = A | B | C
f :: Letter
f = tagToEnum# 0#
See `GHC.Tc.Gen.App.checkTagToEnum`, specifically `check_enumeration`.
(W2) Although `type data` data constructors do not exist at the value level,
it is still possible to match on a value whose type is headed by a `type data`
type constructor, such as this example from #22964:
type data T a where
A :: T Int
B :: T a
f :: T a -> ()
f x = case x of {}
And yet we must guarantee invariant (I1). This has three consequences:
(W2a) During checking the coverage of `f`'s pattern matches, we treat `T`
as if it were an empty data type so that GHC does not warn the user
to match against `A` or `B`. (Otherwise, you end up with the bug
reported in #22964.) See GHC.HsToCore.Pmc.Solver.vanillaCompleteMatchTC.
(W2b) In `GHC.Core.Utils.refineDataAlt`, do /not/ fill in the DEFAULT case
with the data constructor, else (I1) is violated. See GHC.Core.Utils
Note [Refine DEFAULT case alternatives] Exception 2
(W2c) In `GHC.Core.Opt.ConstantFold.caseRules`, we do not want to transform
case dataToTagLarge# x of t -> blah
into
case x of { A -> ...; B -> .. }
because again that conjures up the type-level-only data constructors
`A` and `B` in a pattern, violating (I1) (#23023).
So we check for "type data" TyCons before applying this
transformation. (In practice, this doesn't matter because
we also refuse to solve DataToTag instances at types
corresponding to type data declarations. See rule C1 from
Note [DataToTag overview] in GHC.Tc.Instance.Class.)
The main parts of the implementation are:
* The parser recognizes `type data` (but not `type newtype`); this ensures (R0).
* 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
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 (`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 (a `TyThing`) for each constructor
(`Zero` and `Succ` in our example) is
- just an `ATyCon` for the promoted type constructor,
- not the bundle (`ADataCon` for the data con, `AnId` for the work id,
wrap id) required for a normal data constructor
See 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.isBoxedDataTyCon 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.
* The Template Haskell `Dec` type has an constructor `TypeDataD` for
`type data` declarations. When these are converted back to Hs types
in a splice, the constructors are placed in the TcCls namespace.