Implement the -XUnliftedNewtypes extension.

GHC Proposal: 0013-unlifted-newtypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
Issues: #15219, #1311, #13595, #15883
Implementation Details:
  Note [Implementation of UnliftedNewtypes]
  Note [Unifying data family kinds]
  Note [Compulsory newtype unfolding]

This patch introduces the -XUnliftedNewtypes extension. When this
extension is enabled, GHC drops the restriction that the field in
a newtype must be of kind (TYPE 'LiftedRep). This allows types
like Int# and ByteArray# to be used in a newtype. Additionally,
coerce is made levity-polymorphic so that it can be used with
newtypes over unlifted types.

The bulk of the changes are in TcTyClsDecls.hs. With -XUnliftedNewtypes,
getInitialKind is more liberal, introducing a unification variable to
return the kind (TYPE r0) rather than just returning (TYPE 'LiftedRep).
When kind-checking a data constructor with kcConDecl, we attempt to
unify the kind of a newtype with the kind of its field's type. When
typechecking a data declaration with tcTyClDecl, we again perform a
unification. See the implementation note for more on this.

Co-authored-by: Richard Eisenberg <rae@richarde.dev>

1 files changed, 91 insertions, 0 deletions

diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index fdc3b2cafa..36e29c5253 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -178,6 +178,10 @@ There are some restrictions on the use of primitive types:
 
          newtype A = MkA Int#
 
+   However, this restriction can be relaxed by enabling
+   :extension:`-XUnliftedNewtypes`.  The `section on unlifted newtypes
+   <#unlifted-newtypes>`__ details the behavior of such types.
+
 -  You cannot bind a variable with an unboxed type in a *top-level*
    binding.
 
@@ -359,6 +363,77 @@ layout for a sum type works like this:
   as the ``Bool``-like ``(# (# #) | (# #) #)``, the unboxed sum layout only
   has an ``Int32`` tag field (i.e., the whole thing is represented by an integer).
 
+.. _unlifted-newtypes:
+
+Unlifted Newtypes
+-----------------
+
+.. extension:: UnliftedNewtypes
+    :shortdesc: Enable unlifted newtypes.
+
+    :since: 8.10.1
+
+    Enable the use of newtypes over types with non-lifted runtime representations.
+
+``-XUnliftedNewtypes`` relaxes the restrictions around what types can appear inside
+of a `newtype`. For example, the type ::
+
+    newtype A = MkA Int#
+
+is accepted when this extension is enabled. This creates a type
+``A :: TYPE 'IntRep`` and a data constructor ``MkA :: Int# -> A``.
+Although the kind of ``A`` is inferred by GHC, there is nothing visually
+distictive about this type that indicated that is it not of kind ``Type``
+like newtypes typically are. `GADTSyntax <#gadt-style>`__ can be used to
+provide a kind signature for additional clarity ::
+
+    newtype A :: TYPE 'IntRep where
+      MkA :: Int# -> A
+
+The ``Coercible`` machinery works with unlifted newtypes just like it does with
+lifted types. In either of the equivalent formulations of ``A`` given above,
+users would additionally have access to a coercion between ``A`` and ``Int#``.
+
+As a consequence of the
+`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__,
+levity-polymorphic fields are disallowed in data constructors
+of data types declared using ``data``. However, since ``newtype`` data
+constructor application is implemented as a coercion instead of as function
+application, this restriction does not apply to the field inside a ``newtype``
+data constructor. Thus, the type checker accepts ::
+
+    newtype Identity# :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+      MkIdentity# :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity# a
+
+And with `UnboxedSums <#unboxed-sums>`__ enabled ::
+
+    newtype Maybe# :: forall (r :: RuntimeRep). TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where
+      MkMaybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a
+
+This extension also relaxes some of the restrictions around data families.
+It must be enabled in modules where either of the following occur:
+
+- A data family is declared with a kind other than ``Type``. Both ``Foo``
+  and ``Bar``, defined below, fall into this category:
+  ::
+     class Foo a where
+       data FooKey a :: TYPE 'IntRep
+     class Bar (r :: RuntimeRep) where
+       data BarType r :: TYPE r
+
+- A ``newtype instance`` is written with a kind other than ``Type``. The
+  following instances of ``Foo`` and ``Bar`` as defined above fall into
+  this category.
+  ::
+     instance Foo Bool where
+       newtype FooKey Bool = FooKeyBoolC Int#
+     instance Bar 'WordRep where
+       newtype BarType 'WordRep = BarTypeWordRepC Word#
+
+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>`__.
+
 .. _syntax-extns:
 
 Syntactic extensions
@@ -9097,6 +9172,20 @@ signature" for a type constructor? These are the forms:
      data T2 :: forall k. k -> Type  -- CUSK: `k` is bound explicitly
      data T3 :: forall (k :: Type). k -> Type   -- still a CUSK
 
+-  For a newtype, the rules are the same as they are for a data type
+   unless `UnliftedNewtypes <#unboxed-newtypes>`__ is enabled.
+   With `UnliftedNewtypes <#unboxed-newtypes>`__, the type constructor
+   only has a CUSK if a kind signature is present. As with a datatype
+   with a top-level ``::``, all kind variables must introduced after
+   the ``::`` must be explicitly quantified ::
+
+       {-# LANGUAGE UnliftedNewtypes #-}
+       newtype N1 where                 -- No; missing kind signature
+       newtype N2 :: TYPE 'IntRep where -- Yes; kind signature present
+       newtype N3 (a :: Type) where     -- No; missing kind signature
+       newtype N4 :: k -> Type where    -- No; `k` is not explicitly quantified
+       newtype N5 :: forall (k :: Type). k -> Type where -- Yes; good signature
+
 -  For a class, every type variable must be annotated with a kind.
 
 -  For a type synonym, every type variable and the result type must all
@@ -9617,6 +9706,8 @@ thus say that ``->`` has type
 ``TYPE r1 -> TYPE r2 -> TYPE 'LiftedRep``. The result is always lifted
 because all functions are lifted in GHC.
 
+.. _levity-polymorphic-restrictions:
+
 No levity-polymorphic variables or arguments
 --------------------------------------------