Fix backwards subtyping checks in pattern type checking #6087
Conversation
This file contains hidden or 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
The code was systematically checking that pattern type <: scrutinee type However, this is actually wrong. If the scrutinee type is a _subtype_ of the pattern type, that is fine, because you could promote the scrutinee to the type of the pattern. This matters e.g. when matching on something with type forall x. T against patterns of type T[x := U]. Doing so would fail previously. I think that the pattern language was too limited previously to cause any actual problems. Attempts to do something erroneous would run into the fact that leaves of the pattern checking problem would always be checks like: T <: a, a <: T These both solve identically, by instantiating the variable a to the more elaborate type T. There were also a few obstacles that happened to save us, like `Request` being invariant in the ability list. So, the previous implementation ended up behaving as would pattern matching with equality checks rather than subtyping checks.
Contributor
|
@dolio With the new transcript, would you say this is ready to merge? |
aryairani
approved these changes
Jan 6, 2026
Contributor
Author
|
Yeah, I think so. There was one case I was concerned about, because I didn't change it (no |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
This PR fixes some backwards subtyping checks for patterns.
The code was systematically checking that
However, this is actually wrong. If the scrutinee type is a subtype of the pattern type, that is fine, because you could promote the scrutinee to the type of the pattern. This matters e.g. when matching on something with type
against patterns of type
T[x := U]. Doing so would fail previously.I think that the pattern language was too limited previously to cause any actual problems. Attempts to do something erroneous would run into the fact that leaves of the pattern checking problem would always be checks like:
These both solve identically, by instantiating the variable
ato the more elaborate typeT. There were also a few obstacles that happened to save us, likeRequestbeing invariant in the ability list. So, the previous implementation ended up behaving as would pattern matching with equality checks rather than subtyping checks.I also needed to tweak the pattern coverage checker, because it wasn't set up to handle treating
forall x. Tas having patterns asT, so it would complain that you aren't actually covering everything.Transcripts pass, but I'll probably do some more testing tomorrow, and add a regression test.
Fixes #6018