Dotty: False “match may not be exhaustive warning”

[julienrf]

Minimized code

def f(xs: List[Int]) =
  xs match
    case init :+ last => ()
    case Nil => ()

@main def run = f(List(1, 2))

https://scastie.scala-lang.org/NVdH00JGS36HLzTs7F8vhw

Output

[warn] 60 |    case init :+ last =>
[warn]    |    ^
[warn]    |    match may not be exhaustive.
[warn]    |
[warn]    |    It would fail on pattern case: List(_, _: _*)
[warn] one warning found

Expectation

There is no warning.

[odersky]

I have also noted overzealous "not exhaustive" warnings linked to unapplies. What's the algorithm used there?

[liufengyun]

The problem is that the extractor does not tell the algorithm it is irrefutable for non-empty list. The following code works without any problem:

object :+ {
  def unapply[T](l: ::[T]): (List[T], T) = (l.init, l.last)
}

def f(xs: List[Int]) =
  xs match
    case init :+ last => ()
    case Nil => ()

@main def run = f(List(1, 2))

[odersky]

I have other problems with extractors.

type ParamClause = List[ValDef] | List[TypeDef]

object ValDefs:
  def unapply(pc: ParamClause): Option[List[ValDef]] = ... // matches empty list and all lists of ValDefs

object TypeDefs:
  def unapply(pc: ParamClause): Option[List[TypeDef]] = ... // matches non-empty lists of TypeDefs

(pc: ParamClause) match
  case ValDefs(vdefs) => ...
  case TypeDefs(tdefs) => ...

Gives an exhaustivity warning, even though they should be none. What can be done about this?

[liufengyun]

@odersky The fix is to make the extractors irrefutable:

object ValDefs:
  def unapply(pc: List[ValDef]): Some[List[ValDef]] = ... // matches empty list and all lists of ValDefs

object TypeDefs:
  def unapply(pc: List[TypeDef]): Some[List[TypeDef]] = ... // matches non-empty lists of TypeDefs

(pc: ParamClause) match
  case ValDefs(vdefs) => ...
  case TypeDefs(tdefs) => ...

However, the above will get a warning about type test cannot be checked at runtime. The warning seems fair to me: if the value is Nil, it's impossible to check it's List[TypeDef] or List[ValDef].

The following code demonstrates a working example with explicit tagging in union types:

import scala.annotation.targetName

type ParamClause = List[Int] | Some[List[String]]

extension (lst: List[String]) 
  @targetName("asParamsString")
  def asParams: ParamClause = Some(lst)

extension (lst: List[Int]) 
  @targetName("asParamsInt")
  def asParams: ParamClause = lst

object IntList:
  def unapply(pc: List[Int]): Some[List[Int]] = Some(pc)

object StringList:
  def unapply(pc: Some[List[String]]): Some[List[String]] = pc

def foo(pc: ParamClause) = pc match
  case IntList(intL) => 4
  case StringList(strL) => 3


@main def run = 
  println(foo(List(1, 2, 3).asParams))
  println(foo(List("hello").asParams))

[odersky]

The warning seems fair to me: if the value is Nil, it's impossible to check it's List[TypeDef] or List[ValDef].

But in this case the empty list is always classified as a List[ValDef]. That's because () is a valid parameter list but [] isn't. Also, the unapply really wants to see a ParamClause, not a List[ValDef] or a List[TypeDef]. It will check itself the types
by looking at the list elements.

So this looks like a case of a valid semantic distinction with extractors where exhaustivity checks do the wrong thing.

[liufengyun]

But in this case the empty list is always classified as a List[ValDef]. That's because () is a valid parameter list but [] isn't.

• This application-specific knowledge is not encoded in types, the algorithm has no way to reason about this.
• If an unapply returns Option[T], the extractor is assumed to be refutable, as is the case in Scala 2.

The example does suggest that the current mechanism for specifying irrefutable unapply is not expressive enough to encode domain-specific knowledge. One way to improve is to introduce annotations like @irrefutableFor[T] to tell the algorithm that the unapply is irrefutable if the actual scrutinee has the more detailed type T.

[odersky]

But in this case we have two extractors which are both refutable but together cover the scrutinee type completely. How can we express that?

[liufengyun]

