Incorrect exhaustivity warning in pattern matches with GADTs

[nrinaudo]

Compiler version

3.3.1

Minimized code

enum Eq[A, B]: 
  case Refl[A]() extends Eq[A, A]
  
enum T[A]:
  case S(witness: Eq[A, String])
  case I(witness: Eq[A, Int])

def partial(tagged: T[Int]) : Int =
  tagged match
    case T.I(Eq.Refl()) => 0

Output

match may not be exhaustive.
It would fail on pattern case: T.S(_)

Expectation

This warning is incorrect: it's impossible to produce an Eq[A, B] where A and B are distinct, so a T[Int] must be a T.I: a T.S would need an Eq[Int, String], which is impossible.

[sjrd]

That seems like a pretty far-fetched reasoning. I don't think we can expect GADT reasoning to go look that far to rule out cases.

The more standard way to model this constraint would be

enum T[A]:
  case S extends T[String]
  case I extends T[Int]

which would fall into what GADT is meant to perform.

[s5bug]

Also occurs on Scala 3.4.2-RC1-bin-20240213-8776677-NIGHTLY-git-8776677.

I wonder if this is related:

enum Eq[A, B] {
  case Refl[A]() extends Eq[A, A]
}

def foo(x: Eq[Int, String]): Unit = x match { case Eq.Refl() => ??? }
// does not issue an "unreachable case" warning

I want to believe that if the compiler realized Eq[Int, String] was empty, it would also believe that T.S is not meant to match a T[Int].

scala> enum Eq[A, B] {
     |   case Refl1[A]() extends Eq[List[A], List[A]]
     |   case Refl2[A]() extends Eq[Option[A], Option[A]]
     | }
// defined class Eq

scala> def foo(x: Eq[Int, String]): Unit = x match { case Eq.Refl1() => ???; case Eq.Refl2() => ??? }
def foo(x: Eq[Int, String]): Unit

scala> def foo(x: Eq[List[Int], Option[Int]]): Unit = x match { case Eq.Refl1() => ???; case Eq.Refl2() => ??? }
def foo(x: Eq[List[Int], Option[Int]]): Unit

scala> def foo(x: Eq[List[String], List[Int]]): Unit = x match { case Eq.Refl1() => ???; case Eq.Refl2() => ??? }
1 warning found
-- [E030] Match case Unreachable Warning: --------------------------------------
1 |def foo(x: Eq[List[String], List[Int]]): Unit = x match { case Eq.Refl1() => ???; case Eq.Refl2() => ??? }
  |                                                                                       ^^^^^^^^^^
  |                                                          Unreachable case
def foo(x: Eq[List[String], List[Int]]): Unit

[dwijnand]

That seems like a pretty far-fetched reasoning. I don't think we can expect GADT reasoning to go look that far to rule out cases.

This looks in line with things we're able to do in exhaustivity checking, currently. So I'll have a look.

@s5bug

I want to believe that if the compiler realized Eq[Int, String] was empty, it would also believe that T.S is not meant to match a T[Int].

No, we only warn that a case is unreachable because a previous case handles all values covered by the case in question. We don't use match analysis to as a way to indicate that the scrutinee being matched could be understood to be uninhabited, just like we don't do that kind of linting for an if, or a method call, etc.

[nrinaudo]

No, we only warn that a case is unreachable because a previous case handles all values covered by the case in question. We don't use match analysis to as a way to indicate that the scrutinee being matched could be understood to be uninhabited, just like we don't do that kind of linting for an if, or a method call, etc.

Is that true though? I might misunderstand your reply, but here's some code I wrote a while ago which seems to imply differently (again, provided I understood what you meant):

enum Command[Before, After]:
  case Face(dir: Direction) extends Command[Idle, Idle]
  case Start                extends Command[Idle, Moving]
  case Stop                 extends Command[Moving, Idle]
  case Chain[A, B, C](
    cmd1: Command[A, B],
    cmd2: Command[B, C]
  ) extends Command[A, C]

def movingLabel(cmd: Command[Moving, _]) = cmd match
  case Command.Stop              => "stop"
  case _: Command.Chain[_, _, _] => "chain"

This compiles without a warning even though movingLabel doesn't handle Command.Face.

[dwijnand]

"doesn't handle Command.Face" isn't the test for "unreachable", which is what I was responding about. The problem is in the name "unreachable". Internally it used to be referred to "redundant", perhaps that's a better name. The test is "does the sum of all previous cases handle the values covered by this case?".

[nrinaudo]

Is the distinction you're making between a branch that the types make impossible (such as Command.Face) as opposed to one that is covered by previous branches?

If so, I guess it's not super clear to me why T.S is the latter rather than the former. It feels like it's not covered by T.I, but impossible because T.S can never have type T[Int].

[dwijnand]

I never said T.S is unreachable. The first thing I said is that I agreed with you that your false positive exhaustivity warning report is valid, and that we'll see if it's possible to fix the logic.

Then I moved to @s5bug's comment, which is about a false negative reachability warning (a claim that the compiler wasn't, but should be, emitting an unreachable warning) and I responded explaining how that's not what we mean by unreachable (and how it's probably a misnomer at this point).

[nrinaudo]

Ah, that makes sense, I hadn't understood that you were addressing another comment! my apologies.