Fix #17021 by checking more return kinds

All the details are in new Note [Datatype return kinds] in
TcTyClsDecls.

Test case: typecheck/should_fail/T17021{,b}
           typecheck/should_compile/T17021a

Updates haddock submodule

27 files changed, 122 insertions, 68 deletions

diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr
index 6d368d5218..88eca5c1ac 100644
--- a/testsuite/tests/polykinds/T15787.stderr
+++ b/testsuite/tests/polykinds/T15787.stderr
@@ -1,6 +1,6 @@
 
-T15787.hs:15:43: error:
-    • Expected kind ‘ob’, but ‘k’ has kind ‘*’
-    • In the second argument of ‘Kl_kind’, namely ‘k’
-      In the type ‘Kl_kind (m :: ob -> ob) k’
+T15787.hs:15:14: error:
+    • Expected a type, but ‘k’ has kind ‘ob’
+    • In the type ‘k’
       In the definition of data constructor ‘Kl’
+      In the data declaration for ‘Kl_kind’
diff --git a/testsuite/tests/polykinds/T7230.stderr b/testsuite/tests/polykinds/T7230.stderr
index f78ccc0d61..5c5055ea2a 100644
--- a/testsuite/tests/polykinds/T7230.stderr
+++ b/testsuite/tests/polykinds/T7230.stderr
@@ -9,13 +9,13 @@ T7230.hs:48:32: error:
         at T7230.hs:47:1-68
       or from: xs ~ (x : xs1)
         bound by a pattern with constructor:
