Implement BoxedRep proposalwip/boxed-rep

This implements the BoxedRep proposal, refactoring the `RuntimeRep`
hierarchy from:

```haskell
data RuntimeRep = LiftedPtrRep | UnliftedPtrRep | ...
```

to

```haskell
data RuntimeRep = BoxedRep Levity | ...
data Levity = Lifted | Unlifted
```

Updates binary, haddock submodules.

Closes #17526.

Metric Increase:
    T12545

107 files changed, 774 insertions, 380 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 93ea664739..2836c82e72 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -1894,7 +1894,7 @@ statePrimTyConKey, stableNamePrimTyConKey, stableNameTyConKey,
     wordPrimTyConKey, wordTyConKey, word8PrimTyConKey, word8TyConKey,
     word16PrimTyConKey, word16TyConKey, word32PrimTyConKey, word32TyConKey,
     word64PrimTyConKey, word64TyConKey,
-    liftedConKey, unliftedConKey, anyBoxConKey, kindConKey, boxityConKey,
+    anyBoxConKey, kindConKey, boxityConKey,
     typeConKey, threadIdPrimTyConKey, bcoPrimTyConKey, ptrTyConKey,
     funPtrTyConKey, tVarPrimTyConKey, eqPrimTyConKey,
     eqReprPrimTyConKey, eqPhantPrimTyConKey,
@@ -1917,8 +1917,6 @@ word32PrimTyConKey                      = mkPreludeTyConUnique 65
 word32TyConKey                          = mkPreludeTyConUnique 66
 word64PrimTyConKey                      = mkPreludeTyConUnique 67
 word64TyConKey                          = mkPreludeTyConUnique 68
-liftedConKey                            = mkPreludeTyConUnique 69
-unliftedConKey                          = mkPreludeTyConUnique 70
 anyBoxConKey                            = mkPreludeTyConUnique 71
 kindConKey                              = mkPreludeTyConUnique 72
 boxityConKey                            = mkPreludeTyConUnique 73
@@ -1934,15 +1932,20 @@ eitherTyConKey :: Unique
 eitherTyConKey                          = mkPreludeTyConUnique 84
 
 -- Kind constructors
-liftedTypeKindTyConKey, tYPETyConKey,
-  constraintKindTyConKey, runtimeRepTyConKey,
+liftedTypeKindTyConKey, unliftedTypeKindTyConKey,
+  tYPETyConKey, liftedRepTyConKey, unliftedRepTyConKey,
+  constraintKindTyConKey, levityTyConKey, runtimeRepTyConKey,
   vecCountTyConKey, vecElemTyConKey :: Unique
 liftedTypeKindTyConKey                  = mkPreludeTyConUnique 87
-tYPETyConKey                            = mkPreludeTyConUnique 88
+unliftedTypeKindTyConKey                = mkPreludeTyConUnique 88
+tYPETyConKey                            = mkPreludeTyConUnique 89
 constraintKindTyConKey                  = mkPreludeTyConUnique 92
+levityTyConKey                          = mkPreludeTyConUnique 94
 runtimeRepTyConKey                      = mkPreludeTyConUnique 95
 vecCountTyConKey                        = mkPreludeTyConUnique 96
 vecElemTyConKey                         = mkPreludeTyConUnique 97
+liftedRepTyConKey                       = mkPreludeTyConUnique 98
+unliftedRepTyConKey                     = mkPreludeTyConUnique 99
 
 pluginTyConKey, frontendPluginTyConKey :: Unique
 pluginTyConKey                          = mkPreludeTyConUnique 102
@@ -2206,59 +2209,61 @@ metaDataDataConKey                      = mkPreludeDataConUnique 68
 metaConsDataConKey                      = mkPreludeDataConUnique 69
 metaSelDataConKey                       = mkPreludeDataConUnique 70
 
-vecRepDataConKey, tupleRepDataConKey, sumRepDataConKey :: Unique
+vecRepDataConKey, tupleRepDataConKey, sumRepDataConKey,
+  boxedRepDataConKey :: Unique
 vecRepDataConKey                        = mkPreludeDataConUnique 71
 tupleRepDataConKey                      = mkPreludeDataConUnique 72
 sumRepDataConKey                        = mkPreludeDataConUnique 73
+boxedRepDataConKey                      = mkPreludeDataConUnique 74
 
 -- See Note [Wiring in RuntimeRep] in GHC.Builtin.Types
-runtimeRepSimpleDataConKeys, unliftedSimpleRepDataConKeys, unliftedRepDataConKeys :: [Unique]
-liftedRepDataConKey :: Unique
-runtimeRepSimpleDataConKeys@(liftedRepDataConKey : unliftedSimpleRepDataConKeys)
-  = map mkPreludeDataConUnique [74..88]
+-- Includes all nullary-data-constructor reps. Does not
+-- include BoxedRep, VecRep, SumRep, TupleRep.
+runtimeRepSimpleDataConKeys :: [Unique]
+runtimeRepSimpleDataConKeys
+  = map mkPreludeDataConUnique [75..87]
 
-unliftedRepDataConKeys = vecRepDataConKey :
-                         tupleRepDataConKey :
-                         sumRepDataConKey :
-                         unliftedSimpleRepDataConKeys
+liftedDataConKey,unliftedDataConKey :: Unique
+liftedDataConKey = mkPreludeDataConUnique 88
+unliftedDataConKey = mkPreludeDataConUnique 89
 
 -- See Note [Wiring in RuntimeRep] in GHC.Builtin.Types
 -- VecCount
 vecCountDataConKeys :: [Unique]
-vecCountDataConKeys = map mkPreludeDataConUnique [89..94]
+vecCountDataConKeys = map mkPreludeDataConUnique [90..95]
 
 -- See Note [Wiring in RuntimeRep] in GHC.Builtin.Types
 -- VecElem
 vecElemDataConKeys :: [Unique]
-vecElemDataConKeys = map mkPreludeDataConUnique [95..104]
+vecElemDataConKeys = map mkPreludeDataConUnique [96..105]
 
 -- Typeable things
 kindRepTyConAppDataConKey, kindRepVarDataConKey, kindRepAppDataConKey,
     kindRepFunDataConKey, kindRepTYPEDataConKey,
     kindRepTypeLitSDataConKey, kindRepTypeLitDDataConKey
     :: Unique
-kindRepTyConAppDataConKey = mkPreludeDataConUnique 105
-kindRepVarDataConKey      = mkPreludeDataConUnique 106
-kindRepAppDataConKey      = mkPreludeDataConUnique 107
-kindRepFunDataConKey      = mkPreludeDataConUnique 108
-kindRepTYPEDataConKey     = mkPreludeDataConUnique 109
-kindRepTypeLitSDataConKey = mkPreludeDataConUnique 110
-kindRepTypeLitDDataConKey = mkPreludeDataConUnique 111
+kindRepTyConAppDataConKey = mkPreludeDataConUnique 106
+kindRepVarDataConKey      = mkPreludeDataConUnique 107
+kindRepAppDataConKey      = mkPreludeDataConUnique 108
+kindRepFunDataConKey      = mkPreludeDataConUnique 109
+kindRepTYPEDataConKey     = mkPreludeDataConUnique 110
+kindRepTypeLitSDataConKey = mkPreludeDataConUnique 111
+kindRepTypeLitDDataConKey = mkPreludeDataConUnique 112
 
 typeLitSymbolDataConKey, typeLitNatDataConKey, typeLitCharDataConKey :: Unique
-typeLitSymbolDataConKey   = mkPreludeDataConUnique 112
-typeLitNatDataConKey      = mkPreludeDataConUnique 113
-typeLitCharDataConKey     = mkPreludeDataConUnique 114
+typeLitSymbolDataConKey   = mkPreludeDataConUnique 113
+typeLitNatDataConKey      = mkPreludeDataConUnique 114
+typeLitCharDataConKey     = mkPreludeDataConUnique 115
 
 -- Unsafe equality
 unsafeReflDataConKey :: Unique
-unsafeReflDataConKey      = mkPreludeDataConUnique 115
+unsafeReflDataConKey      = mkPreludeDataConUnique 116
 
 -- Multiplicity
 
 oneDataConKey, manyDataConKey :: Unique
-oneDataConKey = mkPreludeDataConUnique 116
-manyDataConKey = mkPreludeDataConUnique 117
+oneDataConKey = mkPreludeDataConUnique 117
+manyDataConKey = mkPreludeDataConUnique 118
 
 -- ghc-bignum
 integerISDataConKey, integerINDataConKey, integerIPDataConKey,
@@ -2505,14 +2510,16 @@ mkTrFunKey            = mkPreludeMiscIdUnique 511
 
 -- Representations for primitive types
 trTYPEKey
-  ,trTYPE'PtrRepLiftedKey
+  , trTYPE'PtrRepLiftedKey
   , trRuntimeRepKey
   , tr'PtrRepLiftedKey
+  , trLiftedRepKey
   :: Unique
 trTYPEKey              = mkPreludeMiscIdUnique 512
 trTYPE'PtrRepLiftedKey = mkPreludeMiscIdUnique 513
 trRuntimeRepKey        = mkPreludeMiscIdUnique 514
 tr'PtrRepLiftedKey     = mkPreludeMiscIdUnique 515
+trLiftedRepKey         = mkPreludeMiscIdUnique 516
 
 -- KindReps for common cases
 starKindRepKey, starArrStarKindRepKey, starArrStarArrStarKindRepKey :: Unique
@@ -2818,5 +2825,6 @@ The following names should be considered by GHCi to be in scope always.
 pretendNameIsInScope :: Name -> Bool
 pretendNameIsInScope n
   = any (n `hasKey`)
-    [ liftedTypeKindTyConKey, tYPETyConKey
-    , runtimeRepTyConKey, liftedRepDataConKey ]
+    [ liftedTypeKindTyConKey, unliftedTypeKindTyConKey
+    , tYPETyConKey
+    , runtimeRepTyConKey, boxedRepDataConKey ]
diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs
index 1a3550fcaa..3b928c801f 100644
--- a/compiler/GHC/Builtin/Types.hs
+++ b/compiler/GHC/Builtin/Types.hs
@@ -98,10 +98,13 @@ module GHC.Builtin.Types (
 
         -- * Kinds
         typeSymbolKindCon, typeSymbolKind,
-        isLiftedTypeKindTyConName, liftedTypeKind,
-        typeToTypeKind, constraintKind,
-        liftedTypeKindTyCon, constraintKindTyCon,  constraintKindTyConName,
-        liftedTypeKindTyConName,
+        isLiftedTypeKindTyConName,
+        typeToTypeKind,
+        liftedRepTyCon, unliftedRepTyCon,
+        constraintKind, liftedTypeKind, unliftedTypeKind,
+        constraintKindTyCon, liftedTypeKindTyCon, unliftedTypeKindTyCon,
+        constraintKindTyConName, liftedTypeKindTyConName, unliftedTypeKindTyConName,
+        liftedRepTyConName, unliftedRepTyConName,
 
         -- * Equality predicates
         heqTyCon, heqTyConName, heqClass, heqDataCon,
@@ -109,13 +112,16 @@ module GHC.Builtin.Types (
         coercibleTyCon, coercibleTyConName, coercibleDataCon, coercibleClass,
 
         -- * RuntimeRep and friends
-        runtimeRepTyCon, vecCountTyCon, vecElemTyCon,
+        runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon,
 
-        runtimeRepTy, liftedRepTy, liftedRepDataCon, liftedRepDataConTyCon,
+        boxedRepDataConTyCon,
+        runtimeRepTy, liftedRepTy, unliftedRepTy,
 
         vecRepDataConTyCon, tupleRepDataConTyCon, sumRepDataConTyCon,
 
-        liftedRepDataConTy, unliftedRepDataConTy,
+        liftedDataConTyCon, unliftedDataConTyCon,
+        liftedDataConTy, unliftedDataConTy,
+
         intRepDataConTy,
         int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy,
         wordRepDataConTy,
@@ -213,6 +219,43 @@ to this Note, so a search for this Note's name should find all the lists.
 
 See also Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
 
+
+Note [Wired-in Types and Type Constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+This module include a lot of wired-in types and type constructors. Here,
+these are presented in a tabular format to make it easier to find the
+wired-in type identifier corresponding to a known Haskell type. Data
+constructors are nested under their corresponding types with two spaces
+of indentation.
+
+Identifier              Type    Haskell name          Notes
+----------------------------------------------------------------------------
+liftedTypeKindTyCon     TyCon   GHC.Types.Type        Synonym for: TYPE LiftedRep
+unliftedTypeKindTyCon   TyCon   GHC.Types.Type        Synonym for: TYPE UnliftedRep
+liftedRepTyCon          TyCon   GHC.Types.LiftedRep   Synonym for: 'BoxedRep 'Lifted
+unliftedRepTyCon        TyCon   GHC.Types.LiftedRep   Synonym for: 'BoxedRep 'Unlifted
+levityTyCon             TyCon   GHC.Types.Levity      Data type
+  liftedDataConTyCon    TyCon   GHC.Types.Lifted      Data constructor
+  unliftedDataConTyCon  TyCon   GHC.Types.Unlifted    Data constructor
+vecCountTyCon           TyCon   GHC.Types.VecCount    Data type
+  vec2DataConTy         Type    GHC.Types.Vec2        Data constructor
+  vec4DataConTy         Type    GHC.Types.Vec4        Data constructor
+  vec8DataConTy         Type    GHC.Types.Vec8        Data constructor
+  vec16DataConTy        Type    GHC.Types.Vec16       Data constructor
+  vec32DataConTy        Type    GHC.Types.Vec32       Data constructor
+  vec64DataConTy        Type    GHC.Types.Vec64       Data constructor
+runtimeRepTyCon         TyCon   GHC.Types.RuntimeRep  Data type
+  boxedRepDataConTyCon  TyCon   GHC.Types.BoxedRep    Data constructor
+  intRepDataConTy       Type    GHC.Types.IntRep      Data constructor
+  doubleRepDataConTy    Type    GHC.Types.DoubleRep   Data constructor
+  floatRepDataConTy     Type    GHC.Types.FloatRep    Data constructor
+boolTyCon               TyCon   GHC.Types.Bool        Data type
+  trueDataCon           DataCon GHC.Types.True        Data constructor
+  falseDataCon          DataCon GHC.Types.False       Data constructor
+  promotedTrueDataCon   TyCon   GHC.Types.True        Data constructor
+  promotedFalseDataCon  TyCon   GHC.Types.False       Data constructor
+
 ************************************************************************
 *                                                                      *
 \subsection{Wired in type constructors}
@@ -221,8 +264,10 @@ See also Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
 
 If you change which things are wired in, make sure you change their
 names in GHC.Builtin.Names, so they use wTcQual, wDataQual, etc
+
 -}
 
+
 -- This list is used only to define GHC.Builtin.Utils.wiredInThings. That in turn
 -- is used to initialise the name environment carried around by the renamer.
 -- This means that if we look up the name of a TyCon (or its implicit binders)
@@ -261,13 +306,17 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
                 , coercibleTyCon
                 , typeSymbolKindCon
                 , runtimeRepTyCon
+                , levityTyCon
                 , vecCountTyCon
                 , vecElemTyCon
                 , constraintKindTyCon
                 , liftedTypeKindTyCon
+                , unliftedTypeKindTyCon
                 , multiplicityTyCon
                 , naturalTyCon
                 , integerTyCon
+                , liftedRepTyCon
+                , unliftedRepTyCon
                 ]
 
 mkWiredInTyConName :: BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
@@ -484,8 +533,13 @@ typeSymbolKindConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Symbol")
 constraintKindTyConName :: Name
 constraintKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Constraint") constraintKindTyConKey   constraintKindTyCon
 
-liftedTypeKindTyConName :: Name
+liftedTypeKindTyConName, unliftedTypeKindTyConName :: Name
 liftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type") liftedTypeKindTyConKey liftedTypeKindTyCon
+unliftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "UnliftedType") unliftedTypeKindTyConKey unliftedTypeKindTyCon
+
+liftedRepTyConName, unliftedRepTyConName :: Name
+liftedRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "LiftedRep") liftedRepTyConKey liftedRepTyCon
+unliftedRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "UnliftedRep") unliftedRepTyConKey unliftedRepTyCon
 
 multiplicityTyConName :: Name
 multiplicityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Multiplicity")
@@ -501,18 +555,24 @@ manyDataConName = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit "Many") ma
  -- reported. Making them built-in make it so that they are always considered in
  -- scope.
 
-runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName :: Name
+runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName, boxedRepDataConName :: Name
 runtimeRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "RuntimeRep") runtimeRepTyConKey runtimeRepTyCon
 vecRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "VecRep") vecRepDataConKey vecRepDataCon
 tupleRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "TupleRep") tupleRepDataConKey tupleRepDataCon
 sumRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "SumRep") sumRepDataConKey sumRepDataCon
+boxedRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "BoxedRep") boxedRepDataConKey boxedRepDataCon
+
+levityTyConName, liftedDataConName, unliftedDataConName :: Name
+levityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Levity") levityTyConKey levityTyCon
+liftedDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Lifted") liftedDataConKey liftedDataCon
+unliftedDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Unlifted") unliftedDataConKey unliftedDataCon
+
 
 -- See Note [Wiring in RuntimeRep]
 runtimeRepSimpleDataConNames :: [Name]
 runtimeRepSimpleDataConNames
   = zipWith3Lazy mk_special_dc_name
