Care with occCheckExpand in kind of occurrences

Issue #18451 showed that we could get an infinite type, through
over-use of occCheckExpand in the kind of an /occurrence/ of a
type variable.

See Note [Occurrence checking: look inside kinds] in GHC.Core.Type

This patch fixes the problem by making occCheckExpand less eager
to expand synonyms in kinds.

It also improves pretty printing of kinds, by *not* suppressing
the kind on a tyvar-binder like
    (a :: Const Type b)
where type Const p q = p.  Even though the kind of 'a' is Type,
we don't want to suppress the kind ascription.  Example: the
error message for polykinds/T18451{a,b}. See GHC.Core.TyCo.Ppr
Note [Suppressing * kinds].

7 files changed, 58 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T18451.hs b/testsuite/tests/polykinds/T18451.hs
new file mode 100644
index 0000000000..da14360ea5
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+type Const a b = a
+data SameKind :: k -> k -> Type
+
+type T (k :: Const Type a) = forall (b :: k). SameKind a b
diff --git a/testsuite/tests/polykinds/T18451.stderr b/testsuite/tests/polykinds/T18451.stderr
new file mode 100644
index 0000000000..5f61afcbbe
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451.stderr
@@ -0,0 +1,9 @@
+
+T18451.hs:10:58: error:
+    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type ‘forall (b :: k). SameKind a b’
+      In the type declaration for ‘T’
+    • Type variable kinds:
+        a :: k0
+        k :: Const (*) a
diff --git a/testsuite/tests/polykinds/T18451a.hs b/testsuite/tests/polykinds/T18451a.hs
new file mode 100644
index 0000000000..9b5248c30f
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+type Const a b = a
+
+foo :: forall a b (c :: Const Type b). Proxy '[a, c]
+foo = error "ruk"
diff --git a/testsuite/tests/polykinds/T18451a.stderr b/testsuite/tests/polykinds/T18451a.stderr
new file mode 100644
index 0000000000..fbfd3ce288
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451a.stderr
@@ -0,0 +1,7 @@
+
+T18451a.hs:10:8: error:
+    • These kind and type variables: a b (c :: Const Type b)
+      are out of dependency order. Perhaps try this ordering:
+        (b :: k) (a :: Const (*) b) (c :: Const (*) b)
+    • In the type signature:
+        foo :: forall a b (c :: Const Type b). Proxy '[a, c]
diff --git a/testsuite/tests/polykinds/T18451b.hs b/testsuite/tests/polykinds/T18451b.hs
new file mode 100644
index 0000000000..9b5248c30f
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+type Const a b = a
+
+foo :: forall a b (c :: Const Type b). Proxy '[a, c]
+foo = error "ruk"
diff --git a/testsuite/tests/polykinds/T18451b.stderr b/testsuite/tests/polykinds/T18451b.stderr
new file mode 100644
index 0000000000..d12d9b382a
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451b.stderr
@@ -0,0 +1,7 @@
+
+T18451b.hs:10:8: error:
+    • These kind and type variables: a b (c :: Const Type b)
+      are out of dependency order. Perhaps try this ordering:
+        (b :: k) (a :: Const (*) b) (c :: Const (*) b)
+    • In the type signature:
+        foo :: forall a b (c :: Const Type b). Proxy '[a, c]
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 00856b8dc3..436bb9dbce 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -220,3 +220,6 @@ test('CuskFam', normal, compile, [''])
 test('T17841', normal, compile_fail, [''])
 test('T17963', normal, compile_fail, [''])
 test('T18300', normal, compile_fail, [''])
+test('T18451', normal, compile_fail, [''])
+test('T18451a', normal, compile_fail, [''])
+test('T18451b', normal, compile_fail, [''])