-                   SCons :: forall {a} (x :: a) (xs :: [a]).
+                   SCons :: forall {k} (x :: k) (xs :: [k]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘crash’
         at T7230.hs:48:8-27
       or from: xs1 ~ (x1 : xs2)
         bound by a pattern with constructor:
-                   SCons :: forall {a} (x :: a) (xs :: [a]).
+                   SCons :: forall {k} (x :: k) (xs :: [k]).
                             Sing x -> Sing xs -> Sing (x : xs),
                  in an equation for ‘crash’
         at T7230.hs:48:17-26
diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr
index 1732bbc12a..c8e98be09a 100644
--- a/testsuite/tests/polykinds/T9222.stderr
+++ b/testsuite/tests/polykinds/T9222.stderr
@@ -8,7 +8,7 @@ T9222.hs:14:3: error:
           at T9222.hs:14:3-43
       ‘c’ is a rigid type variable bound by
         the type of the constructor ‘Want’:
-          forall {i1} {j1} (a :: (i1, j1)) (b :: i1) (c :: j1).
+          forall {k1} {j1} (a :: (k1, j1)) (b :: k1) (c :: j1).
           ((a ~ '(b, c)) => Proxy b) -> Want a
         at T9222.hs:14:3-43
     • In the ambiguity check for ‘Want’
diff --git a/testsuite/tests/typecheck/should_compile/T17021a.hs b/testsuite/tests/typecheck/should_compile/T17021a.hs
new file mode 100644
index 0000000000..6412452680
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17021a.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE StandaloneKindSignatures, PolyKinds, DataKinds, TypeFamilies,
+             UnliftedNewtypes #-}
+
+module T17021a where
+
+import Data.Kind
+import GHC.Exts
+
+type family Id x where
+  Id x = x
+
+type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
+newtype LevId x = MkLevId x
+
+type LevId2 :: (r ~ Id LiftedRep) => TYPE r -> TYPE r
+newtype LevId2 x = MkLevId2 x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d8b309dda6..dd416ad2de 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -700,3 +700,4 @@ test('T12926', reqlib('vector'), compile, ['-O2'])
 test('T17710', normal, compile, [''])
 test('T17792', normal, compile, [''])
 test('T17024', normal, compile, [''])
+test('T17021a', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12729.hs b/testsuite/tests/typecheck/should_fail/T12729.hs
index bb70737e93..d2238c96b0 100644
--- a/testsuite/tests/typecheck/should_fail/T12729.hs
+++ b/testsuite/tests/typecheck/should_fail/T12729.hs
@@ -8,4 +8,3 @@ newtype A where
    MkA :: Int# -> A
 
 newtype B = MkB Int#
-
diff --git a/testsuite/tests/typecheck/should_fail/T12729.stderr b/testsuite/tests/typecheck/should_fail/T12729.stderr
index fafa6316c3..6bf544fe47 100644
--- a/testsuite/tests/typecheck/should_fail/T12729.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12729.stderr
@@ -1,12 +1,5 @@
 
-T12729.hs:8:4: error:
-    • A newtype cannot have an unlifted argument type
+T12729.hs:7:1: error:
+    • Newtype has non-* return kind ‘TYPE 'IntRep’
       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’
+    • In the newtype declaration for ‘A’
diff --git a/testsuite/tests/typecheck/should_fail/T14048a.stderr b/testsuite/tests/typecheck/should_fail/T14048a.stderr
index d75b423df3..9767d3a45c 100644
--- a/testsuite/tests/typecheck/should_fail/T14048a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14048a.stderr
@@ -1,5 +1,4 @@
 
 T14048a.hs:6:1: error:
-    • Kind signature on data type declaration has non-*
-      return kind ‘Constraint’
+    • Data type has non-* return kind ‘Constraint’
     • In the data declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T14048b.stderr b/testsuite/tests/typecheck/should_fail/T14048b.stderr
index 4356d65ef7..d265193b69 100644
--- a/testsuite/tests/typecheck/should_fail/T14048b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14048b.stderr
@@ -1,5 +1,5 @@
 
 T14048b.hs:7:1: error:
-    • Kind signature on data family declaration has non-TYPE
+    • Data family has non-TYPE
       and non-variable return kind ‘Constraint’
     • In the data family declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T14048c.stderr b/testsuite/tests/typecheck/should_fail/T14048c.stderr
index a0465fe4fc..e1bb372958 100644
--- a/testsuite/tests/typecheck/should_fail/T14048c.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14048c.stderr
@@ -1,5 +1,4 @@
 
 T14048c.hs:9:1: error:
-    • Kind signature on data instance declaration has non-*
-      return kind ‘Constraint’
+    • Data instance has non-* return kind ‘Constraint’
     • In the data instance declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T15807.stderr b/testsuite/tests/typecheck/should_fail/T15807.stderr
index e24f5bb855..809398ade0 100644
--- a/testsuite/tests/typecheck/should_fail/T15807.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15807.stderr
@@ -1,16 +1,6 @@
 
-T15807.hs:12:24: error:
-    • Expecting one more argument to ‘f’
-      Expected a type, but ‘f’ has kind ‘k0 -> *’
-    • In the first argument of ‘App’, namely ‘f’
-      In the type ‘App @f a’
-      In the definition of data constructor ‘MkApp’
-
-T15807.hs:12:26: error:
-    • Couldn't match kind ‘*’ with ‘k0 -> *’
-      When matching kinds
-        k0 :: *
-        f :: k0 -> *
-    • In the second argument of ‘App’, namely ‘a’
-      In the type ‘App @f a’
+T15807.hs:12:12: error:
+    • Expected kind ‘f -> *’, but ‘f’ has kind ‘*’
+    • In the type ‘f a’
       In the definition of data constructor ‘MkApp’
+      In the data declaration for ‘App’
diff --git a/testsuite/tests/typecheck/should_fail/T15883.stderr b/testsuite/tests/typecheck/should_fail/T15883.stderr
index 4bfbc615e6..d65ffa5ebc 100644
--- a/testsuite/tests/typecheck/should_fail/T15883.stderr
+++ b/testsuite/tests/typecheck/should_fail/T15883.stderr
@@ -1,5 +1,5 @@
-T15883.hs:9:19:
-     A newtype cannot have an unlifted argument type
+
+T15883.hs:9:1: error:
+    • Newtype has non-* return kind ‘TYPE rep’
       Perhaps you intended to use UnliftedNewtypes
-      In the definition of data constructor ‘MkFoo’
-      In the newtype declaration for ‘Foo’
+    • In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/T16821.stderr b/testsuite/tests/typecheck/should_fail/T16821.stderr
index a93ba8c33f..51eaf52fd7 100644
--- a/testsuite/tests/typecheck/should_fail/T16821.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16821.stderr
@@ -1,5 +1,4 @@
 
 T16821.hs:12:1: error:
-    • Kind signature on newtype declaration has non-TYPE
-      return kind ‘Id (*)’
+    • Newtype has non-TYPE return kind ‘Id (*)’
     • In the newtype declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T16829a.stderr b/testsuite/tests/typecheck/should_fail/T16829a.stderr
index 7ea8845cc9..bbad3415d6 100644
--- a/testsuite/tests/typecheck/should_fail/T16829a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16829a.stderr
@@ -1,6 +1,5 @@
 
 T16829a.hs:9:1: error:
-    • Kind signature on newtype declaration has non-*
-      return kind ‘TYPE 'IntRep’
+    • Newtype has non-* return kind ‘TYPE 'IntRep’
       Perhaps you intended to use UnliftedNewtypes
     • In the newtype declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T16829b.stderr b/testsuite/tests/typecheck/should_fail/T16829b.stderr
index 590a884dc8..633d8988a7 100644
--- a/testsuite/tests/typecheck/should_fail/T16829b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16829b.stderr
@@ -1,6 +1,5 @@
 
 T16829b.hs:10:1: error:
-    • Kind signature on newtype instance declaration has non-*
-      return kind ‘TYPE 'IntRep’
+    • Newtype instance has non-* return kind ‘TYPE 'IntRep’
       Perhaps you intended to use UnliftedNewtypes
     • In the newtype instance declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T17021.hs b/testsuite/tests/typecheck/should_fail/T17021.hs
new file mode 100644
index 0000000000..f02c2f7e42
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17021.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+module T17021 where
+
+import Data.Kind
+import GHC.Exts
+
+type family Id (x :: a) :: a where
+  Id x = x
+
+newtype T :: TYPE (Id LiftedRep) where
+  MkT :: Int -> T
+
+f :: T
+f = MkT 42
diff --git a/testsuite/tests/typecheck/should_fail/T17021.stderr b/testsuite/tests/typecheck/should_fail/T17021.stderr
new file mode 100644
index 0000000000..712858b19f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17021.stderr
@@ -0,0 +1,14 @@
+
+T17021.hs:18:5: error:
+    Cannot use function with levity-polymorphic arguments:
+      T17021.MkT :: Int -> T
+    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
+    are eta-expanded internally because they must occur fully saturated.
+    Use -fprint-typechecker-elaboration to display the full expression.)
+    Levity-polymorphic arguments: Int :: TYPE (Id 'LiftedRep)
+
+T17021.hs:18:9: error:
+    A levity-polymorphic type is not allowed here:
+      Type: Int
+      Kind: TYPE (Id 'LiftedRep)
+    In the type of expression: 42
diff --git a/testsuite/tests/typecheck/should_fail/T17021b.hs b/testsuite/tests/typecheck/should_fail/T17021b.hs
new file mode 100644
index 0000000000..6c9452ca70
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17021b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
+
+module T17021b where
+
+import Data.Kind
+
+data family Fix (f :: Type -> k) :: k
+type family F (a :: Type) :: Type where
+  F Int = Type -> Type
+data instance Fix (f :: Type -> F Int) :: F Int
diff --git a/testsuite/tests/typecheck/should_fail/T17021b.stderr b/testsuite/tests/typecheck/should_fail/T17021b.stderr
new file mode 100644
index 0000000000..8a07f2f534
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17021b.stderr
@@ -0,0 +1,4 @@
+
+T17021b.hs:10:1: error:
+    • Data instance has non-* return kind ‘F Int’
+    • In the data instance declaration for ‘Fix’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
index 93a48850dc..2eff7f0ab7 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr
@@ -1,5 +1,5 @@
 
 UnliftedNewtypesConstraintFamily.hs:11:1: error:
-    • Kind signature on data family declaration has non-TYPE
+    • Data family has non-TYPE
       and non-variable return kind ‘Constraint’
     • In the data family declaration for ‘D’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
index 65db9f5a84..bf50beed5e 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
@@ -1,6 +1,7 @@
 
-UnliftedNewtypesInfinite.hs:9:15: error:
+UnliftedNewtypesInfinite.hs:9:20: 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 type ‘(# Int#, Foo #)’
+      In the definition of data constructor ‘FooC’
       In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
index 1d3cb50f90..b54423576c 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr
@@ -1,4 +1,6 @@
-UnliftedNewtypesMismatchedKind.hs:12:3:
-     Expecting a lifted type, but ‘Int#’ is unlifted
-     In the definition of data constructor ‘MkT’
+
+UnliftedNewtypesMismatchedKind.hs:12:10: error:
+    • Expecting a lifted type, but ‘Int#’ is unlifted
+    • In the type ‘Int#’
+      In the definition of data constructor ‘MkT’
       In the newtype declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
index 2530a438ab..c8386e663f 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr
@@ -1,5 +1,7 @@
-UnliftedNewtypesMismatchedKindRecord.hs:11:3:
-     Expected kind ‘TYPE 'IntRep’,
+
+UnliftedNewtypesMismatchedKindRecord.hs:11:23: error:
+    • Expected kind ‘TYPE 'IntRep’,
         but ‘Word#’ has kind ‘TYPE 'WordRep’
-     In the definition of data constructor ‘FooC’
+    • In the type ‘Word#’
+      In the definition of data constructor ‘FooC’
       In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
index 70493e0d96..3ecec3fdf0 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr
@@ -1,5 +1,12 @@
-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’
+
+UnliftedNewtypesMultiFieldGadt.hs:19:11: error:
+    • Expecting an unlifted type, but ‘Bool’ is lifted
+    • In the type ‘Bool’
+      In the definition of data constructor ‘FooC’
+      In the newtype declaration for ‘Foo’
+
+UnliftedNewtypesMultiFieldGadt.hs:19:19: error:
+    • Expecting an unlifted type, but ‘Char’ is lifted
+    • In the type ‘Char’
+      In the definition of data constructor ‘FooC’
       In the newtype declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
index 37496c4edd..d45f3ca016 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr
@@ -1,5 +1,5 @@
-UnliftedNewtypesNotEnabled.hs:9:15:
-     A newtype cannot have an unlifted argument type
+
+UnliftedNewtypesNotEnabled.hs:9:1: error:
+    • Newtype has non-* return kind ‘TYPE 'GHC.Types.IntRep’
       Perhaps you intended to use UnliftedNewtypes
-     In the definition of data constructor ‘Baz’
-      In the newtype declaration for ‘Baz’
+    • In the newtype declaration for ‘Baz’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 31b1fb3333..60e50ca241 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -555,3 +555,5 @@ test('T16502', expect_broken(12854), compile, [''])
 test('T17566b', normal, compile_fail, [''])
 test('T17566c', normal, compile_fail, [''])
 test('T17773', normal, compile_fail, [''])
+test('T17021', normal, compile_fail, [''])
+test('T17021b', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail079.stderr b/testsuite/tests/typecheck/should_fail/tcfail079.stderr
index 769b8335ed..dce069a456 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
+
+tcfail079.hs:9:1: error:
+    • Newtype has non-* return kind ‘TYPE 'GHC.Types.IntRep’
       Perhaps you intended to use UnliftedNewtypes
-    • In the definition of data constructor ‘Unboxed’
-      In the newtype declaration for ‘Unboxed’
+    • In the newtype declaration for ‘Unboxed’