Update levity polymorphism

This commit implements the proposal in
https://github.com/ghc-proposals/ghc-proposals/pull/29 and
https://github.com/ghc-proposals/ghc-proposals/pull/35.

Here are some of the pieces of that proposal:

* Some of RuntimeRep's constructors have been shortened.

* TupleRep and SumRep are now parameterized over a list of RuntimeReps.
* This
means that two types with the same kind surely have the same
representation.
Previously, all unboxed tuples had the same kind, and thus the fact
above was
false.

* RepType.typePrimRep and friends now return a *list* of PrimReps. These
functions can now work successfully on unboxed tuples. This change is
necessary because we allow abstraction over unboxed tuple types and so
cannot
always handle unboxed tuples specially as we did before.

* We sometimes have to create an Id from a PrimRep. I thus split PtrRep
* into
LiftedRep and UnliftedRep, so that the created Ids have the right
strictness.

* The RepType.RepType type was removed, as it didn't seem to help with
* much.

* The RepType.repType function is also removed, in favor of typePrimRep.

* I have waffled a good deal on whether or not to keep VoidRep in
TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not*
represented in RuntimeRep, and typePrimRep will never return a list
including
VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can
imagine another design choice where we have a PrimRepV type that is
PrimRep
with an extra constructor. That seemed to be a heavier design, though,
and I'm
not sure what the benefit would be.

* The last, unused vestiges of # (unliftedTypeKind) have been removed.

* There were several pretty-printing bugs that this change exposed;
* these are fixed.

* We previously checked for levity polymorphism in the types of binders.
* But we
also must exclude levity polymorphism in function arguments. This is
hard to check
for, requiring a good deal of care in the desugarer. See Note [Levity
polymorphism
checking] in DsMonad.

* In order to efficiently check for levity polymorphism in functions, it
* was necessary
to add a new bit of IdInfo. See Note [Levity info] in IdInfo.

* It is now safe for unlifted types to be unsaturated in Core. Core Lint
* is updated
accordingly.

* We can only know strictness after zonking, so several checks around
* strictness
in the type-checker (checkStrictBinds, the check for unlifted variables
under a ~
pattern) have been moved to the desugarer.

* Along the way, I improved the treatment of unlifted vs. banged
* bindings. See
Note [Strict binds checks] in DsBinds and #13075.

* Now that we print type-checked source, we must be careful to print
* ConLikes correctly.
This is facilitated by a new HsConLikeOut constructor to HsExpr.
Particularly troublesome
are unlifted pattern synonyms that get an extra void# argument.

* Includes a submodule update for haddock, getting rid of #.

* New testcases:
  typecheck/should_fail/StrictBinds
  typecheck/should_fail/T12973
  typecheck/should_run/StrictPats
  typecheck/should_run/T12809
  typecheck/should_fail/T13105
  patsyn/should_fail/UnliftedPSBind
  typecheck/should_fail/LevPolyBounded
  typecheck/should_compile/T12987
  typecheck/should_compile/T11736

* Fixed tickets:
  #12809
  #12973
  #11736
  #13075
  #12987

* This also adds a test case for #13105. This test case is
* "compile_fail" and
succeeds, because I want the testsuite to monitor the error message.
When #13105 is fixed, the test case will compile cleanly.

62 files changed, 487 insertions, 154 deletions

diff --git a/testsuite/tests/deSugar/should_compile/T10662.stderr b/testsuite/tests/deSugar/should_compile/T10662.stderr
index d81891619c..f27fc977b6 100644
--- a/testsuite/tests/deSugar/should_compile/T10662.stderr
+++ b/testsuite/tests/deSugar/should_compile/T10662.stderr
@@ -2,4 +2,4 @@
 T10662.hs:3:3: warning: [-Wunused-do-bind (in -Wall)]
     A do-notation statement discarded a result of type ‘[Char]’
     Suppress this warning by saying
-      ‘_ <- ($) return let a = "hello" in a’
+      ‘_ <- return $ let a = "hello" in a’
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
index 2f0edf8593..e5c2002e0c 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
@@ -82,7 +82,7 @@ data TyCon (a :: k) where
   Arrow :: TyCon (->)
   TYPE  :: TyCon TYPE
   RuntimeRep :: TyCon RuntimeRep
-  PtrRepLifted' :: TyCon 'PtrRepLifted
+  LiftedRep' :: TyCon 'LiftedRep
   -- If extending, add to eqTyCon too
 
 eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
@@ -94,7 +94,7 @@ eqTyCon Maybe Maybe = Just HRefl
 eqTyCon Arrow Arrow = Just HRefl
 eqTyCon TYPE TYPE = Just HRefl
 eqTyCon RuntimeRep RuntimeRep = Just HRefl
-eqTyCon PtrRepLifted' PtrRepLifted' = Just HRefl
+eqTyCon LiftedRep' LiftedRep' = Just HRefl
 eqTyCon _ _ = Nothing
 
 -- Check whether or not a type is really a plain old tycon;
@@ -212,7 +212,7 @@ instance TyConAble []        where tyCon = List
 instance TyConAble Maybe     where tyCon = Maybe
 instance TyConAble (->)      where tyCon = Arrow
 instance TyConAble TYPE      where tyCon = TYPE
-instance TyConAble 'PtrRepLifted   where tyCon = PtrRepLifted'
+instance TyConAble 'LiftedRep   where tyCon = LiftedRep'
 instance TyConAble RuntimeRep    where tyCon = RuntimeRep
 
 -- Can't just define Typeable the way we want, because the instances
diff --git a/testsuite/tests/dependent/should_fail/T11473.stderr b/testsuite/tests/dependent/should_fail/T11473.stderr
index 431c2dff92..3252452eb2 100644
--- a/testsuite/tests/dependent/should_fail/T11473.stderr
+++ b/testsuite/tests/dependent/should_fail/T11473.stderr
@@ -1,6 +1,6 @@
 
 T11473.hs:19:7: error:
-    A representation-polymorphic type is not allowed here:
+    A levity-polymorphic type is not allowed here:
       Type: a
       Kind: TYPE r
     In the type of binder ‘x’
