Fix #12241: Make space computation lazy

bench/profiles/exhaustivity.yml

@@ -35,6 +35,12 @@ charts:
         - key: exhaustivity-mips
           label: bootstrapped
 
+    - name: "exhaustivity i12241"
+      url: https://github.com/lampepfl/dotty/blob/master/tests/patmat/i12241.scala
+      lines:
+        - key: exhaustivity-i12241
+          label: bootstrapped
+
 scripts:
 
     patmatexhaust:
@@ -55,5 +61,8 @@ scripts:
     exhaustivity-mips:
         - measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i7186.scala
 
+    exhaustivity-i12241:
+        - measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i12241.scala
+
 config:
     pr_base_url: "https://github.com/lampepfl/dotty/pull/"

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

@@ -72,7 +72,7 @@ case class Typ(tp: Type, decomposed: Boolean = true) extends Space
 case class Prod(tp: Type, unappTp: TermRef, params: List[Space]) extends Space
 
 /** Union of spaces */
-case class Or(spaces: List[Space]) extends Space
+case class Or(spaces: Seq[Space]) extends Space
 
 /** abstract space logic */
 trait SpaceLogic {
@@ -113,45 +113,37 @@ trait SpaceLogic {
   /** Display space in string format */
   def show(sp: Space): String
 
-  /** Simplify space using the laws, there's no nested union after simplify
-   *
-   *  @param aggressive if true and OR space has less than 5 components, `simplify` will
-   *                    collapse `sp1 | sp2` to `sp1` if `sp2` is a subspace of `sp1`.
-   *
-   *                    This reduces noise in counterexamples.
-   */
-  def simplify(space: Space, aggressive: Boolean = false)(using Context): Space = trace(s"simplify ${show(space)}, aggressive = $aggressive --> ", debug, x => show(x.asInstanceOf[Space]))(space match {
+  /** Simplify space using the laws, there's no nested union after simplify */
+  def simplify(space: Space)(using Context): Space = trace(s"simplify ${show(space)} --> ", debug, x => show(x.asInstanceOf[Space]))(space match {
     case Prod(tp, fun, spaces) =>
       val sp = Prod(tp, fun, spaces.map(simplify(_)))
       if (sp.params.contains(Empty)) Empty
       else if (canDecompose(tp) && decompose(tp).isEmpty) Empty
       else sp
     case Or(spaces) =>
-      val buf = new mutable.ListBuffer[Space]
-      def include(s: Space) = if s != Empty then buf += s
-      for space <- spaces do
-        simplify(space) match
-          case Or(ss) => ss.foreach(include)
-          case s => include(s)
-      val set = buf.toList
-
-      if (set.isEmpty) Empty
-      else if (set.size == 1) set.toList(0)
-      else if (aggressive && spaces.size < 5) {
-        val res = set.map(sp => (sp, set.filter(_ ne sp))).find {
-          case (sp, sps) =>
-            isSubspace(sp, Or(sps))
-        }
-        if (res.isEmpty) Or(set)
-        else simplify(Or(res.get._2), aggressive)
-      }
-      else Or(set)
+      val spaces2 = spaces.map(simplify(_)).filter(_ != Empty)
+      if spaces2.isEmpty then Empty
+      else Or(spaces2)
     case Typ(tp, _) =>
       if (canDecompose(tp) && decompose(tp).isEmpty) Empty
       else space
     case _ => space
   })
 
+  /** Remove a space if it's a subspace of remaining spaces
+   *
+   *  Note: `dedup` will return the same result if the sequence >= 10
+   */
+  def dedup(spaces: Seq[Space])(using Context): Seq[Space] =
+    if (spaces.lengthCompare(1) <= 0 || spaces.lengthCompare(10) >= 0) spaces
+    else {
+      val res = spaces.map(sp => (sp, spaces.filter(_ ne sp))).find {
+        case (sp, sps) => isSubspace(sp, Or(LazyList(sps: _*)))
+      }
+      if (res.isEmpty) spaces
+      else res.get._2
+    }
+
   /** Flatten space to get rid of `Or` for pretty print */
   def flatten(space: Space)(using Context): Seq[Space] = space match {
     case Prod(tp, fun, spaces) =>
@@ -205,8 +197,8 @@ trait SpaceLogic {
 
     (a, b) match {
       case (Empty, _) | (_, Empty) => Empty
-      case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filterConserve(_ ne Empty))
-      case (Or(ss), _) => Or(ss.map(intersect(_, b)).filterConserve(_ ne Empty))
+      case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filter(_ ne Empty))
+      case (Or(ss), _) => Or(ss.map(intersect(_, b)).filter(_ ne Empty))
       case (Typ(tp1, _), Typ(tp2, _)) =>
         if (isSubType(tp1, tp2)) a
         else if (isSubType(tp2, tp1)) b
@@ -263,8 +255,6 @@ trait SpaceLogic {
            Empty
         else if (canDecompose(tp2))
           tryDecompose2(tp2)
-        else if (isSubType(tp2, tp1) &&covers(fun, tp2))
-          minus(a, Prod(tp1, fun, signature(fun, tp1, ss.length).map(Typ(_, false))))
         else
           a
       case (Prod(tp1, fun1, ss1), Prod(tp2, fun2, ss2)) =>
@@ -282,7 +272,7 @@ trait SpaceLogic {
         else if cache.forall(sub => isSubspace(sub, Empty)) then Empty
         else
           // `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
-          Or(range.map { i => Prod(tp1, fun1, ss1.updated(i, sub(i))) })
+          Or(LazyList(range: _*).map { i => Prod(tp1, fun1, ss1.updated(i, sub(i))) })
     }
   }
 }
@@ -601,7 +591,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
     tp.dealias match {
       case AndType(tp1, tp2) =>
         intersect(Typ(tp1, false), Typ(tp2, false)) match {
-          case Or(spaces) => spaces
+          case Or(spaces) => spaces.toList
           case Empty => Nil
           case space => List(space)
         }
@@ -842,14 +832,15 @@ class SpaceEngine(using Context) extends SpaceLogic {
     val checkGADTSAT = shouldCheckExamples(selTyp)
 
     val uncovered =
-      flatten(simplify(minus(project(selTyp), patternSpace), aggressive = true)).filter { s =>
+      flatten(simplify(minus(project(selTyp), patternSpace))).filter({ s =>
         s != Empty && (!checkGADTSAT || satisfiable(s))
-      }
+      })
 
 
     if uncovered.nonEmpty then
       val hasMore = uncovered.lengthCompare(6) > 0
-      report.warning(PatternMatchExhaustivity(show(uncovered.take(6)), hasMore), sel.srcPos)
+      val deduped = dedup(uncovered.take(6))
+      report.warning(PatternMatchExhaustivity(show(deduped), hasMore), sel.srcPos)
   }
 
   private def redundancyCheckable(sel: Tree): Boolean =
@@ -908,11 +899,13 @@ class SpaceEngine(using Context) extends SpaceLogic {
         // If explicit nulls are enabled, this check isn't needed because most of the cases
         // that would trigger it would also trigger unreachability warnings.
         if (!ctx.explicitNulls && i == cases.length - 1 && !isNullLit(pat) ) {
-          simplify(minus(covered, prevs)) match {
-            case Typ(`constantNullType`, _) =>
+          val spaces = flatten(simplify(minus(covered, prevs)))
+          if spaces.lengthCompare(10) < 0 then
+            dedup(spaces).toList match
+            case Typ(`constantNullType`, _) :: Nil =>
               report.warning(MatchCaseOnlyNullWarning(), pat.srcPos)
-            case _ =>
-          }
+            case s =>
+              debug.println("`_` matches = " + s)
         }
       }
     }

tests/patmat/dotty-trees.scala

@@ -0,0 +1,11 @@
+abstract class Tree[-T >: Null]
+
+case class TypeTree[-T >: Null]() extends Tree[T]
+
+abstract class DerivedTypeTree() extends TypeTree[Null]
+
+def foo(tree: Tree[Null]): Unit =
+  tree match
+  case _: DerivedTypeTree =>
+  case TypeTree() =>
+  case _ =>

tests/patmat/i12241.check

@@ -0,0 +1 @@
+54: Pattern Match Exhaustivity: (EndpointInput.Empty(), _), (EndpointInput.Pair(), EndpointInput.MappedPair()), (EndpointInput.Pair(), EndpointInput.Pair2()), (EndpointInput.Pair(), EndpointInput.MappedPair2()), (EndpointInput.Pair(), EndpointInput.FixedMethod()), (EndpointInput.Pair(), EndpointInput.FixedPath())

tests/patmat/i12241.scala

@@ -0,0 +1,75 @@
+sealed trait EndpointInput[T]
+
+object EndpointInput {
+  case class Pair[T]() extends EndpointInput[T]
+  case class MappedPair[T]() extends EndpointInput[T]
+  case class Pair2[T]() extends EndpointInput[T]
+  case class MappedPair2[T]() extends EndpointInput[T]
+  case class FixedMethod[T]() extends EndpointInput[T]
+  case class FixedPath[T]() extends EndpointInput[T]
+  case class PathCapture[T]() extends EndpointInput[T]
+  case class PathsCapture[T]() extends EndpointInput[T]
+  case class Query[T]() extends EndpointInput[T]
+  case class QueryParams[T]() extends EndpointInput[T]
+  case class Cookie[T]() extends EndpointInput[T]
+  case class ExtractFromRequest[T]() extends EndpointInput[T]
+  case class ApiKey[T]() extends EndpointInput[T]
+  case class Http[T]() extends EndpointInput[T]
+  case class Body[R, T]() extends EndpointInput[T]
+  case class FixedHeader[T]() extends EndpointInput[T]
+  case class Header[T]() extends EndpointInput[T]
+  case class Headers[T]() extends EndpointInput[T]
+  case class StatusCode[T]() extends EndpointInput[T]
+  case class Empty[T]() extends EndpointInput[T]
+}
+
+object Test extends App {
+  import EndpointInput._
+
+  def compare(left: EndpointInput[_], right: EndpointInput[_]): Boolean =
+    (left, right) match {
+      case (Pair(), Pair()) => true
+      case (MappedPair(), MappedPair()) => true
+      case (Pair2(), Pair2()) => true
+      case (MappedPair2(), MappedPair2()) => true
+      case (FixedMethod(), FixedMethod()) => true
+      case (FixedPath(), FixedPath()) => true
+      case (PathCapture(), PathCapture()) => true
+      case (PathsCapture(), PathsCapture()) => true
+      case (Query(), Query()) => true
+      case (QueryParams(), QueryParams()) => true
+      case (Cookie(), Cookie()) => true
+      case (ExtractFromRequest(), ExtractFromRequest()) => true
+      case (ApiKey(), ApiKey()) => true
+      case (Http(), Http()) => true
+      case (Body(), Body()) => true
+      case (FixedHeader(), FixedHeader()) => true
+      case (Header(), Header()) => true
+      case (Headers(), Headers()) => true
+      case (StatusCode(), StatusCode()) => true
+      case (_, _) => false
+    }
+
+  def compare2(left: EndpointInput[_], right: EndpointInput[_]): Boolean =
+    (left, right) match {
+      case (Pair(), Pair()) => true
+      case (MappedPair(), MappedPair()) => true
+      case (Pair2(), Pair2()) => true
+      case (MappedPair2(), MappedPair2()) => true
+      case (FixedMethod(), FixedMethod()) => true
+      case (FixedPath(), FixedPath()) => true
+      case (PathCapture(), PathCapture()) => true
+      case (PathsCapture(), PathsCapture()) => true
+      case (Query(), Query()) => true
+      case (QueryParams(), QueryParams()) => true
+      case (Cookie(), Cookie()) => true
+      case (ExtractFromRequest(), ExtractFromRequest()) => true
+      case (ApiKey(), ApiKey()) => true
+      case (Http(), Http()) => true
+      case (Body(), Body()) => true
+      case (FixedHeader(), FixedHeader()) => true
+      case (Header(), Header()) => true
+      case (Headers(), Headers()) => true
+      case (StatusCode(), StatusCode()) => true
+    }
+}

tests/patmat/i8922c.check

@@ -1 +1 @@
-26: Pattern Match Exhaustivity: (true, _: String, _), (true, _: Double, _), (true, true, _), (true, false, _), (true, (), _), (false, _: String, _)
+26: Pattern Match Exhaustivity: (true, _, _), (false, _, _), ((), _, _), (true, _: Double, _), (true, true, _)

tests/patmat/t10019.check

@@ -1,2 +1,2 @@
-2: Pattern Match Exhaustivity: (List(_, _, _*), List(_, _*)), (Nil, List(_, _*)), (List(_, _*), List(_, _, _*)), (List(_, _*), Nil)
+2: Pattern Match Exhaustivity: (List(_, _, _*), List(_, _*)), (Nil, List(_, _*)), (List(_, _*), List(_, _, _*)), (List(_, _*), Nil), (_: List, List(_, _, _*))
 11: Pattern Match Exhaustivity: (Foo(None), Foo(_))