Fix #11648.

We now check that a CUSK is really a CUSK and issue an error if
it isn't. This also involves more solving and zonking in
kcHsTyVarBndrs, which was the outright bug reported in #11648.

Test cases: polykinds/T11648{,b}

This updates the haddock submodule.

[skip ci]

11 files changed, 64 insertions, 2 deletions

diff --git a/testsuite/tests/dependent/should_compile/KindLevels.hs b/testsuite/tests/dependent/should_compile/KindLevels.hs
index 80762978b2..1aad299df3 100644
--- a/testsuite/tests/dependent/should_compile/KindLevels.hs
+++ b/testsuite/tests/dependent/should_compile/KindLevels.hs
@@ -1,7 +1,9 @@
-{-# LANGUAGE DataKinds, PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
 
 module KindLevels where
 
+import Data.Kind
+
 data A
 data B :: A -> *
 data C :: B a -> *
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_fail/InferDependency.hs
new file mode 100644
index 0000000000..47957d47d6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/InferDependency.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeInType #-}
+
+module InferDependency where
+
+data Proxy k (a :: k)
+data Proxy2 k a = P (Proxy k a)
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
new file mode 100644
index 0000000000..7fa900a889
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/InferDependency.stderr
@@ -0,0 +1,8 @@
+
+InferDependency.hs:6:1: error:
+    • Invalid declaration for ‘Proxy2’; you must explicitly
+      declare which variables are dependent on which others.
+      Inferred variable kinds:
+        k :: *
+        a :: k
+    • In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.hs b/testsuite/tests/dependent/should_fail/KindLevelsB.hs
new file mode 100644
index 0000000000..80762978b2
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/KindLevelsB.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds, PolyKinds #-}
+
+module KindLevels where
+
+data A
+data B :: A -> *
+data C :: B a -> *
+data D :: C b -> *
+data E :: D c -> *
diff --git a/testsuite/tests/dependent/should_fail/KindLevelsB.stderr b/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
new file mode 100644
index 0000000000..587eb97bfa
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/KindLevelsB.stderr
@@ -0,0 +1,5 @@
+
+KindLevelsB.hs:7:13: error:
+    • Expected kind ‘A’, but ‘a’ has kind ‘*’
+    • In the first argument of ‘B’, namely ‘a’
+      In the kind ‘B a -> *’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 63f08d238c..a90b7bbcdc 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -10,3 +10,5 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])
+test('KindLevelsB', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/T11648.hs b/testsuite/tests/polykinds/T11648.hs
new file mode 100644
index 0000000000..15fcfa4e05
--- /dev/null
+++ b/testsuite/tests/polykinds/T11648.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PolyKinds, TypeOperators, TypeFamilies,
+             MultiParamTypeClasses #-}
+
+module T11648 where
+
+class Monoidy (to :: k0 -> k1 -> *) (m :: k1)  where
+  type MComp to m :: k1 -> k1 -> k0
+  mjoin :: MComp to m m m `to` m
diff --git a/testsuite/tests/polykinds/T11648b.hs b/testsuite/tests/polykinds/T11648b.hs
new file mode 100644
index 0000000000..2ab27a6166
--- /dev/null
+++ b/testsuite/tests/polykinds/T11648b.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeInType #-}
+
+module T11648b where
+
+import Data.Proxy
+
+data X (a :: Proxy k)
diff --git a/testsuite/tests/polykinds/T11648b.stderr b/testsuite/tests/polykinds/T11648b.stderr
new file mode 100644
index 0000000000..e709e006b0
--- /dev/null
+++ b/testsuite/tests/polykinds/T11648b.stderr
@@ -0,0 +1,8 @@
+
+T11648b.hs:7:1: error:
+    You have written a *complete user-suppled kind signature*,
+    but the following variable is undetermined: k0 :: *
+    Perhaps add a kind signature.
+    Inferred kinds of user-written variables:
+      k :: k0
+      a :: Proxy k
diff --git a/testsuite/tests/polykinds/T6039.stderr b/testsuite/tests/polykinds/T6039.stderr
new file mode 100644
index 0000000000..2ad2935e9b
--- /dev/null
+++ b/testsuite/tests/polykinds/T6039.stderr
@@ -0,0 +1,5 @@
+
+T6039.hs:5:14: error:
+    • Expecting one fewer argument to ‘j’
+      Expected kind ‘* -> *’, but ‘j’ has kind ‘*’
+    • In the kind ‘j k’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index d48d1084ae..45981e9277 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -37,7 +37,7 @@ test('T6035', normal, compile, [''])
 test('T6036', normal, compile, [''])
 test('T6025', normal, run_command, ['$MAKE -s --no-print-directory T6025'])
 test('T6002', normal, compile, [''])
-test('T6039', normal, compile, [''])
+test('T6039', normal, compile_fail, [''])
 test('T6021', normal, compile_fail, [''])
 test('T6020a', normal, compile, [''])
 test('T6044', normal, compile, [''])
@@ -143,3 +143,5 @@ test('T11362', normal, compile, ['-dunique-increment=-1'])
   # -dunique-increment=-1 doesn't work inside the file
 test('T11399', normal, compile_fail, [''])
 test('T11611', normal, compile_fail, [''])
+test('T11648', normal, compile, [''])
+test('T11648b', normal, compile_fail, [''])