Kill floatEqualities completely

This patch delivers on #17656, by entirel killing off the complex
floatEqualities mechanism.  Previously, floatEqualities would float an
equality out of an implication, so that it could be solved at an outer
level. But now we simply do unification in-place, without floating the
constraint, relying on level numbers to determine untouchability.

There are a number of important new Notes:

* GHC.Tc.Utils.Unify Note [Unification preconditions]
  describes the preconditions for unification, including both
  skolem-escape and touchability.

* GHC.Tc.Solver.Interact Note [Solve by unification]
  describes what we do when we do unify

* GHC.Tc.Solver.Monad Note [The Unification Level Flag]
  describes how we control solver iteration under this new scheme

* GHC.Tc.Solver.Monad Note [Tracking Given equalities]
  describes how we track when we have Given equalities

* GHC.Tc.Types.Constraint Note [HasGivenEqs]
  is a new explanation of the ic_given_eqs field of an implication

A big raft of subtle Notes in Solver, concerning floatEqualities,
disappears.

Main code changes:

* GHC.Tc.Solver.floatEqualities disappears entirely

* GHC.Tc.Solver.Monad: new fields in InertCans, inert_given_eq_lvl
  and inert_given_eq, updated by updateGivenEqs
  See Note [Tracking Given equalities].

* In exchange for updateGivenEqa, GHC.Tc.Solver.Monad.getHasGivenEqs
  is much simpler and more efficient

* I found I could kill of metaTyVarUpdateOK entirely

One test case T14683 showed a 5.1% decrease in compile-time
allocation; and T5631 was down 2.2%. Other changes were small.

Metric Decrease:
    T14683
    T5631

3 files changed, 21 insertions, 34 deletions

diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 1a7162d612..f3b6343893 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -14,35 +14,18 @@ T10403.hs:15:12: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • In the type signature: h1 :: _ => _
 
 T10403.hs:19:7: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘(a -> a1) -> f0 a -> H f0’
-      Where: ‘f0’ is an ambiguous type variable
+    • Found type wildcard ‘_’
+        standing for ‘(a -> a1) -> B t0 a -> H (B t0)’
+      Where: ‘t0’ is an ambiguous type variable
              ‘a1’, ‘a’ are rigid type variables bound by
-               the inferred type of h2 :: (a -> a1) -> f0 a -> H f0
+               the inferred type of h2 :: (a -> a1) -> B t0 a -> H (B t0)
                at T10403.hs:22:1-41
     • In the type signature: h2 :: _
 
-T10403.hs:22:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
-      prevents the constraint ‘(Functor f0)’ from being solved.
-      Relevant bindings include
-        b :: f0 a (bound at T10403.hs:22:6)
-        h2 :: (a -> a1) -> f0 a -> H f0 (bound at T10403.hs:22:1)
-      Probable fix: use a type annotation to specify what ‘f0’ should be.
-      These potential instances exist:
-        instance Functor IO -- Defined in ‘GHC.Base’
-        instance Functor (B t) -- Defined at T10403.hs:10:10
-        instance Functor I -- Defined at T10403.hs:6:10
-        ...plus five others
-        ...plus two instances involving out-of-scope types
-        (use -fprint-potential-instances to see them all)
-    • In the second argument of ‘(.)’, namely ‘fmap (const ())’
-      In the expression: (H . fmap (const ())) (fmap f b)
-      In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
-
 T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘f0’ with ‘B t’
+    • Couldn't match type ‘t0’ with ‘t’
       Expected: H (B t)
-        Actual: H f0
+        Actual: H (B t0)
         because type variable ‘t’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
index e352f0d644..4d3a668241 100644
--- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr
@@ -1,12 +1,11 @@
 
 T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found extra-constraints wildcard standing for
-        ‘Reduce (LiftOf zq) zq’
-      Where: ‘zq’ is a rigid type variable bound by
+    • Found extra-constraints wildcard standing for ‘Reduce z zq’
+      Where: ‘z’, ‘zq’ are rigid type variables bound by
                the inferred type of
-                 bench_mulPublic :: (z ~ LiftOf zq, Reduce (LiftOf zq) zq) =>
+                 bench_mulPublic :: (z ~ LiftOf zq, Reduce z zq) =>
                                     Cyc zp -> Cyc z -> IO (zp, zq)
-               at T14715.hs:13:32-33
+               at T14715.hs:13:27-33
     • In the type signature:
-        bench_mulPublic :: forall z zp zq.
-                           (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp, zq)
+        bench_mulPublic :: forall z zp zq. (z ~ LiftOf zq, _) =>
+                                           Cyc zp -> Cyc z -> IO (zp, zq)
diff --git a/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr b/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
index 713bdc65c3..ee618dff56 100644
--- a/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr
@@ -1,6 +1,11 @@
 
-ScopedNamedWildcardsBad.hs:8:21: error:
+ScopedNamedWildcardsBad.hs:11:15: error:
     • Couldn't match expected type ‘Bool’ with actual type ‘Char’
-    • In the first argument of ‘not’, namely ‘x’
-      In the expression: not x
-      In an equation for ‘v’: v = not x
+    • In the first argument of ‘g’, namely ‘'x'’
+      In the expression: g 'x'
+      In the expression:
+        let
+          v = not x
+          g :: _a -> _a
+          g x = x
+        in (g 'x')