Implement the UnliftedDatatypes extension

GHC Proposal: 0265-unlifted-datatypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265
Issues: https://gitlab.haskell.org/ghc/ghc/-/issues/19523
Implementation Details: Note [Implementation of UnliftedDatatypes]

This patch introduces the `UnliftedDatatypes` extension. When this extension is
enabled, GHC relaxes the restrictions around what result kinds are allowed in
data declarations. This allows data types for which an unlifted or
levity-polymorphic result kind is inferred.

The most significant changes are in `GHC.Tc.TyCl`, where
`Note [Implementation of UnliftedDatatypes]` describes the details of the
implementation.

Fixes #19523.

2 files changed, 113 insertions, 4 deletions

diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index 4fdf6b070b..10677b5327 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -13,6 +13,7 @@ Language
   <https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__
   (Serrano et al, ICFP 2020).  More information here: :ref:`impredicative-polymorphism`.
   This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension.
+
 * The first stage of the `Pointer Rep Proposal`_ has been implemented. All
   boxed types, both lifted and unlifted, now have representation kinds of
   the shape ``BoxedRep r``. Code that references ``LiftedRep`` and ``UnliftedRep``
@@ -20,6 +21,24 @@ Language
 
 .. _Pointer Rep Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0203-pointer-rep.rst
 
+* :extension:`UnliftedDatatypes`: The `Unlifted Datatypes Proposal`_ has been
+  implemented. That means GHC Haskell now offers a way to define algebraic
+  data types with strict semantics like in OCaml or Idris! The distinction to
+  ordinary lifted data types is made in the kind system: Unlifted data types
+  live in kind ``TYPE (BoxedRep Unlifted)``. :extension:`UnliftedDatatypes`
+  allows giving data declarations such result kinds, such as in the following
+  example with the help of :extension:`StandaloneKindSignatures`: ::
+
+    type IntSet :: UnliftedType -- type UnliftedType = TYPE (BoxedRep Unlifted)
+    data IntSet = Branch IntSet !Int IntSet | Leaf
+
+  See :extension:`UnliftedDatatypes` for what other declarations are
+  possible. Slight caveat: Most functions in ``base`` (including ``$``)
+  are not levity-polymorphic (yet) and hence won't work with unlifted
+  data types.
+
+.. _Unlifted Datatypes Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-datatypes.rst
+
 * Kind inference for data/newtype instance declarations is slightly
   more restrictive than before.  See the user manual :ref:`kind-inference-data-family-instances`.
   This is a breaking change, albeit a fairly obscure one that corrects a specification bug.
diff --git a/docs/users_guide/exts/primitives.rst b/docs/users_guide/exts/primitives.rst
index 9e82852391..80041dd6ad 100644
--- a/docs/users_guide/exts/primitives.rst
+++ b/docs/users_guide/exts/primitives.rst
@@ -70,16 +70,16 @@ Unboxed type kinds
 ------------------
 
 Because unboxed types are represented without the use of pointers, we
-cannot store them in a polymorphic datatype.
+cannot store them in a polymorphic data type.
 For example, the ``Just`` node
 of ``Just 42#`` would have to be different from the ``Just`` node of
 ``Just 42``; the former stores an integer directly, while the latter
 stores a pointer. GHC currently does not support this variety of ``Just``
-nodes (nor for any other datatype). Accordingly, the *kind* of an unboxed
+nodes (nor for any other data type). Accordingly, the *kind* of an unboxed
 type is different from the kind of a boxed type.
 
 The Haskell Report describes that ``*`` (spelled ``Type`` and imported from
-``Data.Kind`` in the GHC dialect of Haskell) is the kind of ordinary datatypes,
+``Data.Kind`` in the GHC dialect of Haskell) is the kind of ordinary data types,
 such as ``Int``. Furthermore, type constructors can have kinds with arrows; for
 example, ``Maybe`` has kind ``Type -> Type``. Unboxed types have a kind that
 specifies their runtime representation. For example, the type ``Int#`` has kind
@@ -308,7 +308,7 @@ Unlifted Newtypes
 GHC implements an :extension:`UnliftedNewtypes` extension as specified in
 `this GHC proposal <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst>`_.
 :extension:`UnliftedNewtypes` relaxes the restrictions around what types can appear inside
