Intended semantics of abstract types and projections vs SLS

[Blaisorblade]

To me (and to @milessabin in #4583 and scala/bug#10916), type projections of abstract types are meant to be, indeed, abstract types between their bounds.
But the SLS says that Derived <: Base implies Derived#A <: Base#A. Hence, if Base#A >: S <: U, I can ensure that Base#A = U by defining a subclass with Derived#A = U to ensure that Base#A >: Derived#A = U. That fails in Scalac but works in Dotty, yet it doesn't have justification in either the intended semantics or in the nuObj paper. On the other hand, if that's meant to actually hold, it should be part of type equality — while right now you can only witness this indirectly.

scala> trait Base { type A }
// defined class Base

scala> class Derived extends Base { type A = Any }
// defined class Derived

scala> def cast(x: Any): A#T = (x: B#T): A#T
def cast(x: Any): A#T

scala> def cast2(x: Any): A#T = x: A#T
1 |def cast2(x: Any): A#T = x: A#T
  |                         ^
  |                         found:    Any(x)
  |                         required: A#T
  |

Relatedly, I've long been concerned that underlying on TypeBounds returns the upper bound, even though one would think that tp.underlying is always meant to be =:= tp.

[Blaisorblade]

But the SLS says

More specifically, Sec. 3.5.2 says:

A type projection T#t conforms to U#t if T conforms to U.

[Blaisorblade]

@milessabin in #4583

I think the switch from conforms to equivalent helps here, otherwise I could imagine doing bad things with (empty) intersections of singletons.

I think that proposes:

A type projection T#t conforms to U#t if T is equivalent to U.

EDIT: #4583 (comment) spells out proposed alternative rules.

[Blaisorblade]

Based on lampepfl/dotty-feature-requests#14 (comment), let me close this issue.