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.

1 files changed, 7 insertions, 7 deletions

diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout
index 5d478ae04e..2e86b42713 100644
--- a/testsuite/tests/ghci.debugger/scripts/break012.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout
@@ -1,14 +1,14 @@
 Stopped in Main.g, break012.hs:5:10-18
-_result :: (a1, a2 -> a2, (), a -> a -> a) = _
-a :: a1 = _
-b :: a3 -> a3 = _
+_result :: (p, a1 -> a1, (), a -> a -> a) = _
+a :: p = _
+b :: a2 -> a2 = _
 c :: () = _
 d :: a -> a -> a = _
-a :: a1
-b :: a3 -> a3
+a :: p
+b :: a2 -> a2
 c :: ()
 d :: a -> a -> a
-a = (_t1::a1)
-b = (_t2::a3 -> a3)
+a = (_t1::p)
+b = (_t2::a2 -> a2)
 c = (_t3::())
 d = (_t4::a -> a -> a)