Bad performance on complex patmat

[fomkin]

reproduction steps

using Scala 2.12.10, 2.13.3, 2.13.4,

sealed trait PathAndQuery 
sealed trait Path extends PathAndQuery
sealed trait Query extends PathAndQuery

object PathAndQuery {
  case object Root extends Path
  case class /(prev: Path, value: String) extends Path
  case class ===(k: String, v: String) extends Query
  case class :&(prev: Query, next:(===)) extends Query
  case class +?(path: Path, next:(===)) extends Query
}

import PathAndQuery._

val path = /(/(Root, "page"), "1")
val q1 = ===("k1", "v1")
val q2 = ===("k2", "v2")
val pq = :&(+?(path, q1), q2)

(pq: PathAndQuery) match {
  case Root / "page" / "1" => println("match 1")
  case Root / "page" / "1" +? ("k1" === "v1") => println("match 2")
  case Root / "page" / "1" +? ("k1" === "v1") :& ("k2" === "v2") => println("match 3")
}

problem

It compiles from few minutes to infinite. I understand that problem related to exhaustiveness check and I see warning about it, but I sure it should not hang the compiler.

[Rich2]

I think I'm getting the same problem in 2.13.4. In my case it fails to complete every time. Link to commit and project, However the compiling has failed every time I've tried upgrading to 2.13.4, not just this commit.
If mill Util.compile is run the compile just hangs. If Util/compile is run within Sbt it gives the following output.

//A number of match not exhautive matches ommitted.
[warn] /Common/openstrat/Util/src/pParse/parseStringToken.scala:10:71: match may not be exhaustive.
[warn]     def loop(rem: CharsOff): EMon3[CharsOff, TextPosn, StringToken] = rem match
[warn]                                                                       ^
[warn] /Common/openstrat/Util/src/pParse/srcToETokens.scala:54:71: match may not be exhaustive.
[warn]         def loop(rem: CharsOff, tp: TextPosn): (CharsOff, TextPosn) = rem match
[warn]                                                                       ^
Exception in thread "classloader-cache-cleanup-0" java.lang.OutOfMemoryError: Java heap space
[error] ## Exception when compiling 91 sources to /Common/openstrat/Dev/SbtDir/UtilCore/target/scala-2.13/classes
[error] java.lang.OutOfMemoryError: Java heap space
[error] 
[error]            
[info] shutting down sbt server
java.lang.OutOfMemoryError: Java heap space
[error] [launcher] error during sbt launcher: java.lang.OutOfMemoryError: Java heap space

There are no match exhaustive warnings under 2.13.3.

[dwijnand]

Having broken the match cases down into variables with constraints/"eq axioms", it looks, exhaustively, for the possible variable values that would fail the match, the so-called "models" that satisfy the "can this match fail?" formula. This initial search has a backoff threshold which will give a "Exhaustivity analysis reached max recursion depth, not all missing cases are reported" warning. However, the found models needn't have all their variables set to disprove exhaustivity, so it then spends all its time and memory expanding the models.

Let me show with some local debug output. Using the same pq value above, but with a much simpler match. Note I changed a few names in the original to help me debug it (mentioned below):

    pq match {
      case Root           => println("match 1")
      case Root / "about" => println("match 1")
    }

It first shows how it's statically approximating the cases:

checking exhaustivity...
case #1 (approximately) matches if:
 ET(x1,Root)  ->  V1 == Root
case #2 (approximately) matches if:
  TT(/, x1, /)   ->  (V1 != null && V1 == /)
     P(x3)       ->        V1 != null
  ET(p4,Root)    ->        V2 == Root
 ET(p5,"about")  ->       V3 == "about"

Then the variables of the formula, the eq axioms for the variables, and the pure boolean formula (⊕ means XOR):

vars:
  V1: PathAndQuery ::= :& | / | Kv | Root | +? // = x1
  V2: Path ::= / | Root // = x1.prevP
  V3: String ::= ... // = x1.seg
