Unexpected "java.lang.ClassCastException: Cannot cast to scala.Nothing"

[satorg]

Compiler version

3.2.1 (as well as 3.1.0, 3.0.0, etc)

Minimized code

Scala3MatchCrash.scala

sealed trait Foo[A] {

  def last: Option[A] = this match {
    case _: FooEmpty.type => None
    case FooNode(_: FooEmpty.type, bar) => Some(bar)
    case FooNode(foo, _) => foo.last
  }
}

final case class FooNode[A](foo: Foo[A], bar: A) extends Foo[A]

case object FooEmpty extends Foo[Nothing]

object Scala3MatchCrash extends App {

  val foo0 = FooEmpty.asInstanceOf[Foo[Int]]
  val foo1 = FooNode(foo0, 1)

  println(foo1.last)
}

Output

Exception in thread "main" java.lang.ExceptionInInitializerError
    at Scala3MatchCrash.main(Scala3MatchCrash.scala)
Caused by: java.lang.ClassCastException: Cannot cast to scala.Nothing
    at Foo.last(Scala3MatchCrash.scala:5)
    at Foo.last$(Scala3MatchCrash.scala:1)
    at FooNode.last(Scala3MatchCrash.scala:10)
    at Scala3MatchCrash$.<clinit>(Scala3MatchCrash.scala:19)
    ... 1 more

Expectation

Some(1)

Additional Info

This code snippet compiles and works as expected on previous Scala versions: 2.13.10, 2.13.0, 2.12.17, etc.

[WojciechMazur]

Seems to be problem with type inference, 2nd case after typer phase would be translated to:

          case FooNode.unapply[A](FooEmpty, bar @ _):FooNode[A] => 
            Some.apply[Nothing](bar.$asInstanceOf[(bar : A) & Nothing])

A quick workaround:

sealed trait Foo[A] {
  def last: Option[A] = this match {
    case FooEmpty => None
    case FooNode(FooEmpty, bar) =>   Some[A](bar)  // use explicit type A to mitigate this bug
    case FooNode(foo, _) =>  foo.last
  }
}

[odersky]

I believe it's the refined GADT reasoning in Scala 3 which causes this. The second match case can apply only if the first argument is FooEmpty which is of type Foo[Nothing]. Since Foo is invariant we can conclude that A must be Nothing. So it's impossible to create a Some[A] and that's what's manifested in the cast failure.

/cc @Linyxus @abgruszecki to confirm.

[Linyxus]

It seems that GADT is doing the correct thing here: the only possibility when FooEmpty.type (Foo[Nothing]) and Foo[A] match is when A =:= Nothing due to the invariance. The unsoundness comes from the cast FooEmpty.asInstanceOf[Foo[Int]]. This violates the soundness of the system already.

sealed trait Foo[+A] {

  def last: Option[A] = this match {
    case _: FooEmpty.type => None
    case FooNode(_: FooEmpty.type, bar) => Some(bar)
    case FooNode(foo, _) => foo.last
  }
}

final case class FooNode[A](foo: Foo[A], bar: A) extends Foo[A]

case object FooEmpty extends Foo[Nothing]

object Scala3MatchCrash extends App {

  val foo0: Foo[Int] = FooEmpty
  val foo1 = FooNode(foo0, 1)

  println(foo1.last)
}

This code will not crash. It makes the type argument A covariant so that FooEmpty can be typed as Foo[X] for any X.

[sjrd]

I agree. The original code is not correct, since it performs an invalid cast. Once you do an invalid cast, all bets are off. The rest of the compiler may or may not cause a CCE at that point or at a later point.

[satorg]

I see, thank you all for looking into it and the detailed explanation.

I'm still wondering though how come the first case does not cause CCE, what is the difference between the first and the second one from the prospective of GADT?

    case _: FooEmpty.type => None // does not cause any CCE
    case FooNode(_: FooEmpty.type, bar) => Some(bar)

because if I change the println line to this one:

println(foo0.last)

then it simply prints None and no CCE gets raised.

Just FYI: the snippet above is actually an excerpt from Diet which I'm currently trying to massage up a little bit.

[Linyxus]

CCE in the second case happens because of the cast we insert for it, the typed tree looks like:

case _:FooEmpty.type =>
  None
case FooNode.unapply[A](_:FooEmpty.type, bar @ _):FooNode[A] =>
  Some.apply[Nothing](bar.$asInstanceOf[(bar : A) & Nothing])

In the second case, we have to use the GADT constraint A =:= Nothing to make the clause well-typed, so we insert the cast bar.$asInstanceOf[bar.type & Nothing]. The cast should be safe as long as the constraint A =:= Nothing is sound, which is not the case here.

For the first case, no casts are inserted because no GADT constraint is used to type None as Option[A].