Skip to content

Commit e6da7d8

Browse files
committed
Match types amendment: extractors follow aliases and singletons
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.
1 parent fd3f6dc commit e6da7d8

File tree

1 file changed

+12
-2
lines changed

1 file changed

+12
-2
lines changed

content/match-types-spec.md

+12-2
Original file line numberDiff line numberDiff line change
@@ -286,8 +286,18 @@ At the top level, `variance = 1` and `scrutIsWidenedAbstract = false`.
286286
* If `q` is a skolem type `∃α:X`, fail as not specific.
287287
* Otherwise, compute `matchPattern(ti, q.Y, 0, scrutIsWidenedAbstract)`.
288288
* Otherwise, the underlying type definition of `q.Y` is of the form `= U`:
289-
* If `q` is a skolem type `∃α:X` and `U` refers to `α`, fail as not specific.
290-
* Otherwise, compute `matchPattern(ti, U, 0, scrutIsWidenedAbstract)`.
289+
* If `q` is not a skolem type `∃α:X`, compute `matchPattern(ti, U, 0, scrutIsWidenedAbstract)`.
290+
* Otherwise, let `U' = dropSkolem(U)` be computed as follow:
291+
* `dropSkolem(q)` is undefined.
292+
* `dropSkolem(p.T) = p'.T` where `p' = dropSkolem(p)` if the latter is defined. Otherwise:
293+
* If the underlying type of `p.T` is of the form `= V`, then `dropSkolem(V)`.
294+
* Otherwise `dropSkolem(p.T)` is undefined.
295+
* `dropSkolem(p.x) = p'.x` where `p' = dropSkolem(p)` if the latter is defined. Otherwise:
296+
* If the dealiased underlying type of `p.x` is a singleton type `y`, then `dropSkolem(y)`.
297+
* Otherwise `dropSkolem(p.x)` is undefined.
298+
* For all other types `Y`, `dropSkolem(Y)` is the type formed by replacing each component `Z` of `Y` by `dropSkolem(Z)`.
299+
* If `U'` is undefined, fail as not specific.
300+
* Otherwise, compute `matchPattern(ti, U', 0, scrutIsWidenedAbstract)`.
291301
* If `T` is a concrete type alias to a type lambda:
292302
* Let `P'` be the beta-reduction of `P`.
293303
* Compute `matchPattern(P', X, variance, scrutIsWidenedAbstract)`.

0 commit comments

Comments
 (0)