Simplify treatment of heterogeneous equality

Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would
spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for
a unification. But we needn't do this. Instead, we now spit out
a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original
Wanted. This means that we retain the connection between the
spat-out constraint and the original.

The problem with this new approach is that we cannot use the
casted equality for substitution; it's too like wanteds-rewriting-
wanteds. So, we forbid CTyEqCans that mention coercion holes.

All the details are in Note [Equalities with incompatible kinds]
in TcCanonical.

There are a few knock-on effects, documented where they occur.

While debugging an error in this patch, Simon and I ran into
infelicities in how patterns and matches are printed; we made
small improvements.

This patch includes mitigations for #17828, which causes spurious
pattern-match warnings. When #17828 is fixed, these lines should
be removed.

6 files changed, 45 insertions, 47 deletions

diff --git a/testsuite/tests/polykinds/T11399.stderr b/testsuite/tests/polykinds/T11399.stderr
index e5c9e0e37c..9174cd0b7d 100644
--- a/testsuite/tests/polykinds/T11399.stderr
+++ b/testsuite/tests/polykinds/T11399.stderr
@@ -1,6 +1,6 @@
 
 T11399.hs:10:32: error:
-    • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
+    • Couldn't match kind ‘GHC.Types.RuntimeRep’ with ‘*’
       When matching kinds
         a :: * -> *
         TYPE :: GHC.Types.RuntimeRep -> *
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
index 83e32f7a21..edb19408b2 100644
--- a/testsuite/tests/polykinds/T14846.stderr
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -3,8 +3,8 @@ T14846.hs:38:8: error:
     • Couldn't match type ‘ríki’ with ‘Hom riki’
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
-          i :: forall {k5} {k6} {cls2 :: k6 -> Constraint} (xx :: k5)
-                      (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *).
+          i :: forall {k5} {k6} {cls3 :: k6 -> Constraint} (xx :: k5)
+                      (a :: Struct cls3) (ríki :: Struct cls3 -> Struct cls3 -> *).
                StructI xx a =>
                ríki a a
         at T14846.hs:38:8-48
@@ -23,32 +23,36 @@ T14846.hs:38:8: error:
       In the instance declaration for ‘Category (Hom riki)’
 
 T14846.hs:39:12: error:
-    • Couldn't match kind ‘k4’ with ‘Struct cls2’
-      ‘k4’ is a rigid type variable bound by
-        the instance declaration
-        at T14846.hs:37:10-65
-      When matching kinds
-        cls0 :: Struct cls -> Constraint
-        cls1 :: k4 -> Constraint
+    • Could not deduce (StructI xx1 structured0)
+        arising from a use of ‘struct’
+      from the context: Category riki
+        bound by the instance declaration at T14846.hs:37:10-65
+      or from: StructI xx a
+        bound by the type signature for:
+                   i :: forall {k5} {k6} {cls3 :: k6 -> Constraint} (xx :: k5)
+                               (a :: Struct cls3).
+                        StructI xx a =>
+                        Hom riki a a
+        at T14846.hs:38:8-48
+      The type variables ‘xx1’, ‘structured0’ are ambiguous
+      Relevant bindings include
+        i :: Hom riki a a (bound at T14846.hs:39:3)
+      These potential instance exist:
+        instance forall k (xx :: k) (cls :: k -> Constraint)
+                        (structured :: Struct cls).
+                 (Structured xx cls ~ structured, cls xx) =>
+                 StructI xx structured
+          -- Defined at T14846.hs:28:10
     • In the expression: struct :: AStruct (Structured a cls)
       In the expression: case struct :: AStruct (Structured a cls) of
       In an equation for ‘i’:
           i = case struct :: AStruct (Structured a cls) of
-    • Relevant bindings include
-        i :: Hom riki a a (bound at T14846.hs:39:3)
 
-T14846.hs:39:31: error:
-    • Couldn't match kind ‘k4’ with ‘Struct cls2’
-      ‘k4’ is a rigid type variable bound by
-        the instance declaration
-        at T14846.hs:37:10-65
-      When matching kinds
-        cls1 :: k4 -> Constraint
-        cls0 :: Struct cls -> Constraint
-      Expected kind ‘Struct cls0’,
-        but ‘Structured a cls’ has kind ‘Struct cls1’
-    • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
+T14846.hs:39:44: error:
+    • Expected kind ‘Struct cls3 -> Constraint’,
+        but ‘cls’ has kind ‘k4 -> Constraint’
+    • In the second argument of ‘Structured’, namely ‘cls’
+      In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
-      In the expression: struct :: AStruct (Structured a cls)
     • Relevant bindings include
         i :: Hom riki a a (bound at T14846.hs:39:3)
