diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-21 14:13:54 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-21 14:14:21 +0000 |
| commit | f5cf9d1a1b198edc929e1fa96c6d841d182fe766 (patch) | |
| tree | 21f9daccb8a46e0f5b06ab820861a842cecd91b3 /testsuite/tests/indexed-types | |
| parent | a492af06d3264530d134584f22ffb726a16c78ec (diff) | |
| download | haskell-f5cf9d1a1b198edc929e1fa96c6d841d182fe766.tar.gz | |
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.
Diffstat (limited to 'testsuite/tests/indexed-types')
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T13877.stderr | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/testsuite/tests/indexed-types/should_fail/T13877.stderr b/testsuite/tests/indexed-types/should_fail/T13877.stderr index a90a4dd93a..9dc8534ca1 100644 --- a/testsuite/tests/indexed-types/should_fail/T13877.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13877.stderr @@ -2,7 +2,9 @@ T13877.hs:65:17: error: • Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’ Expected type: Sing x - -> Sing xs -> App [a] (':->) * p xs -> App [a] (':->) * p (x : xs) + -> Sing xs + -> App [a1] (':->) * p xs + -> App [a1] (':->) * p (x : xs) Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs) • In the expression: listElimPoly @(:->) @a @p @l In an equation for ‘listElimTyFun’: @@ -10,14 +12,14 @@ T13877.hs:65:17: error: • Relevant bindings include listElimTyFun :: Sing l -> (p @@ '[]) - -> (forall (x :: a) (xs :: [a]). + -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)) -> p @@ l (bound at T13877.hs:65:1) T13877.hs:65:41: error: • Expecting one more argument to ‘p’ - Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’ + Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’ • In the type ‘p’ In the expression: listElimPoly @(:->) @a @p @l In an equation for ‘listElimTyFun’: @@ -25,7 +27,7 @@ T13877.hs:65:41: error: • Relevant bindings include listElimTyFun :: Sing l -> (p @@ '[]) - -> (forall (x :: a) (xs :: [a]). + -> (forall (x :: a1) (xs :: [a1]). Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)) -> p @@ l (bound at T13877.hs:65:1) |