From 10b5ca02e2b5135bf79d23e86af8a3c3a8358ccf Mon Sep 17 00:00:00 2001
From: Liu Fengyun <liu@fengy.me>
Date: Fri, 7 May 2021 11:08:49 +0200
Subject: [PATCH 1/4] Fix #12358: Avoid spurious unions in simplification

And be more lazier in product subtraction
---
 .../tools/dotc/transform/patmat/Space.scala    | 18 +++++++++++-------
 tests/patmat/i12358.scala                      |  5 +++++
 2 files changed, 16 insertions(+), 7 deletions(-)
 create mode 100644 tests/patmat/i12358.scala

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index bcb021af7b76..b1bb464f359a 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -113,16 +113,17 @@ trait SpaceLogic {
   /** Display space in string format */
   def show(sp: Space): String
 
-  /** Simplify space using the laws, there's no nested union after simplify */
+  /** Simplify space such that a space equal to `Empty` becomes `Empty` */
   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
+      val sps = spaces.map(simplify(_))
+      if (sps.contains(Empty)) Empty
       else if (canDecompose(tp) && decompose(tp).isEmpty) Empty
-      else sp
+      else Prod(tp, fun, sps)
     case Or(spaces) =>
       val spaces2 = spaces.map(simplify(_)).filter(_ != Empty)
       if spaces2.isEmpty then Empty
+      else if spaces2.lengthCompare(1) == 0 then spaces2.head
       else Or(spaces2)
     case Typ(tp, _) =>
       if (canDecompose(tp) && decompose(tp).isEmpty) Empty
@@ -243,10 +244,10 @@ trait SpaceLogic {
           tryDecompose1(tp1)
         else
           a
-      case (_, Or(ss)) =>
-        ss.foldLeft(a)(minus)
       case (Or(ss), _) =>
         Or(ss.map(minus(_, b)))
+      case (_, Or(ss)) =>
+        ss.foldLeft(a)(minus)
       case (Prod(tp1, fun, ss), Typ(tp2, _)) =>
         // uncovered corner case: tp2 :< tp1, may happen when inheriting case class
         if (isSubType(tp1, tp2))
@@ -272,7 +273,10 @@ trait SpaceLogic {
         else if cache.forall(sub => isSubspace(sub, Empty)) then Empty
         else
           // `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
-          Or(LazyList(range: _*).map { i => Prod(tp1, fun1, ss1.updated(i, sub(i))) })
+          val spaces = LazyList(range: _*).flatMap { i =>
+            flatten(sub(i)).map(s => Prod(tp1, fun1, ss1.updated(i, s)))
+          }
+          Or(spaces)
     }
   }
 }
diff --git a/tests/patmat/i12358.scala b/tests/patmat/i12358.scala
new file mode 100644
index 000000000000..b58d312838ce
--- /dev/null
+++ b/tests/patmat/i12358.scala
@@ -0,0 +1,5 @@
+
+def foo(x: List[Int]): Unit =
+  x match
+  // case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: Nil =>
+  case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: x15 :: x16 :: x17 :: x18 :: x19 :: x20 :: x21 :: x22 :: Nil =>
\ No newline at end of file

From 2433be6f197b405e5634b1639ccb2c97a9a0bc06 Mon Sep 17 00:00:00 2001
From: Liu Fengyun <liu@fengy.me>
Date: Fri, 7 May 2021 14:56:14 +0200
Subject: [PATCH 2/4] Update check files: order of counter examples changed

---
 tests/patmat/i12241.check | 2 +-
 tests/patmat/i12358.check | 1 +
 tests/patmat/i8922c.check | 2 +-
 tests/patmat/t10019.check | 2 +-
 4 files changed, 4 insertions(+), 3 deletions(-)
 create mode 100644 tests/patmat/i12358.check

