Use the eager unifier in the constraint solver

This patch continues the refactoring of the constraint solver
described in #23070.

The Big Deal in this patch is to call the regular, eager unifier from the
constraint solver, when we want to create new equalities. This
replaces the existing, unifyWanted which amounted to
yet-another-unifier, so it reduces duplication of a rather subtle
piece of technology. See

  * Note [The eager unifier] in GHC.Tc.Utils.Unify
  * GHC.Tc.Solver.Monad.wrapUnifierTcS

I did lots of other refactoring along the way

* I simplified the treatment of right hand sides that contain CoercionHoles.
  Now, a constraint that contains a hetero-kind CoercionHole is non-canonical,
  and cannot be used for rewriting or unification alike.  This required me
  to add the ch_hertero_kind flag to CoercionHole, with consequent knock-on
  effects. See wrinkle (2) of `Note [Equalities with incompatible kinds]` in
  GHC.Tc.Solver.Equality.

* I refactored the StopOrContinue type to add StartAgain, so that after a
  fundep improvement (for example) we can simply start the pipeline again.

* I got rid of the unpleasant (and inefficient) rewriterSetFromType/Co functions.
  With Richard I concluded that they are never needed.

* I discovered Wrinkle (W1) in Note [Wanteds rewrite Wanteds] in
  GHC.Tc.Types.Constraint, and therefore now prioritise non-rewritten equalities.

Quite a few error messages change, I think always for the better.

Compiler runtime stays about the same, with one outlier: a 17% improvement in T17836

Metric Decrease:
    T17836
    T18223

1 files changed, 6 insertions, 19 deletions

diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
index fcad722d63..b9beb8c49c 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr
@@ -1,7 +1,7 @@
 
 T14584.hs:57:41: warning: [GHC-39999] [-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)
+      from the context: (Action act, Monoid a, Good m)
         bound by the instance declaration at T14584.hs:55:10-89
     • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
@@ -10,23 +10,11 @@ T14584.hs:57:41: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
       In the expression:
         act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
 
-T14584.hs:57:41: warning: [GHC-06200] [-Wdeferred-type-errors (in -Wdefault)]
-    • Cannot use equality for substitution: a0 ~ a
-      Doing so would be ill-kinded.
-    • 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:57:3)
-
 T14584.hs:57:50: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce ‘m1 ~ *’
-      from the context: (Action act, Monoid a, Good m1)
+    • Could not deduce ‘m ~ *’
+      from the context: (Action act, Monoid a, Good m)
         bound by the instance declaration at T14584.hs:55:10-89
-      ‘m1’ is a rigid type variable bound by
+      ‘m’ is a rigid type variable bound by
         the instance declaration
         at T14584.hs:55:10-89
     • In the type ‘a’
@@ -36,9 +24,8 @@ T14584.hs:57:50: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)]
         ‘(fromSing @m (sing @m @a :: Sing _))’
 
 T14584.hs:57:60: warning: [GHC-88464] [-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:55:10-89
     • In the first argument of ‘Sing’, namely ‘_’