Implement the UnliftedDatatypes extensionwip/unlifted-data

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.

39 files changed, 719 insertions, 163 deletions

diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs
index 3b928c801f..321b20e877 100644
--- a/compiler/GHC/Builtin/Types.hs
+++ b/compiler/GHC/Builtin/Types.hs
@@ -1485,22 +1485,25 @@ runtimeRepTy = mkTyConTy runtimeRepTyCon
 
 -- Type synonyms; see Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim
 -- and Note [Prefer Type over TYPE 'LiftedRep] in GHC.Core.TyCo.Rep.
--- type Type = TYPE ('BoxedRep 'Lifted)
--- type LiftedRep = 'BoxedRep 'Lifted
+--
+-- @type Type = TYPE ('BoxedRep 'Lifted)@
 liftedTypeKindTyCon :: TyCon
 liftedTypeKindTyCon =
     buildSynTyCon liftedTypeKindTyConName [] liftedTypeKind [] rhs
   where rhs = TyCoRep.TyConApp tYPETyCon [mkTyConApp liftedRepTyCon []]
 
+-- | @type UnliftedType = TYPE ('BoxedRep 'Unlifted)@
 unliftedTypeKindTyCon :: TyCon
 unliftedTypeKindTyCon =
     buildSynTyCon unliftedTypeKindTyConName [] liftedTypeKind [] rhs
   where rhs = TyCoRep.TyConApp tYPETyCon [mkTyConApp unliftedRepTyCon []]
 
+-- | @type LiftedRep = 'BoxedRep 'Lifted@
 liftedRepTyCon :: TyCon
 liftedRepTyCon = buildSynTyCon
   liftedRepTyConName [] runtimeRepTy [] liftedRepTy
 
+-- | @type UnliftedRep = 'BoxedRep 'Unlifted@
 unliftedRepTyCon :: TyCon
 unliftedRepTyCon = buildSynTyCon
   unliftedRepTyConName [] runtimeRepTy [] unliftedRepTy
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 40de306802..89914e967f 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -635,6 +635,7 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty
        ; checkL ( isJoinId binder
                || not (isUnliftedType binder_ty)
                || (isNonRec rec_flag && exprOkForSpeculation rhs)
+               || isDataConWorkId binder || isDataConWrapId binder -- until #17521 is fixed
                || exprIsTickedString rhs)
            (badBndrTyMsg binder (text "unlifted"))
 
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index 4b517027da..87b7336a76 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -1480,7 +1480,7 @@ data PrimRep
   | FloatRep
   | DoubleRep
   | VecRep Int PrimElemRep  -- ^ A vector
-  deriving( Show )
+  deriving( Eq, Show )
 
 data PrimElemRep
   = Int8ElemRep
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index b0aa10c4cd..5ed621d404 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -120,10 +120,10 @@ module GHC.Core.Type (
 
         -- *** Levity and boxity
         isLiftedType_maybe,
-        isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
-        isLiftedRuntimeRep, isUnliftedRuntimeRep,
+        isLiftedTypeKind, isUnliftedTypeKind, isBoxedTypeKind, pickyIsLiftedTypeKind,
+        isLiftedRuntimeRep, isUnliftedRuntimeRep, isBoxedRuntimeRep,
         isLiftedLevity, isUnliftedLevity,
-        isUnliftedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType,
+        isUnliftedType, isBoxedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType,
         isAlgType, isDataFamilyAppType,
         isPrimitiveType, isStrictType,
         isLevityTy, isLevityVar,
@@ -146,10 +146,10 @@ module GHC.Core.Type (
         -- ** Finding the kind of a type
         typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly,
         tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
-        tcIsRuntimeTypeKind,
+        tcIsBoxedTypeKind, tcIsRuntimeTypeKind,
 
         -- ** Common Kind
-        liftedTypeKind,
+        liftedTypeKind, unliftedTypeKind,
 
         -- * Type free variables
         tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
@@ -294,26 +294,29 @@ import Control.Monad    ( guard )
 -- $type_classification
 -- #type_classification#
 --
--- Types are one of:
+-- Types are any, but at least one, of:
 --
--- [Unboxed]            Iff its representation is other than a pointer
---                      Unboxed types are also unlifted.
+-- [Boxed]              Iff its representation is a pointer to an object on the
+--                      GC'd heap. Operationally, heap objects can be entered as
+--                      a means of evaluation.
 --
--- [Lifted]             Iff it has bottom as an element.
---                      Closures always have lifted types: i.e. any
---                      let-bound identifier in Core must have a lifted
---                      type. Operationally, a lifted object is one that
---                      can be entered.
+-- [Lifted]             Iff it has bottom as an element: An instance of a
+--                      lifted type might diverge when evaluated.
+--                      GHC Haskell's unboxed types are unlifted.
+--                      An unboxed, but lifted type is not very useful.
+--                      (Example: A byte-represented type, where evaluating 0xff
+--                      computes the 12345678th collatz number modulo 0xff.)
 --                      Only lifted types may be unified with a type variable.
 --
 -- [Algebraic]          Iff it is a type with one or more constructors, whether
 --                      declared with @data@ or @newtype@.
 --                      An algebraic type is one that can be deconstructed
---                      with a case expression. This is /not/ the same as
---                      lifted types, because we also include unboxed
---                      tuples in this classification.
+--                      with a case expression. There are algebraic types that
+--                      are not lifted types, like unlifted data types or
+--                      unboxed tuples.
 --
 -- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
+--                      There are also /unlifted/ data types.
 --
 -- [Primitive]          Iff it is a built-in type that can't be expressed in Haskell.
 --
@@ -473,8 +476,8 @@ coreFullView ty@(TyConApp tc _)
 coreFullView ty = ty
 {-# INLINE coreFullView #-}
 
-{- Note [Inlining coreView] in GHC.Core.Type
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Inlining coreView]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It is very common to have a function
 
   f :: Type -> ...
@@ -585,6 +588,18 @@ expandTypeSynonyms ty
       -- order of a coercion)
     go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst
 
+-- | An INLINE helper for function such as 'kindRep_maybe' below.
+--
+-- @isTyConKeyApp_maybe key ty@ returns @Just tys@ iff
+-- the type @ty = T tys@, where T's unique = key
+isTyConKeyApp_maybe :: Unique -> Type -> Maybe [Type]
+isTyConKeyApp_maybe key ty
+  | TyConApp tc args <- coreFullView ty
+  , tc `hasKey` key
+  = Just args
+  | otherwise
+  = Nothing
+{-# INLINE isTyConKeyApp_maybe #-}
 
 -- | Extract the RuntimeRep classifier of a type from its kind. For example,
 -- @kindRep * = LiftedRep@; Panics if this is not possible.
@@ -600,9 +615,18 @@ kindRep k = case kindRep_maybe k of
 -- Treats * and Constraint as the same
 kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
 kindRep_maybe kind
-  | TyConApp tc [arg] <- coreFullView kind
-  , tc `hasKey` tYPETyConKey    = Just arg
-  | otherwise                   = Nothing
+  | Just [arg] <- isTyConKeyApp_maybe tYPETyConKey kind = Just arg
+  | otherwise                                           = Nothing
+
+-- | Returns True if the kind classifies types which are allocated on
+-- the GC'd heap and False otherwise. Note that this returns False for
+-- levity-polymorphic kinds, which may be specialized to a kind that
+-- classifies AddrRep or even unboxed kinds.
+isBoxedTypeKind :: Kind -> Bool
+isBoxedTypeKind kind
+  = case kindRep_maybe kind of
+      Just rep -> isBoxedRuntimeRep rep
+      Nothing  -> False
 
 -- | This version considers Constraint to be the same as *. Returns True
 -- if the argument is equivalent to Type/Constraint and False otherwise.
@@ -636,54 +660,49 @@ pickyIsLiftedTypeKind kind
   , tc `hasKey` liftedTypeKindTyConKey = True
   | otherwise                          = False
 
+-- | Returns True if the kind classifies unlifted types (like 'Int#') and False
+-- otherwise. Note that this returns False for levity-polymorphic kinds, which
+-- may be specialized to a kind that classifies unlifted types.
+isUnliftedTypeKind :: Kind -> Bool
+isUnliftedTypeKind kind
+  = case kindRep_maybe kind of
+      Just rep -> isUnliftedRuntimeRep rep
+      Nothing  -> False
+
+-- | See 'isBoxedRuntimeRep_maybe'.
+isBoxedRuntimeRep :: Type -> Bool
+isBoxedRuntimeRep rep = isJust (isBoxedRuntimeRep_maybe rep)
+
+-- | `isBoxedRuntimeRep_maybe (rep :: RuntimeRep)` returns `Just lev` if `rep`
+-- expands to `Boxed lev` and returns `Nothing` otherwise.
+--
+-- Types with this runtime rep are represented by pointers on the GC'd heap.
+isBoxedRuntimeRep_maybe :: Type -> Maybe Type
+isBoxedRuntimeRep_maybe rep
+  | Just [lev] <- isTyConKeyApp_maybe boxedRepDataConKey rep
+  = Just lev
+  | otherwise
+  = Nothing
+
 isLiftedRuntimeRep :: Type -> Bool
 -- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep
 -- False of type variables (a :: RuntimeRep)
 --   and of other reps e.g. (IntRep :: RuntimeRep)
 isLiftedRuntimeRep rep
-  | Just rep' <- coreView rep
-  = isLiftedRuntimeRep rep'
-  | TyConApp rr_tc [rr_arg] <- rep
-  , rr_tc `hasKey` boxedRepDataConKey
-  = isLiftedLevity rr_arg
+  | Just [lev] <- isTyConKeyApp_maybe boxedRepDataConKey rep
+  = isLiftedLevity lev
   | otherwise
   = False
 
-isLiftedLevity :: Type -> Bool
-isLiftedLevity lev
-  | Just lev' <- coreView lev          = isLiftedLevity lev'
-  | TyConApp lev_tc lev_args <- lev
-  , lev_tc `hasKey` liftedDataConKey
-  = ASSERT( null lev_args ) True
-  | otherwise                          = False
-
-isUnliftedLevity :: Type -> Bool
-isUnliftedLevity lev
-  | Just lev' <- coreView lev          = isUnliftedLevity lev'
-  | TyConApp lev_tc lev_args <- lev
-  , lev_tc `hasKey` unliftedDataConKey
-  = ASSERT( null lev_args ) True
-  | otherwise                          = False
-
--- | Returns True if the kind classifies unlifted types and False otherwise.
--- Note that this returns False for levity-polymorphic kinds, which may
--- be specialized to a kind that classifies unlifted types.
-isUnliftedTypeKind :: Kind -> Bool
-isUnliftedTypeKind kind
-  = case kindRep_maybe kind of
-      Just rep -> isUnliftedRuntimeRep rep
-      Nothing  -> False
-
 isUnliftedRuntimeRep :: Type -> Bool
+-- PRECONDITION: The type has kind RuntimeRep
 -- True of definitely-unlifted RuntimeReps
 -- False of           (LiftedRep :: RuntimeRep)
 --   and of variables (a :: RuntimeRep)
 isUnliftedRuntimeRep rep
-  | Just rep' <- coreView rep   -- NB: args might be non-empty
-                                --     e.g. TupleRep [r1, .., rn]
-  = isUnliftedRuntimeRep rep'
-isUnliftedRuntimeRep (TyConApp rr_tc args)
-  | isPromotedDataCon rr_tc =
+  | TyConApp rr_tc args <- coreFullView rep -- NB: args might be non-empty
+                                            --     e.g. TupleRep [r1, .., rn]
+  , isPromotedDataCon rr_tc =
       -- NB: args might be non-empty e.g. TupleRep [r1, .., rn]
       if (rr_tc `hasKey` boxedRepDataConKey)
         then case args of
@@ -696,21 +715,28 @@ isUnliftedRuntimeRep (TyConApp rr_tc args)
         -- hence the isPromotedDataCon rr_tc
 isUnliftedRuntimeRep _ = False
 
--- | Is this the type 'RuntimeRep'?
-isRuntimeRepTy :: Type -> Bool
-isRuntimeRepTy ty
-  | Just ty' <- coreView ty        = isRuntimeRepTy ty'
-  | TyConApp tc args <- ty
-  , tc `hasKey` runtimeRepTyConKey = ASSERT( null args ) True
-  | otherwise                      = False
+-- | An INLINE helper for function such as 'isLiftedRuntimeRep' below.
+isNullaryTyConKeyApp :: Unique -> Type -> Bool
+isNullaryTyConKeyApp key ty
+  | Just args <- isTyConKeyApp_maybe key ty
+  = ASSERT( null args ) True
+  | otherwise
+  = False
+{-# INLINE isNullaryTyConKeyApp #-}
+
+isLiftedLevity :: Type -> Bool
+isLiftedLevity = isNullaryTyConKeyApp liftedDataConKey
+
+isUnliftedLevity :: Type -> Bool
+isUnliftedLevity = isNullaryTyConKeyApp unliftedDataConKey
 
 -- | Is this the type 'Levity'?
 isLevityTy :: Type -> Bool
-isLevityTy lev
-  | Just lev' <- coreView lev      = isLevityTy lev'
-  | TyConApp tc args <- coreFullView lev
-  , tc `hasKey` levityTyConKey     = ASSERT( null args ) True
-  | otherwise                      = False
+isLevityTy = isNullaryTyConKeyApp levityTyConKey
+
+-- | Is this the type 'RuntimeRep'?
+isRuntimeRepTy :: Type -> Bool
+isRuntimeRepTy = isNullaryTyConKeyApp runtimeRepTyConKey
 
 -- | Is a tyvar of type 'RuntimeRep'?
 isRuntimeRepVar :: TyVar -> Bool
@@ -722,9 +748,7 @@ isLevityVar = isLevityTy . tyVarKind
 
 -- | Is this the type 'Multiplicity'?
 isMultiplicityTy :: Type -> Bool
-isMultiplicityTy ty
-  | TyConApp tc [] <- coreFullView ty = tc `hasKey` multiplicityTyConKey
-  | otherwise                         = False
+isMultiplicityTy  = isNullaryTyConKeyApp multiplicityTyConKey
 
 -- | Is a tyvar of type 'Multiplicity'?
 isMultiplicityVar :: TyVar -> Bool
@@ -2219,6 +2243,13 @@ mightBeUnliftedType ty
       Just is_lifted -> not is_lifted
       Nothing -> True
 
+-- | See "Type#type_classification" for what a boxed type is.
+-- Panics on levity polymorphic types; See 'mightBeUnliftedType' for
+-- a more approximate predicate that behaves better in the presence of
+-- levity polymorphism.
+isBoxedType :: Type -> Bool
+isBoxedType ty = isBoxedRuntimeRep (getRuntimeRep ty)
+
 -- | Is this a type of kind RuntimeRep? (e.g. LiftedRep)
 isRuntimeRepKindedTy :: Type -> Bool
 isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
@@ -2799,28 +2830,40 @@ tcIsConstraintKind ty
   | otherwise
   = False
 
--- | Is this kind equivalent to @*@?
+-- | Like 'kindRep_maybe', but considers 'Constraint' to be distinct
+-- from 'Type'. For a version that treats them as the same type, see
+-- 'kindRep_maybe'.
+tcKindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
+tcKindRep_maybe kind
+  | Just (tc, [arg]) <- tcSplitTyConApp_maybe kind    -- Note: tcSplit here
+  , tc `hasKey` tYPETyConKey    = Just arg
+  | otherwise                   = Nothing
+
+-- | Is this kind equivalent to 'Type'?
 --
--- This considers 'Constraint' to be distinct from @*@. For a version that
+-- This considers 'Constraint' to be distinct from 'Type'. For a version that
 -- treats them as the same type, see 'isLiftedTypeKind'.
 tcIsLiftedTypeKind :: Kind -> Bool
-tcIsLiftedTypeKind ty
-  | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty    -- Note: tcSplit here
-  , tc `hasKey` tYPETyConKey
-  = isLiftedRuntimeRep arg
-  | otherwise
-  = False
+tcIsLiftedTypeKind kind
+  = case tcKindRep_maybe kind of
+      Just rep -> isLiftedRuntimeRep rep
+      Nothing  -> False
+
+-- | Is this kind equivalent to @TYPE (BoxedRep l)@ for some @l :: Levity@?
+--
+-- This considers 'Constraint' to be distinct from 'Type'. For a version that
+-- treats them as the same type, see 'isLiftedTypeKind'.
+tcIsBoxedTypeKind :: Kind -> Bool
+tcIsBoxedTypeKind kind
+  = case tcKindRep_maybe kind of
+      Just rep -> isBoxedRuntimeRep rep
+      Nothing  -> False
 
 -- | Is this kind equivalent to @TYPE r@ (for some unknown r)?
 --
 -- This considers 'Constraint' to be distinct from @*@.
 tcIsRuntimeTypeKind :: Kind -> Bool
-tcIsRuntimeTypeKind ty
-  | Just (tc, _) <- tcSplitTyConApp_maybe ty    -- Note: tcSplit here
-  , tc `hasKey` tYPETyConKey
-  = True
-  | otherwise
-  = False
+tcIsRuntimeTypeKind kind = isJust (tcKindRep_maybe kind)
 
 tcReturnsConstraintKind :: Kind -> Bool
 -- True <=> the Kind ultimately returns a Constraint
diff --git a/compiler/GHC/CoreToStg.hs b/compiler/GHC/CoreToStg.hs
index 1bcf5bdfe9..bfe9a6c89b 100644
--- a/compiler/GHC/CoreToStg.hs
+++ b/compiler/GHC/CoreToStg.hs
@@ -484,15 +484,16 @@ mkStgAltType bndr alts
 
   | otherwise
   = case prim_reps of
-      [LiftedRep] -> case tyConAppTyCon_maybe (unwrapType bndr_ty) of
-        Just tc
-          | isAbstractTyCon tc -> look_for_better_tycon
-          | isAlgTyCon tc      -> AlgAlt tc
-          | otherwise          -> ASSERT2( _is_poly_alt_tycon tc, ppr tc )
-                                  PolyAlt
-        Nothing                -> PolyAlt
-      [unlifted] -> PrimAlt unlifted
-      not_unary  -> MultiValAlt (length not_unary)
+      [rep] | isGcPtrRep rep ->
+        case tyConAppTyCon_maybe (unwrapType bndr_ty) of
+          Just tc
+            | isAbstractTyCon tc -> look_for_better_tycon
+            | isAlgTyCon tc      -> AlgAlt tc
+            | otherwise          -> ASSERT2( _is_poly_alt_tycon tc, ppr tc )
+                                    PolyAlt
+          Nothing                -> PolyAlt
+      [non_gcd] -> PrimAlt non_gcd
+      not_unary -> MultiValAlt (length not_unary)
   where
    bndr_ty   = idType bndr
    prim_reps = typePrimRep bndr_ty
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 8b7ddd321d..000063eb82 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -3566,6 +3566,7 @@ xFlagsDeps = [
   flagSpec "UndecidableInstances"             LangExt.UndecidableInstances,
   flagSpec "UndecidableSuperClasses"          LangExt.UndecidableSuperClasses,
   flagSpec "UnicodeSyntax"                    LangExt.UnicodeSyntax,
+  flagSpec "UnliftedDatatypes"                LangExt.UnliftedDatatypes,
   flagSpec "UnliftedFFITypes"                 LangExt.UnliftedFFITypes,
   flagSpec "UnliftedNewtypes"                 LangExt.UnliftedNewtypes,
   flagSpec "ViewPatterns"                     LangExt.ViewPatterns
@@ -3749,6 +3750,10 @@ impliedXFlags
 
     , (LangExt.TemplateHaskell, turnOn, LangExt.TemplateHaskellQuotes)
     , (LangExt.Strict, turnOn, LangExt.StrictData)
+
+    -- The extensions needed to declare an H98 unlifted data type
+    , (LangExt.UnliftedDatatypes, turnOn, LangExt.DataKinds)
+    , (LangExt.UnliftedDatatypes, turnOn, LangExt.StandaloneKindSignatures)
   ]
 
 -- Note [When is StarIsType enabled]
diff --git a/compiler/GHC/Stg/Lint.hs b/compiler/GHC/Stg/Lint.hs
index bf52840f5c..1e12e9bab9 100644
--- a/compiler/GHC/Stg/Lint.hs
+++ b/compiler/GHC/Stg/Lint.hs
@@ -45,7 +45,7 @@ import GHC.Driver.Session
 import GHC.Data.Bag         ( Bag, emptyBag, isEmptyBag, snocBag, bagToList )
 import GHC.Types.Basic      ( TopLevelFlag(..), isTopLevel )
 import GHC.Types.CostCentre ( isCurrentCCS )
-import GHC.Types.Id         ( Id, idType, isJoinId, idName )
+import GHC.Types.Id
 import GHC.Types.Var.Set
 import GHC.Core.DataCon
 import GHC.Core             ( AltCon(..) )
@@ -134,8 +134,10 @@ lint_binds_help top_lvl (binder, rhs)
         lintStgRhs rhs
         opts <- getStgPprOpts
         -- Check binder doesn't have unlifted type or it's a join point
-        checkL (isJoinId binder || not (isUnliftedType (idType binder)))
-               (mkUnliftedTyMsg opts binder rhs)
+        checkL ( isJoinId binder
+              || not (isUnliftedType (idType binder))
+              || isDataConWorkId binder || isDataConWrapId binder) -- until #17521 is fixed
+          (mkUnliftedTyMsg opts binder rhs)
 
 -- | Top-level bindings can't inherit the cost centre stack from their
 -- (static) allocation site.
diff --git a/compiler/GHC/Stg/Syntax.hs b/compiler/GHC/Stg/Syntax.hs
index 185433100a..53e4b07c69 100644
--- a/compiler/GHC/Stg/Syntax.hs
+++ b/compiler/GHC/Stg/Syntax.hs
@@ -531,7 +531,7 @@ type GenStgAlt pass
      GenStgExpr pass) -- ...right-hand side.
 
 data AltType
-  = PolyAlt             -- Polymorphic (a lifted type variable)
+  = PolyAlt             -- Polymorphic (a boxed type variable, lifted or unlifted)
   | MultiValAlt Int     -- Multi value of this arity (unboxed tuple or sum)
                         -- the arity could indeed be 1 for unary unboxed tuple
                         -- or enum-like unboxed sums
diff --git a/compiler/GHC/StgToCmm/Env.hs b/compiler/GHC/StgToCmm/Env.hs
index 3ad42fd19d..ebfff0185f 100644
--- a/compiler/GHC/StgToCmm/Env.hs
+++ b/compiler/GHC/StgToCmm/Env.hs
@@ -136,12 +136,15 @@ getCgIdInfo id
           let name = idName id
         ; if isExternalName name then
               let ext_lbl
-                      | isUnliftedType (idType id) =
+                      | isBoxedType (idType id)
+                      = mkClosureLabel name $ idCafInfo id
+                      | isUnliftedType (idType id)
                           -- An unlifted external Id must refer to a top-level
                           -- string literal. See Note [Bytes label] in "GHC.Cmm.CLabel".
-                          ASSERT( idType id `eqType` addrPrimTy )
-                          mkBytesLabel name
-                      | otherwise = mkClosureLabel name $ idCafInfo id
+                      = ASSERT( idType id `eqType` addrPrimTy )
+                        mkBytesLabel name
+                      | otherwise
+                      = pprPanic "GHC.StgToCmm.Env: label not found" (ppr id <+> dcolon <+> ppr (idType id))
               in return $
                   litIdInfo platform id (mkLFImported id) (CmmLabel ext_lbl)
           else
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index cc82f30dbc..61b66f3919 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2908,9 +2908,9 @@ data ContextKind = TheKind Kind   -- ^ a specific kind
 
 -----------------------
 newExpectedKind :: ContextKind -> TcM Kind
-newExpectedKind (TheKind k) = return k
-newExpectedKind AnyKind     = newMetaKindVar
-newExpectedKind OpenKind    = newOpenTypeKind
+newExpectedKind (TheKind k)   = return k
+newExpectedKind AnyKind       = newMetaKindVar
+newExpectedKind OpenKind      = newOpenTypeKind
 
 -----------------------
 expectedKindInCtxt :: UserTypeCtxt -> ContextKind
@@ -3579,6 +3579,22 @@ data DataSort
   | DataInstanceSort NewOrData
   | DataFamilySort
 
+-- | Local helper type used in 'checkDataKindSig'.
+--
+-- Superficially similar to 'ContextKind', but it lacks 'AnyKind'
+-- and 'AnyBoxedKind', and instead of @'TheKind' liftedTypeKind@
+-- provides 'LiftedKind', which is much simpler to match on and
+-- handle in 'isAllowedDataResKind'.
+data AllowedDataResKind
+  = AnyTYPEKind
+  | AnyBoxedKind
+  | LiftedKind
+
+isAllowedDataResKind :: AllowedDataResKind -> Kind -> Bool
+isAllowedDataResKind AnyTYPEKind  kind = tcIsRuntimeTypeKind kind
+isAllowedDataResKind AnyBoxedKind kind = tcIsBoxedTypeKind kind
+isAllowedDataResKind LiftedKind   kind = tcIsLiftedTypeKind kind
+
 -- | Checks that the return kind in a data declaration's kind signature is
 -- permissible. There are three cases:
 --
@@ -3603,7 +3619,7 @@ checkDataKindSig :: DataSort -> Kind  -- any arguments in the kind are stripped
 checkDataKindSig data_sort kind
   = do { dflags <- getDynFlags
        ; traceTc "checkDataKindSig" (ppr kind)
-       ; checkTc (is_TYPE_or_Type dflags || is_kind_var)
+       ; checkTc (tYPE_ok dflags || is_kind_var)
                  (err_msg dflags) }
   where
     res_kind = snd (tcSplitPiTys kind)
@@ -3626,6 +3642,13 @@ checkDataKindSig data_sort kind
         DataInstanceSort new_or_data -> new_or_data == NewType
         DataFamilySort               -> False
 
+    is_datatype :: Bool
+    is_datatype =
+      case data_sort of
+        DataDeclSort     DataType -> True
+        DataInstanceSort DataType -> True
+        _                         -> False
+
     is_data_family :: Bool
     is_data_family =
       case data_sort of
@@ -3633,27 +3656,30 @@ checkDataKindSig data_sort kind
         DataInstanceSort{} -> False
         DataFamilySort     -> True
 
+    allowed_kind :: DynFlags -> AllowedDataResKind
+    allowed_kind dflags
+      | is_newtype && xopt LangExt.UnliftedNewtypes dflags
+        -- With UnliftedNewtypes, we allow kinds other than Type, but they
+        -- must still be of the form `TYPE r` since we don't want to accept
+        -- Constraint or Nat.
+        -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl.
+      = AnyTYPEKind
+      | is_data_family
+        -- If this is a `data family` declaration, we don't need to check if
+        -- UnliftedNewtypes is enabled, since data family declarations can
+        -- have return kind `TYPE r` unconditionally (#16827).
+      = AnyTYPEKind
+      | is_datatype && xopt LangExt.UnliftedDatatypes dflags
+        -- With UnliftedDatatypes, we allow kinds other than Type, but they
+        -- must still be of the form `TYPE (BoxedRep l)`, so that we don't
+        -- accept result kinds like `TYPE IntRep`.
+        -- See Note [Implementation of UnliftedDatatypes] in GHC.Tc.TyCl.
+      = AnyBoxedKind
+      | otherwise
+      = LiftedKind
+
     tYPE_ok :: DynFlags -> Bool
-    tYPE_ok dflags =
-         (is_newtype && xopt LangExt.UnliftedNewtypes dflags)
-           -- With UnliftedNewtypes, we allow kinds other than Type, but they
-           -- must still be of the form `TYPE r` since we don't want to accept
-           -- Constraint or Nat.
-           -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl.
-      || is_data_family
-           -- If this is a `data family` declaration, we don't need to check if
-           -- UnliftedNewtypes is enabled, since data family declarations can
-           -- have return kind `TYPE r` unconditionally (#16827).
-
-    is_TYPE :: Bool
-    is_TYPE = tcIsRuntimeTypeKind res_kind
-
-    is_Type :: Bool
-    is_Type = tcIsLiftedTypeKind res_kind
-
-    is_TYPE_or_Type :: DynFlags -> Bool
-    is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE
-                           | otherwise      = is_Type
+    tYPE_ok dflags = isAllowedDataResKind (allowed_kind dflags) res_kind
 
     -- In the particular case of a data family, permit a return kind of the
     -- form `:: k` (where `k` is a bare kind variable).
@@ -3661,17 +3687,32 @@ checkDataKindSig data_sort kind
     is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe res_kind)
                 | otherwise      = False
 
+    pp_allowed_kind dflags =
+      case allowed_kind dflags of
+        AnyTYPEKind  -> ppr tYPETyCon
+        AnyBoxedKind -> ppr boxedRepDataConTyCon
+        LiftedKind   -> ppr liftedTypeKind
+
     err_msg :: DynFlags -> SDoc
     err_msg dflags =
-      sep [ (sep [ pp_dec <+>
-                   text "has non-" <>
-                   (if tYPE_ok dflags then text "TYPE" else ppr liftedTypeKind)
-                 , (if is_data_family then text "and non-variable" else empty) <+>
-                   text "return kind" <+> quotes (ppr res_kind) ])
-          , if not (tYPE_ok dflags) && is_TYPE && is_newtype &&
-               not (xopt LangExt.UnliftedNewtypes dflags)
-            then text "Perhaps you intended to use UnliftedNewtypes"
-            else empty ]
+      sep [ sep [ pp_dec <+>
+                  text "has non-" <>
+                  pp_allowed_kind dflags
+                , (if is_data_family then text "and non-variable" else empty) <+>
+                  text "return kind" <+> quotes (ppr kind) ]
+          , ext_hint dflags ]
+
+    ext_hint dflags
+      | tcIsRuntimeTypeKind kind
+      , is_newtype
+      , not (xopt LangExt.UnliftedNewtypes dflags)
+      = text "Perhaps you intended to use UnliftedNewtypes"
+      | tcIsBoxedTypeKind kind
+      , is_datatype
+      , not (xopt LangExt.UnliftedDatatypes dflags)
+      = text "Perhaps you intended to use UnliftedDatatypes"
+      | otherwise
+      = empty
 
 -- | Checks that the result kind of a class is exactly `Constraint`, rejecting
 -- type synonyms and type families that reduce to `Constraint`. See #16826.
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index e1da82d3bb..ec8c2bb66e 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -945,7 +945,7 @@ Each forall'd type variable in a type or kind is one of
   * Specified: the argument can be inferred at call sites, but
     may be instantiated with visible type/kind application
 
-  * Inferred: the must be inferred at call sites; it
+  * Inferred: the argument must be inferred at call sites; it
     is unavailable for use with visible type/kind application.
 
 Why have Inferred at all? Because we just can't make user-facing
@@ -1115,7 +1115,7 @@ We do kind inference as follows:
   All this is very similar at the level of terms: see GHC.Tc.Gen.Bind
   Note [Quantified variables in partial type signatures]
 
-  But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon]
+  But there are some tricky corners: Note [Tricky scoping in generaliseTcTyCon]
 
 * Step 4.  Extend the type environment with a TcTyCon for S and T, now
   with their utterly-final polymorphic kinds (needed for recursive
@@ -1345,7 +1345,7 @@ getInitialKind strategy
         ; tc <- kcDeclHeader strategy name flav ktvs $
                 case m_sig of
                   Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig
-                  Nothing -> return $ dataDeclDefaultResultKind new_or_data
+                  Nothing   -> return $ dataDeclDefaultResultKind strategy new_or_data
         ; return [tc] }
 
 getInitialKind InitialKindInfer (FamDecl { tcdFam = decl })
@@ -1454,14 +1454,18 @@ have before standalone kind signatures:
 -}
 
 -- See Note [Data declaration default result kind]
-dataDeclDefaultResultKind :: NewOrData -> ContextKind
-dataDeclDefaultResultKind NewType  = OpenKind
-  -- See Note [Implementation of UnliftedNewtypes], point <Error Messages>.
-dataDeclDefaultResultKind DataType = TheKind liftedTypeKind
+dataDeclDefaultResultKind :: InitialKindStrategy ->  NewOrData -> ContextKind
+dataDeclDefaultResultKind strategy new_or_data
+  | NewType <- new_or_data
+  = OpenKind -- See Note [Implementation of UnliftedNewtypes], point <Error Messages>.
+  | DataType <- new_or_data
+  , InitialKindCheck (SAKS _) <- strategy
+  = OpenKind -- See Note [Implementation of UnliftedDatatypes]
+  | otherwise
+  = TheKind liftedTypeKind
 
 {- Note [Data declaration default result kind]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 When the user has not written an inline result kind annotation on a data
 declaration, we assume it to be 'Type'. That is, the following declarations
 D1 and D2 are considered equivalent:
@@ -1478,14 +1482,25 @@ accept D4:
   data D4 :: Type -> Type where
     MkD4 :: ... -> D4 param
 
-However, there's a twist: for newtypes, we must relax
-the assumed result kind to (TYPE r):
+However, there are two twists:
+
+  * For unlifted newtypes, we must relax the assumed result kind to (TYPE r):
+
+      newtype D5 where
+        MkD5 :: Int# -> D5
+
+    See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note
+    <Error Messages>.
+
+  * For unlifted datatypes, we must relax the assumed result kind to
+    (TYPE (BoxedRep l)) in the presence of a SAKS:
 
-  newtype D5 where
-    MkD5 :: Int# -> D5
+      type D6 :: Type -> TYPE (BoxedRep Unlifted)
+      data D6 a = MkD6 a
+
+    Otherwise, it would be impossible to declare unlifted data types in H98
+    syntax (which doesn't allow specification of a result kind).
 
-See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note
-<Error Messages>.
 -}
 
 ---------------------------------
@@ -2252,6 +2267,52 @@ the validity checker), that will not happen. But I cannot think of a non-contriv
 example that will notice this lack of inference, so it seems better to improve
 error messages than be able to infer this instantiation.
 
+Note [Implementation of UnliftedDatatypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Expected behavior of UnliftedDatatypes:
+
+* Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-datatypes.rst
+* Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265
+
+The implementation heavily leans on Note [Implementation of UnliftedNewtypes].
+
+In the frontend, the following tweaks have been made in the typechecker:
+
+* STEP 1: In the inferInitialKinds phase, newExpectedKind gives data type
+  constructors a result kind of `TYPE r` with a fresh unification variable
+  `r :: RuntimeRep` when there is a SAKS. (Same as for UnliftedNewtypes.)
+  Not needed with a CUSK, because it can't specify result kinds.
+  If there's a GADTSyntax result kind signature, we keep on using that kind.
+
+  Similarly, for data instances without a kind signature, we use
+  `TYPE r` as the result kind, to support the following code:
+
+    data family F a :: UnliftedType
+    data instance F Int = TInt
+
+  The ommission of a kind signature for `F` should not mean a result kind
+  of `Type` (and thus a kind error) here.
+
+* STEP 2: No change to kcTyClDecl.
+
+* STEP 3: In GHC.Tc.Gen.HsType.checkDataKindSig, we make sure that the result
+  kind of the data declaration is actually `Type` or `TYPE (BoxedRep l)`,
+  for some `l`. If UnliftedDatatypes is not activated, we emit an error with a
+  suggestion in the latter case.
+
+  Why not start out with `TYPE (BoxedRep l)` in the first place? Because then
+  we get worse kind error messages in e.g. saks_fail010:
+
+     -     Couldn't match expected kind: TYPE ('GHC.Types.BoxedRep t0)
+     -                  with actual kind: * -> *
+     +     Expected a type, but found something with kind ‘* -> *’
+           In the data type declaration for ‘T’
+
+  It seems `TYPE r` already has appropriate pretty-printing support.
+
+The changes to Core, STG and Cmm are of rather cosmetic nature.
+The IRs are already well-equipped to handle unlifted types, and unlifted
+datatypes are just a new sub-class thereof.
 -}
 
 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo])
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 657e1bffe7..8bfb5370bb 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -727,7 +727,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
        ; traceTc "tcDataFamInstDecl" $
          vcat [ text "Fam tycon:" <+> ppr fam_tc
               , text "Pats:" <+> ppr pats
-              , text "visiblities:" <+> ppr (tcbVisibilities fam_tc pats)
+              , text "visibilities:" <+> ppr (tcbVisibilities fam_tc pats)
               , text "all_pats:" <+> ppr all_pats
               , text "ty_binders" <+> ppr ty_binders
               , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
@@ -940,12 +940,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
     fam_name  = tyConName fam_tc
     data_ctxt = DataKindCtxt fam_name
 
-    -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2).
+    -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, families (2),
+    -- and Note [Implementation of UnliftedDatatypes].
     tc_kind_sig Nothing
