Overriding members having Path Dependent types in

Question

Consider the following simple Scala experiment:

scala> trait A {class C;val c:C}
defined trait A

scala> object O1 extends A {val c=new C}
defined object O1

scala> object O2 extends A {val c=O1.c}
<console>:9: error: overriding value c in trait A of type O2.C;
 value c has incompatible type
       object O2 extends A {val c=O1.c}

According to the Scala Language Specification (SLS 5.1.4):

The type of the value O1.c should conform to the type of A.c because the former overrides the latter.

Question 1:

Where in the SLS it is specified the rule from which it follows that the type of O1.c indeed does conform to the type of A.c?

So why should object O1 extends A {val c=new C} compile according to the SLS ?

Question 2:

Where in the SLS it is specified the rule from which it follows that the type of the value O1.c does not conform to the type of the value O2.c?

In other words, from which SLS rule it follows that object O2 extends A {val c=O1.c} should not compile?

Related : why should the type of the value of O2.cbe O2.C according to the SLS ?

Update:

What is the type of the value O1.c and of the abstract value member A.c according to the SLS ?

Answer 1

The type of A.c is A#C, and O1.c (update: of type O1.C, which per the SLS is O1.type#C) does indeed conform to A#c.

Question 1: inside O1, the type C is O1.C and new C is new O1.C (see the rules for type designators in 3.2.3). O1.C conforms to O1.C because it is equivalent (because equivalence is a congruence).

Question 2: It follows because O1 does not conform to O2, because none of the rules in 3.5.1 or 3.5.2 would make O1 conform to O2. So the rule for type projections in 3.5.2 doesn't apply.

A constructor invocation returns a value of that type, per 5.1.1.

(I really don't think the specification is the best way to learn these things; better to get a practical sense of how things work first).