Unsoundness due to GADT bounds being inferred too optimistically

[abgruszecki]

object Test {
  enum Base {
    case Case1
    case Case2
  }

  enum Invariant[T] {
    case Inv(t: T)
  }

  def unsound[T](t: T): T = Inv(t) match {
    case Inv(_: Base) =>
      // here we still shouldn't know anything about T
      Case1 // but instead, we have a bound T === Base, which is bogus 
  }

  val notCase2: Case2.type = unsound(Case2) // == Case1
}

There are probably many variations on the above - for example, T could be used in another function argument as well.

The issue appears to be caused by Dotty inferring GADT bounds based on pattern types - it decides that:

• T in Invariant[T] is GADT-valid
• type of Inv(_: Base) pattern is Invariant[Base]
  and then based on an Invariant[T] <: Inv[Base] check it infers that T === Base.

A possible fix might be to assign better types to patterns - Inv(_: Base) can match values of Inv[T] type, not Inv[Base].

Another avenue might be noticing that from the pattern matching we should know only that:

• $scrutinee.type <: Inv[T]
• $scrutinee.t.type <: Base

[Blaisorblade]

$scrutinee.t.type <: Int

Whence Int? Typo for what?

[abgruszecki]

Right, it was supposed to be Base. For clarity, there are two nested patterns - Inv(_), and _: Base - one matches on $scrutinee and the other on $scrutinee.t.