-      = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
-           ; if unlifted_newtypes && new_or_data == NewType
-               then newOpenTypeKind
-               else pure liftedTypeKind
+      = do { unlifted_newtypes  <- xoptM LangExt.UnliftedNewtypes
+           ; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes
+           ; case new_or_data of
+               NewType  | unlifted_newtypes  -> newOpenTypeKind
+               DataType | unlifted_datatypes -> newOpenTypeKind
+               _                             -> pure liftedTypeKind
            }
 
     -- See Note [Result kind signature for a data family instance]
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index a3cda06cac..b6f5065997 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -23,6 +23,7 @@ module GHC.Tc.Utils.TcMType (
   newFlexiTyVarTy,              -- Kind -> TcM TcType
   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
   newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
+  newOpenBoxedTypeKind,
   newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
   newAnonMetaTyVar, cloneMetaTyVar,
   newCycleBreakerTyVar,
@@ -1075,6 +1076,12 @@ newOpenFlexiTyVar
   = do { kind <- newOpenTypeKind
        ; newFlexiTyVar kind }
 
+newOpenBoxedTypeKind :: TcM TcKind
+newOpenBoxedTypeKind
+  = do { lev <- newFlexiTyVarTy (mkTyConTy levityTyCon)
+       ; let rr = mkTyConApp boxedRepDataConTyCon [lev]
+       ; return (tYPE rr) }
+
 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Instantiate with META type variables
 -- Note that this works for a sequence of kind, type, and coercion variables
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index de4a983001..b0f80e93c3 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.
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index b75977c74c..8dc2b67a36 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -51,6 +51,7 @@ data Extension
    | UnboxedTuples
    | UnboxedSums
    | UnliftedNewtypes
+   | UnliftedDatatypes
    | BangPatterns
    | TypeFamilies
    | TypeFamilyDependencies
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 59edeec8af..7ce559739f 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -96,7 +96,8 @@ type UnliftedRep = 'BoxedRep 'Unlifted
 -- | The kind of types with lifted values. For example @Int :: Type@.
 type Type = TYPE LiftedRep
 
--- | The kind of types with unlifted values. For example @Int# :: UnliftedType@.
+-- | The kind of boxed, unlifted values, for example @Array#@ or a user-defined
+-- unlifted data type, using @-XUnliftedDataTypes@.
 type UnliftedType = TYPE UnliftedRep
 
 data Multiplicity = Many | One
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index cbcbefc573..d55dae5484 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -43,6 +43,7 @@ expectedGhcOnlyExtensions =
     , "FieldSelectors"
     , "OverloadedRecordDot"
     , "OverloadedRecordUpdate"
+    , "UnliftedDatatypes"
     ]
 
 expectedCabalOnlyExtensions :: [String]
