Fix floating of equalities

This rather subtle patch fixes Trac #14584.  The problem was
that we'd allowed a coercion, bound in a nested scope, to escape
into an outer scope.

The main changes are

* TcSimplify.floatEqualities takes more care when floating
  equalities to make sure we don't float one out that mentions
  a locally-bound coercion.
  See Note [What prevents a constraint from floating]

* TcSimplify.emitResidualConstraints (which emits the residual
  constraints in simplifyInfer) now avoids burying the constraints
  for escaping CoVars inside the implication constraint.

* Since I had do to this stuff with CoVars, I moved the
  fancy footwork about not quantifying over CoVars from
  TcMType.quantifyTyVars to its caller
  TcSimplify.decideQuantifiedTyVars.  I think its other
  callers don't need to worry about all this CoVar stuff.

This turned out to be surprisigly tricky, and took me a solid
day to get right.  I think the result is reasonably neat, though,
and well documented with Notes.

1 files changed, 0 insertions, 6 deletions

diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index 17486dfefa..a9958016ce 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -6,12 +6,6 @@ VtaFail.hs:7:16: error:
       In an equation for ‘answer_nosig’:
           answer_nosig = pairup_nosig @Int @Bool 5 True
 
-VtaFail.hs:12:26: error:
-    • No instance for (Num Bool) arising from a use of ‘addOne’
-    • In the expression: addOne @Bool 5
-      In an equation for ‘answer_constraint_fail’:
-          answer_constraint_fail = addOne @Bool 5
-
 VtaFail.hs:14:17: error:
     • Cannot apply expression of type ‘p0 -> p0’
       to a visible type argument ‘Int’