Unsound GADT infered constraints when mixing invariant and variant type constructors

[mario-bucev]

Compiler version

Scala compiler version 3.0.0-RC2-bin-SNAPSHOT-nonbootstrapped-git-7bef33b -- Copyright 2002-2021, LAMP/EPFL

Minimized code

@main def test: Unit = {
  trait TyCon[+A]
  trait S[T]
  trait P[T] extends S[TyCon[T]] {
    def consume(t: T): Unit
  }

  def patmat(s: S[TyCon[Int]]) = s match {
    case p: P[t] =>
      // "t is a type in method patmat which is an alias of Any"
      // def whatist(x: t): Nothing = x
      p.consume("Hi")
  }

  patmat(new P[Int] {
    override def consume(t: Int): Unit = t + 1 // ClassCastException: class String cannot be cast to class Integer 
  })
}

Output

Click to expand

Exception in thread "main" java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Integer (java.lang.String and java.lang.Integer are in module java.base of loader 'bootstrap')
	at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:99)
	at Test$$anon$1.consume(Test.scala:15)
	at Test$.patmat$1(Test.scala:11)
	at Test$.main(Test.scala:16)
	at Test.main(Test.scala)

Expectation

The code should be rejected (by not concluding that t =:= Any).

By putting some logs, we observe the following run:

• PatternTypeConstrainer#constrainPatternType is given P[t] and S[TyCon[Int]]
• In S, types appearing in variant positions are (recursively) widened, yielding S[TyCon[?]]. P[t] is wrapped in a Skolem type
• The algorithm then calls isSubType with (?1 : P[t]) and S[TyCon[?]]
  • which leads to S[TyCon[t]] <:< S[TyCon[?]]
  • Since S is invariant, we have:
    • TyCon[?] <:< TyCon[t] which records that Any <:< t (from ⊥..⊤ <:< t)
    • and TyCon[t] <:< TyCon[?] (true; nothing inferred)

If I understand it correctly, it seems that, in GADT constraint inferencing mode, it is unwanted to deduce anything from ⊥..⊤ <:< x (and from x <:< ⊥..⊤ too) as ⊥..⊤ is used as a placeholder more than anything else.

[LPTK]

I don't think the issue is with ⊥..⊤, which are just the default bounds for unconstrained types. They would be something else if you had constrained A in TyCon[+A].

Why is S[TyCon[Int]] "widened" to S[TyCon[?]]? That seems wrong to me. S[TyCon[?]] conceptually means S[TyCon[t] forSome { type t }], which is very different from S[TyCon[t]] forSome { type t }. Unlike the latter, the former shares no subtyping relationship with S[TyCon[Int]].

PS: in other words, X is not in variant position in S[TyCon[X]] and can't be replaced by ?.