Fix SigTvs at the kind level

This patch fixes two bugs in the treatment of SigTvs at the
kind level:

- We should always generalise them, never default them
  (Trac #14555, #14563)

- We should check if they get unified with each other
  (Trac #11203)

Both are described in TcHsType
   Note [Kind generalisation and SigTvs]

8 files changed, 54 insertions, 1 deletions

diff --git a/testsuite/tests/polykinds/T11203.hs b/testsuite/tests/polykinds/T11203.hs
new file mode 100644
index 0000000000..cff89dff79
--- /dev/null
+++ b/testsuite/tests/polykinds/T11203.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds, KindSignatures #-}
+
+module T11203 where
+
+data SameKind :: k -> k -> *
+
+data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr
new file mode 100644
index 0000000000..5d62e00304
--- /dev/null
+++ b/testsuite/tests/polykinds/T11203.stderr
@@ -0,0 +1,4 @@
+
+T11203.hs:7:24: error:
+    • Couldn't match ‘k1’ with ‘k2’
+    • In the data declaration for ‘Q’
diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr
new file mode 100644
index 0000000000..09077f83d3
--- /dev/null
+++ b/testsuite/tests/polykinds/T11821a.stderr
@@ -0,0 +1,4 @@
+
+T11821a.hs:4:77: error:
+    • Couldn't match ‘k1’ with ‘k2’
+    • In the type declaration for ‘SameKind’
diff --git a/testsuite/tests/polykinds/T14555.hs b/testsuite/tests/polykinds/T14555.hs
new file mode 100644
index 0000000000..0ab71b1b76
--- /dev/null
+++ b/testsuite/tests/polykinds/T14555.hs
@@ -0,0 +1,12 @@
+{-# Language TypeInType #-}
+{-# Language TypeOperators, DataKinds, PolyKinds, GADTs #-}
+
+module T14555 where
+
+import Data.Kind
+import GHC.Types (TYPE)
+
+data Exp :: [TYPE rep] -> TYPE rep -> Type where
+--data Exp (x :: [TYPE rep]) (y :: TYPE rep) where
+--data Exp (x :: [TYPE rep]) y where
+  Lam :: Exp (a:xs) b -> Exp xs (a -> b)
diff --git a/testsuite/tests/polykinds/T14555.stderr b/testsuite/tests/polykinds/T14555.stderr
new file mode 100644
index 0000000000..66fb55ae4f
--- /dev/null
+++ b/testsuite/tests/polykinds/T14555.stderr
@@ -0,0 +1,6 @@
+
+T14555.hs:12:34: error:
+    • Expected kind ‘TYPE rep’, but ‘a -> b’ has kind ‘*’
+    • In the second argument of ‘Exp’, namely ‘(a -> b)’
+      In the type ‘Exp xs (a -> b)’
+      In the definition of data constructor ‘Lam’
diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs
new file mode 100644
index 0000000000..7959d927c3
--- /dev/null
+++ b/testsuite/tests/polykinds/T14563.hs
@@ -0,0 +1,9 @@
+{-# Language TypeInType #-}
+{-# Language RankNTypes, KindSignatures, PolyKinds #-}
+
+import GHC.Types (TYPE)
+import Data.Kind
+
+data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where
+  Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a.
+         (g xx -> a) -> h xx -> Lan g h a
diff --git a/testsuite/tests/polykinds/T14563.stderr b/testsuite/tests/polykinds/T14563.stderr
new file mode 100644
index 0000000000..1265ec0e3a
--- /dev/null
+++ b/testsuite/tests/polykinds/T14563.stderr
@@ -0,0 +1,7 @@
+
+T14563.hs:9:39: error:
+    • Expected kind ‘TYPE rep -> TYPE rep''’,
+        but ‘h’ has kind ‘TYPE rep -> *’
+    • In the second argument of ‘Lan’, namely ‘h’
+      In the type ‘Lan g h a’
+      In the definition of data constructor ‘Lan’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 9f34f30d00..8a03e89155 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -146,7 +146,7 @@ test('T11648', normal, compile, [''])
 test('T11648b', normal, compile_fail, [''])
 test('KindVType', normal, compile_fail, [''])
 test('T11821', normal, compile, [''])
-test('T11821a', normal, compile, [''])
+test('T11821a', normal, compile_fail, [''])
 test('T11640', normal, compile, [''])
 test('T11554', normal, compile_fail, [''])
 test('T12055', normal, compile, [''])
@@ -177,3 +177,7 @@ test('T14450', normal, compile_fail, [''])
 test('T14174', normal, compile_fail, [''])
 test('T14174a', expect_broken(14174), compile_fail, [''])
 test('T14520', normal, compile_fail, [''])
+test('T11203', normal, compile_fail, [''])
+test('T14555', normal, compile_fail, [''])
+test('T14563', normal, compile_fail, [''])
+