From eb6d82f9ae34ef2bfda88910743a7acfb3c70865 Mon Sep 17 00:00:00 2001
From: Guillaume Martres <smarter@ubuntu.com>
Date: Wed, 10 Apr 2024 14:36:55 +0200
Subject: [PATCH] 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.

More motivating examples can be found in the implementation at
https://github.com/scala/scala3/pull/20161.
---
 content/match-types-spec.md | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/content/match-types-spec.md b/content/match-types-spec.md
index 1624e64c..aa868061 100644
--- a/content/match-types-spec.md
+++ b/content/match-types-spec.md
@@ -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)`.