-      [ fsLit "LiftedRep", fsLit "UnliftedRep"
-      , fsLit "IntRep"
+      [ fsLit "IntRep"
       , fsLit "Int8Rep", fsLit "Int16Rep", fsLit "Int32Rep", fsLit "Int64Rep"
       , fsLit "WordRep"
       , fsLit "Word8Rep", fsLit "Word16Rep", fsLit "Word32Rep", fsLit "Word64Rep"
@@ -691,8 +751,9 @@ constraintKindTyCon :: TyCon
 constraintKindTyCon = pcTyCon constraintKindTyConName Nothing [] []
 
 -- See Note [Prefer Type over TYPE 'LiftedRep] in GHC.Core.TyCo.Rep.
-liftedTypeKind, typeToTypeKind, constraintKind :: Kind
+liftedTypeKind, unliftedTypeKind, typeToTypeKind, constraintKind :: Kind
 liftedTypeKind   = mkTyConTy liftedTypeKindTyCon
+unliftedTypeKind = mkTyConTy unliftedTypeKindTyCon
 typeToTypeKind   = liftedTypeKind `mkVisFunTyMany` liftedTypeKind
 constraintKind   = mkTyConTy constraintKindTyCon
 
@@ -1424,16 +1485,52 @@ 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 'LiftedRep
+-- type Type = TYPE ('BoxedRep 'Lifted)
+-- type LiftedRep = 'BoxedRep 'Lifted
 liftedTypeKindTyCon :: TyCon
-liftedTypeKindTyCon   = buildSynTyCon liftedTypeKindTyConName
-                                       [] liftedTypeKind [] rhs
-  where rhs = TyCoRep.TyConApp tYPETyCon [liftedRepTy]
+liftedTypeKindTyCon =
+    buildSynTyCon liftedTypeKindTyConName [] liftedTypeKind [] rhs
+  where rhs = TyCoRep.TyConApp tYPETyCon [mkTyConApp liftedRepTyCon []]
+
+unliftedTypeKindTyCon :: TyCon
+unliftedTypeKindTyCon =
+    buildSynTyCon unliftedTypeKindTyConName [] liftedTypeKind [] rhs
+  where rhs = TyCoRep.TyConApp tYPETyCon [mkTyConApp unliftedRepTyCon []]
+
+liftedRepTyCon :: TyCon
+liftedRepTyCon = buildSynTyCon
+  liftedRepTyConName [] runtimeRepTy [] liftedRepTy
+
+unliftedRepTyCon :: TyCon
+unliftedRepTyCon = buildSynTyCon
+  unliftedRepTyConName [] runtimeRepTy [] unliftedRepTy
 
 runtimeRepTyCon :: TyCon
 runtimeRepTyCon = pcTyCon runtimeRepTyConName Nothing []
-                          (vecRepDataCon : tupleRepDataCon :
-                           sumRepDataCon : runtimeRepSimpleDataCons)
+    (vecRepDataCon : tupleRepDataCon :
+     sumRepDataCon : boxedRepDataCon : runtimeRepSimpleDataCons)
+
+levityTyCon :: TyCon
+levityTyCon = pcTyCon levityTyConName Nothing [] [liftedDataCon,unliftedDataCon]
+
+liftedDataCon, unliftedDataCon :: DataCon
+liftedDataCon = pcSpecialDataCon liftedDataConName
+    [] levityTyCon LiftedInfo
+unliftedDataCon = pcSpecialDataCon unliftedDataConName
+    [] levityTyCon UnliftedInfo
+
+boxedRepDataCon :: DataCon
+boxedRepDataCon = pcSpecialDataCon boxedRepDataConName
+  [ mkTyConTy levityTyCon ] runtimeRepTyCon (RuntimeRep prim_rep_fun)
+  where
+    -- See Note [Getting from RuntimeRep to PrimRep] in RepType
+    prim_rep_fun [lev]
+      = case tyConRuntimeRepInfo (tyConAppTyCon lev) of
+          LiftedInfo -> [LiftedRep]
+          UnliftedInfo -> [UnliftedRep]
+          _ -> pprPanic "boxedRepDataCon" (ppr lev)
+    prim_rep_fun args
+      = pprPanic "boxedRepDataCon" (ppr args)
 
 vecRepDataCon :: DataCon
 vecRepDataCon = pcSpecialDataCon vecRepDataConName [ mkTyConTy vecCountTyCon
@@ -1488,11 +1585,9 @@ sumRepDataConTyCon = promoteDataCon sumRepDataCon
 -- See Note [Wiring in RuntimeRep]
 -- See Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType
 runtimeRepSimpleDataCons :: [DataCon]
-liftedRepDataCon :: DataCon
-runtimeRepSimpleDataCons@(liftedRepDataCon : _)
+runtimeRepSimpleDataCons
   = zipWithLazy mk_runtime_rep_dc
-    [ LiftedRep, UnliftedRep
-    , IntRep
+    [ IntRep
     , Int8Rep, Int16Rep, Int32Rep, Int64Rep
     , WordRep
     , Word8Rep, Word16Rep, Word32Rep, Word64Rep
@@ -1505,15 +1600,13 @@ runtimeRepSimpleDataCons@(liftedRepDataCon : _)
       = pcSpecialDataCon name [] runtimeRepTyCon (RuntimeRep (\_ -> [primrep]))
 
 -- See Note [Wiring in RuntimeRep]
-liftedRepDataConTy, unliftedRepDataConTy,
-  intRepDataConTy,
+intRepDataConTy,
   int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy,
   wordRepDataConTy,
   word8RepDataConTy, word16RepDataConTy, word32RepDataConTy, word64RepDataConTy,
   addrRepDataConTy,
   floatRepDataConTy, doubleRepDataConTy :: Type
-[liftedRepDataConTy, unliftedRepDataConTy,
-   intRepDataConTy,
+[intRepDataConTy,
    int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy,
    wordRepDataConTy,
    word8RepDataConTy, word16RepDataConTy, word32RepDataConTy, word64RepDataConTy,
@@ -1565,12 +1658,29 @@ int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
   doubleElemRepDataConTy] = map (mkTyConTy . promoteDataCon)
                                 vecElemDataCons
 
-liftedRepDataConTyCon :: TyCon
-liftedRepDataConTyCon = promoteDataCon liftedRepDataCon
 
--- The type ('LiftedRep)
+liftedDataConTyCon :: TyCon
+liftedDataConTyCon = promoteDataCon liftedDataCon
+
+unliftedDataConTyCon :: TyCon
+unliftedDataConTyCon = promoteDataCon unliftedDataCon
+
+liftedDataConTy :: Type
+liftedDataConTy = mkTyConTy liftedDataConTyCon
+
+unliftedDataConTy :: Type
+unliftedDataConTy = mkTyConTy unliftedDataConTyCon
+
+boxedRepDataConTyCon :: TyCon
+boxedRepDataConTyCon = promoteDataCon boxedRepDataCon
+
+-- The type ('BoxedRep 'Lifted)
 liftedRepTy :: Type
-liftedRepTy = liftedRepDataConTy
+liftedRepTy = mkTyConApp boxedRepDataConTyCon [liftedDataConTy]
+
+-- The type ('BoxedRep 'Unlifted)
+unliftedRepTy :: Type
+unliftedRepTy = mkTyConApp boxedRepDataConTyCon [unliftedDataConTy]
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Builtin/Types.hs-boot b/compiler/GHC/Builtin/Types.hs-boot
index c19137e148..1c341de418 100644
--- a/compiler/GHC/Builtin/Types.hs-boot
+++ b/compiler/GHC/Builtin/Types.hs-boot
@@ -17,17 +17,27 @@ coercibleTyCon, heqTyCon :: TyCon
 unitTy :: Type
 
 liftedTypeKind :: Kind
+unliftedTypeKind :: Kind
+
 liftedTypeKindTyCon :: TyCon
+unliftedTypeKindTyCon :: TyCon
+
+liftedRepTyCon :: TyCon
+unliftedRepTyCon :: TyCon
 
 constraintKind :: Kind
 
-runtimeRepTyCon, vecCountTyCon, vecElemTyCon :: TyCon
+runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon :: TyCon
 runtimeRepTy :: Type
 
-liftedRepDataConTyCon, vecRepDataConTyCon, tupleRepDataConTyCon :: TyCon
+boxedRepDataConTyCon :: TyCon
+liftedDataConTyCon :: TyCon
+vecRepDataConTyCon, tupleRepDataConTyCon :: TyCon
+
+liftedRepTy, unliftedRepTy :: Type
+liftedDataConTy, unliftedDataConTy :: Type
 
-liftedRepDataConTy, unliftedRepDataConTy,
-  intRepDataConTy,
+intRepDataConTy,
   int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy,
   wordRepDataConTy,
   word8RepDataConTy, word16RepDataConTy, word32RepDataConTy, word64RepDataConTy,
diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs
index 27df5236a3..29bb386001 100644
--- a/compiler/GHC/Builtin/Types/Prim.hs
+++ b/compiler/GHC/Builtin/Types/Prim.hs
@@ -101,7 +101,7 @@ import GHC.Prelude
 import {-# SOURCE #-} GHC.Builtin.Types
   ( runtimeRepTy, unboxedTupleKind, liftedTypeKind
   , vecRepDataConTyCon, tupleRepDataConTyCon
-  , liftedRepDataConTy, unliftedRepDataConTy
+  , liftedRepTy, unliftedRepTy
   , intRepDataConTy
   , int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy
   , wordRepDataConTy
@@ -129,7 +129,7 @@ import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Core.TyCo.Rep -- Doesn't need special access, but this is easier to avoid
                          -- import loops which show up if you import Type instead
-import {-# SOURCE #-} GHC.Core.Type ( mkTyConTy )
+import {-# SOURCE #-} GHC.Core.Type ( mkTyConTy, tYPE )
 
 import Data.Char
 
@@ -368,7 +368,7 @@ alphaTy, betaTy, gammaTy, deltaTy :: Type
 (alphaTy:betaTy:gammaTy:deltaTy:_) = alphaTys
 
 alphaTyVarsUnliftedRep :: [TyVar]
-alphaTyVarsUnliftedRep = mkTemplateTyVars $ repeat (tYPE unliftedRepDataConTy)
+alphaTyVarsUnliftedRep = mkTemplateTyVars $ repeat (tYPE unliftedRepTy)
 
 alphaTyVarUnliftedRep :: TyVar
 (alphaTyVarUnliftedRep:_) = alphaTyVarsUnliftedRep
@@ -460,26 +460,28 @@ Note [TYPE and RuntimeRep]
 All types that classify values have a kind of the form (TYPE rr), where
 
     data RuntimeRep     -- Defined in ghc-prim:GHC.Types
-      = LiftedRep
-      | UnliftedRep
+      = BoxedRep Levity
       | IntRep
       | FloatRep
       .. etc ..
 
+    data Levity = Lifted | Unlifted
+
     rr :: RuntimeRep
 
     TYPE :: RuntimeRep -> TYPE 'LiftedRep  -- Built in
 
 So for example:
-    Int        :: TYPE 'LiftedRep
-    Array# Int :: TYPE 'UnliftedRep
+    Int        :: TYPE ('BoxedRep 'Lifted)
+    Array# Int :: TYPE ('BoxedRep 'Unlifted)
     Int#       :: TYPE 'IntRep
     Float#     :: TYPE 'FloatRep
-    Maybe      :: TYPE 'LiftedRep -> TYPE 'LiftedRep
+    Maybe      :: TYPE ('BoxedRep 'Lifted) -> TYPE ('BoxedRep 'Lifted)
     (# , #)    :: TYPE r1 -> TYPE r2 -> TYPE (TupleRep [r1, r2])
 
 We abbreviate '*' specially:
-    type * = TYPE 'LiftedRep
+    type LiftedRep = 'BoxedRep 'Lifted
+    type * = TYPE LiftedRep
 
 The 'rr' parameter tells us how the value is represented at runtime.
 
@@ -512,7 +514,7 @@ generator never has to manipulate a value of type 'a :: TYPE rr'.
 Note [PrimRep and kindPrimRep]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 As part of its source code, in GHC.Core.TyCon, GHC has
-  data PrimRep = LiftedRep | UnliftedRep | IntRep | FloatRep | ...etc...
+  data PrimRep = BoxedRep Levity | IntRep | FloatRep | ...etc...
 
 Notice that
  * RuntimeRep is part of the syntax tree of the program being compiled
@@ -586,8 +588,8 @@ pcPrimTyCon name roles rep
 primRepToRuntimeRep :: PrimRep -> Type
 primRepToRuntimeRep rep = case rep of
   VoidRep       -> TyConApp tupleRepDataConTyCon [mkPromotedListTy runtimeRepTy []]
-  LiftedRep     -> liftedRepDataConTy
-  UnliftedRep   -> unliftedRepDataConTy
+  LiftedRep     -> liftedRepTy
+  UnliftedRep   -> unliftedRepTy
   IntRep        -> intRepDataConTy
   Int8Rep       -> int8RepDataConTy
   Int16Rep      -> int16RepDataConTy
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 2d9867e427..75d56ed501 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE CPP                #-}
 {-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE MultiWayIf         #-}
 
 {-# OPTIONS_HADDOCK not-home #-}
 
@@ -51,7 +52,6 @@ module GHC.Core.TyCo.Rep (
         mkScaledFunTy,
         mkVisFunTyMany, mkVisFunTysMany,
         mkInvisFunTyMany, mkInvisFunTysMany,
-        tYPE,
 
         -- * Functions over binders
         TyCoBinder(..), TyCoVarBinder, TyBinder,
@@ -90,11 +90,9 @@ import GHC.Core.TyCon
 import GHC.Core.Coercion.Axiom
 
 -- others
-import GHC.Builtin.Names ( liftedRepDataConKey )
-import {-# SOURCE #-} GHC.Builtin.Types ( liftedTypeKind, manyDataConTy )
-import {-# SOURCE #-} GHC.Builtin.Types.Prim ( tYPETyCon )
+import {-# SOURCE #-} GHC.Builtin.Types ( manyDataConTy )
 import GHC.Types.Basic ( LeftOrRight(..), pickLR )
-import GHC.Types.Unique ( hasKey, Uniquable(..) )
+import GHC.Types.Unique ( Uniquable(..) )
 import GHC.Utils.Outputable
 import GHC.Data.FastString
 import GHC.Utils.Misc
@@ -1010,66 +1008,6 @@ mkTyConTy_ :: TyCon -> Type
 mkTyConTy_ tycon = TyConApp tycon []
 
 {-
-Note [Prefer Type over TYPE 'LiftedRep]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The Core of nearly any program will have numerous occurrences of
-@TYPE 'LiftedRep@ (and, equivalently, 'Type') floating about. Concretely, while
-investigating #17292 we found that these constituting a majority of TyConApp
-constructors on the heap:
-
-```
-(From a sample of 100000 TyConApp closures)
-0x45f3523    - 28732 - `Type`
-0x420b840702 - 9629  - generic type constructors
-0x42055b7e46 - 9596
-0x420559b582 - 9511
-0x420bb15a1e - 9509
-0x420b86c6ba - 9501
-0x42055bac1e - 9496
-0x45e68fd    - 538 - `TYPE ...`
-```
-
-Consequently, we try hard to ensure that operations on such types are
-efficient. Specifically, we strive to
-
- a. Avoid heap allocation of such types
- b. Use a small (shallow in the tree-depth sense) representation
-    for such types
-
-Goal (b) is particularly useful as it makes traversals (e.g. free variable
-traversal, substitution, and comparison) more efficient.
-Comparison in particular takes special advantage of nullary type synonym
-applications (e.g. things like @TyConApp typeTyCon []@), Note [Comparing
-nullary type synonyms] in "GHC.Core.Type".
-
-To accomplish these we use a number of tricks:
-
- 1. Instead of representing the lifted kind as
-    @TyConApp tYPETyCon [liftedRepDataCon]@ we rather prefer to
-    use the 'GHC.Types.Type' type synonym (represented as a nullary TyConApp).
-    This serves goal (b) since there are no applied type arguments to traverse,
-    e.g., during comparison.
-
- 2. We have a top-level binding to represent `TyConApp GHC.Types.Type []`
-    (namely 'GHC.Builtin.Types.Prim.liftedTypeKind'), ensuring that we
-    don't need to allocate such types (goal (a)).
-
- 3. We use the sharing mechanism described in Note [Sharing nullary TyConApps]
-    in GHC.Core.TyCon to ensure that we never need to allocate such
-    nullary applications (goal (a)).
-
-See #17958.
--}
-
--- | Given a RuntimeRep, applies TYPE to it.
--- See Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim.
-tYPE :: Type -> Type
-tYPE (TyConApp tc [])
-  -- See Note [Prefer Type of TYPE 'LiftedRep]
-  | tc `hasKey` liftedRepDataConKey = liftedTypeKind  -- TYPE 'LiftedRep
-tYPE rr = TyConApp tYPETyCon [rr]
-
-{-
 %************************************************************************
 %*                                                                      *
             Coercions
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index babcbce347..4b517027da 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -140,7 +140,7 @@ import {-# SOURCE #-} GHC.Core.TyCo.Rep
 import {-# SOURCE #-} GHC.Core.TyCo.Ppr
    ( pprType )
 import {-# SOURCE #-} GHC.Builtin.Types
-   ( runtimeRepTyCon, constraintKind
+   ( runtimeRepTyCon, constraintKind, levityTyCon
    , multiplicityTyCon
    , vecCountTyCon, vecElemTyCon, liftedTypeKind )
 import {-# SOURCE #-} GHC.Core.DataCon
@@ -1095,6 +1095,8 @@ data RuntimeRepInfo
       -- be the list of arguments to the promoted datacon.
   | VecCount Int         -- ^ A constructor of @VecCount@
   | VecElem PrimElemRep  -- ^ A constructor of @VecElem@
+  | LiftedInfo           -- ^ A constructor of @Levity@
+  | UnliftedInfo         -- ^ A constructor of @Levity@
 
 -- | Extract those 'DataCon's that we are able to learn about.  Note
 -- that visibility in this sense does not correspond to visibility in
@@ -2215,8 +2217,8 @@ isKindTyCon tc = getUnique tc `elementOfUniqSet` kindTyConKeys
 -- -XDataKinds.
 kindTyConKeys :: UniqSet Unique
 kindTyConKeys = unionManyUniqSets
-  ( mkUniqSet [ liftedTypeKindTyConKey, constraintKindTyConKey, tYPETyConKey ]
-  : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon
+  ( mkUniqSet [ liftedTypeKindTyConKey, liftedRepTyConKey, constraintKindTyConKey, tYPETyConKey ]
+  : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon, levityTyCon
                                           , multiplicityTyCon
                                           , vecCountTyCon, vecElemTyCon ] )
   where
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 6a9eeed6fa..25276c155f 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -3,7 +3,7 @@
 --
 -- Type - public interface
 
-{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, ViewPatterns #-}
+{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, ViewPatterns, MultiWayIf #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
 
@@ -36,7 +36,7 @@ module GHC.Core.Type (
         splitFunTy, splitFunTy_maybe,
         splitFunTys, funResultTy, funArgTy,
 
-        mkTyConApp, mkTyConTy,
+        mkTyConApp, mkTyConTy, tYPE,
         tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
         tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
         splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
@@ -122,9 +122,11 @@ module GHC.Core.Type (
         isLiftedType_maybe,
         isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
         isLiftedRuntimeRep, isUnliftedRuntimeRep,
+        isLiftedLevity, isUnliftedLevity,
         isUnliftedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType,
         isAlgType, isDataFamilyAppType,
         isPrimitiveType, isStrictType,
+        isLevityTy, isLevityVar,
         isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
         dropRuntimeRepArgs,
         getRuntimeRep,
@@ -257,7 +259,8 @@ import GHC.Core.TyCon
 import GHC.Builtin.Types.Prim
 import {-# SOURCE #-} GHC.Builtin.Types
                                  ( charTy, naturalTy, listTyCon
-                                 , typeSymbolKind, liftedTypeKind
+                                 , typeSymbolKind, liftedTypeKind, unliftedTypeKind
+                                 , liftedRepTyCon, unliftedRepTyCon
                                  , constraintKind
                                  , unrestrictedFunTyCon
                                  , manyDataConTy, oneDataConTy )
@@ -613,6 +616,7 @@ isLiftedTypeKind kind
 pickyIsLiftedTypeKind :: Kind -> Bool
 -- Checks whether the kind is literally
 --      TYPE LiftedRep
+-- or   TYPE ('BoxedRep 'Lifted)
 -- or   Type
 -- without expanding type synonyms or anything
 -- Used only when deciding whether to suppress the ":: *" in
@@ -621,8 +625,13 @@ pickyIsLiftedTypeKind :: Kind -> Bool
 pickyIsLiftedTypeKind kind
   | TyConApp tc [arg] <- kind
   , tc `hasKey` tYPETyConKey
-  , TyConApp rr_tc [] <- arg
-  , rr_tc `hasKey` liftedRepDataConKey = True
+  , TyConApp rr_tc rr_args <- arg = case rr_args of
+      [] -> rr_tc `hasKey` liftedRepTyConKey
+      [rr_arg]
+        | rr_tc `hasKey` boxedRepDataConKey
+        , TyConApp lev [] <- rr_arg
+        , lev `hasKey` liftedDataConKey -> True
+      _ -> False
   | TyConApp tc [] <- kind
   , tc `hasKey` liftedTypeKindTyConKey = True
   | otherwise                          = False
@@ -632,8 +641,28 @@ isLiftedRuntimeRep :: Type -> Bool
 -- False of type variables (a :: RuntimeRep)
 --   and of other reps e.g. (IntRep :: RuntimeRep)
 isLiftedRuntimeRep rep
-  | TyConApp rr_tc args <- coreFullView rep
-  , rr_tc `hasKey` liftedRepDataConKey = ASSERT( null args ) True
+  | Just rep' <- coreView rep
+  = isLiftedRuntimeRep rep'
+  | TyConApp rr_tc [rr_arg] <- rep
+  , rr_tc `hasKey` boxedRepDataConKey
+  = isLiftedLevity rr_arg
+  | 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.
@@ -650,27 +679,47 @@ isUnliftedRuntimeRep :: Type -> Bool
 -- False of           (LiftedRep :: RuntimeRep)
 --   and of variables (a :: RuntimeRep)
 isUnliftedRuntimeRep rep
-  | TyConApp rr_tc _ <- coreFullView rep   -- NB: args might be non-empty
-                                           --     e.g. TupleRep [r1, .., rn]
-  = isPromotedDataCon rr_tc && not (rr_tc `hasKey` liftedRepDataConKey)
+  | 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 =
+      -- NB: args might be non-empty e.g. TupleRep [r1, .., rn]
+      if (rr_tc `hasKey` boxedRepDataConKey)
+        then case args of
+          [lev] -> isUnliftedLevity lev
+          _     -> False
+        else True
         -- Avoid searching all the unlifted RuntimeRep type cons
         -- In the RuntimeRep data type, only LiftedRep is lifted
-        -- But be careful of type families (F tys) :: RuntimeRep
-  | otherwise {- Variables, applications -}
-  = False
+        -- But be careful of type families (F tys) :: RuntimeRep,
+        -- hence the isPromotedDataCon rr_tc
+isUnliftedRuntimeRep _ = False
 
 -- | Is this the type 'RuntimeRep'?
 isRuntimeRepTy :: Type -> Bool
 isRuntimeRepTy ty
-  | TyConApp tc args <- coreFullView ty
+  | Just ty' <- coreView ty        = isRuntimeRepTy ty'
+  | TyConApp tc args <- ty
   , tc `hasKey` runtimeRepTyConKey = ASSERT( null args ) True
+  | otherwise                      = False
 
-  | otherwise = False
+-- | 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
 
 -- | Is a tyvar of type 'RuntimeRep'?
 isRuntimeRepVar :: TyVar -> Bool
 isRuntimeRepVar = isRuntimeRepTy . tyVarKind
 
+-- | Is a tyvar of type 'Levity'?
+isLevityVar :: TyVar -> Bool
+isLevityVar = isLevityTy . tyVarKind
+
 -- | Is this the type 'Multiplicity'?
 isMultiplicityTy :: Type -> Bool
 isMultiplicityTy ty
@@ -1499,7 +1548,7 @@ mkTyConTy tycon = tyConNullaryTy tycon
 -- its arguments.  Applies its arguments to the constructor from left to right.
 mkTyConApp :: TyCon -> [Type] -> Type
 mkTyConApp tycon tys
-  | [] <- tys
+  | null tys
   = mkTyConTy tycon
 
   | isFunTyCon tycon
@@ -1515,6 +1564,75 @@ mkTyConApp tycon tys
   | otherwise
   = TyConApp tycon tys
 
+{-
+Note [Prefer Type over TYPE 'LiftedRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The Core of nearly any program will have numerous occurrences of
+@TYPE 'LiftedRep@ (and, equivalently, 'Type') floating about. Concretely, while
+investigating #17292 we found that these constituting a majority of TyConApp
+constructors on the heap:
+
+```
+(From a sample of 100000 TyConApp closures)
+0x45f3523    - 28732 - `Type`
+0x420b840702 - 9629  - generic type constructors
+0x42055b7e46 - 9596
+0x420559b582 - 9511
+0x420bb15a1e - 9509
+0x420b86c6ba - 9501
+0x42055bac1e - 9496
+0x45e68fd    - 538 - `TYPE ...`
+```
+
+Consequently, we try hard to ensure that operations on such types are
+efficient. Specifically, we strive to
+
+ a. Avoid heap allocation of such types
+ b. Use a small (shallow in the tree-depth sense) representation
+    for such types
+
+Goal (b) is particularly useful as it makes traversals (e.g. free variable
+traversal, substitution, and comparison) more efficient.
+Comparison in particular takes special advantage of nullary type synonym
+applications (e.g. things like @TyConApp typeTyCon []@), Note [Comparing
+nullary type synonyms] in "GHC.Core.Type".
+
+To accomplish these we use a number of tricks:
+
+ 1. Instead of representing the lifted kind as
+    @TyConApp tYPETyCon [liftedRepDataCon]@ we rather prefer to
+    use the 'GHC.Types.Type' type synonym (represented as a nullary TyConApp).
+    This serves goal (b) since there are no applied type arguments to traverse,
+    e.g., during comparison.
+
+ 2. We have a top-level binding to represent `TyConApp GHC.Types.Type []`
+    (namely 'GHC.Builtin.Types.Prim.liftedTypeKind'), ensuring that we
+    don't need to allocate such types (goal (a)).
+
+ 3. We use the sharing mechanism described in Note [Sharing nullary TyConApps]
+    in GHC.Core.TyCon to ensure that we never need to allocate such
+    nullary applications (goal (a)).
+
+See #17958.
+-}
+
+
+-- | Given a @RuntimeRep@, applies @TYPE@ to it.
+-- See Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim.
+tYPE :: Type -> Type
+tYPE rr@(TyConApp tc [arg])
+  -- See Note [Prefer Type of TYPE 'LiftedRep]
+  | tc `hasKey` boxedRepDataConKey
+  , TyConApp tc' [] <- arg
+  = if | tc' `hasKey` liftedDataConKey   -> liftedTypeKind   -- TYPE (BoxedRep 'Lifted)
+       | tc' `hasKey` unliftedDataConKey -> unliftedTypeKind -- TYPE (BoxedRep 'Unlifted)
+       | otherwise                       -> TyConApp tYPETyCon [rr]
+  | tc == liftedRepTyCon                               -- TYPE LiftedRep
+  = liftedTypeKind
+  | tc == unliftedRepTyCon                             -- TYPE UnliftedRep
+  = unliftedTypeKind
+tYPE rr = TyConApp tYPETyCon [rr]
+
 
 {-
 --------------------------------------------------------------------
diff --git a/compiler/GHC/Core/Type.hs-boot b/compiler/GHC/Core/Type.hs-boot
index 8afa22c771..c38f6fc89d 100644
--- a/compiler/GHC/Core/Type.hs-boot
+++ b/compiler/GHC/Core/Type.hs-boot
@@ -21,6 +21,7 @@ tcView :: Type -> Maybe Type
 isRuntimeRepTy :: Type -> Bool
 isMultiplicityTy :: Type -> Bool
 isLiftedTypeKind :: Type -> Bool
+tYPE :: Type -> Type
 
 splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
 tyConAppTyCon_maybe :: Type -> Maybe TyCon
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 67f27410e8..eaba819a74 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -77,8 +77,9 @@ import GHC.Prelude
 
 import {-# SOURCE #-} GHC.Builtin.Types
                                  ( coercibleTyCon, heqTyCon
-                                 , liftedRepDataConTyCon, tupleTyConName
-                                 , manyDataConTyCon, oneDataConTyCon )
+                                 , tupleTyConName
+                                 , manyDataConTyCon, oneDataConTyCon
+                                 , liftedRepTyCon )
 import {-# SOURCE #-} GHC.Core.Type ( isRuntimeRepTy, isMultiplicityTy )
 
 import GHC.Core.TyCon hiding ( pprPromotionQuote )
@@ -414,16 +415,36 @@ IfaceHoleCo to ensure that they don't end up in an interface file.
 ifaceTyConHasKey :: IfaceTyCon -> Unique -> Bool
 ifaceTyConHasKey tc key = ifaceTyConName tc `hasKey` key
 
+-- | Given a kind K, is K of the form (TYPE ('BoxedRep 'LiftedRep))?
 isIfaceLiftedTypeKind :: IfaceKind -> Bool
 isIfaceLiftedTypeKind (IfaceTyConApp tc IA_Nil)
   = isLiftedTypeKindTyConName (ifaceTyConName tc)
-isIfaceLiftedTypeKind (IfaceTyConApp tc
-                       (IA_Arg (IfaceTyConApp ptr_rep_lifted IA_Nil)
-                               Required IA_Nil))
-  =  tc `ifaceTyConHasKey` tYPETyConKey
-  && ptr_rep_lifted `ifaceTyConHasKey` liftedRepDataConKey
+isIfaceLiftedTypeKind (IfaceTyConApp tc1 args1)
+  = isIfaceTyConAppLiftedTypeKind tc1 args1
 isIfaceLiftedTypeKind _ = False
 
+-- | Given a kind constructor K and arguments A, returns true if
+-- both of the following statements are true:
+--
+-- * K is TYPE
+-- * A is a singleton IfaceAppArgs of the form ('BoxedRep 'Lifted)
+--
+-- For the second condition, we must also check for the type
+-- synonym LiftedRep.
+isIfaceTyConAppLiftedTypeKind :: IfaceTyCon -> IfaceAppArgs -> Bool
+isIfaceTyConAppLiftedTypeKind tc1 args1
+  | tc1 `ifaceTyConHasKey` tYPETyConKey
+  , IA_Arg soleArg1 Required IA_Nil <- args1
+  , IfaceTyConApp rep args2 <- soleArg1 =
+    if | rep `ifaceTyConHasKey` boxedRepDataConKey
+       , IA_Arg soleArg2 Required IA_Nil <- args2
+       , IfaceTyConApp lev IA_Nil <- soleArg2
+       , lev `ifaceTyConHasKey` liftedDataConKey -> True
+       | rep `ifaceTyConHasKey` liftedRepTyConKey
+       , IA_Nil <- args2 -> True
+       | otherwise -> False
+  | otherwise = False
+
 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
 -- Mainly for printing purposes
 --
@@ -1081,11 +1102,14 @@ defaultNonStandardVars do_runtimereps do_multiplicities ty = go False emptyFsEnv
         | do_multiplicities, tc `ifaceTyConHasKey` multiplicityTyConKey = Just many_ty
     check_substitution _ = Nothing
 
+-- | The type ('BoxedRep 'Lifted), also known as LiftedRep.
 liftedRep_ty :: IfaceType
 liftedRep_ty =
-    IfaceTyConApp (IfaceTyCon dc_name (IfaceTyConInfo IsPromoted IfaceNormalTyCon))
-                  IA_Nil
-  where dc_name = getName liftedRepDataConTyCon
+  IfaceTyConApp liftedRep IA_Nil
+  where
+    liftedRep :: IfaceTyCon
+    liftedRep = IfaceTyCon tc_name (IfaceTyConInfo NotPromoted IfaceNormalTyCon)
+      where tc_name = getName liftedRepTyCon
 
 many_ty :: IfaceType
 many_ty =
@@ -1409,9 +1433,7 @@ pprTyTcApp ctxt_prec tc tys =
        , isInvisibleArgFlag argf
        -> pprIfaceTyList ctxt_prec ty1 ty2
 
-       | tc `ifaceTyConHasKey` tYPETyConKey
-       , IA_Arg (IfaceTyConApp rep IA_Nil) Required IA_Nil <- tys
-       , rep `ifaceTyConHasKey` liftedRepDataConKey
+       | isIfaceTyConAppLiftedTypeKind tc tys
        , print_type_abbreviations  -- See Note [Printing type abbreviations]
        -> ppr_kind_type ctxt_prec
 
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 82dbd65848..f5641766d3 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1793,7 +1793,9 @@ headline_eq_msg :: Bool -> Ct -> Type -> Type -> SDoc
 headline_eq_msg add_ea ct ty1 ty2
 
   | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) ||
-    (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1)
+    (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1) ||
+    (isLiftedLevity ty1 && isUnliftedLevity ty2) ||
+    (isLiftedLevity ty2 && isUnliftedLevity ty1)
   = text "Couldn't match a lifted type with an unlifted type"
 
   | isAtomicTy ty1 || isAtomicTy ty2
diff --git a/compiler/GHC/Tc/Instance/Typeable.hs b/compiler/GHC/Tc/Instance/Typeable.hs
index 0f0b7a0a11..6c4aeaeb49 100644
--- a/compiler/GHC/Tc/Instance/Typeable.hs
+++ b/compiler/GHC/Tc/Instance/Typeable.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiWayIf #-}
 
 module GHC.Tc.Instance.Typeable(mkTypeableBinds, tyConIsTypeable) where
 
@@ -28,7 +29,7 @@ import GHC.Builtin.Names
 import GHC.Builtin.Types.Prim ( primTyCons )
 import GHC.Builtin.Types
                   ( tupleTyCon, sumTyCon, runtimeRepTyCon
-                  , vecCountTyCon, vecElemTyCon
+                  , levityTyCon, vecCountTyCon, vecElemTyCon
                   , nilDataCon, consDataCon )
 import GHC.Types.Name
 import GHC.Types.Id
@@ -175,7 +176,7 @@ mkTypeableBinds
        } } }
   where
     needs_typeable_binds tc
-      | tc `elem` [runtimeRepTyCon, vecCountTyCon, vecElemTyCon]
+      | tc `elem` [runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon]
       = False
       | otherwise =
           isAlgTyCon tc
@@ -351,7 +352,7 @@ mkPrimTypeableTodos
 -- Note [Built-in syntax and the OrigNameCache] in "GHC.Iface.Env" for more.
 ghcPrimTypeableTyCons :: [TyCon]
 ghcPrimTypeableTyCons = concat
-    [ [ runtimeRepTyCon, vecCountTyCon, vecElemTyCon ]
+    [ [ runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon ]
     , map (tupleTyCon Unboxed) [0..mAX_TUPLE_SIZE]
     , map sumTyCon [2..mAX_SUM_SIZE]
     , primTyCons
@@ -557,9 +558,9 @@ mkKindRepRhs :: TypeableStuff
              -> CmEnv       -- ^ in-scope kind variables
              -> Kind        -- ^ the kind we want a 'KindRep' for
              -> KindRepM (LHsExpr GhcTc) -- ^ RHS expression
-mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep
+mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep_shortcut
   where
-    new_kind_rep k
+    new_kind_rep_shortcut k
         -- We handle (TYPE LiftedRep) etc separately to make it
         -- clear to consumers (e.g. serializers) that there is
         -- a loop here (as TYPE :: RuntimeRep -> TYPE 'LiftedRep)
@@ -567,9 +568,20 @@ mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep
               -- Typeable respects the Constraint/Type distinction
               -- so do not follow the special case here
       , Just arg <- kindRep_maybe k
-      , Just (tc, []) <- splitTyConApp_maybe arg
-      , Just dc <- isPromotedDataCon_maybe tc
-      = return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon dc
+      = case splitTyConApp_maybe arg of
+          Just (tc, [])
+            | Just dc <- isPromotedDataCon_maybe tc
+              -> return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon dc
+
+          Just (rep, [levArg])
+            | Just dcRep <- isPromotedDataCon_maybe rep
+            , Just (lev, []) <- splitTyConApp_maybe levArg
+            , Just dcLev <- isPromotedDataCon_maybe lev
+              -> return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` (nlHsDataCon dcRep `nlHsApp` nlHsDataCon dcLev)
+
+          _   -> new_kind_rep k
+      | otherwise = new_kind_rep k
+
 
     new_kind_rep (TyVarTy v)
       | Just idx <- lookupCME in_scope v
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 1e82be0f0e..a3cda06cac 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1793,6 +1793,10 @@ defaultTyVar default_kind tv
   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
+  | isLevityVar tv
+  = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv)
+       ; writeMetaTyVar tv liftedDataConTy
+       ; return True }
   | isMultiplicityVar tv
   = do { traceTc "Defaulting a Multiplicty var to Many" (ppr tv)
        ; writeMetaTyVar tv manyDataConTy
diff --git a/compiler/GHC/Types/RepType.hs b/compiler/GHC/Types/RepType.hs
index 0ef8cfe9c9..2957dddb5d 100644
--- a/compiler/GHC/Types/RepType.hs
+++ b/compiler/GHC/Types/RepType.hs
@@ -361,10 +361,11 @@ but RuntimeRep has some extra cases:
 data RuntimeRep = VecRep VecCount VecElem   -- ^ a SIMD vector type
                 | TupleRep [RuntimeRep]     -- ^ An unboxed tuple of the given reps
                 | SumRep [RuntimeRep]       -- ^ An unboxed sum of the given reps
-                | LiftedRep       -- ^ lifted; represented by a pointer
-                | UnliftedRep     -- ^ unlifted; represented by a pointer
+                | BoxedRep Levity -- ^ boxed; represented by a pointer
                 | IntRep          -- ^ signed, word-sized value
                 ...etc...
+data Levity     = Lifted
+                | Unlifted
 
 It's all in 1-1 correspondence with PrimRep except for TupleRep and SumRep,
 which describe unboxed products and sums respectively. RuntimeRep is defined
@@ -374,6 +375,13 @@ program, so that every variable has a type that has a PrimRep. For
 example, unarisation transforms our utup function above, to take two Int
 arguments instead of one (# Int, Int #) argument.
 
+Also, note that boxed types are represented slightly differently in RuntimeRep
+and PrimRep. PrimRep just has the nullary LiftedRep and UnliftedRep data
+constructors. RuntimeRep has a BoxedRep data constructor, which accepts a
+Levity. The subtle distinction is that since BoxedRep can accept a variable
+argument, RuntimeRep can talk about levity polymorphic types. PrimRep, by
+contrast, cannot.
+
 See also Note [Getting from RuntimeRep to PrimRep] and Note [VoidRep].
 
 Note [VoidRep]
diff --git a/compiler/GHC/Utils/Binary.hs b/compiler/GHC/Utils/Binary.hs
index ce533ed127..5ee0806cc1 100644
--- a/compiler/GHC/Utils/Binary.hs
+++ b/compiler/GHC/Utils/Binary.hs
@@ -876,7 +876,6 @@ instance Binary (Bin a) where
   get bh = do i <- getWord32 bh; return (BinPtr (fromIntegral (i :: Word32)))
 
 
-
 -- -----------------------------------------------------------------------------
 -- Lazy reading/writing
 
diff --git a/compiler/GHC/Utils/Binary/Typeable.hs b/compiler/GHC/Utils/Binary/Typeable.hs
index c5b89bf35a..ebee92e211 100644
--- a/compiler/GHC/Utils/Binary/Typeable.hs
+++ b/compiler/GHC/Utils/Binary/Typeable.hs
@@ -22,6 +22,9 @@ import GHC.Prelude
 import GHC.Utils.Binary
 
 import GHC.Exts (TYPE, RuntimeRep(..), VecCount(..), VecElem(..))
+#if __GLASGOW_HASKELL__ >= 901
+import GHC.Exts (Levity(Lifted, Unlifted))
+#endif
 import GHC.Serialized
 
 import Foreign
@@ -115,8 +118,13 @@ instance Binary RuntimeRep where
     put_ bh (VecRep a b)    = putByte bh 0 >> put_ bh a >> put_ bh b
     put_ bh (TupleRep reps) = putByte bh 1 >> put_ bh reps
     put_ bh (SumRep reps)   = putByte bh 2 >> put_ bh reps
+#if __GLASGOW_HASKELL__ >= 901
+    put_ bh (BoxedRep Lifted)   = putByte bh 3
+    put_ bh (BoxedRep Unlifted) = putByte bh 4
+#else
     put_ bh LiftedRep       = putByte bh 3
     put_ bh UnliftedRep     = putByte bh 4
+#endif
     put_ bh IntRep          = putByte bh 5
     put_ bh WordRep         = putByte bh 6
     put_ bh Int64Rep        = putByte bh 7
@@ -139,8 +147,13 @@ instance Binary RuntimeRep where
           0  -> VecRep <$> get bh <*> get bh
           1  -> TupleRep <$> get bh
           2  -> SumRep <$> get bh
+#if __GLASGOW_HASKELL__ >= 901
+          3  -> pure (BoxedRep Lifted)
+          4  -> pure (BoxedRep Unlifted)
+#else
           3  -> pure LiftedRep
           4  -> pure UnliftedRep
+#endif
           5  -> pure IntRep
           6  -> pure WordRep
           7  -> pure Int64Rep
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index 5e0bf1c317..e8bd59f61a 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -13,6 +13,12 @@ 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``
+  will need to be updated.
+
+.. _Pointer Rep Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0203-pointer-rep.rst
 
 * Kind inference for data/newtype instance declarations is slightly
   more restrictive than before.  See the user manual :ref:`kind-inference-data-family-instances`.
diff --git a/docs/users_guide/exts/levity_polymorphism.rst b/docs/users_guide/exts/levity_polymorphism.rst
index a65f878b41..80a544e54b 100644
--- a/docs/users_guide/exts/levity_polymorphism.rst
+++ b/docs/users_guide/exts/levity_polymorphism.rst
@@ -13,21 +13,25 @@ Here are the key definitions, all available from ``GHC.Exts``: ::
 
   TYPE :: RuntimeRep -> Type   -- highly magical, built into GHC
 
-  data RuntimeRep = LiftedRep     -- for things like `Int`
-                  | UnliftedRep   -- for things like `Array#`
-                  | IntRep        -- for `Int#`
+  data Levity = Lifted    -- for things like `Int`
+              | Unlifted  -- for things like `Array#`
+
+  data RuntimeRep = BoxedRep Levity  -- for anything represented by a GC-managed pointer
+                  | IntRep           -- for `Int#`
                   | TupleRep [RuntimeRep]  -- unboxed tuples, indexed by the representations of the elements
                   | SumRep [RuntimeRep]    -- unboxed sums, indexed by the representations of the disjuncts
                   | ...
 
+  type LiftedRep = BoxedRep Lifted
+
   type Type = TYPE LiftedRep    -- Type is just an ordinary type synonym
 
 The idea is that we have a new fundamental type constant ``TYPE``, which
 is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE 'IntRep``
-and ``Bool :: TYPE 'LiftedRep``. Anything with a type of the form
+and ``Bool :: TYPE LiftedRep``. Anything with a type of the form
 ``TYPE x`` can appear to either side of a function arrow ``->``. We can
 thus say that ``->`` has type
-``TYPE r1 -> TYPE r2 -> TYPE 'LiftedRep``. The result is always lifted
+``TYPE r1 -> TYPE r2 -> TYPE LiftedRep``. The result is always lifted
 because all functions are lifted in GHC.
 
 .. _levity-polymorphic-restrictions:
@@ -102,13 +106,13 @@ Printing levity-polymorphic types
     :category: verbosity
 
     Print ``RuntimeRep`` parameters as they appear; otherwise, they are
-    defaulted to ``'LiftedRep``.
+    defaulted to ``LiftedRep``.
 
 Most GHC users will not need to worry about levity polymorphism
 or unboxed types. For these users, seeing the levity polymorphism
 in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
-by supposing all type variables of type ``RuntimeRep`` to be ``'LiftedRep``
-when printing, and printing ``TYPE 'LiftedRep`` as ``Type`` (or ``*`` when
+by supposing all type variables of type ``RuntimeRep`` to be ``LiftedRep``
+when printing, and printing ``TYPE LiftedRep`` as ``Type`` (or ``*`` when
 :extension:`StarIsType` is on).
 
 Should you wish to see levity polymorphism in your types, enable
diff --git a/docs/users_guide/exts/typed_holes.rst b/docs/users_guide/exts/typed_holes.rst
index 7ad2d633a5..f58f8475f2 100644
--- a/docs/users_guide/exts/typed_holes.rst
+++ b/docs/users_guide/exts/typed_holes.rst
@@ -443,7 +443,7 @@ it will additionally offer up a list of refinement hole fits, in this case: ::
       with const @Integer @[Integer]
       where const :: forall a b. a -> b -> a
     ($) (_ :: [Integer] -> Integer)
-      with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
+      with ($) @GHC.Types.LiftedRep @[Integer] @Integer
       where ($) :: forall a b. (a -> b) -> a -> b
     fail (_ :: String)
       with fail @((->) [Integer]) @Integer
diff --git a/libraries/base/Data/Typeable.hs b/libraries/base/Data/Typeable.hs
index 43c9aa187d..1c84c99021 100644
--- a/libraries/base/Data/Typeable.hs
+++ b/libraries/base/Data/Typeable.hs
@@ -89,6 +89,8 @@ module Data.Typeable
 
       -- * For backwards compatibility
     , typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7
+      -- Jank
+    , I.trLiftedRep
     ) where
 
 import qualified Data.Typeable.Internal as I
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 008ac1b81b..39974b4052 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE UnliftedFFITypes #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ViewPatterns #-}
@@ -79,7 +80,10 @@ module Data.Typeable.Internal (
     -- | These are for internal use only
     mkTrType, mkTrCon, mkTrApp, mkTrAppChecked, mkTrFun,
     mkTyCon, mkTyCon#,
-    typeSymbolTypeRep, typeNatTypeRep, typeCharTypeRep
+    typeSymbolTypeRep, typeNatTypeRep, typeCharTypeRep,
+
+    -- * For internal use
+    trLiftedRep
   ) where
 
 import GHC.Prim ( FUN )
@@ -375,7 +379,12 @@ mkTrCon tc kind_vars = TrTyCon
 -- constructor, so we need to build it here.
 fpTYPELiftedRep :: Fingerprint
 fpTYPELiftedRep = fingerprintFingerprints
-      [tyConFingerprint tyConTYPE, typeRepFingerprint trLiftedRep]
+      [ tyConFingerprint tyConTYPE
+      , fingerprintFingerprints
+        [ tyConFingerprint tyCon'BoxedRep
+        , tyConFingerprint tyCon'Lifted
+        ]
+      ]
 -- There is absolutely nothing to gain and everything to lose
 -- by inlining the worker. The wrapper should inline anyway.
 {-# NOINLINE fpTYPELiftedRep #-}
@@ -383,7 +392,7 @@ fpTYPELiftedRep = fingerprintFingerprints
 trTYPE :: TypeRep TYPE
 trTYPE = typeRep
 
-trLiftedRep :: TypeRep 'LiftedRep
+trLiftedRep :: TypeRep ('BoxedRep 'Lifted)
 trLiftedRep = typeRep
 
 trMany :: TypeRep 'Many
@@ -623,7 +632,7 @@ instantiateKindRep vars = go
       = SomeTypeRep $ mkTrApp (unsafeCoerceRep $ go f) (unsafeCoerceRep $ go a)
     go (KindRepFun a b)
       = SomeTypeRep $ mkTrFun trMany (unsafeCoerceRep $ go a) (unsafeCoerceRep $ go b)
-    go (KindRepTYPE LiftedRep) = SomeTypeRep TrType
+    go (KindRepTYPE (BoxedRep Lifted)) = SomeTypeRep TrType
     go (KindRepTYPE r) = unkindedTypeRep $ tYPE `kApp` runtimeRepTypeRep r
     go (KindRepTypeLitS sort s)
       = mkTypeLitFromString sort (unpackCStringUtf8# s)
@@ -662,8 +671,9 @@ buildList = foldr cons nil
 runtimeRepTypeRep :: RuntimeRep -> SomeKindedTypeRep RuntimeRep
 runtimeRepTypeRep r =
     case r of
-      LiftedRep   -> rep @'LiftedRep
-      UnliftedRep -> rep @'UnliftedRep
+      BoxedRep Lifted -> SomeKindedTypeRep trLiftedRep
+      BoxedRep v  -> kindedTypeRep @_ @'BoxedRep
+                     `kApp` levityTypeRep v
       VecRep c e  -> kindedTypeRep @_ @'VecRep
                      `kApp` vecCountTypeRep c
                      `kApp` vecElemTypeRep e
@@ -688,6 +698,15 @@ runtimeRepTypeRep r =
     rep :: forall (a :: RuntimeRep). Typeable a => SomeKindedTypeRep RuntimeRep
     rep = kindedTypeRep @RuntimeRep @a
 
+levityTypeRep :: Levity -> SomeKindedTypeRep Levity
+levityTypeRep c =
+    case c of
+      Lifted   -> rep @'Lifted
+      Unlifted -> rep @'Unlifted
+  where
+    rep :: forall (a :: Levity). Typeable a => SomeKindedTypeRep Levity
+    rep = kindedTypeRep @Levity @a
+
 vecCountTypeRep :: VecCount -> SomeKindedTypeRep VecCount
 vecCountTypeRep c =
     case c of
@@ -840,13 +859,40 @@ splitApps = go []
 -- produce a TypeRep for without difficulty), and then just substitute in the
 -- appropriate module and constructor names.
 --
+-- Prior to the introduction of BoxedRep, this was bad, but now it is
+-- even worse! We have to construct several different TyCons by hand
+-- so that we can build the fingerprint for TYPE ('BoxedRep 'LiftedRep).
+-- If we call `typeRep @('BoxedRep 'LiftedRep)` while trying to compute
+-- the fingerprint of `TYPE ('BoxedRep 'LiftedRep)`, we get a loop.
+--
 -- The ticket to find a better way to deal with this is
 -- #14480.
+
+tyConRuntimeRep :: TyCon
+tyConRuntimeRep = mkTyCon ghcPrimPackage "GHC.Types" "RuntimeRep" 0
+  (KindRepTYPE (BoxedRep Lifted))
+
 tyConTYPE :: TyCon
-tyConTYPE = mkTyCon (tyConPackage liftedRepTyCon) "GHC.Prim" "TYPE" 0
-       (KindRepFun (KindRepTyConApp liftedRepTyCon []) (KindRepTYPE LiftedRep))
-  where
-    liftedRepTyCon = typeRepTyCon (typeRep @RuntimeRep)
+tyConTYPE = mkTyCon ghcPrimPackage "GHC.Prim" "TYPE" 0
+    (KindRepFun
+      (KindRepTyConApp tyConRuntimeRep [])
+      (KindRepTYPE (BoxedRep Lifted))
+    )
+
+tyConLevity :: TyCon
+tyConLevity = mkTyCon ghcPrimPackage "GHC.Types" "Levity" 0
+  (KindRepTYPE (BoxedRep Lifted))
+
+tyCon'Lifted :: TyCon
+tyCon'Lifted = mkTyCon ghcPrimPackage "GHC.Types" "'Lifted" 0
+  (KindRepTyConApp tyConLevity [])
+
+tyCon'BoxedRep :: TyCon
+tyCon'BoxedRep = mkTyCon ghcPrimPackage "GHC.Types" "'BoxedRep" 0
+  (KindRepFun (KindRepTyConApp tyConLevity []) (KindRepTyConApp tyConRuntimeRep []))
+
+ghcPrimPackage :: String
+ghcPrimPackage = tyConPackage (typeRepTyCon (typeRep @Bool))
 
 funTyCon :: TyCon
 funTyCon = typeRepTyCon (typeRep @(->))
diff --git a/libraries/base/GHC/Enum.hs b/libraries/base/GHC/Enum.hs
index d107c1eb12..02b3d0e784 100644
--- a/libraries/base/GHC/Enum.hs
+++ b/libraries/base/GHC/Enum.hs
@@ -1005,6 +1005,11 @@ enumNegDeltaToNatural x0 ndelta lim = go x0
 
 -- Instances from GHC.Types
 
+-- | @since 4.16.0.0
+deriving instance Bounded Levity
+-- | @since 4.16.0.0
+deriving instance Enum Levity
+
 -- | @since 4.10.0.0
 deriving instance Bounded VecCount
 -- | @since 4.10.0.0
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index 106c7e9ea6..4b88d34c63 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -90,7 +90,8 @@ module GHC.Exts
         type (~~),
 
         -- * Representation polymorphism
-        GHC.Prim.TYPE, RuntimeRep(..), VecCount(..), VecElem(..),
+        GHC.Prim.TYPE, RuntimeRep(..), LiftedRep, Levity(..),
+        VecCount(..), VecElem(..),
 
         -- * Transform comprehensions
         Down(..), groupWith, sortWith, the,
diff --git a/libraries/base/GHC/Show.hs b/libraries/base/GHC/Show.hs
index 97d6ad31c7..0d90006432 100644
--- a/libraries/base/GHC/Show.hs
+++ b/libraries/base/GHC/Show.hs
@@ -598,6 +598,9 @@ instance Show KindRep where
       . showString " "
       . showsPrec 11 q
 
+-- | @since 4.15.0.0
+deriving instance Show Levity
+
 -- | @since 4.11.0.0
 deriving instance Show RuntimeRep
 
diff --git a/libraries/base/Unsafe/Coerce.hs b/libraries/base/Unsafe/Coerce.hs
index 7c8e39e92e..1341a4d1d7 100644
--- a/libraries/base/Unsafe/Coerce.hs
+++ b/libraries/base/Unsafe/Coerce.hs
@@ -285,7 +285,7 @@ unsafeEqualityProof = case unsafeEqualityProof @a @b of UnsafeRefl -> UnsafeRefl
 unsafeCoerce :: forall (a :: Type) (b :: Type) . a -> b
 unsafeCoerce x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
 
-unsafeCoerceUnlifted :: forall (a :: TYPE 'UnliftedRep) (b :: TYPE 'UnliftedRep) . a -> b
+unsafeCoerceUnlifted :: forall (a :: TYPE ('BoxedRep 'Unlifted)) (b :: TYPE ('BoxedRep 'Unlifted)) . a -> b
 -- Kind-homogeneous, but levity monomorphic (TYPE UnliftedRep)
 unsafeCoerceUnlifted x = case unsafeEqualityProof @a @b of UnsafeRefl -> x
 
diff --git a/libraries/base/tests/T11334a.hs b/libraries/base/tests/T11334a.hs
index 0cf91eaa2a..ad296967a7 100644
--- a/libraries/base/tests/T11334a.hs
+++ b/libraries/base/tests/T11334a.hs
@@ -7,5 +7,5 @@ import GHC.Types
 main :: IO ()
 main = do
   print (typeOf (Proxy :: Proxy 'Just))
-  print (typeOf (Proxy :: Proxy (TYPE 'LiftedRep)))
-  print (typeOf (Proxy :: Proxy (TYPE 'UnliftedRep)))
+  print (typeOf (Proxy :: Proxy (TYPE ('BoxedRep 'Lifted))))
+  print (typeOf (Proxy :: Proxy (TYPE ('BoxedRep 'Unlifted))))
diff --git a/libraries/base/tests/T11334a.stdout b/libraries/base/tests/T11334a.stdout
index c2d860d653..b46a92d366 100644
--- a/libraries/base/tests/T11334a.stdout
+++ b/libraries/base/tests/T11334a.stdout
@@ -1,3 +1,3 @@
 Proxy (* -> Maybe *) ('Just *)
 Proxy * *
-Proxy * (TYPE 'UnliftedRep)
+Proxy * (TYPE ('BoxedRep 'Unlifted))
diff --git a/libraries/binary b/libraries/binary
-Subproject d0c3f06716be373e4195535a76f94f1bba8ab97
+Subproject 6d3cb9fdc961cc6cce23860d74316c635ed9094
diff --git a/libraries/ghc-heap/GHC/Exts/Heap.hs b/libraries/ghc-heap/GHC/Exts/Heap.hs
index 10a9ea8be9..1e429ca054 100644
--- a/libraries/ghc-heap/GHC/Exts/Heap.hs
+++ b/libraries/ghc-heap/GHC/Exts/Heap.hs
@@ -91,10 +91,18 @@ class HasHeapRep (a :: TYPE rep) where
         -> IO Closure
         -- ^ Heap representation of the closure.
 
+#if __GLASGOW_HASKELL__ >= 901
+instance HasHeapRep (a :: TYPE ('BoxedRep 'Lifted)) where
+#else
 instance HasHeapRep (a :: TYPE 'LiftedRep) where
+#endif
     getClosureData = getClosureDataFromHeapObject
 
+#if __GLASGOW_HASKELL__ >= 901
+instance HasHeapRep (a :: TYPE ('BoxedRep 'Unlifted)) where
+#else
 instance HasHeapRep (a :: TYPE 'UnliftedRep) where
+#endif
     getClosureData x = getClosureDataFromHeapObject (unsafeCoerce# x)
 
 instance Int# ~ a => HasHeapRep (a :: TYPE 'IntRep) where
diff --git a/libraries/ghc-heap/tests/ClosureSizeUtils.hs b/libraries/ghc-heap/tests/ClosureSizeUtils.hs
index 5fafa4f7a5..3b1578451a 100644
--- a/libraries/ghc-heap/tests/ClosureSizeUtils.hs
+++ b/libraries/ghc-heap/tests/ClosureSizeUtils.hs
@@ -30,7 +30,7 @@ assertSize x =
   assertSizeBox (asBox x) (typeRep @a)
 
 assertSizeUnlifted
-  :: forall (a :: TYPE 'UnliftedRep). (HasCallStack, Typeable a)
+  :: forall (a :: TYPE ('BoxedRep 'Unlifted)). (HasCallStack, Typeable a)
   => a     -- ^ closure
   -> Int   -- ^ expected size in words
   -> IO ()
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index f558619ac1..59edeec8af 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -33,7 +33,9 @@ module GHC.Types (
         Symbol,
         Any,
         type (~~), Coercible,
-        TYPE, RuntimeRep(..), Type, Constraint,
+        TYPE, Levity(..), RuntimeRep(..),
+        LiftedRep, UnliftedRep,
+        Type, UnliftedType, Constraint,
           -- The historical type * should ideally be written as
           -- `type *`, without the parentheses. But that's a true
           -- pain to parse, and for little gain.
@@ -85,8 +87,17 @@ type (->) = FUN 'Many
 -- | The kind of constraints, like @Show a@
 data Constraint
 
+-- | The runtime representation of lifted types.
+type LiftedRep = 'BoxedRep 'Lifted
+
+-- | The runtime representation of unlifted types.
+type UnliftedRep = 'BoxedRep 'Unlifted
+
 -- | The kind of types with lifted values. For example @Int :: Type@.
-type Type = TYPE 'LiftedRep
+type Type = TYPE LiftedRep
+
+-- | The kind of types with unlifted values. For example @Int# :: UnliftedType@.
+type UnliftedType = TYPE UnliftedRep
 
 data Multiplicity = Many | One
 
@@ -410,6 +421,8 @@ data SPEC = SPEC | SPEC2
 *                                                                      *
 ********************************************************************* -}
 
+-- | Whether a boxed type is lifted or unlifted.
+data Levity = Lifted | Unlifted
 
 -- | GHC maintains a property that the kind of all inhabited types
 -- (as distinct from type constructors or type-level data) tells us
@@ -425,8 +438,7 @@ data SPEC = SPEC | SPEC2
 data RuntimeRep = VecRep VecCount VecElem   -- ^ a SIMD vector type
                 | TupleRep [RuntimeRep]     -- ^ An unboxed tuple of the given reps
                 | SumRep [RuntimeRep]       -- ^ An unboxed sum of the given reps
-                | LiftedRep       -- ^ lifted; represented by a pointer
-                | UnliftedRep     -- ^ unlifted; represented by a pointer
+                | BoxedRep Levity -- ^ boxed; represented by a pointer
                 | IntRep          -- ^ signed, word-sized value
                 | Int8Rep         -- ^ signed,  8-bit value
                 | Int16Rep        -- ^ signed, 16-bit value
@@ -444,6 +456,7 @@ data RuntimeRep = VecRep VecCount VecElem   -- ^ a SIMD vector type
 -- RuntimeRep is intimately tied to TyCon.RuntimeRep (in GHC proper). See
 -- Note [RuntimeRep and PrimRep] in RepType.
 -- See also Note [Wiring in RuntimeRep] in GHC.Builtin.Types
+-- See also Note [TYPE and RuntimeRep] in GHC.Builtin.Type.Prim
 
 -- | Length of a SIMD vector type
 data VecCount = Vec2
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index 6508c07a65..3cb5a44ee8 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -61,6 +61,10 @@ import Foreign.ForeignPtr
 import Foreign.C.String
 import Foreign.C.Types
 
+#if __GLASGOW_HASKELL__ >= 901
+import GHC.Types ( Levity(..) )
+#endif
+
 -----------------------------------------------------
 --
 --              The Quasi class
@@ -816,7 +820,11 @@ class Lift (t :: TYPE r) where
   -- | Turn a value into a Template Haskell expression, suitable for use in
   -- a splice.
   lift :: Quote m => t -> m Exp
+#if __GLASGOW_HASKELL__ >= 901
+  default lift :: (r ~ ('BoxedRep 'Lifted), Quote m) => t -> m Exp
+#else
   default lift :: (r ~ 'LiftedRep, Quote m) => t -> m Exp
+#endif
   lift = unTypeCode . liftTyped
 
   -- | Turn a value into a Template Haskell typed expression, suitable for use
diff --git a/testsuite/tests/backpack/should_run/T13955.bkp b/testsuite/tests/backpack/should_run/T13955.bkp
index a7d447f169..eadeee6f5c 100644
--- a/testsuite/tests/backpack/should_run/T13955.bkp
+++ b/testsuite/tests/backpack/should_run/T13955.bkp
@@ -18,7 +18,7 @@ unit number-unknown where
 unit number-int where
   module NumberUnknown where
     import GHC.Types
-    type Rep = LiftedRep
+    type Rep = 'BoxedRep 'Lifted
     type Number = Int
     plus :: Int -> Int -> Int
     plus = (+)
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
index 6c74e10a7c..90a72c2a9a 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
@@ -14,12 +14,14 @@ import Data.Type.Bool
 import Data.Type.Equality hiding ((:~~:)(..))
 import GHC.TypeLits
 import Data.Proxy
-import GHC.Exts
+import GHC.Exts hiding (Lifted, BoxedRep)
 import Data.Kind
 import Unsafe.Coerce
 import Data.Char
 import Data.Maybe
 
+import qualified GHC.Exts as Exts
+
 -------------------------------
 -- Utilities
 
@@ -82,7 +84,9 @@ data TyCon (a :: k) where
   Arrow :: TyCon (->)
   TYPE  :: TyCon TYPE
   RuntimeRep :: TyCon RuntimeRep
-  LiftedRep' :: TyCon 'LiftedRep
+  Levity :: TyCon Levity
+  BoxedRep :: TyCon 'Exts.BoxedRep
+  Lifted :: TyCon 'Exts.Lifted
   -- If extending, add to eqTyCon too
 
 eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
@@ -94,7 +98,9 @@ eqTyCon Maybe Maybe = Just HRefl
 eqTyCon Arrow Arrow = Just HRefl
 eqTyCon TYPE TYPE = Just HRefl
 eqTyCon RuntimeRep RuntimeRep = Just HRefl
-eqTyCon LiftedRep' LiftedRep' = Just HRefl
+eqTyCon Levity Levity = Just HRefl
+eqTyCon BoxedRep BoxedRep = Just HRefl
+eqTyCon Lifted Lifted = Just HRefl
 eqTyCon _ _ = Nothing
 
 -- Check whether or not a type is really a plain old tycon;
@@ -212,8 +218,10 @@ instance TyConAble []        where tyCon = List
 instance TyConAble Maybe     where tyCon = Maybe
 instance TyConAble (->)      where tyCon = Arrow
 instance TyConAble TYPE      where tyCon = TYPE
-instance TyConAble 'LiftedRep   where tyCon = LiftedRep'
-instance TyConAble RuntimeRep    where tyCon = RuntimeRep
+instance TyConAble 'Exts.Lifted    where tyCon = Lifted
+instance TyConAble 'Exts.BoxedRep  where tyCon = BoxedRep
+instance TyConAble RuntimeRep      where tyCon = RuntimeRep
+instance TyConAble Levity          where tyCon = Levity
 
 -- Can't just define Typeable the way we want, because the instances
 -- overlap. So we have to mock up instance chains via closed type families.
diff --git a/testsuite/tests/dependent/should_fail/T17131.stderr b/testsuite/tests/dependent/should_fail/T17131.stderr
index daad6ac054..b2af8ab7b8 100644
--- a/testsuite/tests/dependent/should_fail/T17131.stderr
+++ b/testsuite/tests/dependent/should_fail/T17131.stderr
@@ -1,9 +1,9 @@
 
 T17131.hs:12:34: error:
     • Couldn't match kind: TypeReps xs
-                     with: '[ 'LiftedRep]
+                     with: '[ 'BoxedRep 'Lifted]
       Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
-        but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
+        but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'BoxedRep 'Lifted])’
       The type variable ‘xs’ is ambiguous
     • In the type ‘(# a #)’
       In the type family declaration for ‘Tuple#’
diff --git a/testsuite/tests/deriving/should_compile/T13154b.hs b/testsuite/tests/deriving/should_compile/T13154b.hs
index 9df828b111..585f010eba 100644
--- a/testsuite/tests/deriving/should_compile/T13154b.hs
+++ b/testsuite/tests/deriving/should_compile/T13154b.hs
@@ -24,10 +24,10 @@ deriving instance Foo1 a
 class Foo2 (a :: TYPE ('TupleRep '[]))
 deriving instance Foo2 (##)
 
-class Foo3 (a :: TYPE ('SumRep '[ 'LiftedRep, 'LiftedRep ]))
+class Foo3 (a :: TYPE ('SumRep '[ 'BoxedRep 'Lifted, 'BoxedRep 'Lifted ]))
 deriving instance Foo3 a
 
-class Foo4 (a :: TYPE ('SumRep '[ 'LiftedRep, 'LiftedRep ]))
+class Foo4 (a :: TYPE ('SumRep '[ 'BoxedRep 'Lifted, 'BoxedRep 'Lifted ]))
 deriving instance Foo4 (# a | b #)
 
 class Foo5 (a :: Type)
diff --git a/testsuite/tests/deriving/should_fail/T12512.hs b/testsuite/tests/deriving/should_fail/T12512.hs
index 804bfd31da..61410d84cf 100644
--- a/testsuite/tests/deriving/should_fail/T12512.hs
+++ b/testsuite/tests/deriving/should_fail/T12512.hs
@@ -6,8 +6,8 @@ module T12512 where
 
 import GHC.Exts
 
-class Wat1 (a :: TYPE ('TupleRep ['LiftedRep, 'LiftedRep]))
+class Wat1 (a :: TYPE ('TupleRep ['BoxedRep 'Lifted, 'BoxedRep 'Lifted]))
 deriving instance Wat1 (# a, b #)
 
-class Wat2 (a :: TYPE ('SumRep ['LiftedRep, 'LiftedRep]))
+class Wat2 (a :: TYPE ('SumRep ['BoxedRep 'Lifted, 'BoxedRep 'Lifted]))
 deriving instance Wat2 (# a | b #)
diff --git a/testsuite/tests/ffi/should_run/T16650a.hs b/testsuite/tests/ffi/should_run/T16650a.hs
index 3424a2c4f2..e14954d3ee 100644
--- a/testsuite/tests/ffi/should_run/T16650a.hs
+++ b/testsuite/tests/ffi/should_run/T16650a.hs
@@ -27,7 +27,7 @@ foreign import ccall unsafe "head_bytearray"
   c_head_bytearray :: MutableByteArray# RealWorld -> IO Word8
 
 data Box :: Type where
-  Box :: (Any :: TYPE 'UnliftedRep) -> Box
+  Box :: (Any :: TYPE ('BoxedRep 'Unlifted)) -> Box
 
 data MutableByteArray :: Type where
   MutableByteArray :: MutableByteArray# RealWorld -> MutableByteArray
diff --git a/testsuite/tests/ffi/should_run/T16650b.hs b/testsuite/tests/ffi/should_run/T16650b.hs
index 06ffcb1d5e..e1537c757d 100644
--- a/testsuite/tests/ffi/should_run/T16650b.hs
+++ b/testsuite/tests/ffi/should_run/T16650b.hs
@@ -31,7 +31,7 @@ foreign import ccall unsafe "is_doubleton_homogenous"
   c_is_doubleton_homogeneous :: MutableArrayArray# RealWorld -> IO Word8
 
 data Box :: Type where
-  Box :: (Any :: TYPE 'UnliftedRep) -> Box
+  Box :: (Any :: TYPE ('BoxedRep 'Unlifted)) -> Box
 
 -- An array of bytes
 data MutableByteArray :: Type where
diff --git a/testsuite/tests/ffi/should_run/T16650c.hs b/testsuite/tests/ffi/should_run/T16650c.hs
index 968731b3bd..0d8e9ac8ec 100644
--- a/testsuite/tests/ffi/should_run/T16650c.hs
+++ b/testsuite/tests/ffi/should_run/T16650c.hs
@@ -26,7 +26,7 @@ foreign import ccall unsafe "is_doubleton_homogenous"
     MutableArray# RealWorld a -> IO Word8
 
 data Box :: Type where
-  Box :: (Any :: TYPE 'UnliftedRep) -> Box
+  Box :: (Any :: TYPE ('BoxedRep 'Unlifted)) -> Box
 
 -- An array of unary integer functions
 data MutableArray :: Type where
diff --git a/testsuite/tests/ffi/should_run/T16650d.hs b/testsuite/tests/ffi/should_run/T16650d.hs
index 8bb4a4697b..874701b40a 100644
--- a/testsuite/tests/ffi/should_run/T16650d.hs
+++ b/testsuite/tests/ffi/should_run/T16650d.hs
@@ -26,7 +26,7 @@ foreign import ccall unsafe "is_doubleton_homogenous"
     SmallMutableArray# RealWorld a -> IO Word8
 
 data Box :: Type where
-  Box :: (Any :: TYPE 'UnliftedRep) -> Box
+  Box :: (Any :: TYPE ('BoxedRep 'Unlifted)) -> Box
 
 -- An array of unary integer functions
 data SmallMutableArray :: Type where
diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs
index 02a2c55c91..119324c28e 100644
--- a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs
+++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs
@@ -19,7 +19,7 @@ foreign import ccall unsafe "head_bytearray"
 foreign import ccall unsafe "head_bytearray"
   c_head_bytearray_b :: MyArray# -> IO Word8
 
-newtype MyArray# :: TYPE 'UnliftedRep where
+newtype MyArray# :: TYPE ('BoxedRep 'Unlifted) where
   MyArray# :: MutableByteArray# RealWorld -> MyArray#
 
 data MutableByteArray :: Type where
diff --git a/testsuite/tests/ghci/T18060/T18060.stdout b/testsuite/tests/ghci/T18060/T18060.stdout
index e60b6346a4..0d5d798db6 100644
--- a/testsuite/tests/ghci/T18060/T18060.stdout
+++ b/testsuite/tests/ghci/T18060/T18060.stdout
@@ -2,9 +2,6 @@ type (->) :: * -> * -> *
 type (->) = FUN 'Many :: * -> * -> *
   	-- Defined in ‘GHC.Types’
 infixr -1 ->
-instance Applicative ((->) r) -- Defined in ‘GHC.Base’
-instance Functor ((->) r) -- Defined in ‘GHC.Base’
-instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’
 type (~) :: forall k. k -> k -> Constraint
diff --git a/testsuite/tests/ghci/scripts/T12550.stdout b/testsuite/tests/ghci/scripts/T12550.stdout
index 05baf3e900..f5d6d7ba05 100644
--- a/testsuite/tests/ghci/scripts/T12550.stdout
+++ b/testsuite/tests/ghci/scripts/T12550.stdout
@@ -23,37 +23,12 @@ class Functor f where
   (<$) ∷ ∀ a b. a → f b → f a
   {-# MINIMAL fmap #-}
   	-- Defined in ‘GHC.Base’
-instance Functor V1 -- Defined in ‘GHC.Generics’
-instance Functor (URec Char) -- Defined in ‘GHC.Generics’
-instance Functor (URec Double) -- Defined in ‘GHC.Generics’
-instance Functor (URec Float) -- Defined in ‘GHC.Generics’
-instance Functor (URec Int) -- Defined in ‘GHC.Generics’
-instance Functor (URec Word) -- Defined in ‘GHC.Generics’
-instance Functor U1 -- Defined in ‘GHC.Generics’
-instance ∀ (f ∷ ★ → ★). Functor f ⇒ Functor (Rec1 f)
-  -- Defined in ‘GHC.Generics’
 instance Functor Par1 -- Defined in ‘GHC.Generics’
-instance ∀ i (c ∷ Meta) (f ∷ ★ → ★). Functor f ⇒ Functor (M1 i c f)
-  -- Defined in ‘GHC.Generics’
-instance ∀ i c. Functor (K1 i c) -- Defined in ‘GHC.Generics’
-instance ∀ (f ∷ ★ → ★) (g ∷ ★ → ★).
-         (Functor f, Functor g) ⇒
-         Functor (f :.: g)
-  -- Defined in ‘GHC.Generics’
-instance ∀ (f ∷ ★ → ★) (g ∷ ★ → ★).
-         (Functor f, Functor g) ⇒
-         Functor (f :+: g)
-  -- Defined in ‘GHC.Generics’
-instance ∀ (f ∷ ★ → ★) (g ∷ ★ → ★).
-         (Functor f, Functor g) ⇒
-         Functor (f :*: g)
-  -- Defined in ‘GHC.Generics’
 instance ∀ a. Functor (Either a) -- Defined in ‘Data.Either’
 instance Functor [] -- Defined in ‘GHC.Base’
 instance Functor Solo -- Defined in ‘GHC.Base’
 instance Functor Maybe -- Defined in ‘GHC.Base’
 instance Functor IO -- Defined in ‘GHC.Base’
-instance ∀ r. Functor ((->) r) -- Defined in ‘GHC.Base’
 instance ∀ a b c. Functor ((,,,) a b c) -- Defined in ‘GHC.Base’
 instance ∀ a b. Functor ((,,) a b) -- Defined in ‘GHC.Base’
 instance ∀ a. Functor ((,) a) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/T13963.script b/testsuite/tests/ghci/scripts/T13963.script
index c5e830aad1..030e8087a9 100644
--- a/testsuite/tests/ghci/scripts/T13963.script
+++ b/testsuite/tests/ghci/scripts/T13963.script
@@ -1,5 +1,5 @@
 :set -XPolyKinds -XDataKinds -XRankNTypes
-import GHC.Exts (TYPE, RuntimeRep(LiftedRep))
+import GHC.Exts (TYPE, RuntimeRep, LiftedRep)
 type Pair (a :: TYPE rep) (b :: TYPE rep') rep'' = forall (r :: TYPE rep''). (a -> b -> r)
 :kind Pair
 :kind Pair Int
diff --git a/testsuite/tests/ghci/scripts/T15941.stdout b/testsuite/tests/ghci/scripts/T15941.stdout
index f9e6d339f9..803aa9ebd0 100644
--- a/testsuite/tests/ghci/scripts/T15941.stdout
+++ b/testsuite/tests/ghci/scripts/T15941.stdout
@@ -1,4 +1,4 @@
 type T :: * -> * -> *
 type T =
-  (->) @{'GHC.Types.LiftedRep} @{'GHC.Types.LiftedRep} :: * -> * -> *
+  (->) @{GHC.Types.LiftedRep} @{GHC.Types.LiftedRep} :: * -> * -> *
   	-- Defined at <interactive>:2:1
diff --git a/testsuite/tests/ghci/scripts/T19310.stdout b/testsuite/tests/ghci/scripts/T19310.stdout
index 4e7ad631fc..943aa126dd 100644
--- a/testsuite/tests/ghci/scripts/T19310.stdout
+++ b/testsuite/tests/ghci/scripts/T19310.stdout
@@ -1,3 +1,3 @@
 type T :: * -> * -> *
-type T = (->) @{'LiftedRep} @{'LiftedRep} :: * -> * -> *
+type T = (->) @{LiftedRep} @{LiftedRep} :: * -> * -> *
   	-- Defined at <interactive>:3:1
diff --git a/testsuite/tests/ghci/scripts/T7627.stdout b/testsuite/tests/ghci/scripts/T7627.stdout
index b86ea432ff..2a2b8bd58f 100644
--- a/testsuite/tests/ghci/scripts/T7627.stdout
+++ b/testsuite/tests/ghci/scripts/T7627.stdout
@@ -37,8 +37,7 @@ instance (Bounded a, Bounded b) => Bounded (a, b)
 type (#,#) :: *
               -> *
               -> TYPE
-                   ('GHC.Types.TupleRep
-                      '[ 'GHC.Types.LiftedRep, 'GHC.Types.LiftedRep])
+                   ('GHC.Types.TupleRep '[GHC.Types.LiftedRep, GHC.Types.LiftedRep])
 data (#,#) a b = (#,#) a b
   	-- Defined in ‘GHC.Prim’
 (,) :: a -> b -> (a, b)
diff --git a/testsuite/tests/ghci/scripts/T8535.stdout b/testsuite/tests/ghci/scripts/T8535.stdout
index 5786372e9d..981124c9cb 100644
--- a/testsuite/tests/ghci/scripts/T8535.stdout
+++ b/testsuite/tests/ghci/scripts/T8535.stdout
@@ -2,8 +2,5 @@ type (->) :: * -> * -> *
 type (->) = FUN 'Many :: * -> * -> *
   	-- Defined in ‘GHC.Types’
 infixr -1 ->
-instance Applicative ((->) r) -- Defined in ‘GHC.Base’
-instance Functor ((->) r) -- Defined in ‘GHC.Base’
-instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/T8674.stdout b/testsuite/tests/ghci/scripts/T8674.stdout
index 7d7beeb1cd..ff0355b617 100644
--- a/testsuite/tests/ghci/scripts/T8674.stdout
+++ b/testsuite/tests/ghci/scripts/T8674.stdout
@@ -1,6 +1,5 @@
 type Sing :: forall k. k -> *
 data family Sing a
   	-- Defined at T8674.hs:4:1
-data instance Sing Bool = SBool 	-- Defined at T8674.hs:6:15
 data instance forall k (a :: [k]). Sing a = SNil
   	-- Defined at T8674.hs:5:15
diff --git a/testsuite/tests/ghci/scripts/ghci020.stdout b/testsuite/tests/ghci/scripts/ghci020.stdout
index 5786372e9d..981124c9cb 100644
--- a/testsuite/tests/ghci/scripts/ghci020.stdout
+++ b/testsuite/tests/ghci/scripts/ghci020.stdout
@@ -2,8 +2,5 @@ type (->) :: * -> * -> *
 type (->) = FUN 'Many :: * -> * -> *
   	-- Defined in ‘GHC.Types’
 infixr -1 ->
-instance Applicative ((->) r) -- Defined in ‘GHC.Base’
-instance Functor ((->) r) -- Defined in ‘GHC.Base’
-instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/should_run/T10145.stdout b/testsuite/tests/ghci/should_run/T10145.stdout
index 5786372e9d..981124c9cb 100644
--- a/testsuite/tests/ghci/should_run/T10145.stdout
+++ b/testsuite/tests/ghci/should_run/T10145.stdout
@@ -2,8 +2,5 @@ type (->) :: * -> * -> *
 type (->) = FUN 'Many :: * -> * -> *
   	-- Defined in ‘GHC.Types’
 infixr -1 ->
-instance Applicative ((->) r) -- Defined in ‘GHC.Base’
-instance Functor ((->) r) -- Defined in ‘GHC.Base’
-instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/should_run/T16096.stdout b/testsuite/tests/ghci/should_run/T16096.stdout
index 5826057d42..2749f06586 100644
--- a/testsuite/tests/ghci/should_run/T16096.stdout
+++ b/testsuite/tests/ghci/should_run/T16096.stdout
@@ -17,7 +17,7 @@ GHC.Base.returnIO
   (GHC.Types.:
      @()
      (Unsafe.Coerce.unsafeCoerce#
-        @'GHC.Types.LiftedRep @'GHC.Types.LiftedRep @[GHC.Types.Int] @() x)
+        @GHC.Types.LiftedRep @GHC.Types.LiftedRep @[GHC.Types.Int] @() x)
      (GHC.Types.[] @()))
 
 
@@ -40,7 +40,7 @@ GHC.Base.returnIO
   (GHC.Types.:
      @()
      (Unsafe.Coerce.unsafeCoerce#
-        @'GHC.Types.LiftedRep @'GHC.Types.LiftedRep @[GHC.Types.Int] @() x)
+        @GHC.Types.LiftedRep @GHC.Types.LiftedRep @[GHC.Types.Int] @() x)
      (GHC.Types.[] @()))
 
 
diff --git a/testsuite/tests/ghci/should_run/T18594.stdout b/testsuite/tests/ghci/should_run/T18594.stdout
index 9e2e79cd8b..d3219de45e 100644
--- a/testsuite/tests/ghci/should_run/T18594.stdout
+++ b/testsuite/tests/ghci/should_run/T18594.stdout
@@ -8,8 +8,8 @@ instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Semigroup b => Semigroup (a -> b) -- Defined in ‘GHC.Base’
 type Type :: *
-type Type = TYPE 'LiftedRep
+type Type = TYPE LiftedRep
   	-- Defined in ‘GHC.Types’
 type Type :: Type
-type Type = TYPE 'LiftedRep
+type Type = TYPE LiftedRep
   	-- Defined in ‘GHC.Types’
diff --git a/testsuite/tests/indexed-types/should_compile/T14111.hs b/testsuite/tests/indexed-types/should_compile/T14111.hs
index d1af549187..4e304e5d90 100644
--- a/testsuite/tests/indexed-types/should_compile/T14111.hs
+++ b/testsuite/tests/indexed-types/should_compile/T14111.hs
@@ -20,5 +20,5 @@ data family Maybe(x :: TYPE (r :: RuntimeRep))
 data instance Maybe (a :: Type ) where
   MaybeSum :: (# a  | (# #) #) -> Maybe a
 
-data instance Maybe (x :: TYPE 'UnliftedRep) where
+data instance Maybe (x :: TYPE ('BoxedRep 'Unlifted)) where
   MaybeSumU :: (# x | (# #) #) -> Maybe x
diff --git a/testsuite/tests/plugins/plugins09.stdout b/testsuite/tests/plugins/plugins09.stdout
index 61f96283ff..776f34b5f3 100644
--- a/testsuite/tests/plugins/plugins09.stdout
+++ b/testsuite/tests/plugins/plugins09.stdout
@@ -3,5 +3,6 @@ interfacePlugin: Prelude
 interfacePlugin: GHC.Float
 interfacePlugin: GHC.Base
 typeCheckPlugin (rn)
+interfacePlugin: GHC.Prim
 typeCheckPlugin (tc)
 interfacePlugin: GHC.Num.BigNat
diff --git a/testsuite/tests/plugins/plugins10.stdout b/testsuite/tests/plugins/plugins10.stdout
index 37f424b076..47e7d29b93 100644
--- a/testsuite/tests/plugins/plugins10.stdout
+++ b/testsuite/tests/plugins/plugins10.stdout
@@ -6,6 +6,7 @@ interfacePlugin: GHC.Float
 interfacePlugin: GHC.Base
 interfacePlugin: Language.Haskell.TH.Syntax
 typeCheckPlugin (rn)
+interfacePlugin: GHC.Prim
 typeCheckPlugin (tc)
 interfacePlugin: GHC.Num.BigNat
 parsePlugin(a)
diff --git a/testsuite/tests/plugins/plugins11.stdout b/testsuite/tests/plugins/plugins11.stdout
index 6bab3559b1..b3e835f2bf 100644
--- a/testsuite/tests/plugins/plugins11.stdout
+++ b/testsuite/tests/plugins/plugins11.stdout
@@ -3,5 +3,6 @@ interfacePlugin: Prelude
 interfacePlugin: GHC.Float
 interfacePlugin: GHC.Base
 typeCheckPlugin (rn)
+interfacePlugin: GHC.Prim
 typeCheckPlugin (tc)
 interfacePlugin: GHC.Num.BigNat
diff --git a/testsuite/tests/plugins/static-plugins.stdout b/testsuite/tests/plugins/static-plugins.stdout
index 032992824f..65af518b7f 100644
--- a/testsuite/tests/plugins/static-plugins.stdout
+++ b/testsuite/tests/plugins/static-plugins.stdout
@@ -5,11 +5,11 @@ interfacePlugin: GHC.Float
 interfacePlugin: GHC.Base
 interfacePlugin: System.IO
 typeCheckPlugin (rn)
+interfacePlugin: GHC.Prim
 interfacePlugin: GHC.Types
 interfacePlugin: GHC.Show
 interfacePlugin: GHC.TopHandler
 typeCheckPlugin (tc)
-interfacePlugin: GHC.Prim
 interfacePlugin: GHC.CString
 interfacePlugin: GHC.Num.BigNat
 ==pure.1
diff --git a/testsuite/tests/pmcheck/should_compile/T18249.hs b/testsuite/tests/pmcheck/should_compile/T18249.hs
index b9bd048cbd..2a343b08e1 100644
--- a/testsuite/tests/pmcheck/should_compile/T18249.hs
+++ b/testsuite/tests/pmcheck/should_compile/T18249.hs
@@ -14,7 +14,7 @@ f :: Int# -> Int
 f !_ | False = 1
 f _ = 2
 
-newtype UVoid :: TYPE 'UnliftedRep where
+newtype UVoid :: TYPE ('BoxedRep 'Unlifted) where
   UVoid :: UVoid -> UVoid
 
 g :: UVoid -> Int
diff --git a/testsuite/tests/polykinds/T14555.stderr b/testsuite/tests/polykinds/T14555.stderr
index 3861872124..f85c1b44cc 100644
--- a/testsuite/tests/polykinds/T14555.stderr
+++ b/testsuite/tests/polykinds/T14555.stderr
@@ -1,6 +1,6 @@
 
 T14555.hs:12:34: error:
-    • Couldn't match kind ‘rep’ with ‘'GHC.Types.LiftedRep’
+    • Couldn't match kind ‘rep’ with ‘GHC.Types.LiftedRep’
       Expected kind ‘TYPE rep’, but ‘a -> b’ has kind ‘*’
     • In the second argument of ‘Exp’, namely ‘(a -> b)’
       In the type ‘Exp xs (a -> b)’
diff --git a/testsuite/tests/polykinds/T14563.stderr b/testsuite/tests/polykinds/T14563.stderr
index 2d81507659..e2dd07a6d6 100644
--- a/testsuite/tests/polykinds/T14563.stderr
+++ b/testsuite/tests/polykinds/T14563.stderr
@@ -1,6 +1,6 @@
 
 T14563.hs:9:39: error:
-    • Couldn't match kind ‘rep''’ with ‘'GHC.Types.LiftedRep’
+    • Couldn't match kind ‘rep''’ with ‘GHC.Types.LiftedRep’
       Expected kind ‘TYPE rep -> TYPE rep''’,
         but ‘h’ has kind ‘TYPE rep -> *’
     • In the second argument of ‘Lan’, namely ‘h’
diff --git a/testsuite/tests/polykinds/T17963.stderr b/testsuite/tests/polykinds/T17963.stderr
index e38d216faf..aa0e4d0d3e 100644
--- a/testsuite/tests/polykinds/T17963.stderr
+++ b/testsuite/tests/polykinds/T17963.stderr
@@ -1,6 +1,6 @@
 
 T17963.hs:15:23: error:
-    • Couldn't match kind ‘rep’ with ‘'LiftedRep’
+    • Couldn't match kind ‘rep’ with ‘GHC.Types.LiftedRep’
       When matching kinds
         k0 :: *
         ob :: TYPE rep
diff --git a/testsuite/tests/polykinds/T18300.stderr b/testsuite/tests/polykinds/T18300.stderr
index 53ea72b1b8..3ddd175d55 100644
--- a/testsuite/tests/polykinds/T18300.stderr
+++ b/testsuite/tests/polykinds/T18300.stderr
@@ -1,4 +1,2 @@
 
-T18300.hs:13:1: error:
-    • Data instance has non-* return kind ‘TYPE (F Int)’
-    • In the data instance declaration for ‘T’
+T18300.hs:9:23: error: Not in scope: data constructor ‘LiftedRep’
diff --git a/testsuite/tests/simplCore/should_compile/T18013.stderr b/testsuite/tests/simplCore/should_compile/T18013.stderr
index 8b1b57e6bd..45640d9ebc 100644
--- a/testsuite/tests/simplCore/should_compile/T18013.stderr
+++ b/testsuite/tests/simplCore/should_compile/T18013.stderr
@@ -129,9 +129,9 @@ Rule fired: Class op fmap (BUILTIN)
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 52, types: 101, coercions: 17, joins: 0/1}
+  = {terms: 52, types: 102, coercions: 17, joins: 0/1}
 
--- RHS size: {terms: 37, types: 84, coercions: 17, joins: 0/1}
+-- RHS size: {terms: 37, types: 85, coercions: 17, joins: 0/1}
 mapMaybeRule [InlPrag=[2]]
   :: forall a b. Rule IO a b -> Rule IO (Maybe a) (Maybe b)
 [GblId,
diff --git a/testsuite/tests/simplCore/should_compile/T9400.stderr b/testsuite/tests/simplCore/should_compile/T9400.stderr
index 7825071aea..c4584f460e 100644
--- a/testsuite/tests/simplCore/should_compile/T9400.stderr
+++ b/testsuite/tests/simplCore/should_compile/T9400.stderr
@@ -65,7 +65,7 @@ main
                @()
                (putStrLn (unpackCString# "efg"#))
                (case Control.Exception.Base.patError
-                       @'LiftedRep @() "T9400.hs:(17,5)-(18,29)|case"#
+                       @LiftedRep @() "T9400.hs:(17,5)-(18,29)|case"#
                 of wild {
                 }))))
 
diff --git a/testsuite/tests/simplCore/should_compile/spec-inline.stderr b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
index a8fa8e58e8..683ff4d6ac 100644
--- a/testsuite/tests/simplCore/should_compile/spec-inline.stderr
+++ b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
@@ -48,8 +48,7 @@ lvl = "spec-inline.hs:(19,5)-(29,25)|function go"#
 Roman.foo3 :: ()
 [GblId, Str=b, Cpr=b]
 Roman.foo3
-  = Control.Exception.Base.patError
-      @'GHC.Types.LiftedRep @() lvl
+  = Control.Exception.Base.patError @GHC.Types.LiftedRep @() lvl
 
 Rec {
 -- RHS size: {terms: 40, types: 5, coercions: 0, joins: 0/0}
diff --git a/testsuite/tests/th/T14869.hs b/testsuite/tests/th/T14869.hs
index 4b0dcdc171..5bd2a0806a 100644
--- a/testsuite/tests/th/T14869.hs
+++ b/testsuite/tests/th/T14869.hs
@@ -9,7 +9,7 @@ import GHC.Exts
 import Language.Haskell.TH (pprint, reify, stringE)
 
 type MyConstraint = Constraint
-type MyLiftedRep  = LiftedRep
+type MyLiftedRep  = BoxedRep Lifted
 
 type family Foo1 :: Type
 type family Foo2 :: Constraint
diff --git a/testsuite/tests/typecheck/should_compile/LevPolyResult.hs b/testsuite/tests/typecheck/should_compile/LevPolyResult.hs
new file mode 100644
index 0000000000..22bfc0e2ae
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/LevPolyResult.hs
@@ -0,0 +1,11 @@
+{-# language DataKinds #-}
+{-# language KindSignatures #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+
+module LevPolyResult (example) where
+
+import GHC.Exts
+
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)). (Int -> a) -> a
+example f = f 42
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
index 0a8143b0b6..dd7890d33c 100644
--- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
@@ -12,14 +12,15 @@ module UnliftedNewtypesUnassociatedFamily where
 import GHC.Int (Int(I#))
 import GHC.Word (Word(W#))
 import GHC.Exts (Int#,Word#)
-import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep))
+import GHC.Exts (TYPE,Levity(Lifted))
+import GHC.Exts (RuntimeRep(BoxedRep,IntRep,WordRep,TupleRep))
 
 data family DFT (r :: RuntimeRep) :: TYPE r
 newtype instance DFT 'IntRep = MkDFT1 Int#
 newtype instance DFT 'WordRep = MkDFT2 Word#
 newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep])
   = MkDFT3 (# Int#, Word# #)
-data instance DFT 'LiftedRep = MkDFT4 | MkDFT5
+data instance DFT ('BoxedRep 'Lifted) = MkDFT4 | MkDFT5
 
 data family DF :: TYPE (r :: RuntimeRep)
 
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
index 57214ba181..61ed517535 100644
--- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
@@ -33,20 +33,20 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
                          (a -> b -> b) -> b -> t a -> b
         const (_ :: Integer)
           where const :: forall a b. a -> b -> a
-        ($) (_ :: [Integer] -> Integer)
-          where ($) :: forall a b. (a -> b) -> a -> b
-        ($!) (_ :: [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         curry (_ :: (t0, [Integer]) -> Integer) (_ :: t0)
           where curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
         (.) (_ :: b1 -> Integer) (_ :: [Integer] -> b1)
           where (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
         flip (_ :: [Integer] -> t0 -> Integer) (_ :: t0)
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
+        ($) (_ :: [Integer] -> Integer)
+          where ($) :: forall a b. (a -> b) -> a -> b
         return (_ :: Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: Integer)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
+        ($!) (_ :: [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         (>>=) (_ :: [Integer] -> a8) (_ :: a8 -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
                          Monad m =>
@@ -109,18 +109,18 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where snd :: forall a b. (a, b) -> b
         const (_ :: [Integer] -> Integer) (_ :: t0)
           where const :: forall a b. a -> b -> a
+        uncurry (_ :: a3 -> b3 -> [Integer] -> Integer) (_ :: (a3, b3))
+          where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
         seq (_ :: t2) (_ :: [Integer] -> Integer)
           where seq :: forall a b. a -> b -> b
         ($) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
-        uncurry (_ :: a3 -> b3 -> [Integer] -> Integer) (_ :: (a3, b3))
-          where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
-        ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: [Integer] -> Integer) (_ :: t0)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: [Integer] -> Integer) (_ :: t0)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
+        ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
+          where ($!) :: forall a b. (a -> b) -> a -> b
 
 abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Integer -> [Integer] -> Integer
@@ -148,20 +148,20 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
         const (_ :: [Integer] -> Integer)
           where const :: forall a b. a -> b -> a
-        ($) (_ :: Integer -> [Integer] -> Integer)
-          where ($) :: forall a b. (a -> b) -> a -> b
-        ($!) (_ :: Integer -> [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         curry (_ :: (t0, Integer) -> [Integer] -> Integer) (_ :: t0)
           where curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
         (.) (_ :: b1 -> [Integer] -> Integer) (_ :: Integer -> b1)
           where (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
         flip (_ :: Integer -> t0 -> [Integer] -> Integer) (_ :: t0)
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
+        ($) (_ :: Integer -> [Integer] -> Integer)
+          where ($) :: forall a b. (a -> b) -> a -> b
         return (_ :: [Integer] -> Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: [Integer] -> Integer)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
+        ($!) (_ :: Integer -> [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         (>>=) (_ :: Integer -> a8)
               (_ :: a8 -> Integer -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
@@ -228,16 +228,16 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where snd :: forall a b. (a, b) -> b
         const (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where const :: forall a b. a -> b -> a
+        uncurry (_ :: a3 -> b3 -> Integer -> [Integer] -> Integer)
+                (_ :: (a3, b3))
+          where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
         seq (_ :: t2) (_ :: Integer -> [Integer] -> Integer)
           where seq :: forall a b. a -> b -> b
         ($) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
-        uncurry (_ :: a3 -> b3 -> Integer -> [Integer] -> Integer)
-                (_ :: (a3, b3))
-          where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
-        ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
+        ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
+          where ($!) :: forall a b. (a -> b) -> a -> b
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 68d5f21f49..6d3505c33d 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -694,6 +694,7 @@ test('UnliftedNewtypesForall', normal, compile, [''])
 test('UnlifNewUnify', normal, compile, [''])
 test('UnliftedNewtypesLPFamily', normal, compile, [''])
 test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
+test('LevPolyResult', normal, compile, [''])
 test('T16832', normal, ghci_script, ['T16832.script'])
 test('T15772', normal, compile, [''])
 test('T16995', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
index ffc02228f2..3cc66588f0 100644
--- a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
@@ -36,12 +36,12 @@ constraint_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where const :: forall a b. a -> b -> a
         ($) (_ :: [a] -> a)
           where ($) :: forall a b. (a -> b) -> a -> b
-        ($!) (_ :: [a] -> a)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: a)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: a)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
+        ($!) (_ :: [a] -> a)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         id (_ :: [a] -> a)
           where id :: forall a. a -> a
         head (_ :: [[a] -> a])
diff --git a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
index 9ed1615215..5941b587bf 100644
--- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
@@ -67,12 +67,7 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
            (and originally defined in ‘GHC.Base’))
         ($) (_ :: [Integer] -> Integer)
           where ($) :: forall a b. (a -> b) -> a -> b
-          with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
-          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
-           (and originally defined in ‘GHC.Base’))
-        ($!) (_ :: [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @'GHC.Types.LiftedRep @[Integer] @Integer
+          with ($) @GHC.Types.LiftedRep @[Integer] @Integer
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
         return (_ :: Integer)
@@ -85,6 +80,11 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           with pure @((->) [Integer]) @Integer
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
+        ($!) (_ :: [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+          with ($!) @GHC.Types.LiftedRep @[Integer] @Integer
+          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
         id (_ :: [Integer] -> Integer)
           where id :: forall a. a -> a
           with id @([Integer] -> Integer)
@@ -162,12 +162,7 @@ refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
            (and originally defined in ‘GHC.Base’))
         ($) (_ :: Integer -> [Integer] -> Integer)
           where ($) :: forall a b. (a -> b) -> a -> b
-          with ($) @'GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
-          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
-           (and originally defined in ‘GHC.Base’))
-        ($!) (_ :: Integer -> [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @'GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
+          with ($) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
         return (_ :: [Integer] -> Integer)
@@ -180,6 +175,11 @@ refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           with pure @((->) Integer) @([Integer] -> Integer)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
+        ($!) (_ :: Integer -> [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+          with ($!) @GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
+          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
         id (_ :: Integer -> [Integer] -> Integer)
           where id :: forall a. a -> a
           with id @(Integer -> [Integer] -> Integer)
diff --git a/testsuite/tests/typecheck/should_fail/LevPolyLet.hs b/testsuite/tests/typecheck/should_fail/LevPolyLet.hs
new file mode 100644
index 0000000000..6fb47133ae
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/LevPolyLet.hs
@@ -0,0 +1,19 @@
+{-# language DataKinds #-}
+{-# language KindSignatures #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+
+module LevPolyLet
+  ( example
+  ) where
+
+import GHC.Exts
+
+-- This should be rejected because of the let binding.
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)).
+     (Int -> a)
+  -> (a -> Bool)
+  -> Bool
+example f g =
+  let x = f 42
+   in g x
diff --git a/testsuite/tests/typecheck/should_fail/LevPolyLet.stderr b/testsuite/tests/typecheck/should_fail/LevPolyLet.stderr
new file mode 100644
index 0000000000..8d01f4028b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/LevPolyLet.stderr
@@ -0,0 +1,5 @@
+LevPolyLet.hs:18:7:
+    A levity-polymorphic type is not allowed here:
+      Type: a
+      Kind: TYPE ('BoxedRep v)
+    In the type of binder ‘x’
diff --git a/testsuite/tests/typecheck/should_fail/T12373.stderr b/testsuite/tests/typecheck/should_fail/T12373.stderr
index 20137fbdad..f53f5ea7e2 100644
--- a/testsuite/tests/typecheck/should_fail/T12373.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12373.stderr
@@ -3,7 +3,7 @@ T12373.hs:10:19: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
         a0 :: *
-        MVar# RealWorld a1 :: TYPE 'UnliftedRep
+        MVar# RealWorld a1 :: UnliftedType
       Expected: (# State# RealWorld, a0 #)
         Actual: (# State# RealWorld, MVar# RealWorld a1 #)
     • In the expression: newMVar# rw
diff --git a/testsuite/tests/typecheck/should_fail/T13610.stderr b/testsuite/tests/typecheck/should_fail/T13610.stderr
index c04687988c..cfff3dc863 100644
--- a/testsuite/tests/typecheck/should_fail/T13610.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13610.stderr
@@ -3,7 +3,7 @@ T13610.hs:11:15: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
         a :: *
-        Weak# () :: TYPE 'UnliftedRep
+        Weak# () :: UnliftedType
       Expected: (# State# RealWorld, a #)
         Actual: (# State# RealWorld, Weak# () #)
     • In the expression: mkWeakNoFinalizer# double () s
diff --git a/testsuite/tests/typecheck/should_fail/T14884.stderr b/testsuite/tests/typecheck/should_fail/T14884.stderr
index 6c2c78c0dc..2c5abc33f0 100644
--- a/testsuite/tests/typecheck/should_fail/T14884.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14884.stderr
@@ -19,11 +19,11 @@ T14884.hs:4:5: error:
           (imported from ‘Prelude’ at T14884.hs:1:8-13
            (and originally defined in ‘Data.Foldable’))
         ($) :: forall a b. (a -> b) -> a -> b
-          with ($) @'GHC.Types.LiftedRep @String @(IO ())
+          with ($) @GHC.Types.LiftedRep @String @(IO ())
           (imported from ‘Prelude’ at T14884.hs:1:8-13
            (and originally defined in ‘GHC.Base’))
         ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @'GHC.Types.LiftedRep @String @(IO ())
+          with ($!) @GHC.Types.LiftedRep @String @(IO ())
           (imported from ‘Prelude’ at T14884.hs:1:8-13
            (and originally defined in ‘GHC.Base’))
         id :: forall a. a -> a
diff --git a/testsuite/tests/typecheck/should_fail/T15067.stderr b/testsuite/tests/typecheck/should_fail/T15067.stderr
index 4ed3d3bc0a..a2ecc4326c 100644
--- a/testsuite/tests/typecheck/should_fail/T15067.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15067.stderr
@@ -1,13 +1,13 @@
 
 T15067.hs:9:14: error:
-    • No instance for (Typeable (# 'GHC.Types.LiftedRep #))
+    • No instance for (Typeable (# GHC.Types.LiftedRep #))
         arising from a use of ‘typeRep’
         GHC can't yet do polykinded
-          Typeable ((# 'GHC.Types.LiftedRep #) :: *
-                                                  -> *
-                                                  -> TYPE
-                                                       ('GHC.Types.SumRep
-                                                          '[ 'GHC.Types.LiftedRep,
-                                                             'GHC.Types.LiftedRep]))
+          Typeable ((# GHC.Types.LiftedRep #) :: *
+                                                 -> *
+                                                 -> TYPE
+                                                      ('GHC.Types.SumRep
+                                                         '[GHC.Types.LiftedRep,
+                                                           GHC.Types.LiftedRep]))
     • In the expression: typeRep
       In an equation for ‘floopadoop’: floopadoop = typeRep
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.hs b/testsuite/tests/typecheck/should_fail/T15883b.hs
index 82613943a7..45b7d65360 100644
--- a/testsuite/tests/typecheck/should_fail/T15883b.hs
+++ b/testsuite/tests/typecheck/should_fail/T15883b.hs
@@ -11,4 +11,4 @@ module T15883b where
 import GHC.Exts
 
 newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-deriving stock instance Eq (Foo LiftedRep)
+deriving stock instance Eq (Foo (BoxedRep Lifted))
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.stderr b/testsuite/tests/typecheck/should_fail/T15883b.stderr
index a89403d4af..21b9305315 100644
--- a/testsuite/tests/typecheck/should_fail/T15883b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883b.stderr
@@ -1,5 +1,6 @@
 T15883b.hs:14:1:
      Can't make a derived instance of
-        ‘Eq (Foo 'LiftedRep)’ with the stock strategy:
+        ‘Eq (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
         Don't know how to derive ‘Eq’ for type ‘forall a. a’
-     In the stand-alone deriving instance for ‘Eq (Foo LiftedRep)’
+     In the stand-alone deriving instance for
+        ‘Eq (Foo (BoxedRep Lifted))’
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.hs b/testsuite/tests/typecheck/should_fail/T15883c.hs
index bd031540c2..93d57b784b 100644
--- a/testsuite/tests/typecheck/should_fail/T15883c.hs
+++ b/testsuite/tests/typecheck/should_fail/T15883c.hs
@@ -11,4 +11,4 @@ module T15883c where
 import GHC.Exts
 
 newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-deriving stock instance Ord (Foo LiftedRep)
+deriving stock instance Ord (Foo (BoxedRep Lifted))
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.stderr b/testsuite/tests/typecheck/should_fail/T15883c.stderr
index 5444f5d6c8..60678c4fcb 100644
--- a/testsuite/tests/typecheck/should_fail/T15883c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883c.stderr
@@ -1,5 +1,6 @@
 T15883c.hs:14:1:                 
      Can't make a derived instance of
-        ‘Ord (Foo 'LiftedRep)’ with the stock strategy:
+        ‘Ord (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
         Don't know how to derive ‘Ord’ for type ‘forall a. a’
-     In the stand-alone deriving instance for ‘Ord (Foo LiftedRep)’
+     In the stand-alone deriving instance for
+        ‘Ord (Foo (BoxedRep Lifted))’
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.hs b/testsuite/tests/typecheck/should_fail/T15883d.hs
index fd86c5cab3..dbcd93751e 100644
--- a/testsuite/tests/typecheck/should_fail/T15883d.hs
+++ b/testsuite/tests/typecheck/should_fail/T15883d.hs
@@ -11,5 +11,5 @@ module T15883d where
 import GHC.Exts
 
 newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-deriving stock instance Show (Foo LiftedRep)
+deriving stock instance Show (Foo (BoxedRep Lifted))
 
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.stderr b/testsuite/tests/typecheck/should_fail/T15883d.stderr
index b080ff6544..162b31072e 100644
--- a/testsuite/tests/typecheck/should_fail/T15883d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883d.stderr
@@ -1,5 +1,6 @@
 T15883d.hs:14:1:
      Can't make a derived instance of
-        ‘Show (Foo 'LiftedRep)’ with the stock strategy:
+        ‘Show (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
         Don't know how to derive ‘Show’ for type ‘forall a. a’
-     In the stand-alone deriving instance for ‘Show (Foo LiftedRep)’
+     In the stand-alone deriving instance for
+        ‘Show (Foo (BoxedRep Lifted))’
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.hs b/testsuite/tests/typecheck/should_fail/T15883e.hs
index bb1dcacf92..cfecdb693e 100644
--- a/testsuite/tests/typecheck/should_fail/T15883e.hs
+++ b/testsuite/tests/typecheck/should_fail/T15883e.hs
@@ -13,6 +13,6 @@ import GHC.Exts
 import Data.Data (Data)
 
 newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
-deriving stock instance Data (Foo LiftedRep)
+deriving stock instance Data (Foo (BoxedRep Lifted))
 
 
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.stderr b/testsuite/tests/typecheck/should_fail/T15883e.stderr
index 05e07f0307..a20b3f5d43 100644
--- a/testsuite/tests/typecheck/should_fail/T15883e.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883e.stderr
@@ -1,5 +1,6 @@
 T15883e.hs:16:1:
      Can't make a derived instance of
-        ‘Data (Foo 'LiftedRep)’ with the stock strategy:
+        ‘Data (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
         Don't know how to derive ‘Data’ for type ‘forall a. a’
-     In the stand-alone deriving instance for ‘Data (Foo LiftedRep)’
+     In the stand-alone deriving instance for
+        ‘Data (Foo (BoxedRep Lifted))’
diff --git a/testsuite/tests/typecheck/should_fail/T17021.stderr b/testsuite/tests/typecheck/should_fail/T17021.stderr
index 12d6d687d8..96c700c4b7 100644
--- a/testsuite/tests/typecheck/should_fail/T17021.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17021.stderr
@@ -2,5 +2,5 @@
 T17021.hs:18:5: error:
     A levity-polymorphic type is not allowed here:
       Type: Int
-      Kind: TYPE (Id 'LiftedRep)
+      Kind: TYPE (Id ('BoxedRep 'Lifted))
     When trying to create a variable of type: Int
diff --git a/testsuite/tests/typecheck/should_fail/T18357a.stderr b/testsuite/tests/typecheck/should_fail/T18357a.stderr
index a9e87fed98..f60e09922a 100644
--- a/testsuite/tests/typecheck/should_fail/T18357a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T18357a.stderr
@@ -1,6 +1,6 @@
 
 T18357a.hs:9:10: error:
-    • Couldn't match kind ‘r’ with ‘'LiftedRep’
+    • Couldn't match kind ‘r’ with ‘LiftedRep’
       Expected a type, but ‘Int’ has kind ‘*’
     • In the type ‘Int’
       In the definition of data constructor ‘MkT’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
index adac27fe90..21b1b053fc 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
@@ -11,7 +11,7 @@ module UnliftedNewtypesUnassociatedFamily where
 import GHC.Int (Int(I#))
 import GHC.Word (Word(W#))
 import GHC.Exts (Int#,Word#)
-import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep))
+import GHC.Exts (TYPE,RuntimeRep(IntRep,WordRep,TupleRep))
 
 data family DF :: TYPE (r :: RuntimeRep)
 
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
index 972f873e62..a9cb694807 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
@@ -1,18 +1,18 @@
 
-UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error:
-    • Expecting a lifted type, but ‘Int#’ is unlifted
-    • In the type ‘Int#’
+UnliftedNewtypesUnassociatedFamilyFail.hs:21:30:
+     Expecting a lifted type, but ‘Int#’ is unlifted
+     In the type ‘Int#’
       In the definition of data constructor ‘MkDF1a’
       In the newtype instance declaration for ‘DF’
 
-UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error:
-    • Expecting a lifted type, but ‘Word#’ is unlifted
-    • In the type ‘Word#’
+UnliftedNewtypesUnassociatedFamilyFail.hs:22:30:
+     Expecting a lifted type, but ‘Word#’ is unlifted
+     In the type ‘Word#’
       In the definition of data constructor ‘MkDF2a’
       In the newtype instance declaration for ‘DF’
 
-UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error:
-    • Expecting a lifted type, but ‘(# Int#, Word# #)’ is unlifted
-    • In the type ‘(# Int#, Word# #)’
+UnliftedNewtypesUnassociatedFamilyFail.hs:23:30:
+     Expecting a lifted type, but ‘(# Int#, Word# #)’ is unlifted
+     In the type ‘(# Int#, Word# #)’
       In the definition of data constructor ‘MkDF3a’
       In the newtype instance declaration for ‘DF’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 4768b19263..0bd86e9288 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -442,6 +442,7 @@ test('T13068', [extra_files(['T13068.hs', 'T13068a.hs', 'T13068.hs-boot', 'T1306
 test('T13075', normal, compile_fail, [''])
 test('T13105', normal, compile_fail, [''])
 test('LevPolyBounded', normal, compile_fail, [''])
+test('LevPolyLet', normal, compile_fail, [''])
 test('T13487', normal, compile, [''])
 test('T13292', normal, multimod_compile, ['T13292', '-v0 -fdefer-type-errors'])
 test('T13300', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
index efb81e8ee6..efb73e2d45 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
@@ -3,6 +3,6 @@ tcfail090.hs:11:9: error:
     • Couldn't match a lifted type with an unlifted type
       When matching types
         a0 :: *
-        ByteArray# :: TYPE 'UnliftedRep
+        ByteArray# :: UnliftedType
     • In the expression: my_undefined
       In an equation for ‘die’: die _ = my_undefined
diff --git a/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
index d57d2e1499..82553b4ff2 100644
--- a/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
+++ b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
@@ -6,12 +6,12 @@ module Main where
 import GHC.Exts
 
 data G a where
-  MkG :: G (TupleRep [LiftedRep, IntRep])
+  MkG :: G (TupleRep [BoxedRep Lifted, IntRep])
 
 -- tests that we don't eta-expand functions that are levity-polymorphic
 -- see CoreArity.mkEtaWW
 foo :: forall a (b :: TYPE a). G a -> b -> b
-foo MkG = (\x -> x) :: forall (c :: TYPE (TupleRep [LiftedRep, IntRep])). c -> c
+foo MkG = (\x -> x) :: forall (c :: TYPE (TupleRep [BoxedRep Lifted, IntRep])). c -> c
 
 data H a where
   MkH :: H IntRep
diff --git a/testsuite/tests/typecheck/should_run/LevPolyResultInst.hs b/testsuite/tests/typecheck/should_run/LevPolyResultInst.hs
new file mode 100644
index 0000000000..8302a43693
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/LevPolyResultInst.hs
@@ -0,0 +1,27 @@
+{-# language BangPatterns #-}
+{-# language DataKinds #-}
+{-# language MagicHash #-}
+{-# language PolyKinds #-}
+{-# language RankNTypes #-}
+{-# language UnboxedTuples #-}
+
+import GHC.Exts
+
+main :: IO ()
+main = do
+  print (example (\x -> I# x > 7))
+  case indexArray# (example replicateFalse) 0# of
+    (# r #) -> print r
+
+-- Combines base:runST, primitive:newArray, and primitive:unsafeFreezeArray
+replicateFalse :: Int# -> Array# Bool
+replicateFalse n =
+  let !(# _, r #) = runRW#
+        (\s -> case newArray# n False s of
+          (# s', arr #) -> unsafeFreezeArray# arr s'
+        )
+   in r
+
+example :: forall (v :: Levity) (a :: TYPE ('BoxedRep v)). (Int# -> a) -> a
+{-# noinline example #-}
+example f = f 8#
diff --git a/testsuite/tests/typecheck/should_run/LevPolyResultInst.stdout b/testsuite/tests/typecheck/should_run/LevPolyResultInst.stdout
new file mode 100644
index 0000000000..1cc8b5e10d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/LevPolyResultInst.stdout
@@ -0,0 +1,2 @@
+True
+False
diff --git a/testsuite/tests/typecheck/should_run/T12809.hs b/testsuite/tests/typecheck/should_run/T12809.hs
index 66031a5af7..3e20403add 100644
--- a/testsuite/tests/typecheck/should_run/T12809.hs
+++ b/testsuite/tests/typecheck/should_run/T12809.hs
@@ -32,7 +32,7 @@ g (# b, x #) = show b ++ " " ++ show (I# x)
 h :: (# Double, Int# #) -> String
 h (# d, x #) = show d ++ " " ++ show (I# x)
 
-cond :: forall (a :: TYPE (TupleRep [LiftedRep, IntRep])). Bool -> a -> a -> a
+cond :: forall (a :: TYPE (TupleRep [BoxedRep Lifted, IntRep])). Bool -> a -> a -> a
 cond True x _ = x
 cond False _ x = x
 
diff --git a/testsuite/tests/typecheck/should_run/T14236.stdout b/testsuite/tests/typecheck/should_run/T14236.stdout
index ffa0e65dc9..73c98017f2 100644
--- a/testsuite/tests/typecheck/should_run/T14236.stdout
+++ b/testsuite/tests/typecheck/should_run/T14236.stdout
@@ -1,3 +1,3 @@
-(FUN 'Many 'LiftedRep 'LiftedRep Int,Char)
-(FUN 'Many 'IntRep 'LiftedRep Int#,Char)
+(FUN 'Many ('BoxedRep 'Lifted) ('BoxedRep 'Lifted) Int,Char)
+(FUN 'Many 'IntRep ('BoxedRep 'Lifted) Int#,Char)
 Int# -> [Char]
diff --git a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
index 1303db844c..6ef72dfb83 100644
--- a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
+++ b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
@@ -5,7 +5,7 @@ good: Maybe
 good: TYPE
 good: RuntimeRep
 good: 'IntRep
-good: FUN 'Many 'LiftedRep 'LiftedRep
+good: FUN 'Many ('BoxedRep 'Lifted) ('BoxedRep 'Lifted)
 good: Proxy * Int
 good: Proxy (TYPE 'IntRep) Int#
 good: *
diff --git a/testsuite/tests/typecheck/should_run/TypeOf.hs b/testsuite/tests/typecheck/should_run/TypeOf.hs
index cec6833b64..37113bfe80 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.hs
+++ b/testsuite/tests/typecheck/should_run/TypeOf.hs
@@ -28,9 +28,12 @@ main = do
   print $ typeOf (Proxy :: Proxy [1,2,3])
   print $ typeOf (Proxy :: Proxy 'EQ)
   print $ typeOf (Proxy :: Proxy TYPE)
-  print $ typeOf (Proxy :: Proxy (TYPE 'LiftedRep))
+  print $ typeOf (Proxy :: Proxy (TYPE ('BoxedRep 'Lifted)))
   print $ typeOf (Proxy :: Proxy *)
   print $ typeOf (Proxy :: Proxy ★)
-  print $ typeOf (Proxy :: Proxy 'LiftedRep)
+  print $ typeOf (Proxy :: Proxy ('BoxedRep 'Lifted))
+  print $ typeOf (Proxy :: Proxy 'Lifted)
+  print $ typeOf (Proxy :: Proxy 'Unlifted)
+  print $ typeOf (Proxy :: Proxy LiftedRep)
   print $ typeOf (Proxy :: Proxy '(1, "hello"))
   print $ typeOf (Proxy :: Proxy (~~))
diff --git a/testsuite/tests/typecheck/should_run/TypeOf.stdout b/testsuite/tests/typecheck/should_run/TypeOf.stdout
index 40d2cb5f8f..3344f17193 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeOf.stdout
@@ -19,6 +19,9 @@ Proxy (RuntimeRep -> *) TYPE
 Proxy * *
 Proxy * *
 Proxy * *
-Proxy RuntimeRep 'LiftedRep
+Proxy RuntimeRep ('BoxedRep 'Lifted)
+Proxy Levity 'Lifted
+Proxy Levity 'Unlifted
+Proxy RuntimeRep ('BoxedRep 'Lifted)
 Proxy (Natural,Symbol) ('(,) Natural Symbol 1 "hello")
 Proxy (* -> * -> Constraint) ((~~) * *)
diff --git a/testsuite/tests/typecheck/should_run/TypeRep.hs b/testsuite/tests/typecheck/should_run/TypeRep.hs
index beae93f6b3..886479fd33 100644
--- a/testsuite/tests/typecheck/should_run/TypeRep.hs
+++ b/testsuite/tests/typecheck/should_run/TypeRep.hs
@@ -53,10 +53,10 @@ main = do
   print $ rep @(Proxy [1,2,3])
   print $ rep @(Proxy 'EQ)
   print $ rep @(Proxy TYPE)
-  print $ rep @(Proxy (TYPE 'LiftedRep))
+  print $ rep @(Proxy (TYPE ('BoxedRep 'Lifted)))
   print $ rep @(Proxy *)
   print $ rep @(Proxy ★)
-  print $ rep @(Proxy 'LiftedRep)
+  print $ rep @(Proxy ('BoxedRep 'Lifted))
 
   -- Something lifted and primitive
   print $ rep @RealWorld  -- #12132
diff --git a/testsuite/tests/typecheck/should_run/TypeRep.stdout b/testsuite/tests/typecheck/should_run/TypeRep.stdout
index a0c03e09d8..cf43264714 100644
--- a/testsuite/tests/typecheck/should_run/TypeRep.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeRep.stdout
@@ -13,7 +13,7 @@ Int -> Int
 (%,%) (Eq Int) (Eq [Char])
 Int#
 (##)
-(#,#) 'IntRep 'LiftedRep Int# Int
+(#,#) 'IntRep ('BoxedRep 'Lifted) Int# Int
 Proxy Constraint (Eq Int)
 Proxy * (Int,Int)
 Proxy Symbol "hello world"
@@ -24,5 +24,5 @@ Proxy (RuntimeRep -> *) TYPE
 Proxy * *
 Proxy * *
 Proxy * *
-Proxy RuntimeRep 'LiftedRep
+Proxy RuntimeRep ('BoxedRep 'Lifted)
 RealWorld
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index ef8ae9136d..ef7bedb354 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -145,5 +145,6 @@ test('UnliftedNewtypesFamilyRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesIdentityRun', normal, compile_and_run, [''])
 test('UnliftedNewtypesCoerceRun', normal, compile_and_run, [''])
+test('LevPolyResultInst', normal, compile_and_run, [''])
 test('T17104', normal, compile_and_run, [''])
 test('T18627', normal, compile_and_run, ['-O'])  # Optimisation shows up the bug
diff --git a/testsuite/tests/unboxedsums/T12711.stdout b/testsuite/tests/unboxedsums/T12711.stdout
index 54af3fdfa6..18a67a078d 100644
--- a/testsuite/tests/unboxedsums/T12711.stdout
+++ b/testsuite/tests/unboxedsums/T12711.stdout
@@ -1,2 +1,4 @@
 (# _ | _ #) :: TYPE
-                 ('GHC.Types.SumRep '[ 'GHC.Types.LiftedRep, 'GHC.Types.LiftedRep])
+                 ('GHC.Types.SumRep
+                    '[ 'GHC.Types.BoxedRep 'GHC.Types.Lifted,
+                       'GHC.Types.BoxedRep 'GHC.Types.Lifted])
diff --git a/testsuite/tests/unboxedsums/sum_rr.hs b/testsuite/tests/unboxedsums/sum_rr.hs
index 448a9b2221..11c8cbb648 100644
--- a/testsuite/tests/unboxedsums/sum_rr.hs
+++ b/testsuite/tests/unboxedsums/sum_rr.hs
@@ -5,4 +5,4 @@ module Example where
 import Data.Typeable
 import GHC.Exts
 
-data Wat (a :: TYPE (SumRep '[LiftedRep, IntRep])) = Wat a
+data Wat (a :: TYPE (SumRep '[BoxedRep Lifted, IntRep])) = Wat a
diff --git a/utils/haddock b/utils/haddock
-Subproject 65868397a59e61b575c70c0757dddbbba9cb5ac
+Subproject bd206f09715420aaa62341c9a96411a684eee6e