Unsoundness in GADT casting when using a variant type constructor

[rmgk]

Compiler version

Seems to affect at least 3.1.2, 3.0.2, 2.13.8, and 2.12.15

Minimized code

convenient scastie: https://scastie.scala-lang.org/w1GEk4z8TxO9oF9lGgHzoQ

object PatternMatchRecursiveTypes {

  sealed trait Tree[+T]
  case class Node[+T](innerTree: List[Tree[List[T]]]) extends Tree[List[T]]
  case class Leaf[+T](v: T) extends Tree[T]

  def recurse[Ti](tree: Tree[Ti]): Ti= {
    val res: Ti = tree match {
      case Node(innerTree) =>
        // you know, never can have enough lists
        val yolo: List[List[List[Ti]]] = List(List(List(innerTree.map(recurse))))
        // Now, we somehow have convinced the compiler that `Ti = List[Ti]` so we can remove arbitrary many layers of List and everything still compiles
        val yolo2: Ti = yolo
        val yolo3: List[Ti] = yolo
        yolo
      case Leaf(v) => v: Ti
    }
    res
  }

  def main(args: Array[String]): Unit = {
    println(recurse(Leaf(1)))
    // res4: Int = 1

    val res6: List[Int] = recurse(Node(List(Leaf(List(1)))))
    println(res6)
    // res6: List[Int] = List(List(List(List(List(1)))))
    // ^ !!!! wait … thats not a list of int …
    val res7: Int = res6.head
    // java.lang.ClassCastException: scala.collection.immutable.$colon$colon cannot be cast to java.lang.Integer
  }
}

Output

java.lang.ClassCastException: scala.collection.immutable.$colon$colon cannot be cast to java.lang.Integer

Expectation

expected a compiler erorr List[Ti] is not Ti.

[Kordyjan]

Further minimization:

sealed trait Tree[+T]
case class Node[+T](innerTree: List[Tree[List[T]]]) extends Tree[List[T]]
case class Leaf[+T](v: T) extends Tree[T]

def recurse[Ti](tree: Tree[Ti]): Ti = tree match
  case Node(innerTree) => 
    List(List(List(innerTree.map(recurse)))) // We should have got compilation error here...
  case Leaf(v) => v

@main def run: Unit =
  val res6: List[Int] = recurse(Node(List(Leaf(List(1)))))
  val res7: Int = res6.head                 // ... instead of runtime error here

[ValeriePe]

This issue was picked for the Issue Spree number 16 of May 24th which takes place in a week from now. @dwijnand @griggt
will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.

[ValeriePe]

This issue was picked for the Issue Spree number 17 of June 14th which takes place in a week from now. @dwijnand @gagandeepkalra will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.

[dwijnand]

Further minimised:

sealed trait Tree[+A]
final case class Node[+B](x: Tuple1[B]) extends Tree[Tuple1[B]]

def meth[X](tree: Tree[X]): X = tree match
  case Node(x) =>
    Tuple1("boom") // error

object Test:
  def main(args: Array[String]): Unit = assert(meth(Node(Tuple1(42)))._1 == 42)