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.

13 files changed, 328 insertions, 158 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 f33373b130..eb14bbc91f 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -3611,6 +3611,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
@@ -3794,6 +3795,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