Dotty: Type matches are unsound.

[alexknvl]

object G {
    final class X
    final class Y

    opaque type Foo = X & Y
    object Foo {
        def apply[F[_]](fa: F[X & Y]): F[Y & Foo] = fa
    }

    type Bar[A] = A match {
        case X & Y => String
        case Y => Int
    }

    def main(args: Array[String]): Unit = {
        val a: Bar[X & Y] = "hello"
        val i: Bar[Y & Foo] = Foo.apply[Bar](a)
        val b: Int = i
        println(b + 1)
    }
}

Exception in thread "main" java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
    at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:103)
    at G$.main(test.scala:30)
    at G.main(test.scala)

[alexknvl]

In fact, you do not need the new opaque types:

object G {
    final class X
    final class Y

    trait FooSig {
        type Type
        def apply[F[_]](fa: F[X & Y]): F[Y & Type]
    }
    val Foo: FooSig = new FooSig {
        type Type = X & Y
        def apply[F[_]](fa: F[X & Y]): F[Y & Type] = fa
    }
    type Foo = Foo.Type

    type Bar[A] = A match {
        case X & Y => String
        case Y => Int
    }

    def main(args: Array[String]): Unit = {
        val a: Bar[X & Y] = "hello"
        val i: Bar[Y & Foo] = Foo.apply[Bar](a)
        val b: Int = i
        println(b + 1)
    }
}

[alexknvl]

Here is a cleaner example:

object G {
    final class X
    final class Y

    opaque type Foo = Nothing // or X & Y
    object Foo {
        def apply[F[_]](fa: F[X & Foo]): F[Y & Foo] = fa
    }

    type Bar[A] = A match {
        case X => String
        case Y => Int
    }

    val a: Bar[X & Foo] = "hello"
    val b: Bar[Y & Foo] = 1

    def main(args: Array[String]): Unit = {
        val a: Bar[X & Foo] = "hello"
        val i: Bar[Y & Foo] = Foo.apply[Bar](a)
        val b: Int = i
        println(b + 1)
    }
}

EDIT: this example still compiles with the fix in https://github.com/dotty-staging/dotty/commit/74168ac13746ef43cc3f626cf183b9d452bdc4da

[OlivierBlanvillain]

Thanks for the bug reports, it's very helpful!

That's clearly a bug, Bar[Y & Foo] shouldn't reduce to Int in main: Foo should be treated as an abstract type outside of its companion.

[alexknvl]

I don't think it's just intersections,

object G {
    trait Wizzle[L <: Int with Singleton] {
        type Bar[A] = A match {
            case 0 => String
            case L => Int
        }

        def left(fa: String): Bar[0] = fa
        def right(fa: Bar[L]): Int = fa

        def center[F[_]](fa: F[0]): F[L]

        def run: String => Int = left andThen center[Bar] andThen right
    }

    class Wozzle extends Wizzle[0] {
        def center[F[_]](fa: F[0]): F[0] = fa
    }

    def main(args: Array[String]): Unit = {
        val coerce: String => Int = (new Wozzle).run
        println(coerce("hello") + 1)
    }
}

Singletons are suspect too

object G {
    trait Wizzle {
        type X <: Int with Singleton
        type Y <: Int with Singleton

        type Bar[A] = A match {
            case X => String
            case Y => Int
        }

        def left(fa: String): Bar[X] = fa
        def center[F[_]](fa: F[X]): F[Y]
        def right(fa: Bar[Y]): Int = fa

        def run: String => Int = left andThen center[Bar] andThen right
    }

    class Wozzle extends Wizzle {
        type X = 0
        type Y = 0
        def center[F[_]](fa: F[X]): F[Y] = fa
    }

    def main(args: Array[String]): Unit = {
        val coerce: String => Int = (new Wozzle).run
        println(coerce("hello") + 1)
    }
}

[alexknvl]

Conceptually,

• X = Y => F[X] = F[Y] always holds
• Suppose we somehow make F[X] != F[Y] and X = Y, contradiction.
• Since type equalities are potentially non-local (i.e. X and Y might be imported as type parameters), we can never assume that X != Y. In particular, type Bar[X] = X match { case 0 => String; case L => Int} can not assume that L != 0, so Bar[L] can not be reduced to Int in any context where we don't have a proof of L != 0.

