Avoid incorrect simplifications when updating bounds in the constraint #16410
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
That's brilliant. 😄 Amazing sleuthing. |
dwijnand
reviewed
Nov 25, 2022
dwijnand
reviewed
Nov 25, 2022
dwijnand
approved these changes
Nov 25, 2022
odersky
requested changes
Nov 28, 2022
| @@ -88,6 +88,8 @@ abstract class Constraint extends Showable { | |||
| * - Another type, indicating a solution for the parameter | |||
| * | |||
| * @pre `this contains param`. | |||
| * @pre `tp` does not contain top-level references to `param` | |||
| * (see `ensureNonCyclic`) | |||
There was a problem hiding this comment.
ensureNonCyclic is no longer there.
There was a problem hiding this comment.
Should probably be validBounds. Also: Should there be a way to test the precondition if a Config flag is set? Or can you argue statically that the precondition is always true? If yes, maybe add a note to this effect.
There was a problem hiding this comment.
Should there be a way to test the precondition if a Config flag is set?
I believe this is already checked a posteriori by the call to checkWellFormed() when Config.checkConstraintsNonCyclic is set.
|
Otherwise LGTM |
smarter
force-pushed
the
safe-add-bound-3
branch
from
3dafe20
to
d79bf05
Compare
When combining an old and a new bound, we use `Type#&`/`Type#|` which perform
simplifications. This is usually fine, but if the new bounds refer to the
parameter currently being updated, we can run into cyclic reasoning issues which
make the simplifications invalid after the update.
We already have logic for handling self-references in parameter bounds:
`updateEntry` calls `ensureNonCyclic` which sanitizes the type, but at this point
the simplifications have already occured. This commit simply moves the logic out
of `updateEntry` so that we can sanitize the new bounds before simplification.
More precisely, we rename `ensureNonCyclic` to `validBoundsFor` which calls
`validBoundFor`. Both are used to sanitize bounds where needed in `addOneBound`
and `unify`.
Since all calls to `updateEntry` now have sanitized bounds, we no longer need to
sanitize them in `updateEntry` itself, we document this change by adding a
pre-condition to `updateEntry`.
For the record, here's how `ConstraintsTest#validBoundsInit` used to fail.
It defines a method:
def foo[S >: T <: T | Int, T <: String]: Any
Before this commit, when `foo` was added to the current constraints, the
constraint `S <: T | Int` was propagated to the lower bound `T` of `S`. The
updated upper bound of `T` was thus set to:
String & (T | Int)
But because `Type#&` performs simplifications, this became
T | (String & Int)
by relying on the fact that at this point, `T <: String`. But in fact this
simplified bound no longer ensures that `T <: String`! The self-reference was
then replaced by `Any` in `OrderingConstraint#ensureNonCyclic`.
After this commit, the problematic simplification no longer occurs since the
new `T | Int` is sanitized to `Any` before being intersected with the old bound.
smarter
force-pushed
the
safe-add-bound-3
branch
from
d79bf05
to
50eb0e9
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When combining an old and a new bound, we use
Type#&/Type#|which perform simplifications. This is usually fine, but if the new bounds refer to the parameter currently being updated, we can run into cyclic reasoning issues which make the simplifications invalid after the update.We already have logic for handling self-references in parameter bounds:
updateEntrycallsensureNonCyclicwhich sanitizes the type, but at this point the simplifications have already occured. This commit simply moves the logic out ofupdateEntryso that we can sanitize the new bounds before simplification.More precisely, we rename
ensureNonCyclictovalidBoundsForwhich callsvalidBoundFor(singular). Both are used to sanitize bounds where needed inaddOneBoundandunify.Since all calls to
updateEntrynow have sanitized bounds, we no longer need to sanitize them inupdateEntryitself, we document this change by adding a pre-condition toupdateEntry.For the record, here's how
ConstraintsTest#validBoundsInitused to fail. It defines a method:Before this commit, when
foowas added to the current constraints, the constraintS <: T | Intwas propagated to the lower boundTofS. The updated upper bound ofTwas thus set to:But because
Type#&performs simplifications, this becameby relying on the fact that at this point,
T <: String. But in fact this simplified bound no longer ensures thatT <: String! The self-reference was then replaced byAnyinOrderingConstraint#ensureNonCyclic. After this commit, the problematic simplification no longer occurs since the newT | Intis sanitized toAnybefore being intersected with the old bound.