Implement match type amendment: extractors follow aliases and singletons #20161
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
smarter
added a commit
to smarter/improvement-proposals
that referenced
this pull request
Apr 11, 2024
The existing spec uses as a legal example:
```
class Base {
type Y
}
type YExtractor[t] = Base { type Y = t }
```
And we are allowed to define:
```
type ExtractY[B <: Base] = B match
case YExtractor[t] => t
```
However, with the existing spec, extraction does not always work as one might
expect:
```
class Sub1 extends Base:
type Y = Alias
type Alias = Int
class Sub2[T] extends Base:
type Y = T
class Sub3 extends Base:
val elem: Sub1 = new Sub1
type Y = elem.Y
ExtractY[Base { type Y = Int }] // OK
ExtractY[Sub1] // error
ExtractY[Sub2[Int]] // error
ExtractY[Sub3] // error
```
What's going on here is that when extracting a type `Y` from a non-stable
prefix `X`, the spec mandates that we generate a skolem `q` and use that as a
prefix to lookup the underlying type of `Y`. Extraction only succeeds if the
underlying type does not refer to `q`. For example, for `ExtractY[Sub1]` we
have `q.Y` with underlying type `q.Alias` which is rejected since it refers to
`q`.
We amend the spec to follow aliases and singleton types in the extracted type,
so that `q.Alias` can be dealiased to `Int` which is then accepted as a valid
extracted type.
More motivating examples can be found in the implementation at
scala/scala3#20161.
smarter
added a commit
to smarter/improvement-proposals
that referenced
this pull request
Apr 11, 2024
The existing spec uses as a legal example:
```
class Base {
type Y
}
type YExtractor[t] = Base { type Y = t }
```
And we are allowed to define:
```
type ExtractY[B <: Base] = B match
case YExtractor[t] => t
```
However, with the existing spec, extraction does not always work as one might
expect:
```
class Sub1 extends Base:
type Y = Alias
type Alias = Int
class Sub2[T] extends Base:
type Y = T
class Sub3 extends Base:
val elem: Sub1 = new Sub1
type Y = elem.Y
ExtractY[Base { type Y = Int }] // OK
ExtractY[Sub1] // error
ExtractY[Sub2[Int]] // error
ExtractY[Sub3] // error
```
What's going on here is that when extracting a type `Y` from a non-stable
prefix `X`, the spec mandates that we generate a skolem `q` and use that as a
prefix to lookup the underlying type of `Y`. Extraction only succeeds if the
underlying type does not refer to `q`. For example, for `ExtractY[Sub1]` we
have `q.Y` with underlying type `q.Alias` which is rejected since it refers to
`q`.
We amend the spec to follow aliases and singleton types in the extracted type,
so that `q.Alias` can be dealiased to `Int` which is then accepted as a valid
extracted type.
More motivating examples can be found in the implementation at
scala/scala3#20161.
smarter
added
the
needs-minor-release
|
I think it'd be useful to get this in 3.5.0-RC1 for testing purposes, we'd then revert it before the release if the sip committee votes against it. |
We will not be merging this before SIP committee decision. |
|
I'd like to formally appeal that decision. As can be seen in scala/improvement-proposals#84, there is support among the SIP committee members for not unnecessarily delaying this. Delaying makes sense if we believe that it will improve the quality of the final outcome, but we shouldn't stale things for purely procedural reasons. The procedures were put in place to achieve a certain result (build consensus, give enough time for experimentation, ...), so we should always ask ourselves if what we're doing is aligned with the result we want. |
|
I've now moved the new logic under an experimental language feature so that it can be merged without SIP approval. |
smarter
removed
the
needs-minor-release
sjrd
approved these changes
May 7, 2024
This implements the change proposed in scala/improvement-proposals#84. The added pos test case presents motivating examples, the added neg test cases demonstrate that errors are correctly reported when cycles are present. The potential for cycle is no worse than with the existing extraction logic as demonstrated by the existing test in `tests/neg/mt-deskolemize.scala`.
This way we can merge this PR without waiting for the SIP committee to approve it.
No need to save the value of `refersToSkolem`: if it's true before we enter `NamedType` it will be true after and `dropSkolem` will return `NoType`. The previous logic could still be useful if we want to give more easily actionable error messages in the future by only keeping in the type the skolems we couldn't remove.
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.
This implements the change proposed in
scala/improvement-proposals#84.
The added pos test case presents motivating examples, the added neg test cases demonstrate that errors are correctly reported when cycles are present. The potential for cycle is no worse than with the existing extraction logic as demonstrated by the existing test in
tests/neg/mt-deskolemize.scala.