Stop inferring over-polymorphic kinds

Before this patch GHC was trying to be too clever
(Trac #16344); it succeeded in kind-checking this
polymorphic-recursive declaration

    data T ka (a::ka) b
      = MkT (T Type           Int   Bool)
            (T (Type -> Type) Maybe Bool)

As Note [No polymorphic recursion] discusses, the "solution" was
horribly fragile.  So this patch deletes the key lines in
TcHsType, and a wodge of supporting stuff in the renamer.

There were two regressions, both the same: a closed type family
decl like this (T12785b) does not have a CUSK:
  type family Payload (n :: Peano) (s :: HTree n x) where
    Payload Z (Point a) = a
    Payload (S n) (a `Branch` stru) = a

To kind-check the equations we need a dependent kind for
Payload, and we don't get that any more.  Solution: make it
a CUSK by giving the result kind -- probably a good thing anyway.

The other case (T12442) was very similar: a close type family
declaration without a CUSK.

9 files changed, 50 insertions, 2 deletions

diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs
index c76dfb962e..b4bcdb9d62 100644
--- a/testsuite/tests/dependent/should_compile/T12442.hs
+++ b/testsuite/tests/dependent/should_compile/T12442.hs
@@ -33,7 +33,8 @@ data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
 data instance Sing (elem :: EffElem x a xs) where
   SHere :: Sing Here
 
-type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs)
+type family UpdateResTy (b :: Type) (t :: Type)
+                        (xs :: [EFFECT]) (elem :: EffElem e a xs)
                         (thing :: e @@ a @@ b @@ t) :: [EFFECT] where
   UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
 
diff --git a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
index 109b18e9f7..789798b370 100644
--- a/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
+++ b/testsuite/tests/dependent/should_compile/T16326_Compile1.hs
@@ -20,7 +20,9 @@ type DComp a
            (x :: a) =
   f (g x)
 
-type family ElimList a
+-- Ensure that ElimList has a CUSK, beuas it is
+-- is used polymorphically its RHS (c.f. Trac #16344)
+type family ElimList (a :: Type)
                      (p :: [a] -> Type)
                      (s :: [a])
                      (pNil :: p '[])
diff --git a/testsuite/tests/dependent/should_compile/T16344b.hs b/testsuite/tests/dependent/should_compile/T16344b.hs
new file mode 100644
index 0000000000..1f6fa8a00e
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T16344b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeInType, GADTs, KindSignatures #-}
+
+module T16344 where
+
+import Data.Kind
+
+-- This one is accepted, even though it is polymorphic-recursive.
+-- See Note [No polymorphic recursion] in TcHsType
+
+data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 4ba649ac9d..4e162aed69 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -68,3 +68,5 @@ test('T14729kind', normal, ghci_script, ['T14729kind.script'])
 test('T16326_Compile1', normal, compile, [''])
 test('T16326_Compile2', normal, compile, [''])
 test('T16391a', normal, compile, [''])
+test('T16344b', normal, compile, [''])
+
diff --git a/testsuite/tests/dependent/should_fail/T16344.hs b/testsuite/tests/dependent/should_fail/T16344.hs
new file mode 100644
index 0000000000..0cf4b98642
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType, KindSignatures #-}
+
+module T16344 where
+
+import Data.Kind
+
+data T ka (a::ka) b  = MkT (T Type           Int   Bool)
+                           (T (Type -> Type) Maybe Bool)
diff --git a/testsuite/tests/dependent/should_fail/T16344.stderr b/testsuite/tests/dependent/should_fail/T16344.stderr
new file mode 100644
index 0000000000..b47561771f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344.stderr
@@ -0,0 +1,6 @@
+
+T16344.hs:7:46: error:
+    • Expected kind ‘ka’, but ‘Int’ has kind ‘*’
+    • In the second argument of ‘T’, namely ‘Int’
+      In the type ‘(T Type Int Bool)’
+      In the definition of data constructor ‘MkT’
diff --git a/testsuite/tests/dependent/should_fail/T16344a.hs b/testsuite/tests/dependent/should_fail/T16344a.hs
new file mode 100644
index 0000000000..cb4d1a7f21
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeInType, KindSignatures #-}
+
+module T16344 where
+
+import Data.Kind
+
+-- This one is rejected, but in the typechecking phase
+-- which is a bit nasty.
+-- See Note [No polymorphic recursion] in TcHsType
+
+data T2 ka (a::ka) = MkT2 (T2 Type a)
diff --git a/testsuite/tests/dependent/should_fail/T16344a.stderr b/testsuite/tests/dependent/should_fail/T16344a.stderr
new file mode 100644
index 0000000000..d838d14e57
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16344a.stderr
@@ -0,0 +1,6 @@
+
+T16344a.hs:11:36: error:
+    • Expected a type, but ‘a’ has kind ‘ka’
+    • In the second argument of ‘T2’, namely ‘a’
+      In the type ‘(T2 Type a)’
+      In the definition of data constructor ‘MkT2’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index baaddd7442..1f75a85716 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -53,3 +53,5 @@ test('T16326_Fail10', normal, compile_fail, [''])
 test('T16326_Fail11', normal, compile_fail, [''])
 test('T16326_Fail12', normal, compile_fail, [''])
 test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
+test('T16344', normal, compile_fail, [''])
+test('T16344a', normal, compile_fail, [''])