2.13.10 compiler doesn't detect exhaustive match on Seq

Question
1

I’m attempting to pattern match on a Seq to detect sequences containing at least one element (yes, there are other ways to check this, but…) and the compiler is reporting that a “match may not be exhaustive”.
I just wanted to sanity check here before thinking about a compiler bug report.

I started with just two cases:

   seq match {
      case Seq()         => println(s"$seq is empty")
      case _ +: _         => println(s"$seq has one or more elements")
    }

(equivalently case Seq(_, _ @_*) exhibits the same problem)

This resulted in the compiler warning that:

match may not be exhaustive.
It would fail on the following input: (x: Seq[?] forSome x not in Nil)
def test(seq: Seq[_]): Unit = seq match {

… which seems incorrect to me. Indeed adding an additional case for an empty list does not help:

   seq match {
      case Seq()         => println(s"$seq is empty")
      case Seq(_)        => println(s"$seq has one element")
      case _ +: _         => println(s"$seq has one or more elements")
    }

… and the compiler wants a case _ before it is satisfied that the match is exhaustive, but this case can never be hit, which is easily verified at runtime.
The equivalent matches using classic List cons patterns doesn’t have this problem.

Am I missing something obvious here, or is this just a blindspot in the compiler?

2

Looks like this is related to use of -Xlint:strict-unsealed-patmat in compiler options, so probably a bug in the lint.

3

The compiler can’t possibly know that the match is exhaustive, since those are not matches on an ADT but rather a bunch of custom extractors.
Yes, in this specific case those extractors form a closed set and thus the match is safe, but the compiler doesn’t have any way to know that as of today (I believe there is some WIP in Scala 3, but I could be wrong).

My personal advice is to use List rather than Seq for many reasons; including that head-tail pattern matching works as expected and is safe and efficient. But, since I know many folks will prefer to keep using Seq this is the best way to do that:

seq match {
  case _ +: _ => println(s"$seq has at least one element")
  case _  => println(s"$seq is empty")
}

Another option would be using @nowarm to silence the warning in this match.

4

Yeah, that makes sense I guess (I get used to expecting the Scala compiler to being near omnipotent, so this just felt odd).

The fact that the supposed failure pattern is explicitly handled in the cases is the most jarring part of this, but I guess it would require compiling and evaluating the various extractors at compile time to disprove.