False positive exhaustivity warning on GADTs

[noelwelsh]

I have a case with exhaustivity checking complaining that an exhaustive match is not exhaustive. Amusingly, if I add a placeholder (case _ => ...) the compiler then complains that the placeholder is not reachable. I have checked this in Scala 3.0, 3.0.1, 3.0.2, and 3.1.0-RC2. The full code is in: https://github.com/noelwelsh/repast

Here is a minimization, which demonstrates the exhaustivity checking issue but not the issue with a placeholder. Tested in Scala 3.1.0-RC2:

enum Exhausted[S, A] {
  def parse(
      input: String,
      offset: Int): A = {
    this match {

      case Resume(p) => p.parse(input, offset)

      // case _ =>
      //   throw new IllegalStateException(
      //     "This case should never happen. It's only here to stop exhaustivity checking from complaining."
      // )
    }
  }
  case Resume[S, A](parser: Exhausted[A, A])
      extends Exhausted[A, A]
}

I can create a repo with this if useful.

The issue appears to be related to having two type parameters both having the same type. If I change extends Exhausted[A, A] to extends Exhausted[S, A] the error goes away.

[dwijnand]

Can't tell yet where the problem is but given a scrutinee of type Exhausted[S, A] we get

candidates for Exhausted[S, A] : [class Resume]
class Resume refined to Exhausted.Resume[<?>, <?>]
Exhausted[S, A] decomposes to [Exhausted.Resume[<?>, <?>]]

What would we hope to get? Refined to something like Resume[A & S, A & S]?

Maybe <?> is inscrutable (no pun intended) but actually the right type and the problem is later when we get

signature of Exhausted.Resume.unapply ----> Exhausted[Nothing, Nothing]

I'll check the extends Exhausted[S, A] version to see if I get more insights.

[dwijnand]

What would we hope to get? Refined to something like Resume[A & S, A & S]?

The alternative is something like Resume[A, A] with the constraint A =:= S, but I'm not sure if there's a typerState that sticks around which can hold onto that constraint.

Or maybe Resume[X, X] forSome { type X = A & S } more precisely captures that it must the same type?

[SethTisue]

the minimization we're currently looking at is:

sealed trait Foo[S, A]
final case class Bar[B](foo: Foo[B, B]) extends Foo[B, B]
def pmat[U, C](scrut: Foo[U, C]): Unit =
  scrut match
    case Bar(_) =>

compared to Noel's code, we've eliminated enum and eliminated the recursive method call, but I'm not currently able to minimize it any further, and in particular, the fact that Bar must have the Foo[B, B] parameter puzzles me

and you need U and C: if there aren't type parameters on the method but you just use wildcards, the bug goes away

must it really be that complicated? there are so many parts here

[SethTisue]

aha, finally found something simpler in several respects:

sealed trait Foo[S, A]
final case class Bar[B]() extends Foo[B, B]
def pmat[U](scrut: Foo[U, String]): Unit =
  scrut match
    case Bar() =>

can't see any way to remove anything else (though it's hard to be 100% sure)

but it seems peculiar that this doesn't reproduce the bug:

sealed trait Foo[S, A]
final case class Bar[B]() extends Foo[B, B]
def pmat[U, C](scrut: Foo[U, C]): Unit =
  scrut match
    case Bar() =>

any fix should probably test all these variations, since it isn't clear what the one true minimization is — is it better to eliminate the case class parameter, or better to eliminate the use of a concrete type in the type of scrut? because afaict we must have one or the other to trigger the bug

[noelwelsh]

:clap: Nice one!