[SOLVED] Are type-projection still unsound in scala3?

Are type-projection still unsound in scala3?

Scala3 has dropped general type projection because it was unsound:
It was possible to compile code which was failing at runtime.

(question edited to reflect comments)

Consider the following scala3 code : scastie

class A:
    class X:
        def outer : A.this.type = A.this
    

class B extends A
class C extends A

val b0 = new B
val b1 = b0
val b2 = new B

val c0 = new C
val c1 = c0
val c2 = new C

val b0x : A#X = new b0.X

val pathTypeMatch = b0x match
    case _ : c2.X => "c2.X"
    case _ : c1.X => "c1.x"
    case _ : c0.X => "c0.X"
    case _ : b2.X => "b2.X"
    case _ : b1.X => "b1.X"
    case _ : b0.X => "b0.X"
    case _        => "ELSE"

pathTypeMatch // "b1.x" 

val projectionTypeMatch = b0x match
    case _ : C#X => "C#X"
    case _ : B#X => "B#X"
    case _ : A#X => "A#X"
    case _       => "ELSE"

projectionTypeMatch // "C#X" !!!

val failingTypeMatch = b0x match
    case cx : C#X =>
        val c : C = cx.outer // Fails at runtime

Code compiles, but fails at runtime with "class B cannot be cast to class C".

The compiler considers C#X and B#X erasures to be A#X, so that case cx:C#X branch matches. From there, it is legitimate to consider cx.outer to be a C (which is wrong), hence the exception.

No warning is issued. No TypeTest is involved.

When looking into the bytecode of projectionTypeMatch, the test of all 3 branches is strictly identical.

In type-patterns:

(A type-pattern T is ...) a reference to a class C, p.C, or T#C. This type pattern matches any non-null instance of the given class. Note that the prefix of the class, if it exists, is relevant for determining class instances.

Indeed, when the match is done against path-dependent types, the behavior is the expected one (pathTypeMatch is b1.x). In particular, the compiler had to take X outer into account in the match.

One would expect the match against projection-types to be consistent, isn't it ?

What is the intention ?

It seems the restriction of type projections to concrete types in scala3 would allow a consistent behavior. Is it so ?

Solution

See https://github.com/lampepfl/dotty/issues/16728.

Fixed by https://github.com/lampepfl/dotty/pull/17136

The observed behavior did not reflect intention. scala3 compiler has been fixed: 3.3.1-RC1-bin-20230327-a569057-NIGHTLY behaves as expected.

Note the faulty behavior may be seen as a flavor of general type projection unsoundness, and cannot be fixed in scala2.