Implementation of exhaustivity and redundancy check

[liufengyun]

Todos

• rebase with master & fix for HK change
• migrate more tests from scalac

Fix following scalac open issues

1. tests/patmat/t9672.scala - SI-9672
2. tests/patmat/t9630.scala - SI-9630 (fixed in 2.12-M4)
3. tests/patmat/t9573.scala - SI-9573
4. tests/patmat/t9411.scala - SI-9411 (fixed in 2.12-M4)
5. tests/patmat/t9398.scala - SI-9398 (fixed in 2.12-M4)
6. tests/patmat/t9399.scala - SI-9399 (fixed in 2.12-M4)
7. tests/patmat/t9289.scala - SI-9289
8. tests/patmat/t8511.scala - SI-8511
9. tests/patmat/t8178.scala - SI-8178
10. tests/patmat/t8068.scala - SI-8068
11. tests/patmat/t7466.scala - SI-7466
12. tests/patmat/t6450.scala - SI-6450
13. tests/patmat/t9657.scala - SI-9657

Links

• Description of algorithm - link
• Warnings for pattern matching, L. Maranget, 2007

[liufengyun]

Neither scalac nor this algorithm can handle following cases about GADT. Both are exhaustive, but the compiler incorrectly reports non-exhaustive. AFAIK, only Haskell handles that in the latest paper(2015), which depends on the type constraint solver.

Example 1:

sealed trait Expr[+T]
case class IntExpr(x: Int) extends Expr[Int]
case class BooleanExpr(b: Boolean) extends Expr[Boolean]

object Test {
  def foo[T](x: Expr[T], y: Expr[T]) = (x, y) match {
    case (IntExpr(_), IntExpr(_)) =>
    case (BooleanExpr(_), BooleanExpr(_)) =>
  }
}

Example 2:

sealed trait Nat[+T]
case class Zero() extends Nat[Nothing]
case class Succ[T]() extends Nat[T]

sealed trait Vect[+N <: Nat[_], +T]
case class VN[T]() extends Vect[Zero, T]
case class VC[T, N <: Nat[_]](x: T, xs: Vect[N, T]) extends Vect[Succ[N], T]

object Test {
  def foo[N <: Nat[_], A, B](v1: Vect[N, A], v2: Vect[N, B]) = (v1, v2) match {
    case (VN(), VN()) => 1
    case (VC(x, xs), VC(y, ys)) => 2
  }
}

[liufengyun]

/rebuild

[liufengyun]

The two examples above are in fact both non-exhaustive in Dotty, due to the existence of union types. In Scala, they are exhaustive.

[smarter]

Can you give an example of a case that isn't covered in dotty in these examples?

[liufengyun]

For the first case, Tcould be Int | Boolean, then (IntExpr(3), BooleanExpr(false)) will not be matched.

For the second case, let N be Zero | Succ[_], then (VN(), VC(3, VN())) is not matched.

[liufengyun]

Put it another way, union types break the definiteness of type variables -- the same type variable may take arbitrarily different types in different positions. That's the cause of the discrepancy between Scala and Dotty in the two code examples above.

For example, for the generic product type ∀T. (T, T), we would expect the two components of the pair are of the same type. However, with union types we can't assert any thing about the types of the two components of the pair, as T could be instantiated with A | B for any A and B.

Subtyping also breaks definiteness of type variables to some extent, but not so fundamentally as union types. For example, with subtyping we know for all instantiations of the pair ∀T. (T, T), the type of the two components still observe subtyping relationship.

[smarter]

I need to think more about this but:

For the first case, T could be Int | Boolean, then (IntExpr(3), BooleanExpr(false)) will not be matched.

If T is Int | Boolean then Expr[T] is equivalent to Expr[Int | Boolean] but there are no values with this type since Expr is invariant in T, so you're fine.

Combining variance and GADTs is tricky, see http://lampwww.epfl.ch/~hmiller/scala2013/resources/pdfs/paper5.pdf

[liufengyun]

/rebuild

[DarkDimius]

LGTM