eqAxioms:
  (V1=+?#17 ⊕ V1=:&#15 ⊕ V1=/#12 ⊕ V1=Kv#16 ⊕ V1=Root#11)
  (V2=/#18 ⊕ V2=Root#13)
pure:
  (  !(V1=Root#11)
  &&
    (  !(V1=/#12)
    || !(V2=Root#13)
    || !(V3="about"#14)
    )
  )

I renamed === to Kv. It finds 11 solutions (this minimisation doesn't breach the threshold) and, skipping to the end, here are the counter-examples:

11 solutions
6 counter-examples, pruned from 15
test/files/pos/t12237.scala:22: warning: match may not be exhaustive.
It would fail on the following inputs: +?(_, _), /(/(_, _), "about"), /(/(_, _), (x: String forSome x not in "about")), /(Root, (x: String forSome x not in "about")), :&(_, _), Kv(_, _)
    pq match {
    ^

However, the part in the middle is the problem, that in the original is where the compiler blows up, I'll give the first example:

var assignment #1:
  V1(=x1: PathAndQuery) == (Kv) != (+?, :&, /, Root)
  V2(=x1.prevP: Path) == (Root) != (/)
unassignedSyms:
  V3(=x1.seg: String) =? "about"
cartProd (1 unassigned syms [total 1 vars] -> 2 expanded var assignments -> 2 cart prod var assignments):
  0: V3(=x1.seg: String) == ("about") != ()
  1: V3(=x1.seg: String) == () != ("about")

x1 is a fresh name for the original pq, but basically it found as a counter that pq could be a key-value pair (what in the original is called ===(k, v)), rather than the Root object or the / class. The unassigned symbol is for the variable x1.seg (which was originally called value in /): but it's not necessary for the compiler to expand the model given it's a key value. I believe that's the origin of the pruning: the "pq could be a Kv" counter-example whether it's with V3==about or with V3!=about is still just Kv(_, _)...

So I need to figure out how to preserve everything else and avoid all this needless work.

[dwijnand]

Comparing the counter-example generated from ignoring the unassigned symbols to the counter-examples generated from expanding the model with the combination of assigned symbols is both silly and confusing:

// from test/files/run/virtpatmat_alts.scala
  List(5) match {
    case 1 :: Nil | 2 :: Nil  => println("FAILED")
    case (x@(4 | 5 | 6)) :: Nil => println("OK "+ x)
    case 7 :: Nil  => println("FAILED")
    case Nil  => println("FAILED")
  }

var assignment #2:
  V1(=x1: List[?]) == (scala.collection.immutable.::[?]) != (Nil)
  V2(=x1.head: Int) == (6) != (4, 5)
  V3(=x1.next$access$1: List[?]) == (scala.collection.immutable.::[?]) != (Nil)
unassignedSyms:
  V2(=x1.head: Int) =? 1
  V2(=x1.head: Int) =? 2
  V2(=x1.head: Int) =? 7
cartProd (3 unassigned syms [total 1 vars] -> 0 expanded var assignments -> 2 cart prod var assignments):
  0: V2(=x1.head: Int) == (6, 1, 2, 7) != (4, 5)
  1: V2(=x1.head: Int) == (6) != (4, 5, 1, 2, 7)
ce=Some(List(6, _))
error: java.lang.AssertionError: assertion failed:
  Some(List(6, _)) != Some(List(_, _))

I added the assertion, and it's telling us this: the counter-example without taking the unassigned "what if the head is" 1, 2, 7 symbol is List(6, _) but once you consider (?!?!) that head could also be 1, 2, and 7, in addition to 6, then it's List(_, _). List(6, _) is overly specific to the more general List(_, _) case that isn't being handled by the match, but perhaps it's unnecessary work?

[dwijnand]

Another example:

// from test/files/run/virtpatmat_opt_sharing.scala
    List(1, 3, 4, 7) match {
      case 1 :: 3 :: 4 :: 5 :: x => println("nope")
      case 1 :: 3 :: 4 :: 6 :: x => println("nope")
      case 1 :: 3 :: 4 :: 7 :: x => println(1)
    }

var assignment #5:
  V1(=x1: List[?]) == (scala.collection.immutable.::[?]) != (scala.collection.immutable.Nil.type)
  V2(=x1.head: Int) == (1) != ()
  V3(=x1.next$access$1: List[?]) == (scala.collection.immutable.::[?]) != (scala.collection.immutable.Nil.type)
  V4(=x1.next$access$1.head: Int) == () != (3)
  V5(=x1.next$access$1.next$access$1: List[?]) == (scala.collection.immutable.::[?]) != (scala.collection.immutable.Nil.type)
  V7(=x1.next$access$1.next$access$1.next$access$1: List[?]) == (scala.collection.immutable.Nil.type) != (scala.collection.immutable.::[?])
unassignedSyms:
  V6(=x1.next$access$1.next$access$1.head: Int) =? 4
  V8(=x1.next$access$1.next$access$1.next$access$1.head: Int) =? 5
  V8(=x1.next$access$1.next$access$1.next$access$1.head: Int) =? 6
  V8(=x1.next$access$1.next$access$1.next$access$1.head: Int) =? 7
cartProd (4 unassigned syms [total 2 vars] -> 0 expanded var assignments -> 10 cart prod var assignments):
  0:
  V6(=x1.next$access$1.next$access$1.head: Int) == (4) != ()
  V8(=x1.next$access$1.next$access$1.next$access$1.head: Int) == (5, 6, 7) != ()
<trim>
ce=Some(List(1, (x: Int forSome x not in 3), _))
error: java.lang.AssertionError: assertion failed:
  Some(List(1, (x: Int forSome x not in 3), _)) != Some(List(1, (x: Int forSome x not in 3), 4))

List(1, (x: Int forSome x not in 3), _) seems like a fine counter-example, compared to List(1, (x: Int forSome x not in 3), 4).

[dwijnand]

Last one:

// from test/files/run/virtpatmat_unapplyprod.scala
  case class FooSeq(x: Int, y: String, z: Boolean*)

  FooSeq(1, "a", true, false, true) match {
    case FooSeq(1, "a") => println("nope")
    case FooSeq(1, "a", x@_* ) => println(x.toList)
  }

var assignment #2:
  V1(=x1: Test.FooSeq) == (Test.FooSeq) != ()
  V2(=x1.x: Int) == () != (1)
unassignedSyms:
  V3(=x1.y: String) =? "a"
cartProd (1 unassigned syms [total 1 vars] -> 0 expanded var assignments -> 2 cart prod var assignments):
  0: V3(=x1.y: String) == ("a") != ()
  1: V3(=x1.y: String) == () != ("a")
ce=Some(FooSeq((x: Int forSome x not in 1), _, _))
error: java.lang.AssertionError: assertion failed:
  Some(FooSeq((x: Int forSome x not in 1), _, _)) != Some(FooSeq((x: Int forSome x not in 1), "a", _))

Again, FooSeq((x: Int forSome x not in 1), _, _) seems perfectly adequate, compared to FooSeq((x: Int forSome x not in 1), "a", _).