Remove the type-checking knot.

Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
Looking at the code in tcInferApps, I'm amazed this hasn't happened
before! I couldn't think of a good way to fix it (with dependent
types, we can't really keep types out of kinds, after all), so
I just went ahead and removed the knot.

This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
just use it. (Previously, we looked up the knot-tied TyCon and used
that.) Then, during the final zonk, replace TcTyCons with the real,
full-blooded TyCons in the global environment. It's all very easy.

The new bit is explained in the existing
Note [Type checking recursive type and class declarations]
in TcTyClsDecls.

Naturally, I removed various references to the knot and the
zonkTcTypeInKnot (and related) functions. Now, we can print types
during type checking with abandon!

NB: There is a teensy error message regression with this patch,
around the ordering of quantified type variables. This ordering
problem is fixed (I believe) with the patch for #14880. The ordering
affects only internal variables that cannot be instantiated with
any kind of visible type application.

There is also a teensy regression around the printing of types
in TH splices. I think this is really a TH bug and will file
separately.

Test case: dependent/should_fail/T15380

9 files changed, 38 insertions, 11 deletions

diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
index 906695f3f7..610e434d6c 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.stderr
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -1,5 +1,5 @@
 
 T14066a.hs:13:3: warning:
     Type family instance equation is overlapped:
-      forall c d (x :: c) (y :: d).
+      forall d c (x :: c) (y :: d).
         Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_fail/T15380.hs b/testsuite/tests/dependent/should_fail/T15380.hs
new file mode 100644
index 0000000000..32ea8ec724
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T15380 where
+
+import Data.Kind
+
+class Generic a where
+  type Rep a :: Type
+
+class PGeneric a where
+  type To a (x :: Rep a) :: a
+
+type family MDefault (x :: a) :: a where
+  MDefault x = To (M x)
+
+class C a where
+  type M (x :: a) :: a
+  type M (x :: a) = MDefault x
diff --git a/testsuite/tests/dependent/should_fail/T15380.stderr b/testsuite/tests/dependent/should_fail/T15380.stderr
new file mode 100644
index 0000000000..9b30078c64
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.stderr
@@ -0,0 +1,6 @@
+
+T15380.hs:16:16: error:
+    • Expecting one more argument to ‘To (M x)’
+      Expected a type, but ‘To (M x)’ has kind ‘Rep (M x) -> M x’
+    • In the type ‘To (M x)’
+      In the type family declaration for ‘MDefault’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 59d80375ff..593b7787a1 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -34,4 +34,4 @@ test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
 test('T15343', normal, compile_fail, [''])
-
+test('T15380', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 9765244f1e..d6ba833e35 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -46,7 +46,7 @@
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
diff --git a/testsuite/tests/polykinds/T7524.stderr b/testsuite/tests/polykinds/T7524.stderr
index 26cfe39e8a..2340ce1aa6 100644
--- a/testsuite/tests/polykinds/T7524.stderr
+++ b/testsuite/tests/polykinds/T7524.stderr
@@ -2,5 +2,5 @@
 T7524.hs:5:15: error:
     Conflicting family instance declarations:
       forall k2 (a :: k2). F a a = Int -- Defined at T7524.hs:5:15
-      forall k1 k2 (a :: k1) (b :: k2).
+      forall k2 k1 (a :: k1) (b :: k2).
         F a b = Bool -- Defined at T7524.hs:6:15
diff --git a/testsuite/tests/th/T10267.stderr b/testsuite/tests/th/T10267.stderr
index 0f8e2215bc..71aca96b86 100644
--- a/testsuite/tests/th/T10267.stderr
+++ b/testsuite/tests/th/T10267.stderr
@@ -24,7 +24,7 @@ T10267.hs:8:1: error:
     • Relevant bindings include i :: a -> a (bound at T10267.hs:8:1)
       Valid hole fits include
         i :: a -> a (bound at T10267.hs:8:1)
-        j :: forall a. a -> a
+        j :: forall a0. a0 -> a0
           with j @a
           (bound at T10267.hs:8:1)
         k :: forall a. a -> a
@@ -53,10 +53,10 @@ T10267.hs:14:3: error:
     • Relevant bindings include k :: a -> a (bound at T10267.hs:14:3)
       Valid hole fits include
         k :: a -> a (bound at T10267.hs:14:3)
-        j :: forall a. a -> a
+        j :: forall a0. a0 -> a0
           with j @a
           (bound at T10267.hs:8:1)
-        i :: forall a. a -> a
+        i :: forall a0. a0 -> a0
           with i @a
           (bound at T10267.hs:8:1)
         l :: forall a. a -> a
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 8c7a273ed8..829e14ad70 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -66,7 +66,7 @@ T6018fail.hs:59:10: error:
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at T6018fail.hs:62:15
@@ -153,5 +153,6 @@ T6018fail.hs:129:1: error:
 T6018fail.hs:134:1: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
-    but these LHS type and kind patterns are not bare variables: ‘*’, ‘Char’
+    but these LHS type and kind patterns are not bare variables: ‘*’,
+                                                                 ‘Char’
       FC Char a = a -- Defined at T6018fail.hs:134:1
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index e90dce0620..9914842013 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error:
 
 T6018failclosed.hs:25:5: error:
     • Type family equation violates injectivity annotation.
-      Type and kind variables ‘k1’, ‘b’
+      Type and kind variables ‘k2’, ‘b’
       cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
-        forall k1 k2 (b :: k1) (c :: k2).
+        forall k1 k2 (b :: k2) (c :: k1).
           JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
     • In the equations for closed type family ‘JClosed’
       In the type family declaration for ‘JClosed’