Skip to content

Unsound pattern matching when using lower bounds and union types #23364

@Alex1005a

Description

@Alex1005a
Contributor

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.

Activity

Alex1005a

Alex1005a commented on Jun 13, 2025

@Alex1005a
ContributorAuthor

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

noti0na1 commented on Jun 16, 2025

@noti0na1
Member

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

added
itype:soundnessSoundness bug (it lets us compile code that crashes at runtime with a ClassCastException)
and removed
stat:needs triageEvery issue needs to have an "area" and "itype" label
on Jun 25, 2025
Linyxus

Linyxus commented on Jul 11, 2025

@Linyxus
Contributor

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 _ =>
            ???
        }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

    Development

    No branches or pull requests

      Participants

      @noti0na1@Linyxus@Gedochao@Alex1005a

      Issue actions

        Unsound pattern matching when using lower bounds and union types · Issue #23364 · scala/scala3