gkossakowski · June 19, 2018 18:27 · Jul 27, 2016 · Jul 27, 2016 · Jul 24, 2016 · Jul 24, 2016
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -142,7 +142,7 @@ object TypeMemberOverride {
 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 ask ASF for `B.this.type#U` in `B` as seen from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type` (so `B` can be selected from `S'` with the type projection `ϵ.type#B` and `B` is a base class for `S`). The type projection `B.this.type#U` is a selection of a type member `U` from the singleton type `B.this.type`. Rule 5 applies to the singleton type `B.this.type`.
-  * ASF's query is now `B.this.type` in `B` as seem from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type`. By the same reasoning as explained `this` resolution section, first Rule 4 applies to the singletion type `B.this.type` with the class `D` extracted from it (so `D = B`) and then Rule 4.1 applies so the answer for this ASF's step is the singleton type `x1.type` (the prefix `S`).
+  * ASF's query is now `B.this.type` in `B` as seem from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type`. By the same reasoning as explained `this` resolution section, first Rule 4 applies to the singletion type `B.this.type` with the class `B` extracted from it (so `D = B`) and then Rule 4.1 applies so the answer for this ASF's step is the singleton type `x1.type` (the prefix `S`).
   * ASF completes the application of Rule 5 by returning `x1.type#U` as its final answer.
 
 Now we're done with ASF and we select the member `U` of either the class `BB`, or the class `B` because both classes have instances that are base types of the type `x1.type` (see [SLS 3.4.3](http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#base-types-and-member-definitions) for definition how members of a type are defined). We pick `U` as a member of of the class `BB` because member `U` of the class `BB` subsumes member `U` of the class `B` (see [SLS 5.1.4](http://www.scala-lang.org/files/archive/spec/2.11/05-classes-and-objects.html#overriding). And we get `X` as the final answer by resolving the type alias `U` defined in the class `BB`.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -145,4 +145,6 @@ In order to typecheck the `val x2: X = x1.u` we have to understand the type of `
   * ASF's query is now `B.this.type` in `B` as seem from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type`. By the same reasoning as explained `this` resolution section, first Rule 4 applies to the singletion type `B.this.type` with the class `D` extracted from it (so `D = B`) and then Rule 4.1 applies so the answer for this ASF's step is the singleton type `x1.type` (the prefix `S`).
   * ASF completes the application of Rule 5 by returning `x1.type#U` as its final answer.
 
-Now we're done with ASF and we select the member `U` of either the class `BB`, or the class `B` because both classes have instances that are base types of the type `x1.type` (see SLS 3.4.3 for definition how members of a type are defined). We pick `U` as a member of of the class `BB` because member `U` of the class `BB` subsumes member `U` of the class `B` (see SLS 5.1.4). And we get `X` as the final answer by resolving the type alias `U` defined in the class `BB`.
+Now we're done with ASF and we select the member `U` of either the class `BB`, or the class `B` because both classes have instances that are base types of the type `x1.type` (see [SLS 3.4.3](http://www.scala-lang.org/files/archive/spec/2.11/03-types.html#base-types-and-member-definitions) for definition how members of a type are defined). We pick `U` as a member of of the class `BB` because member `U` of the class `BB` subsumes member `U` of the class `B` (see [SLS 5.1.4](http://www.scala-lang.org/files/archive/spec/2.11/05-classes-and-objects.html#overriding). And we get `X` as the final answer by resolving the type alias `U` defined in the class `BB`.
+
+_Thanks to Nada Amin for raising the bar on my note taking skills and Adriaan Moors for comments._
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -2,7 +2,7 @@
 
 ## Introduction
 
-Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples focused on a specific set of rules (grouped thematically) that helped me gain confidence that I fully understand Scala's core typechecking algorithm.
+Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples together with explanation how specific set of rules (grouped thematically) is applied. These notes helped me gain confidence that I fully understand Scala's core typechecking algorithm.
 
 ## As Seen From
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -1,9 +1,11 @@
 # Scala's "type T in class C as seen from a prefix type S" with examples
 
-### Introduction
+## Introduction
 
 Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples focused on a specific set of rules (grouped thematically) that helped me gain confidence that I fully understand Scala's core typechecking algorithm.
 
+## As Seen From
+
 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.
@@ -118,7 +120,7 @@ In order to typecheck `val x: AA = x2` we need to understand the type of `x2` (w
 
 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
+## 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:
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -1,5 +1,9 @@
 # Scala's "type T in class C as seen from a prefix type S" with examples
 
+### Introduction
+
+Recently, I found myself in need to precisely understand Scala's core typechecking rules. I was particulary interested in understanding rules responsible for typechecking signatures of members defined in classes (and all types derived from them). Scala Language Specification (SLS) contains definition of the rules but lacks any examples. The definition of the rules uses mutual recursion and nested switch-like constructs that make it hard to follow. I've written down examples focused on a specific set of rules (grouped thematically) that helped me gain confidence that I fully understand Scala's core typechecking algorithm.
+
 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.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -1,4 +1,4 @@
-## Scala's "type T in class C as seen from a prefix type S" with examples
+# 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:
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -135,7 +135,8 @@ object TypeMemberOverride {
 
 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 ask ASF for `B.this.type#U` in `B` as seen from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type` (so `B` can be selected from `S'` with the type projection `ϵ.type#B` and `B` is a base class 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.
+  * We ask ASF for `B.this.type#U` in `B` as seen from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type` (so `B` can be selected from `S'` with the type projection `ϵ.type#B` and `B` is a base class for `S`). The type projection `B.this.type#U` is a selection of a type member `U` from the singleton type `B.this.type`. Rule 5 applies to the singleton type `B.this.type`.
+  * ASF's query is now `B.this.type` in `B` as seem from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type`. By the same reasoning as explained `this` resolution section, first Rule 4 applies to the singletion type `B.this.type` with the class `D` extracted from it (so `D = B`) and then Rule 4.1 applies so the answer for this ASF's step is the singleton type `x1.type` (the prefix `S`).
+  * ASF completes the application of Rule 5 by returning `x1.type#U` as its final answer.
+
+Now we're done with ASF and we select the member `U` of either the class `BB`, or the class `B` because both classes have instances that are base types of the type `x1.type` (see SLS 3.4.3 for definition how members of a type are defined). We pick `U` as a member of of the class `BB` because member `U` of the class `BB` subsumes member `U` of the class `B` (see SLS 5.1.4). And we get `X` as the final answer by resolving the type alias `U` defined in the class `BB`.
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -135,7 +135,7 @@ object TypeMemberOverride {
 
 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.
+  * We ask ASF for `B.this.type#U` in `B` as seen from the prefix `S = x1.type`. The prefix `S'` is `ϵ.type` (so `B` can be selected from `S'` with the type projection `ϵ.type#B` and `B` is a base class 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.
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -106,7 +106,7 @@ object Rule4 {
 }
 ```
 
-In order to typecheck `val x: AA = x2` we need to understand the type of `x2`.
+In order to typecheck `val x: AA = x2` we need to understand the type of `x2` (we'll be looking at the type of the term `a`).
 
   * 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`.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -83,7 +83,7 @@ In the example above, we only excercised rules 3.1 and 3.2 but not 3.3. The Rule
 
 ### Rule 4: `this` resolution
 
-The fourth rule is about resolution `this`. Let's see it in action based on this example:
+The fourth rule is about resolving `this`. Let's see it in action based on this example:
 
 ```scala
 object Rule4 {

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -79,7 +79,7 @@ In order to typecheck `val x: X = x2` we need to understand the type of `x2` (we
   * 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.
+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 a 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
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -73,7 +73,7 @@ object Rule3 {
 }
 ```
 
-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`).
+In order to typecheck `val x: X = x2` we need to understand the type of `x2` (we'll be looking 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`.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -73,7 +73,7 @@ object Rule3 {
 }
 ```
 
-In order to typecheck `val x: X = x2` we need to understand the type of `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`.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -42,7 +42,7 @@ To typecheck `val x: X = a.t` we need to understand the type of `a.t`.
   * 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 contains the definition of SRs.
+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`.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -36,7 +36,7 @@ object Rule2 {
 }
 ```
 
-To typecheck `val x: X = a.t` we need to understand the type of `a.x`.
+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.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -16,7 +16,7 @@ Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier r
 >     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".
+> 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.
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -51,7 +51,6 @@ We can simplify the returned existential type by applying Simplification Rules (
 
 The third rule is about resolution of a type parameter for a given type argument.
 
-
 ```scala
 object Rule3 {
   abstract class A[T] {
@@ -77,14 +76,14 @@ object Rule3 {
 In order to typecheck `val x: X = x2` we need to understand the type of `x2`.
 
   * 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` i `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 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.
 
-### `this`
+### Rule 4: `this` resolution
 
-The fourth rule is about resolution `this`. Let's use an example again:
+The fourth rule is about resolution `this`. Let's see it in action based on this example:
 
 ```scala
 object Rule4 {
@@ -109,16 +108,11 @@ object Rule4 {
 
 In order to typecheck `val x: AA = x2` we need to understand the type of `x2`.
 
-  * We're asking about the type A.this.type in C1 as seen from the prefix S = x1.b.c.type,
-    the is S' = x1.b.type (so C1 = x1.b.type#C1 and C1 is a base class for S).
-    We apply 4. with D = A, and then 4.2 and we get:
-  * We're asking about the type A.this.type in B1 as seen from the prefix S = x1.b.type (S' = x1.type)
-    We apply 4. with D=A, and then 4.2 and we get:
-  * We're asking about the type A.this.type in A as seen from the prefix S = x1.type (S' = ϵ.type)
-    We apply 4. with D=A, and then 4.1 and we get:
-    x1.type as a final answer
+  * 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 3.3, the 4.3 rule is not covered by the example. It's again a fallthrough rule. It can be triggered by asking about "X.this.type in AA as seen from 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
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -78,7 +78,7 @@ In order to typecheck `val x: X = x2` we need to understand the type of `x2`.
 
   * 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` i `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` and ASF's returns `X` as its final answer.
+  * 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.
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -76,11 +76,11 @@ object Rule3 {
 
 In order to typecheck `val x: X = x2` we need to understand the type of `x2`.
 
-  * We're asking about type A.T in C1 as seen from the prefix S = x1.b.c.type, the is S' = x1.b.type (so C1 = x1.b.type#C1 and C1 is a base class for S). We apply 3. with D = A, and then 3.2 and we get:
-  * Ask for a type A.T in B as seen from S = x1.b.type (S' = x1.type). We apply 3 with D = A, and then 3.2 and we get:
-  * Ask for a type A.T in A as seen from S = x1.type (S' = ϵ.type). We apply 3 with D = A, and then 3.1 because A[X] is a base type of x1.type so we get: X as a final answer.
+  * 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` i `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` and ASF's returns `X` as its final answer.
 
-In the example above, we only excercised rules 3.1 and 3.2 but not 3.3. That rule is a fallthrough rule that is triggered when prefix doesn't encode any interesting information about how to resolve a type parameter. For example, you can ask for "A.T in X as seen from x.type". The definition of ASF ties together class C and the prefix type S but leaves type T to be arbitrary. You can ask ASF for an unrelated type. 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.
+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.
 
 ### `this`
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -38,9 +38,9 @@ object Rule2 {
 
 To typecheck `val x: X = a.t` we need to understand the type of `a.x`.
 
-  * First, 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. We recursively apply ASF to the prefix `A[W]` of the existential type.
-  * We ask ASF for `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.
-  * We complete the application of Rule 2 by substituting prefix `A[W]` with `W` in the existential type and we return `W forSome { type W <: X }` as ASF's final answer.
+  * 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 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 }`.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -38,8 +38,8 @@ object Rule2 {
 
 To typecheck `val x: X = a.t` we need to understand the type of `a.x`.
 
-  * First, we ask 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 -- his is an unfortunate name clash in the spec. We recursively apply ASF to the prefix `A[W]` of the existential type.
-  * We ask for `A.V` in `A` as seen from `A[W]`. Rule 3.1 extracts the type parameter `W` and returns it. Check explanation of Rule 3 for details.
+  * First, 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. We recursively apply ASF to the prefix `A[W]` of the existential type.
+  * We ask ASF for `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.
   * We complete the application of Rule 2 by substituting prefix `A[W]` with `W` in the existential type and we return `W forSome { type W <: X }` as ASF's final answer.
 
 We can simplify the returned existential type by applying Simplification Rules (SRs) specific to existential types. SLS 3.2.10 contains the definition of SRs.

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -20,7 +20,7 @@ Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier r
 
 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.
 
-### Existential types
+### Rule 2: Existential types
 
 Rule 2 is about seeing through existential types. Let's consider an example:
 
@@ -38,15 +38,16 @@ object Rule2 {
 
 To typecheck `val x: X = a.t` we need to understand the type of `a.x`.
 
-  * We're asking about `A.V` in `A` as seen from `a.type`. The `S' = ϵ.type`. The 2. applies with `S' = A[W]`, `Q = { type W <: X }`. Note that second `S'` is not the same as the first one (this is an unfortunate use of names in the spec).
-  * We're asking about `A.V` in `A` as seen from `A[W]`. By 3.1 we get `W` as the answer.
-  * We can complete the application of rule 2. by returning the `W forSome { type W <: X }`.
-  * Let's apply simplification rules (SR) from SLS 3.2.10:
-    - `W forSome { type W <: X }` becomes `X forSome { type W <: X }` (SR4)
-    - `X forSome { type W <: X }` becomes `X forSome { }` (SR2)
-    - `X forSome {}` becomes X (SR3)
+  * First, we ask 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 -- his is an unfortunate name clash in the spec. We recursively apply ASF to the prefix `A[W]` of the existential type.
+  * We ask for `A.V` in `A` as seen from `A[W]`. Rule 3.1 extracts the type parameter `W` and returns it. Check explanation of Rule 3 for details.
+  * We complete the application of Rule 2 by substituting prefix `A[W]` with `W` in the existential type and we return `W forSome { type W <: X }` as ASF's final answer.
 
-### Type parameters
+We can simplify the returned existential type by applying Simplification Rules (SRs) specific to existential types. SLS 3.2.10 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.
 

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -18,11 +18,11 @@ Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier r
 > 
 > 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".
 
-The first rule 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 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.
 
 ### Existential types
 
-The first rule is about seeing through existential types. Let's consider an example:
+Rule 2 is about seeing through existential types. Let's consider an example:
 
 ```scala
 class X
@@ -38,8 +38,8 @@ object Rule2 {
 
 To typecheck `val x: X = a.t` we need to understand the type of `a.x`.
 
-  * We're asking about `A.V` in A as seen from a.type. The `S' = ϵ.type`. The 2. applies with `S' = A[W]`, `Q = { type W <: X }`. Note that second S' is not the same as the first one (this is an unfortunate use of names in the spec).
-  * We're asking about `A.V` in A as seen from `A[W]`. By 3.1 we get W as the answer.
+  * We're asking about `A.V` in `A` as seen from `a.type`. The `S' = ϵ.type`. The 2. applies with `S' = A[W]`, `Q = { type W <: X }`. Note that second `S'` is not the same as the first one (this is an unfortunate use of names in the spec).
+  * We're asking about `A.V` in `A` as seen from `A[W]`. By 3.1 we get `W` as the answer.
   * We can complete the application of rule 2. by returning the `W forSome { type W <: X }`.
   * Let's apply simplification rules (SR) from SLS 3.2.10:
     - `W forSome { type W <: X }` becomes `X forSome { type W <: X }` (SR4)

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -38,7 +38,7 @@ object Rule2 {
 
 To typecheck `val x: X = a.t` we need to understand the type of `a.x`.
 
-  * We're asking about `A.V` in A as seen from a.type. The `S' = ϵ.type`. The 2. applies with `S' = A[W]`, `Q = { type W <: X }`. Note that second S' is not the sample as first one (this is an unfortunate use of names in the spec).
+  * We're asking about `A.V` in A as seen from a.type. The `S' = ϵ.type`. The 2. applies with `S' = A[W]`, `Q = { type W <: X }`. Note that second S' is not the same as the first one (this is an unfortunate use of names in the spec).
   * We're asking about `A.V` in A as seen from `A[W]`. By 3.1 we get W as the answer.
   * We can complete the application of rule 2. by returning the `W forSome { type W <: X }`.
   * Let's apply simplification rules (SR) from SLS 3.2.10:

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -20,16 +20,38 @@ Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier r
 
 The first rule 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.
 
-The illustration of the second rule is a TODO.
+### Existential types
+
+The first rule 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.x`.
+
+  * We're asking about `A.V` in A as seen from a.type. The `S' = ϵ.type`. The 2. applies with `S' = A[W]`, `Q = { type W <: X }`. Note that second S' is not the sample as first one (this is an unfortunate use of names in the spec).
+  * We're asking about `A.V` in A as seen from `A[W]`. By 3.1 we get W as the answer.
+  * We can complete the application of rule 2. by returning the `W forSome { type W <: X }`.
+  * Let's apply simplification rules (SR) from SLS 3.2.10:
+    - `W forSome { type W <: X }` becomes `X forSome { type W <: X }` (SR4)
+    - `X forSome { type W <: X }` becomes `X forSome { }` (SR2)
+    - `X forSome {}` becomes X (SR3)
 
 ### Type parameters
 
 The third rule is about resolution of a type parameter for a given type argument.
 
 
 ```scala
-class X
-
 object Rule3 {
   abstract class A[T] {
     abstract class B {

diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -121,4 +121,4 @@ In order to typecheck the `val x2: X = x1.u` we have to understand the type of `
   * 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 a final answer.
+  * 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.
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -18,7 +18,7 @@ Let's quote the Scala spec for As Seen From (ASF) rules numbered for an easier r
 > 
 > 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".
 
-The first rule is the base case for the recursive definition of ASF. Altough you cannot write `ϵ.type` in Scala program, the ASF might be sent to the first rule by rules that strip the prefix: 2, 3.2 and 4.2.
+The first rule 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.
 
 The illustration of the second rule is a TODO.
 
@@ -112,19 +112,13 @@ object TypeMemberOverride {
     type U = X
   }
   val x1: BB = null
-  val x2: X = x2.u
+  val x2: X = x1.u
 }
 ```
 
-To be rewritten:
+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 = x6.type
-  // the B.this.type#U is a selection of 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 = x6.type
-  // we're asking now for B.this.type in B as seem from the prefix S = x6.type
-  // we apply 4.a with D = B, x6.type has D as one of its base types, so
-  // B.this.type in B as seen from the prefix S = x6.type is x6.type
-  // so we're now at x6.type#U, and we select BB#U because BB is a base type
-  // of x6.type and because BB#U subsumes B#U
-```
+  * 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 a final answer.
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -97,3 +97,34 @@ In order to typecheck `val x: AA = x2` we need to understand the type of `x2`.
 
 Similarly to 3.3, the 4.3 rule is not covered by the example. It's again a fallthrough rule. It can be triggered by asking about "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 = x2.u
+}
+```
+
+To be rewritten:
+
+```
+// we're asking about B.this.type#U in B as seen from the prefix S = x6.type
+  // the B.this.type#U is a selection of 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 = x6.type
+  // we're asking now for B.this.type in B as seem from the prefix S = x6.type
+  // we apply 4.a with D = B, x6.type has D as one of its base types, so
+  // B.this.type in B as seen from the prefix S = x6.type is x6.type
+  // so we're now at x6.type#U, and we select BB#U because BB is a base type
+  // of x6.type and because BB#U subsumes B#U
+```
diff --git a/asSeenFrom.md b/asSeenFrom.md
@@ -22,6 +22,8 @@ The first rule is the base case for the recursive definition of ASF. Altough you
 
 The illustration of the second rule is a TODO.
 
+### Type parameters
+
 The third rule is about resolution of a type parameter for a given type argument.
 
 
@@ -57,6 +59,8 @@ In order to typecheck `val x: X = x2` we need to understand the type of `x2`.
 
 In the example above, we only excercised rules 3.1 and 3.2 but not 3.3. That rule is a fallthrough rule that is triggered when prefix doesn't encode any interesting information about how to resolve a type parameter. For example, you can ask for "A.T in X as seen from x.type". The definition of ASF ties together class C and the prefix type S but leaves type T to be arbitrary. You can ask ASF for an unrelated type. 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.
 
+### `this`
+
 The fourth rule is about resolution `this`. Let's use an example again:
 
 ```scala
@@ -91,4 +95,5 @@ In order to typecheck `val x: AA = x2` we need to understand the type of `x2`.
     We apply 4. with D=A, and then 4.1 and we get:
     x1.type as a final answer
 
-Similarly to 3.3, the 4.3 rule is not covered by the example. It's again a fallthrough rule. It can be triggered by asking about "X.this.type in AA as seen from x1.type".
+Similarly to 3.3, the 4.3 rule is not covered by the example. It's again a fallthrough rule. It can be triggered by asking about "X.this.type in AA as seen from x1.type".
+