Implement the -XUnliftedNewtypes extension.

GHC Proposal: 0013-unlifted-newtypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
Issues: #15219, #1311, #13595, #15883
Implementation Details:
  Note [Implementation of UnliftedNewtypes]
  Note [Unifying data family kinds]
  Note [Compulsory newtype unfolding]

This patch introduces the -XUnliftedNewtypes extension. When this
extension is enabled, GHC drops the restriction that the field in
a newtype must be of kind (TYPE 'LiftedRep). This allows types
like Int# and ByteArray# to be used in a newtype. Additionally,
coerce is made levity-polymorphic so that it can be used with
newtypes over unlifted types.

The bulk of the changes are in TcTyClsDecls.hs. With -XUnliftedNewtypes,
getInitialKind is more liberal, introducing a unification variable to
return the kind (TYPE r0) rather than just returning (TYPE 'LiftedRep).
When kind-checking a data constructor with kcConDecl, we attempt to
unify the kind of a newtype with the kind of its field's type. When
typechecking a data declaration with tcTyClDecl, we again perform a
unification. See the implementation note for more on this.

Co-authored-by: Richard Eisenberg <rae@richarde.dev>

71 files changed, 731 insertions, 32 deletions

diff --git a/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs b/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs
new file mode 100644
index 0000000000..d32eed4ef1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs
@@ -0,0 +1,35 @@
+{-# Language CPP                   #-}
+{-# Language QuantifiedConstraints #-}
+{-# Language TypeApplications      #-}
+{-# Language PolyKinds             #-}
+{-# Language TypeOperators         #-}
+{-# Language DataKinds             #-}
+{-# Language TypeFamilies          #-}
+{-# Language TypeSynonymInstances  #-}
+{-# Language FlexibleInstances     #-}
+{-# Language GADTs                 #-}
+{-# Language UndecidableInstances  #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language FlexibleContexts      #-}
+{-# LANGUAGE UnliftedNewtypes      #-}
+
+module Bug where
+import Data.Coerce
+import Data.Kind
+
+type Cat ob = ob -> ob -> Type
+
+type Obj = Type
+
+class
+  Ríki (obj :: Obj) where
+  type (-->) :: obj -> obj -> Type
+
+  ið :: a --> (a::obj)
+
+data Op a = Op a
+
+type family UnOp op where UnOp ('Op obj) = obj
+
+newtype Y :: Cat (Op a) where
+  Y :: (UnOp b --> UnOp a) -> Y a b
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
new file mode 100644
index 0000000000..de831f9200
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module UnliftedNewtypesDifficultUnification where
+
+import GHC.Exts
+import Data.Kind
+
+data Color = Red | Blue
+
+type family Interpret (x :: Color) :: RuntimeRep where
+  Interpret 'Red = 'IntRep
+  Interpret 'Blue = 'WordRep
+
+data family Foo (x :: Color) :: TYPE (Interpret x)
+newtype instance Foo 'Red = FooRedC Int#
+
+newtype Quux :: TYPE (Interpret Red) where
+  MkQ :: Int# -> Quux
+
+newtype instance Foo 'Blue :: TYPE WordRep where
+  MkFB :: Word# -> Foo 'Blue
+
+type family Lower (x :: Type) :: RuntimeRep where
+  Lower Int = IntRep
+  Lower Word = WordRep
+
+data family Bar (x :: Color) :: TYPE (Interpret x)
+
+newtype instance Bar 'Red :: TYPE (Lower Int) where
+  MkBR :: Int# -> Bar 'Red
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs
new file mode 100644
index 0000000000..68221cb510
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs
@@ -0,0 +1,10 @@
+{-# Language RankNTypes #-}
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language UnliftedNewtypes #-}
+
+module UnliftedNewtypesForall where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs
new file mode 100644
index 0000000000..d664801a08
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs
@@ -0,0 +1,20 @@
+{-# language DataKinds #-}
+{-# language DerivingStrategies #-}
+{-# language GeneralizedNewtypeDeriving #-}
+{-# language KindSignatures #-}
+{-# language MagicHash #-}
+{-# language PolyKinds #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesGnd where
+
+import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep),isTrue#,(==#))
+
+class LevityEq (a :: TYPE 'IntRep) where
+  levityEq :: a -> a -> Bool
+
+instance LevityEq Int# where
+  levityEq x y = isTrue# (x ==# y)
+
+newtype Foo = Foo Int#
+  deriving newtype (LevityEq)
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs
new file mode 100644
index 0000000000..1b8a18fc7c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds, TypeFamilies, GADTs, UnliftedNewtypes #-}
+
+module UnliftedNewtypesLPFamily where
+
+import GHC.Exts
+
+data family DF (a :: k) :: k
+
+newtype instance DF (a :: TYPE r) where
+  MkDF :: forall (r :: RuntimeRep) (a :: TYPE r). a -> DF a
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
new file mode 100644
index 0000000000..60f97bdd53
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep))
+
+data family DFT (r :: RuntimeRep) :: TYPE r
+newtype instance DFT 'IntRep = MkDFT1 Int#
+newtype instance DFT 'WordRep = MkDFT2 Word#
+newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep])
+  = MkDFT3 (# Int#, Word# #)
+data instance DFT 'LiftedRep = MkDFT4 | MkDFT5
+
+data family DF :: TYPE (r :: RuntimeRep)
+newtype instance DF = MkDF1 Int#
+newtype instance DF = MkDF2 Word#
+newtype instance DF = MkDF3 (# Int#, Word# #)
+data instance DF = MkDF4 | MkDF5
diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
new file mode 100644
index 0000000000..9f5b984025
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Exts (Int#,Word#,RuntimeRep(IntRep))
+import GHC.Exts (TYPE)
+
+type KindOf (a :: TYPE k) = k
+data family D (a :: TYPE r) :: TYPE r
+newtype instance D a = MkWordD Word#
+newtype instance D a :: TYPE (KindOf a) where
+  MkIntD :: forall (a :: TYPE 'IntRep). Int# -> D a
diff --git a/testsuite/tests/typecheck/should_compile/VtaCoerce.hs b/testsuite/tests/typecheck/should_compile/VtaCoerce.hs
new file mode 100644
index 0000000000..ab8d7082f7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/VtaCoerce.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes, TypeApplications #-}
+
+module VtaCoerce where
+
+import Data.Coerce (coerce)
+
+newtype Age = Age Int
+
+convert :: Int -> Age
+convert = coerce @Int @Age
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 850b271140..d0f54c0eca 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -470,6 +470,7 @@ test('T10562', normal, compile, [''])
 test('T10564', normal, compile, [''])
 test('Vta1', normal, compile, [''])
 test('Vta2', normal, compile, [''])
+test('VtaCoerce', normal, compile, [''])
 test('PushHRIf', normal, compile, [''])
 test('T10632', normal, compile, ['-Wredundant-constraints'])
 test('T10642', normal, compile, [''])
@@ -674,3 +675,10 @@ test('T16411', normal, compile, [''])
 test('T16609', normal, compile, [''])
 test('T505', normal, compile, [''])
 test('T12928', normal, compile, [''])
+test('UnliftedNewtypesGnd', normal, compile, [''])
+test('UnliftedNewtypesUnassociatedFamily', normal, compile, [''])
+test('UnliftedNewtypesUnifySig', normal, compile, [''])
+test('UnliftedNewtypesForall', normal, compile, [''])
+test('UnlifNewUnify', normal, compile, [''])
+test('UnliftedNewtypesLPFamily', normal, compile, [''])
+test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index 3342cf72e3..ccc3da6fb0 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,7 +1,7 @@
 
 tc211.hs:20:8: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a3 -> a3’
+                  with actual type ‘a9 -> a9’
     • In the expression:
           (:) ::
             (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
@@ -32,7 +32,7 @@ tc211.hs:25:20: error:
 
 tc211.hs:62:18: error:
     • Couldn't match expected type ‘forall a. a -> a’
-                  with actual type ‘a2 -> a2’
+                  with actual type ‘a6 -> a6’
     • In the expression:
           Cons ::
             (forall a. a -> a)
@@ -70,10 +70,10 @@ tc211.hs:68:8: error:
                 (\ x -> x) Nil
 
 tc211.hs:76:9: error:
-    • Couldn't match type ‘forall a5. a5 -> a5’ with ‘a4 -> a4’
+    • Couldn't match type ‘forall a11. a11 -> a11’ with ‘a10 -> a10’
       Expected type: List (forall a. a -> a)
-                     -> (forall a. a -> a) -> a4 -> a4
-        Actual type: List (a4 -> a4) -> (a4 -> a4) -> a4 -> a4
+                     -> (forall a. a -> a) -> a10 -> a10
+        Actual type: List (a10 -> a10) -> (a10 -> a10) -> a10 -> a10
     • In the expression:
           foo2 ::
             List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)
diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
index 355bfe959c..1c108f719b 100644
--- a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
@@ -68,7 +68,8 @@ valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)]
            (and originally defined at ValidHoleFits.hs:4:12-22))
 
 valid_hole_fits.hs:27:5: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: Integer -> Maybe Integer
+    • Found hole: _ :: t0 -> Maybe Integer
+      Where: ‘t0’ is an ambiguous type variable
     • In the expression: _
       In the expression: _ 2
       In an equation for ‘k’: k = _ 2
diff --git a/testsuite/tests/typecheck/should_fail/T10971d.stderr b/testsuite/tests/typecheck/should_fail/T10971d.stderr
index c5ad886683..5cf339bd8d 100644
--- a/testsuite/tests/typecheck/should_fail/T10971d.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10971d.stderr
@@ -1,14 +1,12 @@
 
 T10971d.hs:4:14: error:
-    • Couldn't match expected type ‘[a0]’
-                  with actual type ‘Maybe Integer’
+    • Couldn't match expected type ‘[a0]’ with actual type ‘Maybe a2’
     • In the first argument of ‘f’, namely ‘(Just 1)’
       In the second argument of ‘($)’, namely ‘f (Just 1)’
       In a stmt of a 'do' block: print $ f (Just 1)
 
 T10971d.hs:5:19: error:
-    • Couldn't match expected type ‘[Integer]’
-                  with actual type ‘Maybe Integer’
+    • Couldn't match expected type ‘[b1]’ with actual type ‘Maybe a3’
     • In the second argument of ‘g’, namely ‘(Just 5)’
       In the second argument of ‘($)’, namely ‘g (+ 1) (Just 5)’
       In a stmt of a 'do' block: print $ g (+ 1) (Just 5)
diff --git a/testsuite/tests/typecheck/should_fail/T12729.stderr b/testsuite/tests/typecheck/should_fail/T12729.stderr
index 39dac1116f..fafa6316c3 100644
--- a/testsuite/tests/typecheck/should_fail/T12729.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12729.stderr
@@ -1,10 +1,12 @@
 
 T12729.hs:8:4: error:
     • A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
     • In the definition of data constructor ‘MkA’
       In the newtype declaration for ‘A’
 
 T12729.hs:10:13: error:
     • A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
     • In the definition of data constructor ‘MkB’
       In the newtype declaration for ‘B’
diff --git a/testsuite/tests/typecheck/should_fail/T13902.stderr b/testsuite/tests/typecheck/should_fail/T13902.stderr
index c3d07edfd1..2794ae25ec 100644
--- a/testsuite/tests/typecheck/should_fail/T13902.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13902.stderr
@@ -1,7 +1,6 @@
 
 T13902.hs:8:5: error:
-    • Couldn't match expected type ‘Integer -> Int’
-                  with actual type ‘Int’
+    • Couldn't match expected type ‘t0 -> Int’ with actual type ‘Int’
     • The expression ‘f @Int’ is applied to two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: f @Int 42 5
diff --git a/testsuite/tests/typecheck/should_fail/T15883.hs b/testsuite/tests/typecheck/should_fail/T15883.hs
new file mode 100644
index 0000000000..29ccbc835a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883.hs
@@ -0,0 +1,9 @@
+{-# Language KindSignatures #-}
+{-# Language PolyKinds #-}
+{-# Language RankNTypes #-}
+
+module T15883 where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
diff --git a/testsuite/tests/typecheck/should_fail/T15883.stderr b/testsuite/tests/typecheck/should_fail/T15883.stderr
new file mode 100644
index 0000000000..4bfbc615e6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883.stderr
@@ -0,0 +1,5 @@
+T15883.hs:9:19:
+     A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
+      In the definition of data constructor ‘MkFoo’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.hs b/testsuite/tests/typecheck/should_fail/T15883b.hs
new file mode 100644
index 0000000000..82613943a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883b.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883b where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Eq (Foo LiftedRep)
diff --git a/testsuite/tests/typecheck/should_fail/T15883b.stderr b/testsuite/tests/typecheck/should_fail/T15883b.stderr
new file mode 100644
index 0000000000..a89403d4af
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883b.stderr
@@ -0,0 +1,5 @@
+T15883b.hs:14:1:
+     Can't make a derived instance of
+        ‘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 LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.hs b/testsuite/tests/typecheck/should_fail/T15883c.hs
new file mode 100644
index 0000000000..bd031540c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883c.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883c where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Ord (Foo LiftedRep)
diff --git a/testsuite/tests/typecheck/should_fail/T15883c.stderr b/testsuite/tests/typecheck/should_fail/T15883c.stderr
new file mode 100644
index 0000000000..5444f5d6c8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883c.stderr
@@ -0,0 +1,5 @@
+T15883c.hs:14:1:                 
+     Can't make a derived instance of
+        ‘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 LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.hs b/testsuite/tests/typecheck/should_fail/T15883d.hs
new file mode 100644
index 0000000000..fd86c5cab3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883d.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883d where
+
+import GHC.Exts
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Show (Foo LiftedRep)
+
diff --git a/testsuite/tests/typecheck/should_fail/T15883d.stderr b/testsuite/tests/typecheck/should_fail/T15883d.stderr
new file mode 100644
index 0000000000..b080ff6544
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883d.stderr
@@ -0,0 +1,5 @@
+T15883d.hs:14:1:
+     Can't make a derived instance of
+        ‘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 LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.hs b/testsuite/tests/typecheck/should_fail/T15883e.hs
new file mode 100644
index 0000000000..bb1dcacf92
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883e.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T15883e where
+
+import GHC.Exts
+import Data.Data (Data)
+
+newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
+deriving stock instance Data (Foo LiftedRep)
+
+
diff --git a/testsuite/tests/typecheck/should_fail/T15883e.stderr b/testsuite/tests/typecheck/should_fail/T15883e.stderr
new file mode 100644
index 0000000000..05e07f0307
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15883e.stderr
@@ -0,0 +1,5 @@
+T15883e.hs:16:1:
+     Can't make a derived instance of
+        ‘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 LiftedRep)’
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index d22d13f92b..ec991bc39f 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -1,7 +1,7 @@
 
 T8603.hs:33:17: error:
     • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
-      Expected type: [Integer] -> StateT s RV a0
+      Expected type: [a2] -> StateT s RV a0
         Actual type: t0 ((->) [a1]) (RV a1)
     • The function ‘lift’ is applied to two arguments,
       but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs
new file mode 100644
index 0000000000..f5fd1092ca
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module Goof where
+
+import GHC.Exts (coerce)
+import GHC.Types (RuntimeRep,TYPE,Coercible)
+
+goof :: forall (rep :: RuntimeRep) (x :: TYPE rep) (y :: TYPE rep).
+  Coercible x y => x -> y
+goof = coerce
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
new file mode 100644
index 0000000000..638dc80ff8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesCoerceFail.hs:15:8:
+    Cannot use function with levity-polymorphic arguments:
+      coerce :: x -> y
+    Levity-polymorphic arguments: x :: TYPE rep
+
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs
new file mode 100644
index 0000000000..530b1f5241
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesConstraintFamily where
+
+import Data.Kind (Type,Constraint)
+
+data family D (a :: Type) :: Constraint
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
new file mode 100644
index 0000000000..9c6816b3c1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesConstraintFamily.hs:11:1:
+     Kind signature on data type declaration has non-*
+      and non-variable return kind
+        Constraint
+     In the data family declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs
new file mode 100644
index 0000000000..f37549ed76
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+
+main :: IO ()
+main = return ()
+
+newtype Baz = Baz (Show Int)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr
new file mode 100644
index 0000000000..58b7d65d31
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesFail.hs:6:20:
+     Expected a type, but ‘Show Int’ has kind ‘Constraint’
+     In the type ‘(Show Int)’
+      In the definition of data constructor ‘Baz’
+      In the newtype declaration for ‘Baz’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs
new file mode 100644
index 0000000000..0306a11c9f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module UnliftedNewtypesFamilyKindFail1 where
+
+import Data.Kind (Type)
+
+data family DF (a :: Type) :: 5
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
new file mode 100644
index 0000000000..13c9836c43
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesFamilyKindFail1.hs:11:31:
+     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     In the kind ‘5’
+      In the data family declaration for ‘DF’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs
new file mode 100644
index 0000000000..a2baf8ca5c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesFamilyKindFail2 where
+
+import Data.Kind (Type)
+
+data family F k :: k
+newtype instance F 5 = MkF (F 5)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
new file mode 100644
index 0000000000..57c4a3c2e9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
@@ -0,0 +1,11 @@
+UnliftedNewtypesFamilyKindFail2.hs:12:20:
+     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     In the first argument of ‘F’, namely ‘5’
+      In the newtype instance declaration for ‘F’
+
+UnliftedNewtypesFamilyKindFail2.hs:12:31:
+     Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’
+     In the first argument of ‘F’, namely ‘5’
+      In the type ‘(F 5)’
+      In the definition of data constructor ‘MkF’
+
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs
new file mode 100644
index 0000000000..644943e398
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs
@@ -0,0 +1,9 @@
+{-# language MagicHash #-}
+{-# language UnboxedTuples #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesInfinite where
+
+import GHC.Exts (Int#)
+
+newtype Foo = FooC (# Int#, Foo #)
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
new file mode 100644
index 0000000000..65db9f5a84
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
@@ -0,0 +1,6 @@
+
+UnliftedNewtypesInfinite.hs:9:15: error:
+    • Occurs check: cannot construct the infinite kind:
+        t0 ~ 'GHC.Types.TupleRep '[ 'GHC.Types.IntRep, t0]
+    • In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs
new file mode 100644
index 0000000000..8f1f9b4c65
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module UnliftedNewtypesInstanceFail where
+
+import GHC.Exts
+
+class Foo a where
+  data Bar a :: TYPE 'IntRep
+
+instance Foo Bool where
+  newtype Bar Bool :: TYPE 'WordRep where
+    BarBoolC :: Word# -> Bar Bool
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
new file mode 100644
index 0000000000..3fb2814dab
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesInstanceFail.hs:13:3:
+     Expected kind ‘TYPE 'WordRep’,
+        but ‘Bar Bool’ has kind ‘TYPE 'IntRep’
+     In the newtype instance declaration for ‘Bar’
+      In the instance declaration for ‘Foo Bool’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs
new file mode 100644
index 0000000000..f5d134e3b1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+
+module UnliftedNewtypesLevityBinder where
+
+import GHC.Types (RuntimeRep,TYPE,Coercible)
+
+newtype Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+  IdentC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a
+
+bad :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a
+bad = IdentC
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
new file mode 100644
index 0000000000..90cf5b23aa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesLevityBinder.hs:16:7:
+    Cannot use function with levity-polymorphic arguments:
+      UnliftedNewtypesLevityBinder.IdentC :: a -> Ident a
+    Levity-polymorphic arguments: a :: TYPE r
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs
new file mode 100644
index 0000000000..6c085267db
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs
@@ -0,0 +1,12 @@
+{-# language MagicHash #-}
+{-# language GADTSyntax #-}
+{-# language KindSignatures #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesMismatchedKind where
+
+import Data.Kind (Type)
+import GHC.Exts
+
+newtype T :: Type where
+  MkT :: Int# -> T
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
new file mode 100644
index 0000000000..1d3cb50f90
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesMismatchedKind.hs:12:3:
+     Expecting a lifted type, but ‘Int#’ is unlifted
+     In the definition of data constructor ‘MkT’
+      In the newtype declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs
new file mode 100644
index 0000000000..255643a69d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs
@@ -0,0 +1,11 @@
+{-# language GADTSyntax #-}
+{-# language KindSignatures #-}
+{-# language MagicHash #-}
+{-# language UnliftedNewtypes #-}
+
+module UnliftedNewtypesMismatchedKindRecord where
+
+import GHC.Exts
+
+newtype Foo :: TYPE 'IntRep where
+  FooC :: { getFoo :: Word# } -> Foo
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
new file mode 100644
index 0000000000..2530a438ab
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesMismatchedKindRecord.hs:11:3:
+     Expected kind ‘TYPE 'IntRep’,
+        but ‘Word#’ has kind ‘TYPE 'WordRep’
+     In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs
new file mode 100644
index 0000000000..81a2041d2b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+-- In tcConDecl, there is a place where a panic can happen if
+-- a newtype has multiple fields. This test is here to make
+-- sure that the appropriate validity checks happen before
+-- we get to the panic. See Note [Kind-checking the field type].
+
+module UnliftedNewtypesMultiFieldGadt where
+
+import GHC.Exts
+import Data.Kind
+
+newtype Foo :: TYPE 'IntRep where
+  FooC :: Bool -> Char -> Foo
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
new file mode 100644
index 0000000000..70493e0d96
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesMultiFieldGadt.hs:19:3:
+     The constructor of a newtype must have exactly one field
+        but ‘FooC’ has two
+     In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs
new file mode 100644
index 0000000000..6c6aadccc8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesNotEnabled
+  ( Baz(..)
+  ) where
+
+import GHC.Exts (Int#)
+
+newtype Baz = Baz Int#
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
new file mode 100644
index 0000000000..37496c4edd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
@@ -0,0 +1,5 @@
+UnliftedNewtypesNotEnabled.hs:9:15:
+     A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
+     In the definition of data constructor ‘Baz’
+      In the newtype declaration for ‘Baz’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
new file mode 100644
index 0000000000..6c1959e035
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+
+module UnliftedNewtypesOverlap where
+
+import GHC.Exts (TYPE)
+
+data family DF :: TYPE r
+data instance DF = MkDF4 | MkDF5
+newtype instance DF = MkDF6 Int
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
new file mode 100644
index 0000000000..808e8c0f60
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr
@@ -0,0 +1,4 @@
+UnliftedNewtypesOverlap.hs:12:15:
+    Conflicting family instance declarations:
+      DF -- Defined at UnliftedNewtypesOverlap.hs:12:15
+      DF -- Defined at UnliftedNewtypesOverlap.hs:13:18
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 5be507edbf..7ee15ebc4c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -518,3 +518,21 @@ test('T16456', normal, compile_fail, ['-fprint-explicit-foralls'])
 test('T16627', normal, compile_fail, [''])
 test('T502', normal, compile_fail, [''])
 test('T16517', normal, compile_fail, [''])
+test('T15883', normal, compile_fail, [''])
+test('T15883b', normal, compile_fail, [''])
+test('T15883c', normal, compile_fail, [''])
+test('T15883d', normal, compile_fail, [''])
+test('T15883e', normal, compile_fail, [''])
+test('UnliftedNewtypesFail', normal, compile_fail, [''])
+test('UnliftedNewtypesNotEnabled', normal, compile_fail, [''])
+test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
+test('UnliftedNewtypesInstanceFail', normal, compile_fail, [''])
+test('UnliftedNewtypesInfinite', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
+test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
+test('UnliftedNewtypesOverlap', normal, compile_fail, [''])
+test('UnliftedNewtypesFamilyKindFail1', normal, compile_fail, [''])
+test('UnliftedNewtypesFamilyKindFail2', normal, compile_fail, [''])
+test('UnliftedNewtypesConstraintFamily', normal, compile_fail, [''])
+test('UnliftedNewtypesMismatchedKind', normal, compile_fail, [''])
+test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
+test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/mc24.stderr b/testsuite/tests/typecheck/should_fail/mc24.stderr
index 7f016283b1..06a9c51690 100644
--- a/testsuite/tests/typecheck/should_fail/mc24.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc24.stderr
@@ -1,8 +1,8 @@
 
 mc24.hs:10:31: error:
-    • Couldn't match type ‘[a0]’ with ‘[a] -> m [a]’
-      Expected type: (a -> Integer) -> [a] -> m [a]
-        Actual type: [a0] -> [a0]
+    • Couldn't match type ‘[a1]’ with ‘[a] -> m [a]’
+      Expected type: (a -> a0) -> [a] -> m [a]
+        Actual type: [a1] -> [a1]
     • Possible cause: ‘take’ is applied to too many arguments
       In the expression: take 2
       In a stmt of a monad comprehension: then group by x using take 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
index 7bf64d841a..9d6657e651 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
@@ -1,7 +1,7 @@
 
 tcfail004.hs:3:9: error:
     • Couldn't match expected type ‘(a, b)’
-                  with actual type ‘(Integer, Integer, Integer)’
+                  with actual type ‘(a0, b0, c0)’
     • In the expression: (1, 2, 3)
       In a pattern binding: (f, g) = (1, 2, 3)
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
index 56db4cf58b..d206505cdc 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
@@ -1,7 +1,6 @@
 
 tcfail005.hs:3:9: error:
-    • Couldn't match expected type ‘[a]’
-                  with actual type ‘(Integer, Char)’
+    • Couldn't match expected type ‘[a]’ with actual type ‘(a0, Char)’
     • In the expression: (1, 'a')
       In a pattern binding: (h : i) = (1, 'a')
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_fail/tcfail079.stderr b/testsuite/tests/typecheck/should_fail/tcfail079.stderr
index 78d14f9c35..769b8335ed 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail079.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail079.stderr
@@ -1,5 +1,5 @@
-
 tcfail079.hs:9:19: error:
     • A newtype cannot have an unlifted argument type
+      Perhaps you intended to use UnliftedNewtypes
     • In the definition of data constructor ‘Unboxed’
       In the newtype declaration for ‘Unboxed’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 85217315ca..924e14081b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -1,7 +1,6 @@
 
 tcfail140.hs:10:7: error:
-    • Couldn't match expected type ‘Integer -> t’
-                  with actual type ‘Int’
+    • Couldn't match expected type ‘t0 -> t’ with actual type ‘Int’
     • The function ‘f’ is applied to two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: f 3 9
@@ -9,8 +8,7 @@ tcfail140.hs:10:7: error:
     • Relevant bindings include bar :: t (bound at tcfail140.hs:10:1)
 
 tcfail140.hs:12:10: error:
-    • Couldn't match expected type ‘Integer -> t’
-                  with actual type ‘Int’
+    • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
     • The operator ‘f’ takes two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: 3 `f` 4
diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
index 412ba47d3f..706b3afa32 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
@@ -1,6 +1,6 @@
 
 tcfail159.hs:9:11: error:
-    • Expecting a lifted type, but got an unlifted
+    • Expecting a lifted type, but got an unlifted type
     • In the pattern: ~(# p, q #)
       In a case alternative: ~(# p, q #) -> p
       In the expression: case h x of { ~(# p, q #) -> p }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail189.stderr b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
index f23243bdd0..f33d1e37f6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail189.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail189.stderr
@@ -1,8 +1,8 @@
 
 tcfail189.hs:10:31: error:
-    • Couldn't match type ‘[a0]’ with ‘[a] -> [[a]]’
-      Expected type: (a -> Integer) -> [a] -> [[a]]
-        Actual type: [a0] -> [a0]
+    • Couldn't match type ‘[a1]’ with ‘[a] -> [[a]]’
+      Expected type: (a -> a0) -> [a] -> [[a]]
+        Actual type: [a1] -> [a1]
     • Possible cause: ‘take’ is applied to too many arguments
       In the expression: take 2
       In a stmt of a list comprehension: then group by x using take 2
diff --git a/testsuite/tests/typecheck/should_fail/tcfail206.stderr b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
index 51fbbb3825..7c97fc02af 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail206.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
@@ -7,9 +7,9 @@ tcfail206.hs:5:5: error:
       In an equation for ‘a’: a = (, True)
 
 tcfail206.hs:8:5: error:
-    • Couldn't match type ‘(Integer, Int)’ with ‘Bool -> (Int, Bool)’
+    • Couldn't match type ‘(t1, Int)’ with ‘Bool -> (Int, Bool)’
       Expected type: Int -> Bool -> (Int, Bool)
-        Actual type: Int -> (Integer, Int)
+        Actual type: Int -> (t1, Int)
     • In the expression: (1,)
       In an equation for ‘b’: b = (1,)
 
@@ -34,10 +34,10 @@ tcfail206.hs:14:5: error:
       In an equation for ‘d’: d = (# , True #)
 
 tcfail206.hs:17:5: error:
-    • Couldn't match type ‘(# Integer, Int #)’
+    • Couldn't match type ‘(# t0, Int #)’
                      with ‘Bool -> (# Int, Bool #)’
       Expected type: Int -> Bool -> (# Int, Bool #)
-        Actual type: Int -> (# Integer, Int #)
+        Actual type: Int -> (# t0, Int #)
     • In the expression: (# 1, #)
       In an equation for ‘e’: e = (# 1, #)
 
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs
new file mode 100644
index 0000000000..53905a302a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#,(+#))
+import GHC.Types
+import Data.Coerce (coerce)
+
+main :: IO ()
+main = do
+  print (I# (coerce (Foo 5#)))
+
+newtype Foo = Foo Int#
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout
new file mode 100644
index 0000000000..7ed6ff82de
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout
@@ -0,0 +1 @@
+5
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs
new file mode 100644
index 0000000000..a6331b8329
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import Data.Proxy (Proxy(..))
+import GHC.Exts (TYPE,RuntimeRep(..))
+
+main :: IO ()
+main = case method (Proxy :: Proxy 'IntRep) of
+  BarIntC y -> case method (Proxy :: Proxy 'WordRep) of
+    BarWordC z -> do
+      print (I# y)
+      print (W# z)
+
+class Foo (a :: RuntimeRep) where
+  data Bar a :: TYPE a
+  method :: Proxy a -> Bar a
+
+instance Foo 'IntRep where
+  newtype instance Bar 'IntRep = BarIntC Int#
+  method _ = BarIntC 5#
+
+instance Foo 'WordRep where
+  newtype instance Bar 'WordRep :: TYPE 'WordRep where
+    BarWordC :: Word# -> Bar 'WordRep
+  method _ = BarWordC 7##
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout
new file mode 100644
index 0000000000..b3172d1242
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout
@@ -0,0 +1,2 @@
+5
+7
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs
new file mode 100644
index 0000000000..b0fdc88dbb
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Types
+
+main :: IO ()
+main = do
+  print (method 5 (BarIntC 6#))
+  print (method 13 (BarWordC 9#))
+
+class Foo a where
+  data Bar a :: TYPE 'IntRep
+  method :: a -> Bar a -> a
+
+instance Foo Int where
+  newtype Bar Int = BarIntC Int#
+  method x (BarIntC y) = x + I# y
+
+instance Foo Word where
+  newtype Bar Word = BarWordC Int#
+  method x (BarWordC y) = x - fromIntegral (I# y)
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout
new file mode 100644
index 0000000000..dfa5ffdccf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout
@@ -0,0 +1,2 @@
+11
+4
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs
new file mode 100644
index 0000000000..f81367268b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#,(+#))
+import GHC.Types
+
+main :: IO ()
+main = case (IdentityC 5#) of
+  IdentityC x -> case ex of
+    IdentityC y -> do
+      print (I# x)
+      print y
+      print (maybeInt# 12 increment# (Maybe# (# 42# | #)))
+      print (maybeInt# 27 increment# (Maybe# (# | (# #) #)))
+
+newtype Identity :: forall (r :: RuntimeRep). TYPE r -> TYPE r where
+  IdentityC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity a
+
+newtype Maybe# :: forall (r :: RuntimeRep).
+    TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where
+  Maybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a
+
+maybeInt# :: a -> (Int# -> a) -> Maybe# Int# -> a
+maybeInt# def _ (Maybe# (# | (# #) #)) = def
+maybeInt# _   f (Maybe# (# i | #)) = f i
+
+increment# :: Int# -> Int
+increment# i = I# (i +# 1#)
+
+ex :: Identity Bool
+ex = IdentityC True
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout
new file mode 100644
index 0000000000..e5835b0b94
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout
@@ -0,0 +1,4 @@
+5
+True
+43
+27
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs
new file mode 100644
index 0000000000..b6c07396bf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE RankNTypes #-}
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Types
+
+main :: IO ()
+main = do
+  let a = idIntRep (FooC 6#)
+      b = idWordRep (BarC 7##)
+      c = idWordRep (PatC 3##)
+      d = idIntRep (DarthC 5#)
+  print (I# (getFoo a))
+  print (W# (case b of BarC w -> w))
+  print (W# (case c of PatC w -> w))
+  print (I# (case d of DarthC w -> w))
+  print (A1 13#)
+  print (A2 15##)
+
+newtype Darth = DarthC Int#
+
+newtype Foo = FooC { getFoo :: Int# }
+
+newtype Bar :: TYPE 'WordRep where
+  BarC :: Word# -> Bar
+
+newtype Pat where
+  PatC :: Word# -> Pat
+
+data A1 :: Type where
+  A1 :: Int# -> A1
+  deriving (Show)
+
+data A2 = A2 Word#
+  deriving (Show)
+
+idIntRep :: forall (a :: TYPE 'IntRep). a -> a
+idIntRep x = x
+
+idWordRep :: forall (a :: TYPE 'WordRep). a -> a
+idWordRep x = x
diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout
new file mode 100644
index 0000000000..df8e8ed83d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout
@@ -0,0 +1,6 @@
+6
+7
+3
+5
+A1 13#
+A2 15##
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index 598d467b7e..05fddcb0b0 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -135,3 +135,8 @@ test('T14218', normal, compile_and_run, [''])
 test('T14236', normal, compile_and_run, [''])
 test('T14925', normal, compile_and_run, [''])
 test('T14341', normal, compile_and_run, [''])
+test('UnliftedNewtypesRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesFamilyRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesIdentityRun', normal, compile_and_run, [''])
+test('UnliftedNewtypesCoerceRun', normal, compile_and_run, [''])