diff --git a/testsuite/tests/unlifted-datatypes/Makefile b/testsuite/tests/unlifted-datatypes/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/Makefile b/testsuite/tests/unlifted-datatypes/should_compile/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
new file mode 100644
index 0000000000..443deadc1a
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+
+module UnlDataFams where
+
+import GHC.Exts
+import GHC.Types
+
+data family F a :: UnliftedType
+
+data instance F Int = TInt
+
+data family G a :: TYPE (BoxedRep l)
+
+data instance G Int = GInt
+data instance G Bool :: UnliftedType where
+  GBool :: G Bool
+data instance G Char :: Type where
+  GChar :: G Char
+
+data family H :: Type -> UnliftedType
+data instance H Int = HInt Int
+
+type Interpret :: Bool -> Levity
+type family Interpret b where
+  Interpret True  = Lifted
+  Interpret False = Unlifted
+
+type A :: TYPE (BoxedRep (Interpret b))
+data A = MkA Int
+
+a :: A @True
+a = MkA 42
+
+-- type Interpret :: Bool -> RuntimeRep
+-- type family Interpret b where
+--   Interpret True  = BoxedRep Lifted
+--   Interpret False = BoxedRep Unlifted
+--
+-- type A :: TYPE (Interpret b)
+-- data A = MkA Int
+--
+-- data B :: TYPE (Interpret b) where
+--   MkB :: Int -> B @b
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs
new file mode 100644
index 0000000000..cef48e31e0
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+
+module UnlDataMonoSigs where
+
+import GHC.Exts
+import GHC.Types
+
+data T1 a :: UnliftedType where
+  MkT1 :: T1 a
+
+type T2 :: Type -> UnliftedType
+data T2 a = T2
+
+type T3 :: Type -> UnliftedType
+data T3 a where
+  MkT3 :: T3 a
+
+type T4 :: Type -> UnliftedType
+data T4 a :: UnliftedType where
+  MkT4 :: T4 a
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs
new file mode 100644
index 0000000000..6e998155bf
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+
+module UnlDataPolySigs where
+
+import GHC.Exts
+import GHC.Types
+
+data U1 a :: TYPE (BoxedRep l) where
+  MkU1 :: Int -> U1 a -- (MkU1 :: forall {k} (a :: k). Int -> U1 @{k} @'Lifted a)
+
+type U2 :: Type -> TYPE (BoxedRep l)
+data U2 a = MkU2 Int -- (MkU2 :: forall (l :: Levity) a. Int -> U2 @l a)
+
+type U3 :: Type -> TYPE (BoxedRep l)
+data U3 a where
+  MkU3 :: Int -> U3 a -- (MkU3 :: forall a. Int -> U3 @'Lifted a)
+
+type U4 :: Type -> TYPE (BoxedRep l)
+data U4 a :: TYPE (BoxedRep l) where
+  MkU4 :: Int -> U4 a -- (MkU4 :: forall a. Int -> U4 @'Lifted a)
+
+data U5 a :: forall l. TYPE (BoxedRep l) where
+  MkU5 :: Int -> U5 a -- (MkU5 :: forall {k} (a :: k). Int -> U5 @{k} @'Lifted a)
+
+data U6 a :: forall l. TYPE (BoxedRep l) where
+  MkU6 :: Int -> U6 a @l -- (MkU6 :: forall {k} (a :: k) (l :: Levity). Int -> U6 @{k} a @l)
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs
new file mode 100644
index 0000000000..9023093ee8
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE ConstraintKinds #-}
+
+module UnlDataUsersGuide where
+
+import GHC.Exts
+import GHC.Types
+
+data UList a :: UnliftedType where
+  UCons :: a -> UList a -> UList a
+  UNil :: UList a
+
+type UList2 :: Type -> UnliftedType
+data UList2 a = UCons2 a (UList2 a) | UNil2
+
+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
+
+type T :: TYPE (BoxedRep l)
+data T where
+  MkT :: forall l. (() :: Constraint) => T @l
+  MkT2 :: Proxy# () -> T @l
+
+t1 :: T @Lifted
+t1 = MkT
+
+t2 :: T @Lifted
+t2 = MkT2 proxy#
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/all.T b/testsuite/tests/unlifted-datatypes/should_compile/all.T
new file mode 100644
index 0000000000..d8c3eeb457
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/all.T
@@ -0,0 +1,4 @@
+test('UnlDataMonoSigs', normal, compile, [''])
+test('UnlDataPolySigs', normal, compile, [''])
+test('UnlDataFams', normal, compile, [''])
+test('UnlDataUsersGuide', normal, compile, [''])
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/Makefile b/testsuite/tests/unlifted-datatypes/should_fail/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs
new file mode 100644
index 0000000000..18dcd1a216
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+
+module UnlDataInvalidResKind1 where
+
+import GHC.Exts
+import GHC.Types
+
+type T :: Type -> TYPE IntRep
+data T a = MkT Int
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr
new file mode 100644
index 0000000000..e61b6b4b18
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr
@@ -0,0 +1,4 @@
+
+UnlDataInvalidResKind1.hs:9:1: error:
+    • Data type has non-'BoxedRep return kind ‘TYPE 'IntRep’
+    • In the data declaration for ‘T’
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs
new file mode 100644
index 0000000000..427e41bf0c
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+
+module UnlDataInvalidResKind2 where
+
+import GHC.Exts
+import GHC.Types
+
+type Interpret :: Bool -> RuntimeRep
+type family Interpret b = r | r -> b where
+  Interpret True  = BoxedRep Lifted
+  Interpret False = BoxedRep Unlifted
+
+-- Not allowed, although well-typed after type fam reduction
+type A :: TYPE (Interpret b)
+data A = MkA Int
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs
new file mode 100644
index 0000000000..1b59bdf24f
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE PolyKinds #-}
+
+module UnlDataNullaryPoly where
+
+import GHC.Exts
+import GHC.Types
+
+type T :: TYPE (BoxedRep l)
+data T = MkT -- Not OK, we get (MkT :: forall l. T @l :: TYPE (BoxedRep l)) which is ill-kinded.
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr
new file mode 100644
index 0000000000..7c9b856677
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr
@@ -0,0 +1,7 @@
+
+UnlDataNullaryPoly.hs:10:10: error:
+    • Quantified type's kind mentions quantified type variable
+        type: ‘forall (l :: Levity). T’
+      where the body of the forall has this kind: ‘TYPE ('BoxedRep l)’
+    • In the definition of data constructor ‘MkT’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/all.T b/testsuite/tests/unlifted-datatypes/should_fail/all.T
new file mode 100644
index 0000000000..f8e8c7c833
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/all.T
@@ -0,0 +1,2 @@
+test('UnlDataNullaryPoly', normal, compile_fail, [''])
+test('UnlDataInvalidResKind1', normal, compile_fail, [''])
diff --git a/testsuite/tests/unlifted-datatypes/should_run/Makefile b/testsuite/tests/unlifted-datatypes/should_run/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs
new file mode 100644
index 0000000000..19266ea71e
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+
+import GHC.Exts
+import GHC.Types
+
+type SList :: Type -> UnliftedType
+data SList a = Cons a (SList a) | Nil
+
+-- Sadly no IsList (SList a) or Show a => Show (SList a),
+-- because type classes require lifted rep
+sfromList :: [a] -> SList a
+sfromList []     = Nil
+sfromList (x:xs) = Cons x (sfromList xs)
+stoList :: SList a -> [a]
+stoList (Cons x xs) = x:stoList xs
+stoList Nil         = []
+
+sfromList2 :: [a] -> SList a
+sfromList2 xs = foldl (\acc x xs -> acc (Cons x xs)) (\x -> x) xs Nil
+
+sfromList3 :: [a] -> SList a
+sfromList3 xs = foldr (\x acc xs -> Cons x (acc xs)) (\x -> x) xs Nil
+
+sreverse :: SList a -> SList a
+sreverse = go Nil
+  where
+    go acc Nil         = acc
+    go acc (Cons x xs) = go (Cons x acc) xs
+
+main = do
+  print (stoList (sreverse (Cons 1 (Cons 2 (Cons 3 Nil)))))
+  print (stoList (sreverse (sfromList [2,3,4])))
+  print (stoList (sreverse (sfromList2 [3,4,5])))
+  print (stoList (sreverse (sfromList3 [4,5,6])))
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout
new file mode 100644
index 0000000000..0b1c480e31
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout
@@ -0,0 +1,4 @@
+[3,2,1]
+[4,3,2]
+[5,4,3]
+[6,5,4]
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs
new file mode 100644
index 0000000000..ed19c3236f
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+
+import GHC.Exts
+import GHC.Types
+
+data T a :: UnliftedType where
+  TInt :: T Int
+
+f :: T a -> Int
+f _ = 0
+
+g :: T a -> T a
+g TInt = TInt
+{-# NOINLINE g #-}
+
+main = do
+  case g TInt of TInt -> putStrLn "should see this"
+  print (f (error "boom")) -- crashes!
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr
new file mode 100644
index 0000000000..158e2a12ba
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr
@@ -0,0 +1,3 @@
+UnlGadt1: boom
+CallStack (from HasCallStack):
+  error, called at UnlGadt1.hs:19:13 in main:Main
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout
new file mode 100644
index 0000000000..b31e365734
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout
@@ -0,0 +1 @@
+should see this
diff --git a/testsuite/tests/unlifted-datatypes/should_run/all.T b/testsuite/tests/unlifted-datatypes/should_run/all.T
new file mode 100644
index 0000000000..87b69c89bf
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/all.T
@@ -0,0 +1,2 @@
+test('UnlData1', normal, compile_and_run, [''])
+test('UnlGadt1', exit_code(1), compile_and_run, [''])