diff --git a/testsuite/tests/deriving/should_fail/T12512.hs b/testsuite/tests/deriving/should_fail/T12512.hs
index 87c3d668df..4d4e52c06c 100644
--- a/testsuite/tests/deriving/should_fail/T12512.hs
+++ b/testsuite/tests/deriving/should_fail/T12512.hs
@@ -1,14 +1,13 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UnboxedSums #-}
 {-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE TypeInType #-}
 module T12512 where
 
 import GHC.Exts
 
-class Wat1 (a :: TYPE 'UnboxedTupleRep)
+class Wat1 (a :: TYPE ('TupleRep ['LiftedRep, 'LiftedRep]))
 deriving instance Wat1 (# a, b #)
 
-class Wat2 (a :: TYPE 'UnboxedSumRep)
+class Wat2 (a :: TYPE ('SumRep ['LiftedRep, 'LiftedRep]))
 deriving instance Wat2 (# a | b #)
diff --git a/testsuite/tests/deriving/should_fail/T12512.stderr b/testsuite/tests/deriving/should_fail/T12512.stderr
index 48f0eae205..a62cda6b99 100644
--- a/testsuite/tests/deriving/should_fail/T12512.stderr
+++ b/testsuite/tests/deriving/should_fail/T12512.stderr
@@ -1,10 +1,10 @@
 
-T12512.hs:11:1: error:
+T12512.hs:10:1: error:
     • Can't make a derived instance of ‘Wat1 (# a, b #)’:
         The last argument of the instance cannot be an unboxed tuple
     • In the stand-alone deriving instance for ‘Wat1 (# a, b #)’
 
-T12512.hs:14:1: error:
+T12512.hs:13:1: error:
     • Can't make a derived instance of ‘Wat2 (# a | b #)’:
         The last argument of the instance cannot be an unboxed sum
     • In the stand-alone deriving instance for ‘Wat2 (# a | b #)’
diff --git a/testsuite/tests/ghci/scripts/GhciKinds.stdout b/testsuite/tests/ghci/scripts/GhciKinds.stdout
index 3556e621a4..5431bbc17d 100644
--- a/testsuite/tests/ghci/scripts/GhciKinds.stdout
+++ b/testsuite/tests/ghci/scripts/GhciKinds.stdout
@@ -10,4 +10,8 @@ F (Maybe Bool) :: *
 forall a. F (Maybe a) :: *
 = Char
 $(unboxedTupleT 2) :: forall (k0 :: RuntimeRep) (k1 :: RuntimeRep).
-                      TYPE k0 -> TYPE k1 -> TYPE 'UnboxedTupleRep
+                      TYPE k0
+                      -> TYPE k1
+                      -> TYPE
+                           ('TupleRep
+                              ((':) RuntimeRep k0 ((':) RuntimeRep k1 ('[] RuntimeRep))))
diff --git a/testsuite/tests/ghci/scripts/T9140.stdout b/testsuite/tests/ghci/scripts/T9140.stdout
index 6456067f59..85406d04b6 100644
--- a/testsuite/tests/ghci/scripts/T9140.stdout
+++ b/testsuite/tests/ghci/scripts/T9140.stdout
@@ -1,13 +1,11 @@
 
 <interactive>:2:5: error:
-    You can't mix polymorphic and unlifted bindings
-      a = (# 1 #)
-      Probable fix: add a type signature
+    You can't mix polymorphic and unlifted bindings: a = (# 1 #)
+    Probable fix: add a type signature
 
 <interactive>:3:5: error:
-    You can't mix polymorphic and unlifted bindings
-      a = (# 1, 3 #)
-      Probable fix: add a type signature
+    You can't mix polymorphic and unlifted bindings: a = (# 1, 3 #)
+    Probable fix: add a type signature
 
 <interactive>:1:1: error:
     GHCi can't bind a variable of unlifted type:
diff --git a/testsuite/tests/patsyn/should_fail/UnliftedPSBind.hs b/testsuite/tests/patsyn/should_fail/UnliftedPSBind.hs
new file mode 100644
index 0000000000..9cb38ed404
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/UnliftedPSBind.hs
@@ -0,0 +1,12 @@
+
+-- This is testing the printing of the builder really.
+{-# LANGUAGE MagicHash, PatternSynonyms #-}
+{-# OPTIONS_GHC -Werror -Wunbanged-strict-patterns #-}
+module UnliftedPSBind where
+
+import GHC.Exts
+
+pattern P x = I# x
+
+x = ()
+  where P x = P 4#
diff --git a/testsuite/tests/patsyn/should_fail/UnliftedPSBind.stderr b/testsuite/tests/patsyn/should_fail/UnliftedPSBind.stderr
new file mode 100644
index 0000000000..6b6b97710e
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/UnliftedPSBind.stderr
@@ -0,0 +1,8 @@
+
+UnliftedPSBind.hs:12:9: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
+      P x = P 4#
+
+<no location info>: error: 
+Failing due to -Werror.
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index cb23b3fb2a..50a3eea6c1 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -33,3 +33,4 @@ test('T11265', normal, compile_fail, [''])
 test('T11667', normal, compile_fail, [''])
 test('T12165', normal, compile_fail, [''])
 test('T12819', normal, compile_fail, [''])
+test('UnliftedPSBind', normal, compile_fail, [''])
diff --git a/testsuite/tests/patsyn/should_fail/unboxed-bind.hs b/testsuite/tests/patsyn/should_fail/unboxed-bind.hs
index ef1b070d49..6be73839f2 100644
--- a/testsuite/tests/patsyn/should_fail/unboxed-bind.hs
+++ b/testsuite/tests/patsyn/should_fail/unboxed-bind.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE PatternSynonyms, MagicHash #-}
+{-# OPTIONS_GHC -Wunbanged-strict-patterns -Werror=unbanged-strict-patterns #-}
 module ShouldFail where
 
 import GHC.Base
diff --git a/testsuite/tests/patsyn/should_fail/unboxed-bind.stderr b/testsuite/tests/patsyn/should_fail/unboxed-bind.stderr
index 17ca7afd3b..8f20f91be9 100644
--- a/testsuite/tests/patsyn/should_fail/unboxed-bind.stderr
+++ b/testsuite/tests/patsyn/should_fail/unboxed-bind.stderr
@@ -1,6 +1,8 @@
 
-unboxed-bind.hs:10:11:
-    Pattern bindings containing unlifted types should use an outermost bang pattern:
+unboxed-bind.hs:11:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
       P arg = x
-    In the expression: let P arg = x in arg
-    In an equation for ‘f’: f x = let P arg = x in arg
+
+<no location info>: error: 
+Failing due to -Werror.
diff --git a/testsuite/tests/quasiquotation/T7918.stdout b/testsuite/tests/quasiquotation/T7918.stdout
index 4dff68d1ce..96482371a2 100644
--- a/testsuite/tests/quasiquotation/T7918.stdout
+++ b/testsuite/tests/quasiquotation/T7918.stdout
@@ -1,10 +1,5 @@
-(True, T7918B.hs:6:11-14)
 (id, T7918B.hs:7:11-14)
-(True, T7918B.hs:7:11-14)
-(True, T7918B.hs:8:11-14)
 (||, T7918B.hs:8:11-14)
-(False, T7918B.hs:8:11-14)
-(False, T7918B.hs:9:11-14)
 (undefined, T7918B.hs:11:7-15)
 (Bool, T7918B.hs:11:24-27)
 (undefined, T7918B.hs:12:7-15)
@@ -25,6 +20,3 @@
 (undefined, T7918B.hs:18:16-24)
 (y, T7918B.hs:19:9-12)
 (undefined, T7918B.hs:19:16-24)
-(Module, <no location info>)
-(TrNameS, <no location info>)
-(TrNameS, <no location info>)
diff --git a/testsuite/tests/simplCore/should_compile/T9400.stderr b/testsuite/tests/simplCore/should_compile/T9400.stderr
index d4b7898d83..bab1751a86 100644
--- a/testsuite/tests/simplCore/should_compile/T9400.stderr
+++ b/testsuite/tests/simplCore/should_compile/T9400.stderr
@@ -46,7 +46,7 @@ main =
              @ ()
              (putStrLn (unpackCString# "efg"#))
              (Control.Exception.Base.patError
-                @ 'PtrRepLifted @ (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 732265a8f6..e7fc531a43 100644
--- a/testsuite/tests/simplCore/should_compile/spec-inline.stderr
+++ b/testsuite/tests/simplCore/should_compile/spec-inline.stderr
@@ -35,7 +35,7 @@ Roman.foo3 :: Int
 [GblId, Str=x]
 Roman.foo3 =
   Control.Exception.Base.patError
-    @ 'GHC.Types.PtrRepLifted
+    @ 'GHC.Types.LiftedRep
     @ Int
     "spec-inline.hs:(19,5)-(29,25)|function go"#
 
diff --git a/testsuite/tests/th/T12403.stdout b/testsuite/tests/th/T12403.stdout
index 9b75e8b272..24e222a732 100644
--- a/testsuite/tests/th/T12403.stdout
+++ b/testsuite/tests/th/T12403.stdout
@@ -1 +1,5 @@
-data Main.T = Main.T ((# , #) GHC.Types.Int GHC.Types.Int)
+data Main.T
+    = Main.T ((# , #) GHC.Types.Int
+                      GHC.Types.Int :: GHC.Prim.TYPE (GHC.Types.TupleRep (GHC.Types.: GHC.Types.LiftedRep
+                                                                                      (GHC.Types.: GHC.Types.LiftedRep
+                                                                                                   GHC.Types.[]))))
diff --git a/testsuite/tests/th/T12478_1.stdout b/testsuite/tests/th/T12478_1.stdout
index 8437f925d5..f94db5992d 100644
--- a/testsuite/tests/th/T12478_1.stdout
+++ b/testsuite/tests/th/T12478_1.stdout
@@ -1 +1 @@
-TyConI (DataD [] Main.T [] Nothing [NormalC Main.T [(Bang NoSourceUnpackedness NoSourceStrictness,AppT (AppT (UnboxedSumT 2) (ConT GHC.Types.Int)) (ConT GHC.Types.Char))]] [])
+TyConI (DataD [] Main.T [] Nothing [NormalC Main.T [(Bang NoSourceUnpackedness NoSourceStrictness,SigT (AppT (AppT (UnboxedSumT 2) (ConT GHC.Types.Int)) (ConT GHC.Types.Char)) (AppT (ConT GHC.Prim.TYPE) (AppT (ConT GHC.Types.SumRep) (AppT (AppT (ConT GHC.Types.:) (ConT GHC.Types.LiftedRep)) (AppT (AppT (ConT GHC.Types.:) (ConT GHC.Types.LiftedRep)) (ConT GHC.Types.[]))))))]] [])
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index d9485cebb7..4bfc53a78e 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -1,11 +1,11 @@
 
 T5358.hs:14:12: error:
-    Exception when trying to run compile-time code:
-      runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
-CallStack (from ImplicitParams):
+    • Exception when trying to run compile-time code:
+        runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
+CallStack (from HasCallStack):
   error, called at T5358.hs:15:18 in main:T5358
-    Code: do VarI _ t _ <- reify (mkName "prop_x1")
-             ($) error ((++) "runTest called error: " pprint t)
-    In the untyped splice:
-      $(do VarI _ t _ <- reify (mkName "prop_x1")
-           error $ ("runTest called error: " ++ pprint t))
+      Code: do VarI _ t _ <- reify (mkName "prop_x1")
+               error $ ("runTest called error: " ++ pprint t)
+    • In the untyped splice:
+        $(do VarI _ t _ <- reify (mkName "prop_x1")
+             error $ ("runTest called error: " ++ pprint t))
diff --git a/testsuite/tests/th/T5976.stderr b/testsuite/tests/th/T5976.stderr
index 507d9d8b8d..f4e9568927 100644
--- a/testsuite/tests/th/T5976.stderr
+++ b/testsuite/tests/th/T5976.stderr
@@ -2,6 +2,6 @@
 T5976.hs:1:1: error:
     Exception when trying to run compile-time code:
       bar
-CallStack (from ImplicitParams):
+CallStack (from HasCallStack):
   error, called at T5976.hs:3:21 in main:Main
-    Code: error ((++) "foo " error "bar")
+    Code: error ("foo " ++ error "bar")
diff --git a/testsuite/tests/th/T8987.stderr b/testsuite/tests/th/T8987.stderr
index 1af2e29b7f..7b5f400f6f 100644
--- a/testsuite/tests/th/T8987.stderr
+++ b/testsuite/tests/th/T8987.stderr
@@ -2,7 +2,7 @@
 T8987.hs:1:1: error:
     Exception when trying to run compile-time code:
       Prelude.undefined
-CallStack (from ImplicitParams):
-  error, called at libraries/base/GHC/Err.hs:43:14 in base:GHC.Err
+CallStack (from HasCallStack):
+  error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
   undefined, called at T8987.hs:6:23 in main:T8987
-    Code: (>>) reportWarning ['1', undefined] return []
+    Code: reportWarning ['1', undefined] >> return []
diff --git a/testsuite/tests/typecheck/should_compile/T11723.hs b/testsuite/tests/typecheck/should_compile/T11723.hs
new file mode 100644
index 0000000000..1933024f2e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T11723.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeInType #-}
+module Example where
+
+import Data.Typeable
+import GHC.Exts
+
+data Wat (a :: TYPE ('TupleRep '[])) = Wat a
diff --git a/testsuite/tests/typecheck/should_compile/T11736.hs b/testsuite/tests/typecheck/should_compile/T11736.hs
new file mode 100644
index 0000000000..8bcbc3e06b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T11736.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE UnboxedTuples #-}
+
+module T11736 where
+
+import Data.Proxy
+
+foo :: Proxy (#,#)
+foo = Proxy
diff --git a/testsuite/tests/typecheck/should_compile/T12987.hs b/testsuite/tests/typecheck/should_compile/T12987.hs
new file mode 100644
index 0000000000..0997985601
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12987.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeInType #-}
+
+module T12987 where
+
+import GHC.Exts
+
+class NUM (a :: TYPE rep) where add :: a -> a -> a
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b70ab83b34..c5e9163bbe 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -565,3 +565,6 @@ test('T12919', expect_broken(12919), compile, [''])
 test('T12936', normal, compile, [''])
 test('T13050', normal, compile, ['-fdefer-type-errors'])
 test('T13083', normal, compile, [''])
+test('T11723', normal, compile, [''])
+test('T12987', normal, compile, [''])
+test('T11736', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.hs b/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.hs
deleted file mode 100644
index 2935416538..0000000000
--- a/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.hs
+++ /dev/null
@@ -1,10 +0,0 @@
-{-# LANGUAGE TypeFamilies, KindSignatures, TypeInType #-}
-
-module BadUnboxedTuple where
-
-import GHC.Exts
-
-type family F :: TYPE UnboxedTupleRep
-
-foo :: F -> ()
-foo _ = ()
diff --git a/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.stderr b/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.stderr
deleted file mode 100644
index 7c5ad5762f..0000000000
--- a/testsuite/tests/typecheck/should_fail/BadUnboxedTuple.stderr
+++ /dev/null
@@ -1,6 +0,0 @@
-
-BadUnboxedTuple.hs:10:5: error:
-    The type ‘F’ is not an unboxed tuple,
-    and yet its kind suggests that it has the representation
-    of an unboxed tuple. This is not allowed.
-    In a wildcard pattern
diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs b/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs
new file mode 100644
index 0000000000..0607956784
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs
@@ -0,0 +1,11 @@
+-- inspired by comment:25 on #12708
+
+{-# LANGUAGE TypeInType #-}
+
+module LevPolyBounded where
+
+import GHC.Exts
+
+class XBounded (a :: TYPE r) where
+  minBound :: a
+  maxBound :: a
diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr
new file mode 100644
index 0000000000..21ae68ab85
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.stderr
@@ -0,0 +1,5 @@
+
+LevPolyBounded.hs:10:15: error:
+    • Expected a type, but ‘a’ has kind ‘TYPE r’
+    • In the type signature: LevPolyBounded.minBound :: a
+      In the class declaration for ‘XBounded’
diff --git a/testsuite/tests/typecheck/should_fail/StrictBinds.hs b/testsuite/tests/typecheck/should_fail/StrictBinds.hs
new file mode 100644
index 0000000000..bd951f96b1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/StrictBinds.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE MagicHash #-}
+
+module StrictBinds where
+
+import GHC.Exts
+
+foo = let x = 3# +# y
+          y = x in
+      True
diff --git a/testsuite/tests/typecheck/should_fail/StrictBinds.stderr b/testsuite/tests/typecheck/should_fail/StrictBinds.stderr
new file mode 100644
index 0000000000..082d71176a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/StrictBinds.stderr
@@ -0,0 +1,5 @@
+
+StrictBinds.hs:7:11: error:
+    Recursive bindings for unlifted types aren't allowed:
+      x = 3# +# y
+      y = x
diff --git a/testsuite/tests/typecheck/should_fail/T11723.hs b/testsuite/tests/typecheck/should_fail/T11723.hs
deleted file mode 100644
index 4761cc4131..0000000000
--- a/testsuite/tests/typecheck/should_fail/T11723.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE KindSignatures #-}
-module Example where
-
-import Data.Typeable
-import GHC.Exts
-
-data Wat (a :: TYPE 'UnboxedTupleRep) = Wat a
diff --git a/testsuite/tests/typecheck/should_fail/T11723.stderr b/testsuite/tests/typecheck/should_fail/T11723.stderr
deleted file mode 100644
index b63a182d2c..0000000000
--- a/testsuite/tests/typecheck/should_fail/T11723.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T11723.hs:8:41: error:
-    • The type ‘a’ is not an unboxed tuple,
-      and yet its kind suggests that it has the representation
-      of an unboxed tuple. This is not allowed.
-    • In the definition of data constructor ‘Wat’
-      In the data type declaration for ‘Wat’
diff --git a/testsuite/tests/typecheck/should_fail/T11724.stderr b/testsuite/tests/typecheck/should_fail/T11724.stderr
index 2971b27597..dbdbb6fdef 100644
--- a/testsuite/tests/typecheck/should_fail/T11724.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11724.stderr
@@ -1,6 +1,6 @@
 
 T11724.hs:7:44: error:
-    • A representation-polymorphic type is not allowed here:
+    • A levity-polymorphic type is not allowed here:
         Type: a
         Kind: TYPE r
     • In the definition of data constructor ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T12973.hs b/testsuite/tests/typecheck/should_fail/T12973.hs
new file mode 100644
index 0000000000..624d24be24
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12973.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RebindableSyntax, TypeInType, ExplicitForAll #-}
+
+module T12973 where
+
+import qualified Prelude as P
+import GHC.Exts
+
+class Num (a :: TYPE r) where
+  (+) :: a -> a -> a
+  fromInteger :: P.Integer -> a
+
+foo :: forall (a :: TYPE r). Num a => a
+foo = 3 + 4
+
+
diff --git a/testsuite/tests/typecheck/should_fail/T12973.stderr b/testsuite/tests/typecheck/should_fail/T12973.stderr
new file mode 100644
index 0000000000..a6d97009cd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12973.stderr
@@ -0,0 +1,12 @@
+
+T12973.hs:13:7: error:
+    A levity-polymorphic type is not allowed here:
+      Type: a
+      Kind: TYPE r
+    In the type of expression: 3
+
+T12973.hs:13:11: error:
+    A levity-polymorphic type is not allowed here:
+      Type: a
+      Kind: TYPE r
+    In the type of expression: 4
diff --git a/testsuite/tests/typecheck/should_fail/T13105.hs b/testsuite/tests/typecheck/should_fail/T13105.hs
new file mode 100644
index 0000000000..44384dc19d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13105.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE UnicodeSyntax, MagicHash, TypeInType, TypeFamilies #-}
+
+-- from Conal Elliott
+-- Actually, this *should* work. But I want to put it in the testsuite
+-- as a succeeding "compile_fail" test to make sure that we don't panic.
+
+module RepRep where
+
+import GHC.Exts
+
+type family RepRep a ∷ RuntimeRep
+
+class HasRep a where
+  type Rep a ∷ TYPE (RepRep a)
+  repr ∷ a → Rep a
+  abst ∷ Rep a → a
+
+type instance RepRep Int = IntRep
+
+instance HasRep Int where
+  type Rep Int = Int#
+  abst n = I# n
+  repr (I# n) = n
diff --git a/testsuite/tests/typecheck/should_fail/T13105.stderr b/testsuite/tests/typecheck/should_fail/T13105.stderr
new file mode 100644
index 0000000000..c54327ef70
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13105.stderr
@@ -0,0 +1,6 @@
+
+T13105.hs:22:8: error:
+    A levity-polymorphic type is not allowed here:
+      Type: Rep Int
+      Kind: TYPE (RepRep Int)
+    In the type of binder ‘n’
diff --git a/testsuite/tests/typecheck/should_fail/T2806.hs b/testsuite/tests/typecheck/should_fail/T2806.hs
index 6ada5d83fb..ac95542c94 100644
--- a/testsuite/tests/typecheck/should_fail/T2806.hs
+++ b/testsuite/tests/typecheck/should_fail/T2806.hs
@@ -1,5 +1,6 @@
 
 {-# LANGUAGE MagicHash #-}
+{-# OPTIONS_GHC -Wunbanged-strict-patterns #-}
 
 -- Trac #2806
 
@@ -10,4 +11,3 @@ import GHC.Base
 foo :: Int
 foo = 3
     where (I# _x) = 4
-
diff --git a/testsuite/tests/typecheck/should_fail/T2806.stderr b/testsuite/tests/typecheck/should_fail/T2806.stderr
index 25cc8e65a0..02a4d81c15 100644
--- a/testsuite/tests/typecheck/should_fail/T2806.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2806.stderr
@@ -1,9 +1,5 @@
 
-T2806.hs:12:11:
-    Pattern bindings containing unlifted types should use an outermost bang pattern:
+T2806.hs:13:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
       (I# _x) = 4
-    In an equation for ‘foo’:
-        foo
-          = 3
-          where
-              (I# _x) = 4
diff --git a/testsuite/tests/typecheck/should_fail/T6078.stderr b/testsuite/tests/typecheck/should_fail/T6078.stderr
index b45363bdc3..62a4210443 100644
--- a/testsuite/tests/typecheck/should_fail/T6078.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6078.stderr
@@ -1,11 +1,5 @@
 
 T6078.hs:8:10: error:
-    You can't mix polymorphic and unlifted bindings
+    You can't mix polymorphic and unlifted bindings:
       ip1p@(Ptr ip1) = Ptr ip0 `plusPtr` len
-      Probable fix: add a type signature
-    In the expression:
-      let ip1p@(Ptr ip1) = Ptr ip0 `plusPtr` len in ip1p
-    In the expression:
-      \ fpbuf ip0 ipe s0 -> let ip1p@(Ptr ip1) = ... in ip1p
-    In an equation for ‘byteStringSlice’:
-        byteStringSlice len = \ fpbuf ip0 ipe s0 -> let ... in ip1p
+    Probable fix: add a type signature
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index c490fec10e..9931037e4e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -187,7 +187,7 @@ test('tcfail199', normal, compile_fail, [''])
 test('tcfail200', normal, compile_fail, [''])
 test('tcfail201', normal, compile_fail, [''])
 test('tcfail202', normal, compile_fail, [''])
-test('tcfail203', normal, compile_fail, [''])
+test('tcfail203', normal, compile, [''])
 test('tcfail203a', normal, compile_fail, [''])
 test('tcfail204', normal, compile_fail, [''])
 test('tcfail206', normal, compile_fail, [''])
@@ -204,7 +204,7 @@ test('T2994', normal, compile_fail, [''])
 test('T3155', normal, compile_fail, [''])
 test('T3176', normal, compile_fail, [''])
 test('T1633', normal, compile_fail, [''])
-test('T2806', normal, compile_fail, [''])
+test('T2806', normal, compile, [''])
 test('T3323', normal, compile_fail, [''])
 test('T3406', normal, compile_fail, [''])
 test('T3540', normal, compile_fail, [''])
@@ -406,9 +406,7 @@ test('T11563', normal, compile_fail, [''])
 test('T11541', normal, compile_fail, [''])
 test('T11313', normal, compile_fail, [''])
 test('T11623', normal, compile_fail, [''])
-test('T11723', normal, compile_fail, [''])
 test('T11724', normal, compile_fail, [''])
-test('BadUnboxedTuple', normal, compile_fail, [''])
 test('T11698', normal, compile_fail, [''])
 test('T11947a', normal, compile_fail, [''])
 test('T11948', normal, compile_fail, [''])
@@ -435,3 +433,7 @@ test('T12042', extra_clean(['T12042a.hi', 'T12042a.o', 'T12042.hi-boot', 'T12042
 test('T12966', normal, compile_fail, [''])
 test('T12837', normal, compile_fail, [''])
 test('T12921', normal, compile_fail, [''])
+test('T12973', normal, compile_fail, [''])
+test('StrictBinds', normal, compile_fail, [''])
+test('T13105', normal, compile_fail, [''])
+test('LevPolyBounded', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail203.hs b/testsuite/tests/typecheck/should_fail/tcfail203.hs
index 7f51dae3b5..096cf5796b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail203.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail203.hs
@@ -1,6 +1,7 @@
 -- trac #2806
 
 {-# LANGUAGE MagicHash, UnboxedTuples, BangPatterns #-}
+{-# OPTIONS_GHC -Wunbanged-strict-patterns #-}
 
 module Foo where
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail203.stderr b/testsuite/tests/typecheck/should_fail/tcfail203.stderr
index 21454e345d..d9f7087229 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail203.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail203.stderr
@@ -1,36 +1,40 @@
 
-tcfail203.hs:28:11:
-    Pattern bindings containing unlifted types should use an outermost bang pattern:
+tcfail203.hs:29:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
       (I# x) = 5
-    In an equation for ‘fail2’:
-        fail2
-          = 'a'
-          where
-              (I# x) = 5
-
-tcfail203.hs:31:11:
-    Pattern bindings containing unlifted types should use an outermost bang pattern:
+
+tcfail203.hs:32:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
       (b, I# x) = (True, 5)
-    In an equation for ‘fail3’:
-        fail3
-          = 'a'
-          where
-              (b, I# x) = (True, 5)
-
-tcfail203.hs:40:11:
-    Pattern bindings containing unlifted types should use an outermost bang pattern:
+
+tcfail203.hs:35:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
+      (# b, I# x #) = (# True, 5 #)
+
+tcfail203.hs:38:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
+      (# b, x #) = (# True, 5# #)
+
+tcfail203.hs:41:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
       (I# !x) = 5
-    In an equation for ‘fail6’:
-        fail6
-          = 'a'
-          where
-              (I# !x) = 5
-
-tcfail203.hs:43:11:
-    Pattern bindings containing unlifted types should use an outermost bang pattern:
+
+tcfail203.hs:44:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
       (b, !(I# x)) = (True, 5)
-    In an equation for ‘fail7’:
-        fail7
-          = 'a'
-          where
-              (b, !(I# x)) = (True, 5)
+
+tcfail203.hs:47:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
+      (# b, !(I# x) #) = (# True, 5 #)
+
+tcfail203.hs:50:11: warning: [-Wunbanged-strict-patterns (in -Wextra)]
+    Pattern bindings containing unlifted types should use
+    an outermost bang pattern:
+      (# b, !x #) = (# True, 5# #)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail203a.stderr b/testsuite/tests/typecheck/should_fail/tcfail203a.stderr
index 272ff4254e..153a9259ba 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail203a.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail203a.stderr
@@ -1,6 +1,5 @@
 
-tcfail203a.hs:10:16:
-    A lazy (~) pattern cannot contain unlifted types: ~(c, (I# x))
-    In the pattern: ~(c, (I# x))
-    In the pattern: (b, ~(c, (I# x)))
-    In the pattern: !(b, ~(c, (I# x)))
+tcfail203a.hs:10:17: error:
+    A lazy (~) pattern cannot bind variables of unlifted type.
+    Unlifted variables:
+      x :: Int#
diff --git a/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
new file mode 100644
index 0000000000..e912411209
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE UnboxedTuples, MagicHash, GADTs, TypeInType, ExplicitForAll #-}
+
+
+module Main where
+
+import GHC.Exts
+
+data G a where
+  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 [LiftedRep, IntRep])). c -> c
+
+data H a where
+  MkH :: H IntRep
+
+-- tests that we don't push coercions that make args levity-polymorphic
+-- see Simplify.simplCast
+bar :: forall (r :: RuntimeRep) (a :: TYPE r). H r -> (a -> a -> (# a, a #)) -> a -> (# a, a #)
+bar MkH = (\f x -> f x x) :: forall (b :: TYPE IntRep). (b -> b -> (# b, b #)) -> b -> (# b, b #)
+
+main :: IO ()
+main = do
+  let (# b, x #) = foo MkG (# True, 3# #)
+  print b
+  print (I# x)
+
+  let (# y, z #) = bar MkH (#,#) 8#
+  print (I# y)
+  print (I# z)
diff --git a/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.stdout b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.stdout
new file mode 100644
index 0000000000..97c6c910ed
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.stdout
@@ -0,0 +1,4 @@
+True
+3
+8
+8
diff --git a/testsuite/tests/typecheck/should_run/KindInvariant.stderr b/testsuite/tests/typecheck/should_run/KindInvariant.stderr
index 3fe8131daf..4f6cfffb7f 100644
--- a/testsuite/tests/typecheck/should_run/KindInvariant.stderr
+++ b/testsuite/tests/typecheck/should_run/KindInvariant.stderr
@@ -1,6 +1,6 @@
 
 <interactive>:1:3: error:
     • Expected kind ‘* -> *’,
-        but ‘State#’ has kind ‘* -> TYPE 'VoidRep’
+        but ‘State#’ has kind ‘* -> TYPE ('TupleRep '[])’
     • In the first argument of ‘T’, namely ‘State#’
       In the type ‘T State#’
diff --git a/testsuite/tests/typecheck/should_run/StrictPats.hs b/testsuite/tests/typecheck/should_run/StrictPats.hs
new file mode 100644
index 0000000000..7eed9dc767
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/StrictPats.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE BangPatterns, TypeApplications, UnboxedTuples, MagicHash,
+             UnboxedSums, NoMonomorphismRestriction #-}
+{-# OPTIONS_GHC -Wno-unused-binds -Wno-unbanged-strict-patterns #-}
+
+module Main where
+
+import Control.Exception
+import GHC.Exts
+
+-- This stress-tests the semantics of strict patterns.
+
+ok :: a -> IO ()
+ok x = do
+  evaluate x
+  putStrLn "Evaluation successful."
+
+bad :: a -> IO ()
+bad x = do
+  r <- try @SomeException $ evaluate x
+  case r of
+    Left _  -> putStrLn "Exception thrown as expected."
+    Right _ -> putStrLn "Exception not thrown when expected."
+
+-- OK
+a = True
+  where x :: Num a => a
+        !x = undefined   -- x is a function. Should be OK.
+
+-- should fail
+b = True
+  where x :: a
+        !x = undefined
+
+-- OK
+c = True
+  where I# _ = undefined
+
+-- bad
+d = True
+  where I# _x = undefined
+
+-- OK
+e = True
+  where _ = undefined :: Int#
+
+-- bad
+f = True
+  where _x = undefined :: Int#
+
+-- OK
+g = True
+  where (# _ #) = undefined
+
+-- OK
+h = True
+  where (# _x #) = undefined
+
+-- bad
+i = True
+  where (# _x #) = undefined :: (# Int# #)
+
+-- bad
+j = True
+  where !True = False
+
+-- OK
+k = True
+  where True = False
+
+-- OK
+l = True
+  where 3# = 4#
+
+-- bad
+m = True
+  where !3# = 4#
+
+-- bad
+n = True
+  where _x = undefined :: (# () #)
+
+-- OK
+o = True
+  where (# _x #) = undefined :: (# () #)
+
+-- OK
+p = True
+  where (# _ | #) = (# | True #)
+
+-- bad
+q = True
+  where (# _x | #) = (# | True #) :: (# Int# | Bool #)
+
+-- OK
+r = True
+  where (# _x | #) = (# | True #)
+
+-- bad
+s = True
+  where !(# x #) = undefined
+
+main :: IO ()
+main = do
+  ok a
+  bad b
+  ok c
+  bad d
+  ok e
+  bad f
+  ok g
+  ok h
+  bad i
+  bad j
+  ok k
+  ok l
+  bad m
+  bad n
+  ok o
+  ok p
+  bad q
+  ok r
+  bad s
diff --git a/testsuite/tests/typecheck/should_run/StrictPats.stdout b/testsuite/tests/typecheck/should_run/StrictPats.stdout
new file mode 100644
index 0000000000..509df4e246
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/StrictPats.stdout
@@ -0,0 +1,19 @@
+Evaluation successful.
+Exception thrown as expected.
+Evaluation successful.
+Exception thrown as expected.
+Evaluation successful.
+Exception thrown as expected.
+Evaluation successful.
+Evaluation successful.
+Exception thrown as expected.
+Exception thrown as expected.
+Evaluation successful.
+Evaluation successful.
+Exception thrown as expected.
+Exception thrown as expected.
+Evaluation successful.
+Evaluation successful.
+Exception thrown as expected.
+Evaluation successful.
+Exception thrown as expected.
diff --git a/testsuite/tests/typecheck/should_run/T12809.hs b/testsuite/tests/typecheck/should_run/T12809.hs
new file mode 100644
index 0000000000..9f6da26d76
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T12809.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TypeInType, ExplicitForAll, MagicHash, UnboxedTuples,
+             TypeFamilies, GADTs #-}
+
+module Main where
+
+import GHC.Exts
+
+idint :: forall (a :: TYPE IntRep). a -> a
+idint x = x
+
+five _ = idint 3# +# idint 2#
+
+type family F a where
+  F Int = (# Bool, Int# #)
+  F Char = (# Double, Int# #)
+
+data G a where
+  GInt :: G Int
+  GChar :: G Char
+
+f :: G a -> F a
+f GInt = (# True, 3# #)
+f GChar = (# 3.14, 5# #)
+
+f' :: G a -> F a
+f' GInt = (# False, 7# #)
+f' GChar = (# 2.71829, 11# #)
+
+g :: (# Bool, Int# #) -> String
+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 True x _ = x
+cond False _ x = x
+
+main :: IO ()
+main = do
+  print (I# (five ()))
+  putStrLn (g (f GInt))
+  putStrLn (g (cond False (f GInt) (f' GInt)))
+  putStrLn (h (cond True (f GChar) (f' GChar)))
diff --git a/testsuite/tests/typecheck/should_run/T12809.stdout b/testsuite/tests/typecheck/should_run/T12809.stdout
new file mode 100644
index 0000000000..5d187d8652
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T12809.stdout
@@ -0,0 +1,4 @@
+5
+True 3
+False 7
+3.14 5
diff --git a/testsuite/tests/typecheck/should_run/TypeOf.hs b/testsuite/tests/typecheck/should_run/TypeOf.hs
index 53e035923f..59ea6fdf0d 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.hs
+++ b/testsuite/tests/typecheck/should_run/TypeOf.hs
@@ -27,9 +27,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 'PtrRepLifted))
+  print $ typeOf (Proxy :: Proxy (TYPE 'LiftedRep))
   print $ typeOf (Proxy :: Proxy *)
   print $ typeOf (Proxy :: Proxy ★)
-  print $ typeOf (Proxy :: Proxy 'PtrRepLifted)
+  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 3e3396fa7e..99f113cf00 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeOf.stdout
@@ -19,6 +19,6 @@ Proxy (RuntimeRep -> Constraint) TYPE
 Proxy Constraint Constraint
 Proxy Constraint Constraint
 Proxy Constraint Constraint
-Proxy RuntimeRep 'PtrRepLifted
+Proxy RuntimeRep 'LiftedRep
 Proxy (Nat,Symbol) ('(,) Nat Symbol 1 "hello")
 Proxy (Constraint -> Constraint -> Constraint) ~~
diff --git a/testsuite/tests/typecheck/should_run/TypeRep.hs b/testsuite/tests/typecheck/should_run/TypeRep.hs
index 3ae9577088..5fbf909193 100644
--- a/testsuite/tests/typecheck/should_run/TypeRep.hs
+++ b/testsuite/tests/typecheck/should_run/TypeRep.hs
@@ -39,10 +39,10 @@ main = do
   print $ rep @(Proxy [1,2,3])
   print $ rep @(Proxy 'EQ)
   print $ rep @(Proxy TYPE)
-  print $ rep @(Proxy (TYPE 'PtrRepLifted))
+  print $ rep @(Proxy (TYPE 'LiftedRep))
   print $ rep @(Proxy *)
   print $ rep @(Proxy ★)
-  print $ rep @(Proxy 'PtrRepLifted)
+  print $ rep @(Proxy 'LiftedRep)
 
   -- Something lifted and primitive
   print $ rep @RealWorld
diff --git a/testsuite/tests/typecheck/should_run/TypeRep.stdout b/testsuite/tests/typecheck/should_run/TypeRep.stdout
index de008640f4..09b4cea574 100644
--- a/testsuite/tests/typecheck/should_run/TypeRep.stdout
+++ b/testsuite/tests/typecheck/should_run/TypeRep.stdout
@@ -20,5 +20,5 @@ Proxy (RuntimeRep -> Constraint) TYPE
 Proxy Constraint Constraint
 Proxy Constraint Constraint
 Proxy Constraint Constraint
-Proxy RuntimeRep 'PtrRepLifted
+Proxy RuntimeRep 'LiftedRep
 RealWorld
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index fa6273a06d..ac63f98508 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -117,3 +117,6 @@ test('TypeOf', normal, compile_and_run, [''])
 test('TypeRep', normal, compile_and_run, [''])
 test('T11120', normal, compile_and_run, [''])
 test('KindInvariant', normal, ghci_script, ['KindInvariant.script'])
+test('StrictPats', normal, compile_and_run, [''])
+test('T12809', normal, compile_and_run, [''])
+test('EtaExpandLevPoly', normal, compile_and_run, [''])
diff --git a/testsuite/tests/unboxedsums/T12711.stdout b/testsuite/tests/unboxedsums/T12711.stdout
index 13070dfe77..7a623a3bd6 100644
--- a/testsuite/tests/unboxedsums/T12711.stdout
+++ b/testsuite/tests/unboxedsums/T12711.stdout
@@ -1 +1,2 @@
-(# _ | _ #) :: TYPE 'GHC.Types.UnboxedSumRep
+(# _ | _ #) :: TYPE
+                 ('GHC.Types.SumRep '['GHC.Types.LiftedRep, 'GHC.Types.LiftedRep])
diff --git a/testsuite/tests/unboxedsums/UbxSumLevPoly.hs b/testsuite/tests/unboxedsums/UbxSumLevPoly.hs
new file mode 100644
index 0000000000..3275eb7dfe
--- /dev/null
+++ b/testsuite/tests/unboxedsums/UbxSumLevPoly.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UnboxedSums #-}
+
+module UbxSumLevPoly where
+
+-- this failed thinking that (# Any | True #) :: TYPE (SumRep [LiftedRep, b])
+-- But of course that b should be Lifted!
+
+-- It was due to silliness in TysWiredIn using the same uniques for different
+-- things in mk_sum.
+
+p = True
+  where (# _x | #) = (# | True #)
diff --git a/testsuite/tests/unboxedsums/all.T b/testsuite/tests/unboxedsums/all.T
index 290ae43263..eea818b6f1 100644
--- a/testsuite/tests/unboxedsums/all.T
+++ b/testsuite/tests/unboxedsums/all.T
@@ -21,7 +21,7 @@ test('ffi1', normal, compile_fail, [''])
 test('thunk', only_ways(['normal']), compile_and_run, [''])
 test('T12375', only_ways(['normal']), compile_and_run, [''])
 test('empty_sum', only_ways(['normal']), compile_and_run, [''])
-test('sum_rr', normal, compile_fail, [''])
+test('sum_rr', normal, compile, [''])
 test('T12711', only_ways(['ghci']), ghci_script, ['T12711.script'])
 
 # TODO: Need to run this in --slow mode only
@@ -30,3 +30,5 @@ test('T12711', only_ways(['ghci']), ghci_script, ['T12711.script'])
 #       extra_files([ "unboxedsums" + str(i) + ".hs" for i in range(1, 12) ])],
 #      run_command,
 #      ['$MAKE -s --no-print-directory sum_api_annots'])
+
+test('UbxSumLevPoly', normal, compile, [''])
diff --git a/testsuite/tests/unboxedsums/sum_rr.hs b/testsuite/tests/unboxedsums/sum_rr.hs
index 287edcf452..5f799fe481 100644
--- a/testsuite/tests/unboxedsums/sum_rr.hs
+++ b/testsuite/tests/unboxedsums/sum_rr.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE DataKinds, KindSignatures #-}
+{-# LANGUAGE TypeInType #-}
 
 module Example where
 
 import Data.Typeable
 import GHC.Exts
 
-data Wat (a :: TYPE 'UnboxedSumRep) = Wat a
+data Wat (a :: TYPE (SumRep '[LiftedRep, IntRep])) = Wat a
diff --git a/testsuite/tests/unboxedsums/sum_rr.stderr b/testsuite/tests/unboxedsums/sum_rr.stderr
deleted file mode 100644
index 2ac9b7452f..0000000000
--- a/testsuite/tests/unboxedsums/sum_rr.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-sum_rr.hs:8:39: error:
-    • The type ‘a’ is not an unboxed sum,
-      and yet its kind suggests that it has the representation
-      of an unboxed sum. This is not allowed.
-    • In the definition of data constructor ‘Wat’
-      In the data type declaration for ‘Wat’
diff --git a/testsuite/tests/unboxedsums/unboxedsums_unit_tests.hs b/testsuite/tests/unboxedsums/unboxedsums_unit_tests.hs
index 399e074991..0b6384b6ba 100644
--- a/testsuite/tests/unboxedsums/unboxedsums_unit_tests.hs
+++ b/testsuite/tests/unboxedsums/unboxedsums_unit_tests.hs
@@ -46,7 +46,7 @@ layout_tests = sequence_
   where
     assert_layout tn tys layout =
       let
-        layout_ret = ubxSumRepType tys
+        layout_ret = ubxSumRepType (map typePrimRep tys)
       in
         assert (layout_ret == layout)
                tn