Remove unnecessary and recursive Space decomposition #19216
Merged
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
|
Is it actually possible to have the same behaviour without type projections? |
|
Which behaviour? |
|
To have an overflow during decomposition. |
|
It seems to me like those decompositions are not unnecessary. We could try something better, but I don't know what. If the issue concerns only type projections, then it's possible to just special case them. |
dwijnand
force-pushed
the
recursive-decompose-prefix
branch
2 times, most recently
from
98c10c9 to
b973cf9
Compare
... makes it easier to disable one of them.
Space decomposition recently learnt to decompose prefixes. Given a nested definition like in i19031, aggressively trying to decompose while intersecting can lead to recursive decompositions (building bigger and bigger nested prefixes). Turns out the decomposition isn't necessary.
If refineUsingParent/instantiateToSubType is passed a HK then it's not possible to instantiate a class to that type (at the moment and perhaps ever). So it's important we guard against that. This came up while trying to see if Mark[?] and Foo[Int] (from pos/i19031.ci-reg1.scala) are provably disjoint - which they should be reported not to be. Because they're not applied types of the same type constructor we end up trying to prove that HK type Mark is disjoint from HK type Foo. Because we don't know how to instantiate Foo's subclasses (e.g Bar2) such that it's a subtype of higher-kinded type "Mark", we end up discarding all of Foo's subclasses, which implies that Foo & Mark is uninhabited, thus they are provably disjoint - which is incorrect. We originally didn't encounter this because we eagerly decomposed in Space intersection, while now we've dispatched it to provablyDisjoint. (edit) We allow for some kindness in provablyDisjoint.
Minimising from the `case test.Generic =>` in ParallelTesting, the anonymous pattern match is expanded, wrapping the match with `applyOrElse`, which has a type parameter A1 as the scrutinee type, with an upper bound of the original element type (out.Foo for us). During reachability analysis the pattern type, e.g. out.Bar3.type, is intersected with the scrutinee type, A1 - giving out.Bar3.type & A1. Then that we attempt to decompose that type. Previously the abstract A1 in that type lead to 3 WildcardTypes, for the 3 subclasses, which are a subtype of previous cases. The fix that by generalising how we recognise the singleton types in the scrutinee type, so instead of the ownership chain we use the parameter type info, and we also match term parameters. For extra correctness we consider the failure to be a subtype of a mixin as a failure for instantiating. Also, make sure to handle and avoid recursion in traverseTp2.
dwijnand
force-pushed
the
recursive-decompose-prefix
branch
from
f90db50 to
0931c43
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.
Space decomposition recently learnt to decompose prefixes. Given a
nested definition like in i19031, aggressively trying to decompose while
intersecting can lead to recursive decompositions (building bigger and
bigger nested prefixes). Turns out the decomposition isn't necessary.