Overconstrained GADT bounds in presence of bad bounds

[mario-bucev]

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:

1. The instantiation of new P due to introducing the bad bounds S[Inv[Int] & Inv[String]]
2. The class declaration of P with the extends S[Inv[X] & Inv[String]] clause, which may lead to bad bounds if X != String
3. 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.

[LPTK]

The culprit is clearly 3. In Scala/pDOT, you can't escape type members with members that themselves end up having bad bounds (as you say, bad bounds can still be crafted). So we have to live with bad bounds.

In the pattern match, we know Inv[x] & Inv[String] =:= Inv[A] & Y. It is utterly wrong to decompose that constraint into Inv[x] =:= Inv[A] and Inv[String] =:= Y, which is what Dotty seems to be doing. The latter implies the former, so it's okay for approximating type inference, but the former does not imply the latter.

In DOT-like terms, we have Inv[x | String .. x & String] =:= Inv[A] & Y.
So we do have Inv[x | String .. x & String] <: Inv[A] and thus A <: x | String and x & String <: A.
We also have Inv[A] & Y <: Inv[x | String .. x & String], from which we can't deduce anything (think that Y could be bottom).
None of these implies String <: A, which is needed to make the pattern match type check.

[LPTK]

@liufengyun the issue is not truly solved, as you can see in this slight variaton:

class test0 {
  type AA
  trait S[A]
  trait Inv[A]

  class P[X] extends S[Inv[X] & AA]

}

@main def test: Unit =
  new test0:
    type AA = Inv[String]
    
    def patmat[A, Y](s: S[Inv[A] & Y]): A = s match {
      case p: P[x] =>
        "Hello"
    }
    
    val got: Int = patmat[Int, AA](new P) // ClassCastException: String cannot be cast to Integer

Should it be reopened?

I'm aware that @odersky said in #11549 there were still holes to be fixed by the community, but this particular problem is never going to be fixed completely. The theory of DOT shows we can't avoid bad bounds, so we have to be sound in their presence, and GADT reasoning is currently not.

[liufengyun]

@LPTK In the example, it seems to me type inference (GADT reasoning) is doing the right thing:

P[x] <:< S[Inv[A] & Y]
=> S[Inv[x] & String] <: S[Inv[A] & Y]
=> Inv[x] & Inv[String] =:= Inv[A] & Y
=> Inv[A] <:< (Inv[x] & Inv[String])
=> Inv[A] <:< Inv[x] and Inv[A] <:< Inv[String]
=> x =:= A =:= String

If I understand correctly, handling bad bounds in type inference is more convoluted and has performance penalties.

Another possibility is to add the inferred GADT bounds that are valid to the method type parameters (if they are valid in the method scope). This needs to propagate F-bounds outward and do the join. I'm not sure how practical it is.

/cc: @abgruszecki

[LPTK]

@liufengyun

...
=> Inv[x] & Inv[String] =:= Inv[A] & Y
=> Inv[A] <:< (Inv[x] & Inv[String])
...

How do you justify that step? Similar to what I've said above, Inv[A] & Y <: Inv[x] & Inv[String] does not imply Inv[A] <: Inv[x] & Inv[String]. You can't just remove an intersected term on the left.

This is not about handling bad bounds in type inference, this is about the soundness of type checking GADTs. I wonder why you think the compiler is doing the right thing, despite the fact that executing the program leads to a ClassCastException 🙂

[liufengyun]

How do you justify that step? Similar to what I've said above, Inv[A] & Y <: Inv[x] & Inv[String] does not imply Inv[A] <: Inv[x] & Inv[String]. You can't just remove an intersected term on the left.

Indeed it does not hold generally. I read your previous comment but mistakenly thought there's a way out that only resorts to subtyping.

Nevertheless, given that Inv is invariant, the step seems to be the only possibility to make =:= hold, thus a valid reasoning step for this particular case.

[LPTK]

given that Inv is invariant, the step seems to be the only possibility to make =:= hold

That's not true. Again, referring to my message above, taking Y = Nothing is enough to make Inv[A] & Y <: Inv[x] & Inv[String] hold. If you want to justify a subtyping relationship, you have to make it according to the rules of the type system!

PS: To specifically answer your argument about =:= (and not just <:<) – there is no rule AFAIK to say that Inv[x] & Inv[String] =:= Inv[A] & Nothing does not hold. In fact, if x and String happen to be different, then Inv[x] & Inv[String] is indeed functionally equivalent to Nothing.

[liufengyun]

there is no rule AFAIK to say that Inv[x] & Inv[String] =:= Inv[A] & Nothing does not hold.

If there is no rule says that they hold, they don't hold ;-)

[LPTK]

You have it backwards. The burden of proof is on you to show that it cannot possibly hold, otherwise this GADT reasoning is unsound, as we can see from the ClassCastException this program raises.

[abgruszecki]

I'm reopening this. @LPTK correctly observed that we're still unsound. The correct solution seems to be to check whether we're in GADT constraint inference mode before (approximately) branching on &.

[odersky]

The theory of DOT shows we can't avoid bad bounds, so we have to be sound in their presence, and GADT reasoning is currently not.

That's not quite true. DOT says that good bounds are only guaranteed for members of values. It puts the burden of guaranteeing good bounds on when we construct values. So that's what goes wrong here. Type parameters of classes are treated like member types. Non-variant type parameters are treated like type aliases and we need to have guarantee good bounds for them.

Meanwhile #11995 shows that my fix caused important code out there to fail. So that does not seem to work either.

It looks like an important and urgent problem and it would be good if the people discussing here could invest themselves. How can we let real world code compile and still ensure soundness? If you have some time any contribution to this issue and #11995 would be much appreciated.