Revert "Implement BoxedRep proposal"

This was inadvertently merged.

This reverts commit 6c2eb2232b39ff4720fda0a4a009fb6afbc9dcea.

65 files changed, 111 insertions, 195 deletions

diff --git a/testsuite/tests/backpack/should_run/T13955.bkp b/testsuite/tests/backpack/should_run/T13955.bkp
index eadeee6f5c..a7d447f169 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 = 'BoxedRep 'Lifted
+    type Rep = LiftedRep
     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 90a72c2a9a..6c74e10a7c 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
@@ -14,14 +14,12 @@ import Data.Type.Bool
 import Data.Type.Equality hiding ((:~~:)(..))
 import GHC.TypeLits
 import Data.Proxy
-import GHC.Exts hiding (Lifted, BoxedRep)
+import GHC.Exts
 import Data.Kind
 import Unsafe.Coerce
 import Data.Char
 import Data.Maybe
 
-import qualified GHC.Exts as Exts
-
 -------------------------------
 -- Utilities
 
@@ -84,9 +82,7 @@ data TyCon (a :: k) where
   Arrow :: TyCon (->)
   TYPE  :: TyCon TYPE
   RuntimeRep :: TyCon RuntimeRep
-  Levity :: TyCon Levity
-  BoxedRep :: TyCon 'Exts.BoxedRep
-  Lifted :: TyCon 'Exts.Lifted
+  LiftedRep' :: TyCon 'LiftedRep
   -- If extending, add to eqTyCon too
 
 eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
@@ -98,9 +94,7 @@ eqTyCon Maybe Maybe = Just HRefl
 eqTyCon Arrow Arrow = Just HRefl
 eqTyCon TYPE TYPE = Just HRefl
 eqTyCon RuntimeRep RuntimeRep = Just HRefl
-eqTyCon Levity Levity = Just HRefl
-eqTyCon BoxedRep BoxedRep = Just HRefl
-eqTyCon Lifted Lifted = Just HRefl
+eqTyCon LiftedRep' LiftedRep' = Just HRefl
 eqTyCon _ _ = Nothing
 
 -- Check whether or not a type is really a plain old tycon;
@@ -218,10 +212,8 @@ instance TyConAble []        where tyCon = List
 instance TyConAble Maybe     where tyCon = Maybe
 instance TyConAble (->)      where tyCon = Arrow
 instance TyConAble TYPE      where tyCon = TYPE
-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
+instance TyConAble 'LiftedRep   where tyCon = LiftedRep'
+instance TyConAble RuntimeRep    where tyCon = RuntimeRep
 
 -- 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 b2af8ab7b8..daad6ac054 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: '[ 'BoxedRep 'Lifted]
+                     with: '[ 'LiftedRep]
       Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
-        but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'BoxedRep 'Lifted])’
+        but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
       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 585f010eba..9df828b111 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 '[ 'BoxedRep 'Lifted, 'BoxedRep 'Lifted ]))
+class Foo3 (a :: TYPE ('SumRep '[ 'LiftedRep, 'LiftedRep ]))
 deriving instance Foo3 a
 
-class Foo4 (a :: TYPE ('SumRep '[ 'BoxedRep 'Lifted, 'BoxedRep 'Lifted ]))
+class Foo4 (a :: TYPE ('SumRep '[ 'LiftedRep, 'LiftedRep ]))
 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 61410d84cf..804bfd31da 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 ['BoxedRep 'Lifted, 'BoxedRep 'Lifted]))