But in this case we have two extractors which are both refutable but together cover the scrutinee type completely. How can we express that?

It can be specified like the following (with the hypothetical @irrefutableFor[T]):

type ParamClause = List[ValDef] | List[TypeDef]

object ValDefs:
  @irrefutableFor[::[ValDef] | Nil.type]
  def unapply(pc: ParamClause): Option[List[ValDef]] = ... // matches empty list and all lists of ValDefs

object TypeDefs:
  @irrefutableFor[::[TypeDef]]
  def unapply(pc: ParamClause): Option[List[TypeDef]] = ... // matches non-empty lists of TypeDefs

Or, lie a little bit:

type ParamClause = List[ValDef] | List[TypeDef]

object ValDefs:
  @irrefutableFor[List[ValDef]]
  def unapply(pc: ParamClause): Option[List[ValDef]] = ... // matches empty list and all lists of ValDefs

object TypeDefs:
  @irrefutableFor[List[TypeDef]]
  def unapply(pc: ParamClause): Option[List[TypeDef]] = ... // matches non-empty lists of TypeDefs

[odersky]

I don't understand. Taken alone, each unapply is clearly refutable if the scrutinee is ParamClause. It's only taken together that they become irrefutable.

[liufengyun]

I don't understand. Taken alone, each unapply is clearly refutable if the scrutinee is ParamClause. It's only taken together that they become irrefutable.

Taken together, it is still uncertain that they are irrefutable. This is because from the type signature of unapply(pc: ParamClause): Option[List[ValDef]], we don't know that it matches all values of the type List[ValDef]. We can easily define an extractor that has the same type signature but only matches a subset of values in List[ValDef]. Therefore, from the type signature of the two unapplys alone, they are still refutable.

The two unapplys, taken together, are irrefutable if it's known that one covers _all_ values of List[ValDef] and the other covers _all_ values of List[TypeDef].

To make it known to the algorithm that unapply(pc: ParamClause): Option[List[ValDef]] covers _all_ List[ValDef] instead of a subset, we can invent a new mechanism to specify the knowledge. The hypothetical @irrefutableFor[T] is a way to specify such knowledge for each unapply individually.

Maybe a better name for the hypothetical annotation @irrefutableFor[T] is @covers[T]:

type ParamClause = List[ValDef] | List[TypeDef]

object ValDefs:
  @covers[List[ValDef]]
  def unapply(pc: ParamClause): Option[List[ValDef]] = ... // matches empty list and all lists of ValDefs

object TypeDefs:
  @covers[List[TypeDef]]
  def unapply(pc: ParamClause): Option[List[TypeDef]] = ... // matches non-empty lists of TypeDefs

[odersky]

Yes, covers might work. But there is also the issue that you might have two purely semantic unapplys that cannot be reasoned with in terms of existsing types. E.g.

object Nat:
  def unapply(x: Int): Option[Int] = if x >= 0 then Some(x) else None
object Neg:
  def unapply(x: Int): Option[Int] = if x<  0 then Some(x) else None

anInt match
  case Nat(x) => ...
  case Neg(x) => ...

What escape hatch could exists for these situations?

[liufengyun]

A tentative solution is to introduce @notCovered[T]:

type Nat <: Int
type Neg <: Int

object Nat:
  @covers[Nat]
  @notCovered[Neg]
  def unapply(x: Int): Option[Int] = if x >= 0 then Some(x) else None

object Neg:
  @covers[Neg]
  @notCovered[Nat]
  def unapply(x: Int): Option[Int] = if x<  0 then Some(x) else None

anInt match
  case Nat(x) => ...
  case Neg(x) => ...

[dwijnand]

I like your annotation, @liufengyun. You might also be interested in https://github.com/scala/bug/issues/12252 which is about exhaustivity across variadic extractors.

[liufengyun]

@dwijnand Dotty currently has some support for irrefutable unapplySeq:

object SeqExtractor {
  def unapplySeq(x: Int): Some[List[Int]] = Some(List(1))
}

@main
def Test = (1: String | Int)  match {
 case _: String              => "hello"
 case SeqExtractor()         => "zero"
 case SeqExtractor(_)        => "one"
 case SeqExtractor(_, _, _*) => "two or more"
}

https://scastie.scala-lang.org/H6VaTJyeSVuvZ7Y8kz4Qag