Don't follow BaseType of abstract binders in MT reduction #13780
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
odersky
reviewed
Mar 7, 2022
Fix scala#11982 and the associated soundness problem. The issue with the behavior on master arises from the fact that type binder of match types might change as context gets more precise, which results in a single match type reducing in two different ways. This issue comes from the fact that subtyping looks into base types, and is thus able to match a type such as `T <: Tuple2[Int, Int]` against a pattern `case Tuple2[a, b]`, even if the best solutions for `a` and `b` in the current context are not guaranteed to be the best solution in more precise contexts (such as at call site in the added test case).
OlivierBlanvillain
force-pushed
the
fix-11982-2
branch
from
60fb562 to
c0ca8e9
Compare
odersky
approved these changes
Apr 4, 2022
smarter
added a commit
to dotty-staging/dotty
that referenced
this pull request
Apr 20, 2022
Previously, when reducing `a.T` we checked if the type of `a` was a subtype of `RefinedType(.., T, TypeAlias(...))`, now we extend this check to handle refinements where the `info` is a `TypeBounds` where both bounds are equal. This solves two big issues at once: - We can restore tests/pos/13491.scala to its original form from before scala#13780. The check for abstract types introduced by scala#13780 for soundness reasons is no longer hit because the type selection is reduced before we get to that point. This is important because parboiled2 relies on this and is therefore currently broken on 3.1.3-RC1 and main (sirthias/parboiled2#365). - This fixes scala#14904 (slow compilation issue affecting parboiled2) without caching skolems (as in the alternative fix scala#14909). Again, this is due to the type containing skolem being reducible to a simpler type and therefore cacheable.
smarter
added a commit
to dotty-staging/dotty
that referenced
this pull request
Apr 20, 2022
Previously, when reducing `a.T` we checked if the type of `a` was a subtype of `RefinedType(.., T, TypeAlias(...))`, now we extend this check to handle refinements where the `info` is a `TypeBounds` where both bounds are equal. This solves two big issues at once: - We can restore tests/pos/13491.scala to its original form from before scala#13780. The check for abstract types introduced by scala#13780 for soundness reasons is no longer hit because the type selection is reduced before we get to that point. This is important because parboiled2 relies on this and is therefore currently broken on 3.1.3-RC1 and main (sirthias/parboiled2#365). - This fixes scala#14903 (slow compilation issue affecting parboiled2) without caching skolems (as in the alternative fix scala#14909). Again, this is due to the type containing skolem being reducible to a simpler type and therefore cacheable.
michelou
pushed a commit
to michelou/dotty
that referenced
this pull request
Apr 25, 2022
Previously, when reducing `a.T` we checked if the type of `a` was a subtype of `RefinedType(.., T, TypeAlias(...))`, now we extend this check to handle refinements where the `info` is a `TypeBounds` where both bounds are equal. This solves two big issues at once: - We can restore tests/pos/13491.scala to its original form from before scala#13780. The check for abstract types introduced by scala#13780 for soundness reasons is no longer hit because the type selection is reduced before we get to that point. This is important because parboiled2 relies on this and is therefore currently broken on 3.1.3-RC1 and main (sirthias/parboiled2#365). - This fixes scala#14903 (slow compilation issue affecting parboiled2) without caching skolems (as in the alternative fix scala#14909). Again, this is due to the type containing skolem being reducible to a simpler type and therefore cacheable.
odersky
added a commit
to dotty-staging/dotty
that referenced
this pull request
May 31, 2022
scala#13780 caused several regressions and I think it is too restrictive as a fix. I am reverting it an re-opening the original scala#11982 issue. It would be good to get to the bottom of what the soundness problem hinted at in scala#11982 is, and what a fix should be. As it stands scala#11982 is not obviously a soundness problem but a separate compilation problem.
odersky
added a commit
to dotty-staging/dotty
that referenced
this pull request
May 31, 2022
scala#13780 caused several regressions and I think it is too restrictive as a fix. I am reverting it an re-opening the original scala#11982 issue. It would be good to get to the bottom of what the soundness problem hinted at in scala#11982 is, and what a fix should be. As it stands scala#11982 is not obviously a soundness problem but a separate compilation problem.
odersky
added a commit
to dotty-staging/dotty
that referenced
this pull request
May 31, 2022
scala#13780 caused several regressions and I think it is too restrictive as a fix. I am reverting it an re-opening the original scala#11982 issue. It would be good to get to the bottom of what the soundness problem hinted at in scala#11982 is, and what a fix should be. As it stands scala#11982 is not obviously a soundness problem but a separate compilation problem.
odersky
added a commit
to dotty-staging/dotty
that referenced
this pull request
Jun 12, 2022
Take up scala#13780 again, but refine it so that abstract types are allowed in match type reduction as long as they uniquely instantiate type parameters of the type pattern. Fixes scala#11982
Kordyjan
pushed a commit
to dotty-staging/dotty
that referenced
this pull request
Jun 22, 2022
Take up scala#13780 again, but refine it so that abstract types are allowed in match type reduction as long as they uniquely instantiate type parameters of the type pattern. Fixes scala#11982
bishabosha
pushed a commit
to dotty-staging/dotty
that referenced
this pull request
Oct 18, 2022
scala#13780 caused several regressions and I think it is too restrictive as a fix. I am reverting it an re-opening the original scala#11982 issue. It would be good to get to the bottom of what the soundness problem hinted at in scala#11982 is, and what a fix should be. As it stands scala#11982 is not obviously a soundness problem but a separate compilation problem.
bishabosha
pushed a commit
to dotty-staging/dotty
that referenced
this pull request
Oct 18, 2022
Take up scala#13780 again, but refine it so that abstract types are allowed in match type reduction as long as they uniquely instantiate type parameters of the type pattern. Fixes scala#11982
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.
Fix #11982 and the associated soundness problem. The issue with the behavior on master arises from the fact that type binder of match types might change as context gets more precise, which results in a single match type reducing in two different ways. This issue comes from the fact that subtyping looks into base types, and is thus able to match a type such as
T <: Tuple2[Int, Int]against a patterncase Tuple2[a, b], even if the best solutions foraandbin the current context are not guaranteed to be the best solution in more precise contexts (such as at call site in the added test case).