Implement @covers annotation for partial irrefutable specification

[liufengyun]

We propose two orthogonal annotations to enhance exhaustivity check for custom extractors and virtual ADT data types.

• @covers[T]: specifying that an unapply is partially Irrefutable (implemented in this PR)
• @branch[T]: defining a branch for a virtual ADT data type T (to be implemented)

1. Partially Irrefutable Extractor

Currently, Scala only supports specifying that an unapply is irrefutable if its result type is of the form Some[T], or it is a subtype of ProductN[T1, .., TN], or it has a member isEmpty whose result type true. In all such cases, the extractor is either irrefutable or refutable.

The annotation @covers[T] provides a way to support specifying partial irrefutability. If the result type of unapply has the form U @covers[T], then the extractor is irrefutable when the scrutinee is a subtype of T.

Example 1

  import scala.annotation.covers

  type /[T, U] = T @covers[U]

  object :+ {
    def unapply[T](l: List[T]): Option[(List[T], T)] / ::[T] = ???
  }

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

Example 2

  import scala.annotation.covers

  class ValDef
  class TypeDef
  opaque type ValDefs  <: List[ValDef]  = List[ValDef]
  opaque type TypeDefs <: List[TypeDef] = List[TypeDef]

  type ParamClause = ValDefs | TypeDefs

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

    def apply(vals: List[ValDef]): ValDefs = vals

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

    def apply(tdefs: List[TypeDef]): TypeDefs =
      assert(tdefs.nonEmpty)
      tdefs

  def f(pc: ParamClause) =
    pc match
    case ValDefs(vs) => ()
    case TypeDefs(ts) => ()

2. Virtual ADT

Sometimes, we might want to define a virtual ADT:

• for a set of abstract types (e.g. in final tagless encoding)
• for existing non-ADT types, such as Int

The annotation @branch enables a library author to define a virtual ADT.

Example 3

The following is an example that makes Int a virtual ADT.

  import scala.annotation.covers

  @branch[Num]
  opaque type Nat <: Int = Int

  @branch[Num]
  opaque type Neg <: Int = Int

  type Num = Int

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

    def apply(x: Int): Nat =
      assert(x >= 0)
      x

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

    def apply(x: Int): Nat =
      assert(x < 0)
      x

  def foo(x: Option[Int]) =
    x match
    case Some(Nat(x)) =>
    case Some(Neg(x)) =>
    case None =>

Example 4

This example is a tentative solution to the problem discussed in the contributor forum:

object Opt {
  @branch[Opt]
  type NonEmptyOpt[+T] <: Opt[T]

  @branch[Opt]
  val Empty: Opt[Nothing] = ???

  def unapply[T](x: Opt[T]): Opt[T] @covers[NonEmptyOpt[T]] = x
}

final class Opt[+T](v: T) { ... }

Links

• Related issue: False “match may not be exhaustive warning” #10961
• Contributor discussion

[dwijnand]

Oh, nice @liufengyun! But why did those exhaustivity checkfiles change?

[liufengyun]

Oh, nice @liufengyun! But why did those exhaustivity checkfiles change?

Thanks Dale. The changes are due to the fact that we re-ordered some code: decompose a sealed type a little earlier in the operation. The result is still valid.

[nicolasstucki]

I don't see how we could use this feature in combination with the implementation of TypeTest.unapply.

[liufengyun]

@nicolasstucki For TypeTest.unapply, it will be something like the following:

def unapply(x: S): Option[x.type & T] @covers[S]

[liufengyun]

One floating idea is to introduce another annotation @branch[Num]:

    @branch[Num]
    opaque type Nat <: Int = Int

    @branch[Num]
    opaque type Neg <: Int = Int

    type Num = Int

    object Nat:
      def unapply(x: Num): Option[Nat] @covers[Nat] =

The annotation @branch will make it easy to support existing types:

object Opt {
  @branch[OptAlias]
  type NonEmptyOpt[+T] <: Opt[T]

  @branch[OptAlias]
  val Empty: Opt[Nothing] = ???

  type OptAlias[+T] = Opt[T]

  def unapply[T](x: OptAlias[T]): Opt[T] @covers[NonEmptyOpt[T]] = x
}

[nicolasstucki]

@nicolasstucki For TypeTest.unapply, it will be something like the following:

def unapply(x: S): Option[x.type & T] @covers[S]

I belive it should be

def unapply(x: S): Option[x.type & T] @covers[T]

Still, it should be tested with some concrete examples.

[SethTisue]

It isn't clear to me from the above how +: and :+ extraction could be made to work for types of sequences other than List? Is @branch intended to address that?

[liufengyun]

It isn't clear to me from the above how +: and :+ extraction could be made to work for types of sequences other than List? Is @branch intended to address that?

What kind of sequences you have in mind?

The @covers annotation extends the current specification mechanism for irrefutable extractors to partial or conditionally irrefutable cases. It is implemented in this PR.

The @branch annotation is orthogonal to @covers. It is intended to define a partition of an existing type. For example, Int as Nat and Neg.

[SethTisue]

What kind of sequences you have in mind?

literally any Seq that is not a collection.immutable.List

[liufengyun]

What kind of sequences you have in mind?

literally any Seq that is not a collection.immutable.List

Thanks @SethTisue . I just had a look at :+ in stdlib, it's indeed complex:

  object :+ {
    /** Splits a sequence into init :+ last.
      * @return Some((init, last)) if sequence is non-empty. None otherwise.
      */
    def unapply[A, CC[_] <: Seq[_], C <: SeqOps[A, CC, C]](t: C with SeqOps[A, CC, C]): Option[(C, A)] =
      if(t.isEmpty) None
      else Some(t.init -> t.last)
  }

To make it work, we need to use match types in Scala 3:

  object :+ {
    def unapply[A, CC[_] <: Seq[_], C <: SeqOps[A, CC, C]](t: C with SeqOps[A, CC, C]): Option[(C, A)] @covers[NonEmpty[C]] =
      if(t.isEmpty) None
      else Some(t.init -> t.last)

    type NonEmpty[C] = C match {
       case List[T] => ::[T]
       case Stream[T] => Stream.Cons[T]
       ....
    }

  }

[SethTisue]

To make it work, we need to use match types in Scala 3:

But won't that only work for Stream and List? Those are the only two collection types I know that have different classes/types for empty and nonempty lists.

[liufengyun]

To make it work, we need to use match types in Scala 3:

But won't that only work for Stream and List? Those are the only two collection types I know that have different classes/types for empty and nonempty lists.

For those types other than List and Stream, to benefit from exhaustivity check, either they have to follow the design of List and Stream, or they can be made a virtual ADT (See example 4 Opt[T]). No matter which approach is taken, the extractor :+ will look similar to the one sketched above.

[dwijnand]

Just realised that the way that this is done in Haskell is the COMPLETE pragma:

data Choice a = Choice Bool a

pattern LeftChoice :: a -> Choice a
pattern LeftChoice a = Choice False a

pattern RightChoice :: a -> Choice a
pattern RightChoice a = Choice True a

{-# COMPLETE LeftChoice, RightChoice #-}

foo :: Choice Int -> Int
foo (LeftChoice n) = n * 2
foo (RightChoice n) = n - 2

https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/exts/pragmas.html#complete-pragma

[liufengyun]

This is now deprecated, we have a better SIP.