Unsoundness due to GADT bounds ignoring type (un)injectivity

[abgruszecki]

Current treatment of type constructors by constraint inference is blatantly unsound, as we simply ignore the problem of constructor injectivity. As an example, following test causes a runtime exception:

object Test {
  sealed trait EQ[A, B]
  final case class Refl[T]() extends EQ[T, T]

  def absurd[F[_], X, Y](eq: EQ[F[X], F[Y]], x: X): Y = eq match {
    case Refl() => x
  }

  var ex: Exception = _
  try {
    type Unsoundness[X] = Int
    val s: String = absurd[Unsoundness, Int, String](Refl(), 0)
  } catch {
    case e: ClassCastException => ex = e
  }

  def main(args: Array[String]) =
    assert(ex != null)
}

(https://github.com/dotty-staging/dotty/blob/d1fa5d73c4194448e1ab0d4d4e39a764b6e1f651/tests/run/gadt-injectivity-unsoundness.scala)

This was intentionally extracted out of #5611.

[Blaisorblade]

https://www.microsoft.com/en-us/research/uploads/prod/2019/03/ho-haskell-5c8bb4918a4de.pdf is relevant.

From Sec. 3's intro:

[...] we distinguish the arrow of type constructors (matchable) from that of type families (unmatchable) and use two different symbols: (→), i.e. Haskell’s existing function arrow for the former, and (↠) for the latter. […] matchability corresponds to functions that are both generative and injective.

Works: ∀ (f :: ⋆ → ⋆). (f a ∼ f b) ⇒ a ~ b, because f must be an actual data type (like a class).
Fails: ∀ (f :: ⋆ ↠ ⋆). (f a ∼ f b) ⇒ a ~ b, because f might be any constant function, even a constant one, like Unsoundness above.

[abgruszecki]

Was fixed in #6398.