Unsoundness in GADT pattern matching (falsely assumed injectivity)

[TomasMikula]

Compiler version

3.0.1-RC2

Minimized code

class Functions[*[_, _]] {

  sealed trait Fun[A, B] {
    def ev: A =:= B
  }

  case class Id[X]() extends Fun[X, X] {
    override def ev: X =:= X =
      implicitly[X =:= X]
  }

  case class Par[A1, A2, B1, B2](
    f1: Fun[A1, B1],
    f2: Fun[A2, B2],
  ) extends Fun[A1 * A2, B1 * B2] {
    override def ev: (A1 * A2) =:= (B1 * B2) =
      f2.ev.substituteCo[[x] =>> (A1 * A2) =:= (B1 * x)](
        f1.ev.substituteCo[[x] =>> (A1 * A2) =:= (x * A2)](
          implicitly[(A1 * A2) =:= (A1 * A2)]
        )
      )
  }

  def prove[A1, A2, B1, B2](
    f: Fun[A1 * A2, B1 * B2]
  ): Option[(A1 =:= B1, A2 =:= B2)] =
    f match {
      case Par(f1, f2) => Some((f1.ev, f2.ev)) // falsely assumed injectivity of *[_, _]
      case Id()        => None
    }
}

def main(args: Array[String]): Unit = {
  type *[A, B] = Unit

  val functions = new Functions[*]
  import functions._

  val f: Fun[String * Int, Long * Char] =
    Par(Id[String](), Id[Int]())

  prove[String, Int, Long, Char](f) map {
    case (string_eq_long, _) => string_eq_long("crash")
  }
}

Output

java.lang.ClassCastException: class java.lang.String cannot be cast to class java.lang.Long (java.lang.String and java.lang.Long are in module java.base of loader 'bootstrap')
  at scala.runtime.BoxesRunTime.unboxToLong(BoxesRunTime.java:103)
  at repl$.rs$line$1$.main$$anonfun$1(rs$line$1:43)
  at scala.Option.map(Option.scala:242)
  at repl$.rs$line$1$.main(rs$line$1:44)
  ... 28 elided

Expectation

Soundness problem is on the commented line in the source. Strictly speaking, it should not compile. However, I expect most type constructors to be injective and it is useful to be able to use that fact in pattern matching. So I would like this to be fixed (by rejecting the program at compile time) only after there is a way to tell the compiler that an abstract type constructor is injective.

[LPTK]

Like in #11545, probably another pitfall of mixing type inference (for which it's fine to assume injectivity when there is nothing better to do) with GADT reasoning (for which it's unsound). Cc @abgruszecki

[dwijnand]

You mentioned the soundness problem on the commented line, but I'm confused before that - how does this typecheck?

val f: Fun[String * Int, String * Int] = Par(Id[String](), Id[Int]())
val g: Fun[String * Int, Long * Char]  = f

Is it because * is dealiasing to Unit?

[joroKr21]

The wrong assumption is that:

f: Fun[A1 * A2, B1 * B2]
f: Par[?A, ?B, ?C, ?D] <:< Fun[?A * ?B, ?C * ?D]
// implies (true, Fun is a trait => injective)
(?A * ?B) =:= (A1 * A2)
(?C * ?D) =:= (B1 * B2)
// implies (wrong, * is abstract => injectivity unknown)
?A =:= A1
?B =:= A2
?C =:= B1
?D =:= B2

[TomasMikula]

You mentioned the soundness problem on the commented line, but I'm confused before that - how does this typecheck?

val f: Fun[String * Int, String * Int] = Par(Id[String](), Id[Int]())
val g: Fun[String * Int, Long * Char]  = f

Is it because * is dealiasing to Unit?

Yup, both Fun[String * Int, String * Int] and Fun[String * Int, Long * Char] reduce to F[Unit, Unit].

[smarter]

In Scala >= 3.0.2 we at least get a warning (although a confusing one):

-- [E029] Pattern Match Exhaustivity Warning: try/i13080.scala:27:4 ------------
27 |    f match {
   |    ^
   |match may not be exhaustive.
   |
   |It would fail on pattern case: Functions[?].Id(), Functions[?].Par(_, _)