Fix a bug in occurs checking

1. Trac #12593 exposed a long-standing bug in the occurs
   checking machinery.  When unifying two type variables
          a ~ b
   where a /= b, we were assuming that there could be
   no occurs-check error.  But there can: 'a' can occur
   in b's kind!  When the RHS was a non-tyvar we used
   occurCheckExpand, which /did/ look in kinds, but not
   when the RHS was a tyvar.

   This bug has been lurking ever since TypeInType, maybe
   longer.  And it was present both in TcUnify (the on-the-fly
   unifier), and in TcInteract.

   I ended up refactoring both so that the tyvar/tyvar
   path naturally goes through the same occurs-check as
   non-tyvar rhss.  It's simpler and more robust now.

   One good thing is that both unifiers now share
       TcType.swapOverVars
       TcType.canSolveByUnification
   previously they had different logic for the same goals

2. Fixing this bug exposed another!  In T11635 we end
   up unifying
   (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
   Now that the occurs check is done for tyvars too, we
   look inside beta's kind.  And then reject the program
   becuase of the forall inside there.  But in fact that
   forall is fine -- it does not count as impredicative
   polymoprhism.   See Note [Checking for foralls]
   in TcType.

3. All this fuss around occurrence checking forced me
   to look at TcUnify.checkTauTvUpdate
          and TcType.occurCheckExpand
   There's a lot of duplication there, and I managed
   to elminate quite a bit of it. For example,
   checkTauTvUpdate called a local 'defer_me'; and then
   called occurCheckExpand, which then used a very
   similar 'fast_check'.

   Things are better, but there is more to do.

3 files changed, 46 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T12593.hs b/testsuite/tests/polykinds/T12593.hs
new file mode 100644
index 0000000000..867fb89284
--- /dev/null
+++ b/testsuite/tests/polykinds/T12593.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs, ConstraintKinds, PolyKinds, TypeInType,  KindSignatures, RankNTypes #-}
+
+module T12593 where
+
+import Data.Kind
+
+newtype Free k p a b where
+   Free :: (forall q. k q => (forall c d. p c d -> q c d) -> q a b)
+        -> Free k p a b
+
+run :: k2 q => Free k k1 k2 p a b
+             -> (forall (c :: k) (d :: k1). p c d -> q c d)
+             -> q a b
+run (Free cat) = cat
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
new file mode 100644
index 0000000000..4b551558a1
--- /dev/null
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -0,0 +1,31 @@
+
+T12593.hs:11:16: error:
+    • Expecting two fewer arguments to ‘Free k k4 k5 p’
+      Expected kind ‘k0 -> k1 -> *’, but ‘Free k k4 k5 p’ has kind ‘*’
+    • In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:31: error:
+    • Expecting one more argument to ‘k’
+      Expected a type, but
+      ‘k’ has kind
+      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+       -> Constraint’
+    • In the kind ‘k’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:40: error:
+    • Expecting two more arguments to ‘k4’
+      Expected a type, but
+      ‘k4’ has kind
+      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
+    • In the kind ‘k1’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 1c27dfd82e..6da6ae4439 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -151,3 +151,4 @@ test('T11640', normal, compile, [''])
 test('T11554', normal, compile_fail, [''])
 test('T12055', normal, compile, [''])
 test('T12055a', normal, compile_fail, [''])
+test('T12593', normal, compile_fail, [''])