Unsound pattern matching when using lower bounds and union types

[Alex1005a]

Compiler version

scala 3.7.1

Minimized code

case class Id1[A](val x: A)
case class Id2[A](val y: A)

type IdAll[A] = Id1[A] | Id2[A]

sealed trait Adt[A]
case class Con1[B >: Id1[A], A](x: A) extends Adt[B]
case class Con2[B >: Id2[A], A](x: A) extends Adt[B]

def test[A, T >: IdAll[A]](expr: Adt[T]): A = {
    expr match
        case Con1(x) => x
        case Con2(x) => x
}

val result = test[Int, IdAll[Int] | Id2[String]](Con2(""))
print(result)

Output

java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer

Expectation

Compiler error, because the lower bound of IdAll[A] does not guarantee that type T will not contain any Id2[B], which results in a bounds conflict.

[Alex1005a]

Not surprisingly, replacing union types with intersection types, and lower bounds with upper bounds, the issue remains.

case class Id1[A](val x: A)
case class Id2[A](val y: A)

type IdAll[A] = Id1[A] & Id2[A]

sealed trait Adt[A]
case class Con1[B <: Id1[A], A](x: A) extends Adt[B]
case class Con2[B <: Id2[A], A](x: A) extends Adt[B]

def test[A, T <: IdAll[A]](expr: Adt[T]): A = {
    expr match
        case Con1(x) => x
        case Con2(x) => x
}

val result = test[Int, IdAll[Int] & Id2[String]](Con2(""))
print(result)

[noti0na1]

I agree. Since we can create Adt[Any] for any Con*, the pattern case should not have any information about x.

I think this is related to GADT. cc @Linyxus

[Linyxus]

This does not seem to be solely a GADT problem; it is related to type inference as well. The typed tree:

    def test[X >: Nothing <: Any, T >: IdAll[X] <: Any](expr: Adt[T]): X =
      expr match
        {
          case Con1.unapply[X, T](x @ _):Con1[X, T] =>
            x:X
          case _ =>
            ???
        }