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, 39 deletions

diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index 80c8ce2683..372ca3fba2 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,58 +1,26 @@
 
 T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce: m1 ~ *
-      from the context: (Action act, Monoid a, Good m1)
-        bound by the instance declaration at T14584.hs:54:10-89
-      ‘m1’ is a rigid type variable bound by
-        the instance declaration
-        at T14584.hs:54:10-89
-      When matching types
-        a :: *
-        a0 :: m
-      Expected type: Sing a0
-        Actual type: Sing a
-    • In the second argument of ‘fromSing’, namely
-        ‘(sing @m @a :: Sing _)’
-      In the fourth argument of ‘act’, namely
-        ‘(fromSing @m (sing @m @a :: Sing _))’
-      In the expression:
-        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
-    • Relevant bindings include
-        monHom :: a -> a (bound at T14584.hs:56:3)
-
-T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce: a ~~ a0
+    • Could not deduce (SingI a) arising from a use of ‘sing’
       from the context: (Action act, Monoid a, Good m1)
         bound by the instance declaration at T14584.hs:54:10-89
-      ‘a’ is a rigid type variable bound by
-        the instance declaration
-        at T14584.hs:54:10-89
-      Expected type: Sing a0
-        Actual type: Sing a
     • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
       In the fourth argument of ‘act’, namely
         ‘(fromSing @m (sing @m @a :: Sing _))’
       In the expression:
         act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
-    • Relevant bindings include
-        monHom :: a -> a (bound at T14584.hs:56:3)
 
-T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce (SingI a) arising from a use of ‘sing’
-      from the context: (Action act, Monoid a, Good m1)
-        bound by the instance declaration at T14584.hs:54:10-89
-    • In the second argument of ‘fromSing’, namely
+T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Expected kind ‘m1’, but ‘a’ has kind ‘*’
+    • In the type ‘a’
+      In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
       In the fourth argument of ‘act’, namely
         ‘(fromSing @m (sing @m @a :: Sing _))’
-      In the expression:
-        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
 
 T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘a0 :: m’
-      Where: ‘a0’ is an ambiguous type variable
-             ‘m’ is a rigid type variable bound by
+    • Found type wildcard ‘_’ standing for ‘a :: m’
+      Where: ‘a’, ‘m’ are rigid type variables bound by
                the instance declaration
                at T14584.hs:54:10-89
     • In the first argument of ‘Sing’, namely ‘_’