+class Wat1 (a :: TYPE ('TupleRep ['LiftedRep, 'LiftedRep]))
 deriving instance Wat1 (# a, b #)
 
-class Wat2 (a :: TYPE ('SumRep ['BoxedRep 'Lifted, 'BoxedRep 'Lifted]))
+class Wat2 (a :: TYPE ('SumRep ['LiftedRep, 'LiftedRep]))
 deriving instance Wat2 (# a | b #)
diff --git a/testsuite/tests/ffi/should_run/T16650a.hs b/testsuite/tests/ffi/should_run/T16650a.hs
index 65fc38b57d..6a43a55118 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 ('BoxedRep 'Unlifted)) -> Box
+  Box :: (Any :: TYPE 'UnliftedRep) -> 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 265e5bf65f..ba0d4a72a0 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 ('BoxedRep 'Unlifted)) -> Box
+  Box :: (Any :: TYPE 'UnliftedRep) -> 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 0d8e9ac8ec..968731b3bd 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 ('BoxedRep 'Unlifted)) -> Box
+  Box :: (Any :: TYPE 'UnliftedRep) -> 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 874701b40a..8bb4a4697b 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 ('BoxedRep 'Unlifted)) -> Box
+  Box :: (Any :: TYPE 'UnliftedRep) -> 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 7a0a5cce19..8953e9b02d 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 ('BoxedRep 'Unlifted) where
+newtype MyArray# :: TYPE 'UnliftedRep where
   MyArray# :: MutableByteArray# RealWorld -> MyArray#
 
 data MutableByteArray :: Type where
diff --git a/testsuite/tests/ghci/scripts/T13963.script b/testsuite/tests/ghci/scripts/T13963.script
index 030e8087a9..c5e830aad1 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 803aa9ebd0..f9e6d339f9 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/T7627.stdout b/testsuite/tests/ghci/scripts/T7627.stdout
index 8967544004..b86ea432ff 100644
--- a/testsuite/tests/ghci/scripts/T7627.stdout
+++ b/testsuite/tests/ghci/scripts/T7627.stdout
@@ -38,8 +38,7 @@ type (#,#) :: *
               -> *
               -> TYPE
                    ('GHC.Types.TupleRep
-                      '[ 'GHC.Types.BoxedRep 'GHC.Types.Lifted,
-                         'GHC.Types.BoxedRep 'GHC.Types.Lifted])
+                      '[ '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/should_run/T16096.stdout b/testsuite/tests/ghci/should_run/T16096.stdout
index 2749f06586..5826057d42 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 d3219de45e..9e2e79cd8b 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/plugins/plugins09.stdout b/testsuite/tests/plugins/plugins09.stdout
index 776f34b5f3..61f96283ff 100644
--- a/testsuite/tests/plugins/plugins09.stdout
+++ b/testsuite/tests/plugins/plugins09.stdout
@@ -3,6 +3,5 @@ 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 47e7d29b93..37f424b076 100644
--- a/testsuite/tests/plugins/plugins10.stdout
+++ b/testsuite/tests/plugins/plugins10.stdout
@@ -6,7 +6,6 @@ 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 b3e835f2bf..6bab3559b1 100644
--- a/testsuite/tests/plugins/plugins11.stdout
+++ b/testsuite/tests/plugins/plugins11.stdout
@@ -3,6 +3,5 @@ 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 65af518b7f..032992824f 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 2a343b08e1..b9bd048cbd 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 ('BoxedRep 'Unlifted) where
+newtype UVoid :: TYPE 'UnliftedRep where
   UVoid :: UVoid -> UVoid
 
 g :: UVoid -> Int
diff --git a/testsuite/tests/polykinds/T14555.stderr b/testsuite/tests/polykinds/T14555.stderr
index f85c1b44cc..3861872124 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 e2dd07a6d6..2d81507659 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 aa0e4d0d3e..e38d216faf 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 ‘GHC.Types.LiftedRep’
+    • Couldn't match kind ‘rep’ with ‘'LiftedRep’
       When matching kinds
         k0 :: *
         ob :: TYPE rep
diff --git a/testsuite/tests/polykinds/T18300.stderr b/testsuite/tests/polykinds/T18300.stderr
index 3ddd175d55..53ea72b1b8 100644
--- a/testsuite/tests/polykinds/T18300.stderr
+++ b/testsuite/tests/polykinds/T18300.stderr
@@ -1,2 +1,4 @@
 
-T18300.hs:9:23: error: Not in scope: data constructor ‘LiftedRep’
+T18300.hs:13:1: error:
+    • Data instance has non-* return kind ‘TYPE (F Int)’
+    • In the data instance declaration for ‘T’
diff --git a/testsuite/tests/simplCore/should_compile/T18013.stderr b/testsuite/tests/simplCore/should_compile/T18013.stderr
index 1f9a70946a..20cb606cb4 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: 102, coercions: 17, joins: 0/1}
+  = {terms: 52, types: 101, coercions: 17, joins: 0/1}
 
--- RHS size: {terms: 37, types: 85, coercions: 17, joins: 0/1}
+-- RHS size: {terms: 37, types: 84, coercions: 17, joins: 0/1}
 mapMaybeRule
   :: 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 3b53d2cb02..9e3f4184ea 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"#))
                (Control.Exception.Base.patError
-                  @LiftedRep @(IO ()) "T9400.hs:(17,5)-(18,29)|case"#))))
+                  @'LiftedRep @(IO ()) "T9400.hs:(17,5)-(18,29)|case"#))))
 
 
 
diff --git a/testsuite/tests/simplCore/should_compile/spec-inline.stderr b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
index a26d2ed3bc..87e8bd7980 100644
--- a/testsuite/tests/simplCore/should_compile/spec-inline.stderr
+++ b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
@@ -48,7 +48,7 @@ lvl = "spec-inline.hs:(19,5)-(29,25)|function go"#
 Roman.foo3 :: Int
 [GblId, Str=b, Cpr=b]
 Roman.foo3
-  = Control.Exception.Base.patError @GHC.Types.LiftedRep @Int lvl
+  = Control.Exception.Base.patError @'GHC.Types.LiftedRep @Int 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 5bd2a0806a..4b0dcdc171 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  = BoxedRep Lifted
+type MyLiftedRep  = LiftedRep
 
 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
deleted file mode 100644
index 6c17d5c9ae..0000000000
--- a/testsuite/tests/typecheck/should_compile/LevPolyResult.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# 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 dd7890d33c..0a8143b0b6 100644
--- a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
@@ -12,15 +12,14 @@ module UnliftedNewtypesUnassociatedFamily where
 import GHC.Int (Int(I#))
 import GHC.Word (Word(W#))
 import GHC.Exts (Int#,Word#)
-import GHC.Exts (TYPE,Levity(Lifted))
-import GHC.Exts (RuntimeRep(BoxedRep,IntRep,WordRep,TupleRep))
+import GHC.Exts (TYPE,RuntimeRep(LiftedRep,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 ('BoxedRep 'Lifted) = MkDFT4 | MkDFT5
+data instance DFT 'LiftedRep = 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 61ed517535..57214ba181 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 ce0c3a97a1..344b4394a9 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -689,7 +689,6 @@ 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('T16995', normal, compile, [''])
 test('T17007', 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 3cc66588f0..ffc02228f2 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 5941b587bf..9ed1615215 100644
--- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
@@ -67,7 +67,12 @@ 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
+          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
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
         return (_ :: Integer)
@@ -80,11 +85,6 @@ 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,7 +162,12 @@ 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)
+          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)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
         return (_ :: [Integer] -> Integer)
@@ -175,11 +180,6 @@ 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
deleted file mode 100644
index 6fb47133ae..0000000000
--- a/testsuite/tests/typecheck/should_fail/LevPolyLet.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-{-# 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
deleted file mode 100644
index 8d01f4028b..0000000000
--- a/testsuite/tests/typecheck/should_fail/LevPolyLet.stderr
+++ /dev/null
@@ -1,5 +0,0 @@
-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 f822b72d20..20137fbdad 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 ('BoxedRep 'Unlifted)
+        MVar# RealWorld a1 :: TYPE 'UnliftedRep
       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 155fee8d24..c04687988c 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 ('BoxedRep 'Unlifted)
+        Weak# () :: TYPE 'UnliftedRep
       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 2f63301359..c901811f6f 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 a2ecc4326c..4ed3d3bc0a 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 45b7d65360..82613943a7 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 (BoxedRep Lifted))
+deriving stock instance Eq (Foo LiftedRep)
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.stderr b/testsuite/tests/typecheck/should_fail/T15883b.stderr
index 21b9305315..a89403d4af 100644
--- a/testsuite/tests/typecheck/should_fail/T15883b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883b.stderr
@@ -1,6 +1,5 @@
 T15883b.hs:14:1:
      Can't make a derived instance of
-        ‘Eq (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
+        ‘Eq (Foo 'LiftedRep)’ 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 (BoxedRep Lifted))’
+     In the stand-alone deriving instance for ‘Eq (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.hs b/testsuite/tests/typecheck/should_fail/T15883c.hs
index 93d57b784b..bd031540c2 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 (BoxedRep Lifted))
+deriving stock instance Ord (Foo LiftedRep)
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.stderr b/testsuite/tests/typecheck/should_fail/T15883c.stderr
index 60678c4fcb..5444f5d6c8 100644
--- a/testsuite/tests/typecheck/should_fail/T15883c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883c.stderr
@@ -1,6 +1,5 @@
 T15883c.hs:14:1:                 
      Can't make a derived instance of
-        ‘Ord (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
+        ‘Ord (Foo 'LiftedRep)’ 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 (BoxedRep Lifted))’
+     In the stand-alone deriving instance for ‘Ord (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.hs b/testsuite/tests/typecheck/should_fail/T15883d.hs
index dbcd93751e..fd86c5cab3 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 (BoxedRep Lifted))
+deriving stock instance Show (Foo LiftedRep)
 
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.stderr b/testsuite/tests/typecheck/should_fail/T15883d.stderr
index 162b31072e..b080ff6544 100644
--- a/testsuite/tests/typecheck/should_fail/T15883d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883d.stderr
@@ -1,6 +1,5 @@
 T15883d.hs:14:1:
      Can't make a derived instance of
-        ‘Show (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
+        ‘Show (Foo 'LiftedRep)’ 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 (BoxedRep Lifted))’
+     In the stand-alone deriving instance for ‘Show (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.hs b/testsuite/tests/typecheck/should_fail/T15883e.hs
index cfecdb693e..bb1dcacf92 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 (BoxedRep Lifted))
+deriving stock instance Data (Foo LiftedRep)
 
 
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.stderr b/testsuite/tests/typecheck/should_fail/T15883e.stderr
index a20b3f5d43..05e07f0307 100644
--- a/testsuite/tests/typecheck/should_fail/T15883e.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883e.stderr
@@ -1,6 +1,5 @@
 T15883e.hs:16:1:
      Can't make a derived instance of
-        ‘Data (Foo ('BoxedRep 'Lifted))’ with the stock strategy:
+        ‘Data (Foo 'LiftedRep)’ 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 (BoxedRep Lifted))’
+     In the stand-alone deriving instance for ‘Data (Foo LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T17021.stderr b/testsuite/tests/typecheck/should_fail/T17021.stderr
index 96c700c4b7..12d6d687d8 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 ('BoxedRep 'Lifted))
+      Kind: TYPE (Id 'LiftedRep)
     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 f60e09922a..a9e87fed98 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/all.T b/testsuite/tests/typecheck/should_fail/all.T
index cec7b3c9ef..3eff08d080 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -440,7 +440,6 @@ 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 5e1995d3eb..efb81e8ee6 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 ('BoxedRep 'Unlifted)
+        ByteArray# :: TYPE 'UnliftedRep
     • 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 82553b4ff2..d57d2e1499 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 [BoxedRep Lifted, IntRep])
+  MkG :: G (TupleRep [LiftedRep, 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 [BoxedRep Lifted, IntRep])). c -> c
+foo MkG = (\x -> x) :: forall (c :: TYPE (TupleRep [LiftedRep, 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
deleted file mode 100644
index 8302a43693..0000000000
--- a/testsuite/tests/typecheck/should_run/LevPolyResultInst.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# 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
deleted file mode 100644
index 1cc8b5e10d..0000000000
--- a/testsuite/tests/typecheck/should_run/LevPolyResultInst.stdout
+++ /dev/null
@@ -1,2 +0,0 @@
-True
-False
diff --git a/testsuite/tests/typecheck/should_run/T12809.hs b/testsuite/tests/typecheck/should_run/T12809.hs
index 3e20403add..66031a5af7 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 [BoxedRep Lifted, IntRep])). Bool -> a -> a -> a
+cond :: forall (a :: TYPE (TupleRep [LiftedRep, 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 73c98017f2..ffa0e65dc9 100644
--- a/testsuite/tests/typecheck/should_run/T14236.stdout
+++ b/testsuite/tests/typecheck/should_run/T14236.stdout
@@ -1,3 +1,3 @@
-(FUN 'Many ('BoxedRep 'Lifted) ('BoxedRep 'Lifted) Int,Char)
-(FUN 'Many 'IntRep ('BoxedRep 'Lifted) Int#,Char)
+(FUN 'Many 'LiftedRep 'LiftedRep Int,Char)
+(FUN 'Many 'IntRep 'LiftedRep Int#,Char)
 Int# -> [Char]
diff --git a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
index 6ef72dfb83..1303db844c 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 ('BoxedRep 'Lifted) ('BoxedRep 'Lifted)
+good: FUN 'Many 'LiftedRep 'LiftedRep
 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 8bd8471bdf..cec6833b64 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.hs
+++ b/testsuite/tests/typecheck/should_run/TypeOf.hs
@@ -28,9 +28,9 @@ main = do
   print $ typeOf (Proxy :: Proxy [1,2,3])
   print $ typeOf (Proxy :: Proxy 'EQ)
   print $ typeOf (Proxy :: Proxy TYPE)
-  print $ typeOf (Proxy :: Proxy (TYPE ('BoxedRep 'Lifted)))
+  print $ typeOf (Proxy :: Proxy (TYPE 'LiftedRep))
   print $ typeOf (Proxy :: Proxy *)
   print $ typeOf (Proxy :: Proxy ★)
-  print $ typeOf (Proxy :: Proxy ('BoxedRep 'Lifted))
+  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 3cb5e49036..40d2cb5f8f 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeOf.stdout
@@ -19,6 +19,6 @@ Proxy (RuntimeRep -> *) TYPE
 Proxy * *
 Proxy * *
 Proxy * *
-Proxy RuntimeRep ('BoxedRep 'Lifted)
+Proxy RuntimeRep 'LiftedRep
 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 886479fd33..beae93f6b3 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 ('BoxedRep 'Lifted)))
+  print $ rep @(Proxy (TYPE 'LiftedRep))
   print $ rep @(Proxy *)
   print $ rep @(Proxy ★)
-  print $ rep @(Proxy ('BoxedRep 'Lifted))
+  print $ rep @(Proxy 'LiftedRep)
 
   -- 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 cf43264714..a0c03e09d8 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 ('BoxedRep 'Lifted) Int# Int
+(#,#) 'IntRep 'LiftedRep 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 ('BoxedRep 'Lifted)
+Proxy RuntimeRep 'LiftedRep
 RealWorld
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index ef7bedb354..ef8ae9136d 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -145,6 +145,5 @@ 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 18a67a078d..54af3fdfa6 100644
--- a/testsuite/tests/unboxedsums/T12711.stdout
+++ b/testsuite/tests/unboxedsums/T12711.stdout
@@ -1,4 +1,2 @@
 (# _ | _ #) :: TYPE
-                 ('GHC.Types.SumRep
-                    '[ 'GHC.Types.BoxedRep 'GHC.Types.Lifted,
-                       'GHC.Types.BoxedRep 'GHC.Types.Lifted])
+                 ('GHC.Types.SumRep '[ 'GHC.Types.LiftedRep, 'GHC.Types.LiftedRep])
diff --git a/testsuite/tests/unboxedsums/sum_rr.hs b/testsuite/tests/unboxedsums/sum_rr.hs
index 11c8cbb648..448a9b2221 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 '[BoxedRep Lifted, IntRep])) = Wat a
+data Wat (a :: TYPE (SumRep '[LiftedRep, IntRep])) = Wat a