a path dependent type does not conform to its projection type

[ftucky]

Compiler version

3.2.2 , 3.3.0-RC3

Minimized code

class HiddenInner[+O<:Outer](val outer:O){
}

class Outer{
  type Inner = HiddenInner[this.type]
}

val o : Outer       = new Outer 
val a : o.Inner     = new o.Inner(o)
val b : Outer#Inner = a // DOES NOT COMPILE

Output

Found:    (a : o.Inner)
Required: Outer#Inner

Expectation

Code should compile: o.Inner conforms to Outer#Inner.
Note Outer is a class, so Outer#Inner is legal (sound) in scala3.

Compiles in scala 2.13.

Intention

The intention is to make Inner behave almost as inner class of Outer.

[smarter]

This can be minimized to:

class Outer {
  type This = this.type
  val x: Outer#This = this // error
}

What's happening here is that type This = this.type is equivalent to type This >: this.type <: this.type, and when seen from outside the class scope, this type is approximated to the abstract type type This >: Nothing <: Outer which we conservatively assume has no subtypes but Nothing.

There is a discussion up at lampepfl/dotty-feature-requests#14 about relaxing the subtype checking for type projections which would fix this. The relaxed rule has been proved sound, but it still needs a SIP and some careful consideration of possible interactions with other features.

[smarter]

Note that we don't need the full power of lampepfl/dotty-feature-requests#14 for the original example in this issue, but the more limited rule mentioned in lampepfl/dotty-feature-requests#14 (comment):

Γ ⊨ p : T
------------------------ (Sel-<:-Proj)
Γ ⊨ p.A <: T#A

which should be even less controversial.