diff --git a/tests/patmat/i12241.check b/tests/patmat/i12241.check
index 2b3f2416f40a..1ad41cfa2ac1 100644
--- a/tests/patmat/i12241.check
+++ b/tests/patmat/i12241.check
@@ -1 +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())
+54: Pattern Match Exhaustivity: (EndpointInput.Pair(), EndpointInput.MappedPair()), (EndpointInput.Pair(), EndpointInput.Pair2()), (EndpointInput.Pair(), EndpointInput.MappedPair2()), (EndpointInput.Pair(), EndpointInput.FixedMethod()), (EndpointInput.Pair(), EndpointInput.FixedPath()), (EndpointInput.Pair(), EndpointInput.PathCapture())
diff --git a/tests/patmat/i12358.check b/tests/patmat/i12358.check
new file mode 100644
index 000000000000..d1979b049b29
--- /dev/null
+++ b/tests/patmat/i12358.check
@@ -0,0 +1 @@
+3: Pattern Match Exhaustivity: List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _*), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, )
diff --git a/tests/patmat/i8922c.check b/tests/patmat/i8922c.check
index 608e48c4b67c..acd56ccd2986 100644
--- a/tests/patmat/i8922c.check
+++ b/tests/patmat/i8922c.check
@@ -1 +1 @@
-26: Pattern Match Exhaustivity: (true, _, _), (false, _, _), ((), _, _), (true, _: Double, _), (true, true, _)
+26: Pattern Match Exhaustivity: (_: Int, _: String, _), (_: Int, _: Int, BANG), (_: Int, _: Int, BANG_EQUAL), (_: Int, _: Int, EQUAL), (_: Int, _: Int, EQUAL_EQUAL), (_: Int, true, _)
diff --git a/tests/patmat/t10019.check b/tests/patmat/t10019.check
index 885aba2381e4..4eb648ea2ae4 100644
--- a/tests/patmat/t10019.check
+++ b/tests/patmat/t10019.check
@@ -1,2 +1,2 @@
-2: Pattern Match Exhaustivity: (List(_, _, _*), List(_, _*)), (Nil, List(_, _*)), (List(_, _*), List(_, _, _*)), (List(_, _*), Nil), (_: List, List(_, _, _*))
+2: Pattern Match Exhaustivity: (List(_, _, _*), _: List), (Nil, List(_, _*)), (_: List, List(_, _, _*)), (List(_, _*), Nil)
 11: Pattern Match Exhaustivity: (Foo(None), Foo(_))

From 1f13d1989256b506a3f70c787ab7a449ae099bbc Mon Sep 17 00:00:00 2001
From: Liu Fengyun <liu@fengy.me>
Date: Fri, 7 May 2021 15:04:03 +0200
Subject: [PATCH 3/4] Fix printing of counter-examples for List

---
 compiler/src/dotty/tools/dotc/transform/patmat/Space.scala | 2 +-
 tests/patmat/i12358.check                                  | 2 +-
 tests/patmat/i12358.scala                                  | 1 -
 3 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
index b1bb464f359a..0707587b5b99 100644
--- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -775,7 +775,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
         if (ctx.definitions.isTupleType(tp))
           "(" + params.map(doShow(_)).mkString(", ") + ")"
         else if (tp.isRef(scalaConsType.symbol))
-          if (flattenList) params.map(doShow(_, flattenList)).mkString(", ")
+          if (flattenList) params.map(doShow(_, flattenList)).filter(_.nonEmpty).mkString(", ")
           else params.map(doShow(_, flattenList = true)).filter(!_.isEmpty).mkString("List(", ", ", ")")
         else {
           val sym = fun.symbol
diff --git a/tests/patmat/i12358.check b/tests/patmat/i12358.check
index d1979b049b29..0ffca060173b 100644
--- a/tests/patmat/i12358.check
+++ b/tests/patmat/i12358.check
@@ -1 +1 @@
-3: Pattern Match Exhaustivity: List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _*), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, )
+3: Pattern Match Exhaustivity: List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _*), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _)
diff --git a/tests/patmat/i12358.scala b/tests/patmat/i12358.scala
index b58d312838ce..9b8a865ae000 100644
--- a/tests/patmat/i12358.scala
+++ b/tests/patmat/i12358.scala
@@ -1,5 +1,4 @@
 
 def foo(x: List[Int]): Unit =
   x match
-  // case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: Nil =>
   case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: x15 :: x16 :: x17 :: x18 :: x19 :: x20 :: x21 :: x22 :: Nil =>
\ No newline at end of file

From b3ed6f51c2f040da725244fe09119ba3b04cccfe Mon Sep 17 00:00:00 2001
From: Liu Fengyun <liu@fengy.me>
Date: Fri, 7 May 2021 15:06:03 +0200
Subject: [PATCH 4/4] Add example as bench test

---
 bench/profiles/exhaustivity.yml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/bench/profiles/exhaustivity.yml b/bench/profiles/exhaustivity.yml
index 0e765bb592d9..d8295a27060e 100644
--- a/bench/profiles/exhaustivity.yml
+++ b/bench/profiles/exhaustivity.yml
@@ -41,6 +41,12 @@ charts:
         - key: exhaustivity-i12241
           label: bootstrapped
 
+    - name: "exhaustivity i12358"
+      url: https://github.com/lampepfl/dotty/blob/master/tests/patmat/i12358.scala
+      lines:
+        - key: exhaustivity-i12358
+          label: bootstrapped
+
 scripts:
 
     patmatexhaust:
@@ -64,5 +70,8 @@ scripts:
     exhaustivity-i12241:
         - measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i12241.scala
 
+    exhaustivity-i12358:
+        - measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i12358.scala
+
 config:
     pr_base_url: "https://github.com/lampepfl/dotty/pull/"