Fix reachability of non-reducing match type children #13251
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
dwijnand
force-pushed
the
unreachable-match-type-subpattern
branch
from
21944e9
to
6a85b09
Compare
The reduction of a match type gets "stuck" when a case doesn't match but is also not provably disjoint from it. In these situations the match type reduction returns NoType, which means that in `A <:< B` if B reduces to NoType, then false will be returned. In the reachability/Space logic subtype checks are used to refine the candidate children of the scrutinee type so that impossible children aren't marked as missing and possible cases aren't marked as unreachable. To achieve that there is already some type mapping that runs before subtyping to approximate the parent. We extend that parent approximating logic so that non-reducing match types in the parent don't result in all the candidate children being rejected. The motivating case is NonEmptyTuple, its single-child `*:`, and the `Tuple.Tail` match type. In `Tuple.Tail[NonEmptyTuple]`, `case _ *: xs =>` won't match because NonEmptyTuple isn't a subtype of `*:` but it's also not provably disjoint from it (indeed it's `*:` parent)! So the reduction gets stuck, leading to NoType, leading to not a subtype. I had initially looked to fix this for single-child abstract sealed types, but that would still cause false positives in legitimate multi-child sealed types and an exhaustive match type (see WithExhaustiveMatch in patmat/i13189.scala). Also it's less scary to change the subtyping wrapping logic rather than the actually match type's reduction/matching logic. In a way the problem is that subtyping checks is too boolean: the candidate rejection wants to drop children that are definitely not subtypes, but the match type reduction is too conservative by returning NoType as soon as the obvious case isn't met. What subtyping should say there is ¯\_(ツ)_/¯
dwijnand
force-pushed
the
unreachable-match-type-subpattern
branch
from
6a85b09
to
fb5b562
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.
The reduction of a match type gets "stuck" when a case doesn't match but
is also not provably disjoint from it. In these situations the match
type reduction returns NoType, which means that in
A <:< Bif Breduces to NoType, then false will be returned.
In the reachability/Space logic subtype checks are used to refine the
candidate children of the scrutinee type so that impossible children
aren't marked as missing and possible cases aren't marked as
unreachable. To achieve that there is already some type mapping that
runs before subtyping to approximate the parent.
We extend that parent approximating logic so that non-reducing match
types in the parent don't result in all the candidate children being
rejected.
The motivating case is NonEmptyTuple, its single-child
*:, and theTuple.Tailmatch type. InTuple.Tail[NonEmptyTuple],case _ *: xs =>won't match because NonEmptyTuple isn't a subtype of
*:but it'salso not provably disjoint from it (indeed it's
*:parent)! So thereduction gets stuck, leading to NoType, leading to not a subtype.
I had initially looked to fix this for single-child abstract sealed
types, but that would still cause false positives in legitimate
multi-child sealed types and an exhaustive match type (see
WithExhaustiveMatch in patmat/i13189.scala). Also it's less scary to
change the subtyping wrapping logic rather than the actually match
type's reduction/matching logic.
In a way the problem is that subtyping checks is too boolean: the
candidate rejection wants to drop children that are definitely not
subtypes, but the match type reduction is too conservative by returning
NoType as soon as the obvious case isn't met. What subtyping should say
there is ¯_(ツ)_/¯