Skip to content

Commit

Permalink
Match types amendment: extractors follow aliases and singletons
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
smarter committed Apr 11, 2024
1 parent fd3f6dc commit eb6d82f
Showing 1 changed file with 12 additions and 2 deletions.
14 changes: 12 additions & 2 deletions content/match-types-spec.md
Original file line number Diff line number Diff line change
Expand Up @@ -286,8 +286,18 @@ At the top level, `variance = 1` and `scrutIsWidenedAbstract = false`.
* If `q` is a skolem type `∃α:X`, fail as not specific.
* Otherwise, compute `matchPattern(ti, q.Y, 0, scrutIsWidenedAbstract)`.
* Otherwise, the underlying type definition of `q.Y` is of the form `= U`:
* If `q` is a skolem type `∃α:X` and `U` refers to `α`, fail as not specific.
* Otherwise, compute `matchPattern(ti, U, 0, scrutIsWidenedAbstract)`.
* If `q` is not a skolem type `∃α:X`, compute `matchPattern(ti, U, 0, scrutIsWidenedAbstract)`.
* Otherwise, let `U' = dropSkolem(U)` be computed as follow:
* `dropSkolem(q)` is undefined.
* `dropSkolem(p.T) = p'.T` where `p' = dropSkolem(p)` if the latter is defined. Otherwise:
* If the underlying type of `p.T` is of the form `= V`, then `dropSkolem(V)`.
* Otherwise `dropSkolem(p.T)` is undefined.
* `dropSkolem(p.x) = p'.x` where `p' = dropSkolem(p)` if the latter is defined. Otherwise:
* If the dealiased underlying type of `p.x` is a singleton type `r.y`, then `dropSkolem(r.y)`.
* Otherwise `dropSkolem(p.x)` is undefined.
* For all other types `Y`, `dropSkolem(Y)` is the type formed by replacing each component `Z` of `Y` by `dropSkolem(Z)`.
* If `U'` is undefined, fail as not specific.
* Otherwise, compute `matchPattern(ti, U', 0, scrutIsWidenedAbstract)`.
* If `T` is a concrete type alias to a type lambda:
* Let `P'` be the beta-reduction of `P`.
* Compute `matchPattern(P', X, variance, scrutIsWidenedAbstract)`.
Expand Down

0 comments on commit eb6d82f

Please sign in to comment.