diff --git a/testsuite/tests/polykinds/T17841.stderr b/testsuite/tests/polykinds/T17841.stderr
index 975f5a11d0..6157f55399 100644
--- a/testsuite/tests/polykinds/T17841.stderr
+++ b/testsuite/tests/polykinds/T17841.stderr
@@ -1,13 +1,6 @@
 
-T17841.hs:7:40: error:
-    • Couldn't match kind ‘k’ with ‘*’
-      ‘k’ is a rigid type variable bound by
-        the class declaration for ‘Foo’
-        at T17841.hs:7:17
-      When matching kinds
-        k0 :: *
-        t :: k
-      Expected kind ‘t’, but ‘a’ has kind ‘k0’
-    • In the first argument of ‘Proxy’, namely ‘(a :: t)’
+T17841.hs:7:45: error:
+    • Expected a type, but ‘t’ has kind ‘k2’
+    • In the kind ‘t’
+      In the first argument of ‘Proxy’, namely ‘(a :: t)’
       In the type signature: foo :: Proxy (a :: t)
-      In the class declaration for ‘Foo’
diff --git a/testsuite/tests/polykinds/T7278.stderr b/testsuite/tests/polykinds/T7278.stderr
index 265e27892b..37b00a7a70 100644
--- a/testsuite/tests/polykinds/T7278.stderr
+++ b/testsuite/tests/polykinds/T7278.stderr
@@ -1,5 +1,5 @@
 
 T7278.hs:9:43: error:
-    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’
+    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k1’
     • In the type signature:
         f :: (C (t :: k) (TF t)) => TF t p1 p0 -> t p1 p0
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 4341b3051a..2a8b6482aa 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -1,13 +1,13 @@
 
 T8616.hs:8:16: error:
-    • Couldn't match kind ‘k’ with ‘*’
-      ‘k’ is a rigid type variable bound by
+    • Couldn't match kind ‘k1’ with ‘*’
+      ‘k1’ is a rigid type variable bound by
         the type signature for:
-          withSomeSing :: forall k (kproxy :: k). Proxy kproxy
+          withSomeSing :: forall k1 (kproxy :: k1). Proxy kproxy
         at T8616.hs:7:1-52
       When matching types
         a0 :: *
-        Any :: k
+        Any :: k1
     • In the expression: undefined :: (Any :: k)
       In an equation for ‘withSomeSing’:
           withSomeSing = undefined :: (Any :: k)
@@ -15,7 +15,7 @@ T8616.hs:8:16: error:
         withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1)
 
 T8616.hs:8:30: error:
-    • Expected a type, but ‘Any :: k’ has kind ‘k’
+    • Expected a type, but ‘Any :: k’ has kind ‘k1’
     • In an expression type signature: (Any :: k)
       In the expression: undefined :: (Any :: k)
       In an equation for ‘withSomeSing’:
diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr
index b1d336646a..8acf58c9b5 100644
--- a/testsuite/tests/polykinds/T9017.stderr
+++ b/testsuite/tests/polykinds/T9017.stderr
@@ -1,16 +1,17 @@
 
 T9017.hs:8:7: error:
-    • Couldn't match kind ‘k1’ with ‘*’
-      ‘k1’ is a rigid type variable bound by
+    • Couldn't match kind ‘k2’ with ‘*’
+      ‘k2’ is a rigid type variable bound by
         the type signature for:
-          foo :: forall {k} {k1} (a :: k -> k1 -> *) (b :: k) (m :: k -> k1).
+          foo :: forall {k2} {k3} (a :: k2 -> k3 -> *) (b :: k2)
+                        (m :: k2 -> k3).
                  a b (m b)
         at T9017.hs:7:1-16
       When matching types
-        a1 :: * -> * -> *
-        a :: k -> k1 -> *
+        a0 :: * -> * -> *
+        a :: k2 -> k3 -> *
       Expected type: a b (m b)
-        Actual type: a1 a0 (m0 a0)
+        Actual type: a0 a1 (m0 a1)
     • In the expression: arr return
       In an equation for ‘foo’: foo = arr return
     • Relevant bindings include