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

37 files changed, 160 insertions, 82 deletions

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