All of the examples above attack compiler's over-eagerness to reduce Bar[X] to some type even though it does not have enough information about X to rule out all but one case.

type Foo

type Bar[A] = A match {
   case X => String
   case Y => Int
}

Bar[Y & Foo] should NOT reduce to Int because the first case can not be ruled out, Foo could be equal to X, in which case Bar[Y & Foo] = Bar[Y & X] = String.

type X <: Int with Singleton
type Y <: Int with Singleton

type Bar[A] = A match {
   case X => String
   case Y => Int
}

Bar[Y] should NOT reduce to Int since the first case can not be ruled out, X might be equal to Y, in which case Bar[Y] = Bar[X] = String.

[OlivierBlanvillain]

Makes perfect sense, this is exactly what the implementation is supposed to do: never "reduce past" a case unless there is proof that the two types (the scrutinee type and the pattern type) are non intersecting.

[alexknvl]

After snooping around the code for a bit, I found another example:

object G {
    type Void <: Nothing
    trait Wizzle {
        type Razzle[+X >: Void]
        type X = 0
        type Y = 1

        type Bar[A] = A match {
            case Razzle[X] => String
            case Razzle[Y] => Int
        }

        def left(fa: String): Bar[Razzle[X]] = fa
        def center[F[_]](fa: F[Razzle[X]]): F[Razzle[Y]]
        def right(fa: Bar[Razzle[Y]]): Int = fa

        def run: String => Int = left andThen center[Bar] andThen right
    }

    class Wozzle extends Wizzle {
        type Razzle[+X >: Void] = Int
        def center[F[_]](fa: F[Razzle[X]]): F[Razzle[Y]] = fa
    }

    def main(args: Array[String]): Unit = {
        val coerce: String => Int = (new Wozzle).run
        println(coerce("hello") + 1)
    }
}

This one attacks line https://github.com/dotty-staging/dotty/blob/74168ac13746ef43cc3f626cf183b9d452bdc4da/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1959 and the surrounding case for AppliedTypes.

[alexknvl]

I think the code might be mixing the inhabitance of intersections (∃ x: A & B) and subtyping (A <: B). A <: B does not imply ∃ x: A & B (nor vice-versa in general) and ¬(∃ x: A & B) does not imply ¬(A <: B).

final class A
final class B

type Select[X] = X match {
    case A => Int
    case B => String
}

type Type

val a : Select[A & Type] = 1
val b : Select[B & Type] = "hey"

attacks https://github.com/dotty-staging/dotty/blob/74168ac13746ef43cc3f626cf183b9d452bdc4da/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L1931 - A & (B & Type) is not inhabited, but that doesn't mean that we can "reduce past" the first case, since we are not really interested in inhabitance, but in a subtyping relation. We want to check whether B & Type <: A is possible (which it is), which is not directly related to whether their intersection is inhabited.

EDIT: clarified the first statement

[OlivierBlanvillain]

You nailed it with this last example. I'm now convinced that there is no way to soundly reduce any match types when abstract type are involved.

[alexknvl]

There are some cases where it is possible.

final case class X()
type Y
type Select[X] = X match {
    case List[X] => Int
    case Option[Y] => String
}

final class X
final class Y
type Select[X] = X match {
    case X => Int
    case Y => String
}
type Type <: X

type Foo = Select[X | Type] // can not be a subtype of Y, subtype of X, hence reduces to Int

final class X
final class Y
type Select[X] = X match {
    case X => Int
    case Y => String
}
type Type <: X

type Foo = Select[X & Type] // can not be a subtype of Y, subtype of X, hence reduces to Int

If the compiler could use implicit evidence (probably not any time soon):

final class X
final class Y
type Select[X] = X match {
    case X => Int
    case Y => String
}

type Type
implicit val p: (Type <:< X) => Nothing // a proof that Type is not a subtype of X
type Foo = Select[Y & Type] // safe to reduce to String

But otherwise yes, things get really tricky when you are dealing with abstract types in type matches.