Unsound GADT constraints with pattern alternatives

[lrytz]

Originally reported by @szeiger at scala/bug#13090

scala> sealed trait A[T] { def x: T }
     | final case class B(x: String) extends A[String]
     | final case class C(x: Int) extends A[Int]

scala> def f[T](a: A[T]): T = a match { case B(_) | C(_) => "plop" }

scala> f(C(1)) + 1
java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer (java.lang.String and java.lang.Integer are in module java.base of loader 'bootstrap')
  at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99)

It seems only the constraints from the first pattern are applied, so T = String when typing the case body.

The bug report initially asked if it's possible to support this case:

scala> def f[T](a: A[T]): T = a match {
     |   case B(_) | C(_) => a match { case C(_) => 42 }
     | }
-- [E007] Type Mismatch Error: -------------------------------------------------
2 |  case B(_) | C(_) => a match { case C(_) => 42 }
  |                                             ^^
  |             Found:    (42 : Int)
  |             Required: T
  |
  |             where:    T is a type in method f which is an alias of String

[szeiger]

@lrytz Are you saying that the original example is unsound and should not compile?

Note that the problematic part under the outer match is completely independent from said match. This was not the case in the original problem that I was debugging and I assumed that this was the reason why it failed, but that was not the case. The definition val v2: T = a match { case C(x) => 42 } only refers to the top-level symbols a, x and T which have not been shadowed or re-bound by the match (e.g. case a @ (B(_) | C(_)) =>), and Scala does not have flow-typing, either. Why would v2 be different than the identical definition of v?

sealed trait A[T] { def x: T }
final case class B(x: String) extends A[String]
final case class C(x: Int) extends A[Int]

def f[T](a: A[T]): Unit = {
  def v: T = a match { case C(x) => 42 }
  a match {
    case B(_) | C(_) =>
      val v1: T = v
      val v2: T = a match { case C(x) => 42 }
      ()
  }
}

[Linyxus]

scala> sealed trait A[T] { def x: T }
     | final case class B(x: String) extends A[String]
     | final case class C(x: Int) extends A[Int]

scala> def f[T](a: A[T]): T = a match { case B(_) | C(_) => "plop" }

scala> f(C(1)) + 1
java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer (java.lang.String and java.lang.Integer are in module java.base of loader 'bootstrap')
  at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99)

is unsound and should be prevented, which is what the associated PR does.

But I agree that this code:

sealed trait A[T] { def x: T }
final case class B(x: String) extends A[String]
final case class C(x: Int) extends A[Int]

def f[T](a: A[T]): Unit = {
  def v: T = a match { case C(x) => 42 }
  a match {
    case B(_) | C(_) =>
      val v1: T = v
      val v2: T = a match { case C(x) => 42 }
      ()
  }
}

is sound and could be supported. Not sure about the status in Scala 2 but Scala 3 compiles it with only pattern matching exclusivity warnings.