-of a `newtype`. For example, the type ::
+of a ``newtype``. For example, the type ::
 
     newtype A = MkA Int#
 
@@ -368,3 +368,93 @@ This extension impacts the determination of whether or not a newtype has
 a Complete User-Specified Kind Signature (CUSK). The exact impact is specified
 `the section on CUSKs <#complete-kind-signatures>`__.
 
+Unlifted Datatypes
+------------------
+
+.. extension:: UnliftedDatatypes
+    :shortdesc: Enable unlifted data types.
+
+    :implies: :extension:`DataKinds`, :extension:`StandaloneKindSignatures`
+    :since: 9.2.1
+
+    Enable the declaration of data types with unlifted or levity-polymorphic
+    result kind.
+
+GHC implements the :extension:`UnliftedDatatypes` extension as specified in
+`this GHC proposal <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-data types.rst>`_.
+:extension:`UnliftedDatatypes` relaxes the restrictions around what result kinds
+are allowed in data declarations. For example, the type ::
+
+  data UList a :: UnliftedType where
+    UCons :: a -> UList a -> UList a
+    UNil :: UList a
+
+defines a list type that lives in kind ``UnliftedType``
+(e.g., ``TYPE (BoxedRep Unlifted)``). As such, each occurrence of a term of that
+type is assumed to be evaluated (and the compiler makes sure that is indeed the
+case). In other words: Unlifted data types behave like data types in strict
+languages such as OCaml or Idris. However unlike :extension:`StrictData`,
+this extension will not change whether the fields of a (perhaps unlifted)
+data type are strict or lazy. For example, ``UCons`` is lazy in its first
+argument as its field has kind ``Type``.
+
+The fact that unlifted types are always evaluated allows GHC to elide
+evaluatedness checks at runtime. See the Motivation section of the proposal
+for how this can improve performance for some programs.
+
+The above data declaration in GADT syntax correctly suggests that unlifted
+data types are compatible with the full GADT feature set. Somewhat conversely,
+you can also declare unlifted data types in Haskell98 syntax, which requires you
+to specify the result kind via :extension:`StandaloneKindSignatures`: ::
+
+  type UList :: Type -> UnliftedType
+  data UList a = UCons a (UList a) | UNil
+
+You may even declare levity-polymorphic data types: ::
+
+  type PEither :: Type -> Type -> TYPE (BoxedRep l)
+  data PEither l r = PLeft l | PRight r
+
+  f :: PEither @Unlifted Int Bool -> Bool
+  f (PRight b) = b
+  f _          = False
+
+While ``f`` above could reasonably be levity-polymorphic (as it evaluates its
+argument either way), GHC currently disallows the more general type
+``PEither @l Int Bool -> Bool``. This is a consequence of the
+`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__,
+
+Due to `ticket 19487 <https://gitlab.haskell.org/ghc/ghc/-/issues/19487>`, it's
+currently not possible to declare levity-polymorphic data types with nullary
+data constructors. There's a workaround, though: ::
+
+  type T :: TYPE (BoxedRep l)
+  data T where
+    MkT :: forall l. (() :: Constraint) => T @l
+
+The use of ``=>`` makes the type of ``MkT`` lifted.
+If you want a zero-runtime-cost alternative, use ``MkT :: Proxy# () -> T @l``
+instead and bear with the additional ``proxy#`` argument at construction sites.
+
+This extension also relaxes some of the restrictions around data family
+instances. In particular, :extension:`UnliftedDatatypes` permits a
+``data instance`` to be given a return kind that unifies with
+``TYPE (BoxedRep l)``, not just ``Type``. For example, the following ``data
+instance`` declarations would be permitted: ::
+
+  data family F a :: UnliftedType
+  data instance F Int = FInt
+
+  data family G a :: TYPE (BoxedRep l)
+  data instance G Int = GInt Int -- defaults to Type
+  data instance G Bool :: UnliftedType where
+    GBool :: Bool -> G Bool
+  data instance G Char :: Type where
+    GChar :: Char -> G Char
+  data instance G Double :: forall l. TYPE (BoxedRep l) where
+    GDouble :: Int -> G @l Double
+
+It is worth noting that :extension:`UnliftedDatatypes` is *not* required to give
+the data families themselves return kinds involving ``TYPE``, such as the
+``G`` example above. The extension is only required for ``data instance``
+declarations, such as ``FInt`` and ``GBool`` above.