Fix floating of equalities
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 21 Dec 2017 14:13:54 +0000 (14:13 +0000)
committerBen Gamari <ben@smart-cactus.org>
Sun, 14 Jan 2018 22:07:21 +0000 (17:07 -0500)
commit594879dcb2fd5421d5f6ce5341442de32a4aac0a
treeaa9aa198c240f551c29bcb5044af85f1a5a74b65
parentb586f77b3384ce4d38e83205e7c0355c9b626b0a
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.

(cherry picked from commit f5cf9d1a1b198edc929e1fa96c6d841d182fe766)
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/indexed-types/should_fail/T13877.stderr
testsuite/tests/partial-sigs/should_fail/T14584.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/T14584.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/T14584a.hs [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/T14584a.stderr [new file with mode: 0644]
testsuite/tests/partial-sigs/should_fail/all.T
testsuite/tests/typecheck/should_fail/VtaFail.stderr