Warn on inferred polymorphic recursion

Silly users sometimes try to use visible dependent quantification
and polymorphic recursion without a CUSK or SAK. This causes
unexpected errors. So we now adjust expectations with a bit
of helpful messaging.

Closes #17541 and closes #17131.

test cases: dependent/should_fail/T{17541{,b},17131}

15 files changed, 91 insertions, 1 deletions

diff --git a/testsuite/tests/dependent/should_fail/T16344.stderr b/testsuite/tests/dependent/should_fail/T16344.stderr
index b47561771f..d567defeee 100644
--- a/testsuite/tests/dependent/should_fail/T16344.stderr
+++ b/testsuite/tests/dependent/should_fail/T16344.stderr
@@ -4,3 +4,7 @@ T16344.hs:7:46: error:
     • In the second argument of ‘T’, namely ‘Int’
       In the type ‘(T Type Int Bool)’
       In the definition of data constructor ‘MkT’
+      NB: Type ‘T’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/T17131.hs b/testsuite/tests/dependent/should_fail/T17131.hs
new file mode 100644
index 0000000000..d4294c0216
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17131.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MagicHash, UnboxedTuples, TypeInType, TypeFamilies, TypeOperators #-}
+
+module T17131 where
+
+import GHC.Exts
+
+type family TypeReps xs where
+   TypeReps '[]                 = '[]
+   TypeReps ((a::TYPE k) ': as) = k ': TypeReps as
+
+type family Tuple# xs = (t :: TYPE ('TupleRep (TypeReps xs))) where
+   Tuple# '[a]                 = (# a #)
diff --git a/testsuite/tests/dependent/should_fail/T17131.stderr b/testsuite/tests/dependent/should_fail/T17131.stderr
new file mode 100644
index 0000000000..dd250ed414
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17131.stderr
@@ -0,0 +1,10 @@
+
+T17131.hs:12:34: error:
+    • Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
+        but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
+    • In the type ‘(# a #)’
+      In the type family declaration for ‘Tuple#’
+      NB: Type ‘Tuple#’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/T17541.hs b/testsuite/tests/dependent/should_fail/T17541.hs
new file mode 100644
index 0000000000..dcf6e91381
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE
+             MagicHash,
+             FlexibleInstances,
+             MultiParamTypeClasses,
+             TypeFamilies,
+             PolyKinds,
+             DataKinds,
+             FunctionalDependencies,
+             TypeFamilyDependencies #-}
+module T17541 where
+
+import GHC.Prim
+import GHC.Exts
+
+
+type family Rep rep where
+  Rep Int = IntRep
+
+type family Unboxed rep = (urep :: TYPE (Rep rep)) | urep -> rep where
+  Unboxed Int = Int#
diff --git a/testsuite/tests/dependent/should_fail/T17541.stderr b/testsuite/tests/dependent/should_fail/T17541.stderr
new file mode 100644
index 0000000000..e17206c734
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541.stderr
@@ -0,0 +1,10 @@
+
+T17541.hs:20:17: error:
+    • Expected kind ‘TYPE (Rep rep)’,
+        but ‘Int#’ has kind ‘TYPE 'IntRep’
+    • In the type ‘Int#’
+      In the type family declaration for ‘Unboxed’
+      NB: Type ‘Unboxed’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/T17541b.hs b/testsuite/tests/dependent/should_fail/T17541b.hs
new file mode 100644
index 0000000000..6defdf705a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds, GADTs #-}
+
+module T17541b where
+
+import Data.Kind
+
+data T k :: k -> Type where
+    MkT1 :: T Type Int
+    MkT2 :: T (Type -> Type) Maybe
diff --git a/testsuite/tests/dependent/should_fail/T17541b.stderr b/testsuite/tests/dependent/should_fail/T17541b.stderr
new file mode 100644
index 0000000000..7502f21373
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541b.stderr
@@ -0,0 +1,10 @@
+
+T17541b.hs:8:20: error:
+    • Expected kind ‘k’, but ‘Int’ has kind ‘*’
+    • In the second argument of ‘T’, namely ‘Int’
+      In the type ‘T Type Int’
+      In the definition of data constructor ‘MkT1’
+      NB: Type ‘T’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 97580ce1cd..8ff5a88961 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -57,3 +57,6 @@ test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T16344', normal, compile_fail, [''])
 test('T16344a', normal, compile_fail, [''])
 test('T16418', normal, compile_fail, [''])
+test('T17541', normal, compile_fail, [''])
+test('T17541b', normal, compile_fail, [''])
+test('T17131', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/T15789.stderr b/testsuite/tests/polykinds/T15789.stderr
index c0fd4eab34..dc052ceaa7 100644
--- a/testsuite/tests/polykinds/T15789.stderr
+++ b/testsuite/tests/polykinds/T15789.stderr
@@ -4,3 +4,4 @@ T15789.hs:10:80: error:
     • In the first argument of ‘Cat’, namely ‘(forall b. cat b u)’
       In the kind ‘forall (cat :: forall xx. xx -> Type) a.
                    forall b. Cat (forall b. cat b u)’
+      In the data type declaration for ‘Zero’
diff --git a/testsuite/tests/polykinds/T15804.stderr b/testsuite/tests/polykinds/T15804.stderr
index 52262b675f..e89bbf8c80 100644
--- a/testsuite/tests/polykinds/T15804.stderr
+++ b/testsuite/tests/polykinds/T15804.stderr
@@ -2,3 +2,4 @@
 T15804.hs:5:12: error:
     • Expected a type, but ‘a :: k’ has kind ‘k’
     • In the kind ‘(a :: k) -> *’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/polykinds/T15881.stderr b/testsuite/tests/polykinds/T15881.stderr
index 4fde71dab7..8f395735db 100644
--- a/testsuite/tests/polykinds/T15881.stderr
+++ b/testsuite/tests/polykinds/T15881.stderr
@@ -3,3 +3,4 @@ T15881.hs:8:18: error:
     • Occurs check: cannot construct the infinite kind: k0 ~ k0 -> *
     • In the first argument of ‘n’, namely ‘n’
       In the kind ‘n n’
+      In the data type declaration for ‘A’
diff --git a/testsuite/tests/polykinds/T15881a.stderr b/testsuite/tests/polykinds/T15881a.stderr
index 84014c7abc..23f207dff3 100644
--- a/testsuite/tests/polykinds/T15881a.stderr
+++ b/testsuite/tests/polykinds/T15881a.stderr
@@ -2,3 +2,4 @@
 T15881a.hs:8:22: error:
     • Expected a type, but ‘a’ has kind ‘n’
     • In the kind ‘a -> Type’
+      In the data type declaration for ‘A’
diff --git a/testsuite/tests/polykinds/T16263.stderr b/testsuite/tests/polykinds/T16263.stderr
index 821a5fe307..9696f2238d 100644
--- a/testsuite/tests/polykinds/T16263.stderr
+++ b/testsuite/tests/polykinds/T16263.stderr
@@ -1,2 +1,4 @@
 
-T16263.hs:7:1: error: Illegal constraint in a kind: Eq a => *
+T16263.hs:7:1: error:
+    • Illegal constraint in a kind: Eq a => *
+    • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/saks/should_compile/Makefile b/testsuite/tests/saks/should_compile/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/saks/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/saks/should_fail/Makefile b/testsuite/tests/saks/should_fail/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk