Overconstrained GADT bounds in presence of bad bounds #11545
Description
Compiler version
3.0.0-RC1 (Scastie)
Minimized code
@main def test: Unit = { trait S[A] trait Inv[A] class P[X] extends S[Inv[X] & Inv[String]] def patmat[A, Y](s: S[Inv[A] & Y]): A = s match { case p: P[x] => "Hello" } val got: Int = patmat[Int, Inv[String]](new P) // ClassCastException: String cannot be cast to Integer }Output
Click to expand
java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99) at main$package$.test(main.scala:11) 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
The code should be rejected, but it is unclear what part is problematic:
- The instantiation of
new Pdue to introducing the bad boundsS[Inv[Int] & Inv[String]] - The class declaration of P with the
extends S[Inv[X] & Inv[String]]clause, which may lead to bad bounds ifX != String - Deducing that
x = A = String
I think that the problem comes from 1 (and not necessarily from 3). I believe, however, that this is not sufficient, as it seems that bad bounds can still be crafted.
Translating the above into pDOT shows that we can allow 3. if we require a witness value for Inv[A] & Y. Then, the above would not cause a ClassCastException since providing a value for Inv[Int] & Inv[String] is not possible.