Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Match types amendment: extractors follow aliases and singletons #84

Merged
merged 1 commit into from
Aug 19, 2024

Conversation

smarter
Copy link
Member

@smarter smarter commented 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 smarter requested a review from sjrd April 11, 2024 12:08
smarter added a commit to dotty-staging/dotty that referenced this pull request Apr 11, 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`.
smarter added a commit to dotty-staging/dotty that referenced this pull request Apr 11, 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`.
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 dotty-staging/dotty that referenced this pull request Apr 11, 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`.
@bjornregnell
Copy link

I'm in favor of promoting this fix; amendments seem better to do sooner than later and it increases the power of match types, so I recommend voting yes to this at our next meeting.

@soronpo
Copy link
Contributor

soronpo commented Apr 21, 2024

I'm also in favor. Now that we have a spec, we can reason well about such changes. From my perspective, as long as it's sound and doesn't cause performance issues, any change that expands the match type capability is a welcome addition.

@odersky
Copy link
Contributor

odersky commented Apr 21, 2024

I agree with Bjoern and Oron. It's a logical generalization, and elsewhere in the compiler we implement similar behavior.

smarter added a commit to dotty-staging/dotty that referenced this pull request May 5, 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`.
smarter added a commit to dotty-staging/dotty that referenced this pull request 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`.
smarter added a commit to dotty-staging/dotty that referenced this pull request May 8, 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`.
smarter added a commit to scala/scala3 that referenced this pull request May 8, 2024
…ons (#20161)

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`.
Kordyjan pushed a commit to scala/scala3 that referenced this pull request May 10, 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`.

[Cherry-picked 1a235c6]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants