## Scala's "type T in class C as seen from a prefix type S" with examples

Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier reference:

> The notion of a type T in class C seen from some prefix type S makes sense only if the prefix type S has a type instance of class C as a base type, say S′#C[T1,…,Tn]. Then we define as follows.
> 
> 1. If S = ϵ.type, then T in C seen from S is T itself.
> 2. Otherwise, if S is an existential type S′ forSome { Q }, and T in C seen from S′ is T′, then T in C seen from S is T′ forSome {Q}.
> 3. Otherwise, if T is the i'th type parameter of some class D, then
>     1. If S has a base type D[U1,…,Un], for some type parameters [U1,…,Un], then T in C seen from S is Ui.
>     2. Otherwise, if C is defined in a class C′, then T in C seen from S is the same as T in C′ seen from S′.
>     3. Otherwise, if C is not defined in another class, then T in C seen from S is T itself.
> 4. Otherwise, if T is the singleton type D.this.type for some class D then
>     1. If D is a subclass of C and S has a type instance of class D among its base types, then T in C seen from S is S.
>     2. Otherwise, if C is defined in a class C′, then T in C seen from S is the same as T in C′ seen from S′.
>     3. Otherwise, if C is not defined in another class, then T in C seen from S is T itself.
> 5. If T is some other type, then the described mapping is performed to all its type components.
> 
> If T is a possibly parameterized class type, where T's class is defined in some other class D, and S is some prefix type, then we use "T seen from S" as a shorthand for "T in D seen from S".

Rule 1 is the base case for the recursive definition of ASF. Altough you cannot write `ϵ.type` in a Scala program, the ASF might be sent to the first rule by rules that strip the prefix: 2, 3.2 and 4.2.

### Rule 2: Existential types

Rule 2 is about seeing through existential types. Let's consider an example:

```scala
class X

object Rule2 {
  abstract class A[V] {
    val t: V
  }
  val a: A[W] forSome { type W <: X } = null
  val x: X = a.t
}
```

To typecheck `val x: X = a.t` we need to understand the type of `a.t`.

  * We ask ASF for `A.V` in `A` as seen from `a.type`. The prefix `S'` is `ϵ.type`. Rule 2 applies with the existential type `S' forSome {Q}` decomposed into the types `S' = A[W]` and `Q = { type W <: X }`. Note that the two `S'`s are not the same -- the first is the prefix of the ASF, the second the prefix of the existential type -- this is an unfortunate name clash in the spec. ASF applies itself recursively to the prefix `A[W]` of the existential type.
  * ASF's query is `A.V` in `A` as seen from `A[W]`. Rule 3.1 extracts the type parameter `W` and returns it. Check the explanation of Rule 3 for details.
  * ASF completes the application of Rule 2 by substituting prefix `A[W]` with `W` in the existential type and returns `W forSome { type W <: X }` as its final answer.

We can simplify the returned existential type by applying Simplification Rules (SRs) specific to existential types. [SLS 3.2.10](http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#existential-types) contains the definition of SRs.
  - By application of SR4, we subsitute the upper bound `X` of the type `W` in the prefix of the existential type `W forSome { type W <: X }` and we simplify the existential type to `X forSome { type W <: X }`.
  - By application of SR2, we drop the unused quantification `type W <: X` in `X forSome { type W <: X }` and simplify the existential type to `X forSome {}`.
  - By application of SR3, we drop the empty sequence of quantifications in `X forSome {}` and further simplify the existential type to `X`.

### Rule 3: Type parameters

The third rule is about resolution of a type parameter for a given type argument.

```scala
object Rule3 {
  abstract class A[T] {
    abstract class B {
      abstract class C1 {
        val t: T
      }
      abstract class C2 extends C1
      val c: C2
    }
    val b: B
  }

  abstract class AA[T] extends A[T]

  val x1: AA[X] = null
  // the type of x1.b.c.t.type is type A.T in C1 as seen from x1.b.c.type
  val x2: x1.b.c.t.type = null
  val x: X = x2
}
```

In order to typecheck `val x: X = x2` we need to understand the type of `x2` (we'll be look at the type of the term `t`).

  * We ask ASF for `A.T` in `C1` as seen from the prefix `S = x1.b.c.type`. The prefix `S'` is `x1.b.type` (so `C1` can be selected from `S'` with the type projection `x1.b.type#C1` and `C1` is a base class for `S`). Rule 3 applies with `A.T` being the first type paramemter of the class `A`; the class `D` is `A`. The prefix `S` doesn't have an application of the parametric type `A` amongst its base types so Rule 3.1 doesn't apply. Rule 3.2 applies because the class `C1` is nested in the class `B`. ASF applies itself recursively to the same type `A.T` but in the class one level up in the class nesting relationship.
  * ASF's query is `A.T` in `B` as seen from the prefix `S = x1.b.type` (so `S' = x1.type`). By the same reasoning as in the step above, first Rule 3 applies and then Rule 3.2 applies because the class `B` is nested in the class `A`. ASF applies itself recursively to the same type `A.T` but in the class `A`.
  * ASF's query now is `A.T` in `A` as seen from the prefix `S = x1.type` (so `S' = ϵ.type`). Rule 3 still applies because `A.T` is the first type parameter of the class `A`. Rule 3.1 applies because the type `A[X]` is a base type of the prefix `S`; ASF extracts the type argument from the type `A[X]` and returns `X` as its final answer.

In the example above, we only excercised rules 3.1 and 3.2 but not 3.3. The Rule 3.3 is a fallthrough rule that is triggered when prefix doesn't encode any relevant information about how to resolve a type parameter. For example, you can ask for the type `A.T` in the class `X` as seen from the prefix `x.type` to trigger Rule 3.3. The definition of ASF ties together the class `C` and the prefix type `S` but leaves the type `T` arbitrary. You can ask ASF for a type unrelated to the passed prefix. The 3.3 cannot be triggered directly by writing a type in user program because in order to access a type parameter, you have to be inside the class and then other rules will apply.

### Rule 4: `this` resolution

The fourth rule is about resolution `this`. Let's see it in action based on this example:

```scala
object Rule4 {
  abstract class A {
    abstract class B1 {
      abstract class C1 {
        val a: A.this.type
      }
      abstract class C2 extends C1
      val c: C2
    }
    abstract class B2 extends B1
    val b: B2
  }
  abstract class AA extends A

  val x1: AA = null
  val x2: x1.b.c.a.type = null
  val x: AA = x2
}
```

In order to typecheck `val x: AA = x2` we need to understand the type of `x2`.

  * We ask ASF for `A.this.type` in `C1` as seen from the prefix `S = x1.b.c.type`. The prefix `S'` is `x1.b.type` (so `C1` can be selected from `S'` with the type projection `x1.b.type#C1` and `C1` is a base class for `S`). Rule 4 applies to the singleton type `A.this.type` with the class `A` extracted from it (so `D = A`). Rule 4.1 is skipped because the class `A` is not a subclass of the class `C1`. Rule 3.2 applies because the class `C1` is nested in the class `B1`. ASF applies itself recursively to the same type `A.this.type` but in the class one level up in the class nesting relationship.
  * ASF's query is `A.this.type` in `B1` as seen from the prefix `S = x1.b.type` (so `S' = x1.type`). By the same reasoning as in the step above, first Rule 4 applies and then Rule 4.2 applies because the class `B1` is nested in the class `A`. ASF applies itself recursively to the same type `A.this.type` but in the class `A`.
  * ASF's query is now `A.this.type` in `A` as seen from the prefix `S = x1.type` (so `S' = ϵ.type`). Rule 4 still applies because the singleton type `A.this.type` matches the definition of the rule (with the class `D = A`). Rule 4.1 applies with the class `A` being its own subclass and `A` found amongst base types of the prefix `S` because the class `AA` is a subclass of `A`. ASF's final answer is `x1.type`.

Similarly to Rule 3.3, Rule 4.3 is not covered by the example above. It's again a fallthrough rule. Rule 4.3 can be triggered by asking ASF for `X.this.type` in `AA` as seen from `x1.type`.

### Type members

We saw that rule 3. in ASF definition is about resolution of type parameters. Where's resolution of type members defined? Let's study this with an example:

```scala
object TypeMemberOverride {
  abstract class B {
    type U
    // when you write `U`, this a shorthand for `B.this.type#U` (see Scala spec 3.2.3)
    val u: U
  }
  abstract class BB extends B {
    type U = X
  }
  val x1: BB = null
  val x2: X = x1.u
}
```

In order to typecheck the `val x2: X = x1.u` we have to understand the type of `x1.u`. We ignore the object `TypeMemberOverride` to shorten the considered paths so we're looking at `x1.u` instead of `TypeMemberOverride.x1.u`, etc.

  * We're asking about B.this.type#U in B as seen from the prefix S = x1.type, the S' = ϵ.type so B = ϵ.type#B and B is a base type for S.
  * The B.this.type#U is a selection of a type member U from a type B.this.type. By 5. we select U from B.this.type in B as seen from the prefix S = x1.type (the ASF is applied to the `B.this.type`).
  * We're asking now for B.this.type in B as seem from the prefix S = x1.type, the S' = ϵ.type. We apply 4.1 with D = B, x1.type has D as one of its base types, so the answer is x1.type
  * We're now at x6.type#U, and we select BB#U because BB is a base type of x6.type and BB#U subsumes B#U (see SLS 5.1.4). We get X as the final answer.