Matching against a recursive type (RecType) is unsound

[mario-bucev]

Minimized code

@main def test: Unit = {
  class C { type T1; type T2 }

  def pmatch(s: C): s.T2 = s match {
    case p: (C { type T1 = Int; type T2 >: T1  } & s.type) =>
      (3: p.T1): p.T2
    case p: (C { type T1 = String; type T2 >: T1  } & s.type) =>
      ("this branch should be matched": p.T1): p.T2
  }

  // ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String
  val x = pmatch(new C { type T1 = String; type T2 = String })
}

Output

Click to expand

java.lang.ClassCastException: java.lang.Integer cannot be cast to java.lang.String
	at main$package$.test(main.scala:12)
	at test.main(main.scala:1)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at sbt.Run.invokeMain(Run.scala:115)
	at sbt.Run.execute$1(Run.scala:79)
	at sbt.Run.$anonfun$runWithLoader$4(Run.scala:92)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
	at sbt.util.InterfaceUtil$$anon$1.get(InterfaceUtil.scala:10)
	at sbt.TrapExit$App.run(TrapExit.scala:257)
	at java.lang.Thread.run(Thread.java:748)

Expectation

We could expect the second branch to be matched, but due to erasure, I do not think it is possible.

I believe issuing a warning specifying that such a runtime check cannot be performed could be a consideration. I also think that (3: p.T1): p.T2 should be rejected since we cannot be certain that we have { type T1 = Int; type T2 >: T1 } (similarly for the second match branch).

[liufengyun]

The compiler needs to issue unchecked warning & unreachable case here as it is done for non-recursive refinement types.

[mario-bucev]

It seems that something similar happens for type refinement:

trait S[A]
trait P[A] extends S[A]

def pmatch[A](s: S[A]): A = s match {
  case p: P[_ >: Int] =>
    10
}
// ClassCastException: class java.lang.Integer cannot be cast to class java.lang.Boolean
val x = pmatch(new P[Boolean]{})

[liufengyun]

Thanks @mario-bucev , an unchecked warning is indeed missing for the 2nd example as well.

The following code

  class C { type T1; type T2 }

  def pmatch(s: C) = s match {
    case p: (C { type T1 = Int }) =>
    case p: (C { type T1 = String }) =>
  }

gets the expected warning:

-- [E030] Match case Unreachable Warning: examples/patmat.scala:5:7 ------------
5 |  case p: (C { type T1 = String }) =>
  |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |       Unreachable case
-- Warning: examples/patmat.scala:4:7 ------------------------------------------
4 |  case p: (C { type T1 = Int }) =>
  |       ^^^^^^^^^^^^^^^^^^^^^^^^
  |       the type test for C{T1 = Int} cannot be checked at runtime
2 warnings found