initial work on excluding GADT exhaustivity check

Author: liufengyun

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -708,6 +708,42 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     else text
   }
 
+  /** Whether the counterexample is satisfiable */
+  def satisfiable(sp: Space): Boolean = {
+    def genConstraint(space: Space): List[(Type, Type)] = space match {
+      case Prod(tp, unappTp, unappSym, ss, _) =>
+        val tps = signature(unappTp, unappSym, ss.length)
+        ss.zip(tps).flatMap {
+          case (sp: Prod, _) => genConstraint(sp)
+          case (Typ(tp1, _), tp2) => tp1 -> tp2 :: Nil
+          // case _ => ???  // impossible
+        }
+      case Typ(_, _) => Nil
+      // case _ => ??? // impossible
+    }
+
+    def checkConstraint(constrs: List[(Type, Type)]): Boolean = {
+      implicit val ctx1 = ctx.fresh.setNewTyperState()
+      val tvarMap = collection.mutable.Map.empty[Symbol, TypeVar]
+      val typeParamMap = new TypeMap() {
+        override def apply(tp: Type): Type = tp match {
+          case tref: TypeRef if tref.symbol.is(TypeParam) =>
+            if (tvarMap.contains(tref.symbol)) tvarMap(tref.symbol)
+            else {
+              val tvar = newTypeVar(tref.underlying.bounds)
+              tvarMap(tref.symbol) = tvar
+              tvar
+            }
+          case tp => mapOver(tp)
+        }
+      }
+
+      constrs.foldLeft(true) { case (acc, (tp1, tp2)) => acc && typeParamMap(tp1) <:< typeParamMap(tp2) }
+    }
+
+    checkConstraint(genConstraint(sp))
+  }
+
   /** Display spaces */
   def show(s: Space): String = {
     def params(tp: Type): List[Type] = tp.classSymbol.primaryConstructor.info.firstParamTypes
@@ -775,6 +811,15 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     res
   }
 
+  def checkGADT(tp: Type): Boolean = {
+    new TypeAccumulator[Boolean] {
+      override def apply(b: Boolean, tp: Type): Boolean = tp match {
+        case tref: TypeRef if tref.symbol.is(TypeParam) => true
+        case tp => b || foldOver(b, tp)
+      }
+    }.apply(false, tp)
+  }
+
   def checkExhaustivity(_match: Match): Unit = {
     val Match(sel, cases) = _match
     val selTyp = sel.tpe.widen.dealias
@@ -785,10 +830,15 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       debug.println(s"${x.pat.show} ====> ${show(space)}")
       space
     }).reduce((a, b) => Or(List(a, b)))
-    val uncovered = simplify(minus(Typ(selTyp, true), patternSpace), aggressive = true)
 
-    if (uncovered != Empty)
-      ctx.warning(PatternMatchExhaustivity(show(uncovered)), sel.pos)
+    val checkGADTSAT = checkGADT(selTyp)
+
+    val uncovered =
+      flatten(simplify(minus(Typ(selTyp, true), patternSpace), aggressive = true))
+        .filter(s => s != Empty && (!checkGADTSAT || satisfiable(s)))
+
+    if (uncovered.nonEmpty)
+      ctx.warning(PatternMatchExhaustivity(show(Or(uncovered))), sel.pos)
   }
 
   def checkRedundancy(_match: Match): Unit = {

tests/patmat/3454.scala

@@ -0,0 +1,10 @@
+object O {
+  sealed trait Expr[T]
+  case class BExpr(bool: Boolean) extends Expr[Boolean]
+  case class IExpr(int: Int) extends Expr[Int]
+
+  def join[T](e1: Expr[T], e2: Expr[T]): Expr[T] = (e1, e2) match {
+    case (IExpr(i1), IExpr(i2)) => IExpr(i1 + i2)
+    case (BExpr(b1), BExpr(b2)) => BExpr(b1 & b2)
+  }
+}

tests/patmat/exhausting.check

@@ -3,4 +3,4 @@
 32: Pattern Match Exhaustivity: List(_, _: _*)
 39: Pattern Match Exhaustivity: Bar3
 44: Pattern Match Exhaustivity: (Bar2, Bar2)
-53: Pattern Match Exhaustivity: (Bar2, Bar2), (Bar2, Bar1), (Bar1, Bar3), (Bar1, Bar2)
+50: Pattern Match Exhaustivity: (Bar2, Bar2)

tests/patmat/exhausting.scala

@@ -46,9 +46,6 @@ object Test {
     case (Bar2, Bar3) => ()
     case (Bar3, _) => ()
   }
-  // fails for: (Bar1, Bar2)
-  // fails for: (Bar1, Bar3)
-  // fails for: (Bar2, Bar1)
   // fails for: (Bar2, Bar2)
   def fail5[T](xx: (Foo[T], Foo[T])) = xx match {
     case (Bar1, Bar1) => ()