Incorrect non-exhaustivity warning in pattern matches

[nrinaudo]

Compiler version

3.1.2

Minimized code

enum Foo[A, B]:
  case Bar[A]() extends Foo[A, A]

def doFoo[A](foo: Foo[A, String]): String = foo match
  case Foo.Bar() => "baz"

Output

[warn] -- [E029] Pattern Match Exhaustivity Warning: /path/to/gadt/src/main/scala/repro.scala:6:44 
[warn] 6 |def doFoo[A](foo: Foo[A, String]): String = foo match
[warn]   |                                            ^^^
[warn]   |                                  match may not be exhaustive.
[warn]   |
[warn]   |                                  It would fail on pattern case: Foo.Bar()

Expectation

I would expect this not to warn, since there's a clear case Foo.Bar() => ... statement.

[nrinaudo]

This might also need a GADT tag. I didn't realise while minifying the reproduction scenario, but isn't it exactly Refl?

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

[nrinaudo]

Interestingly, this compiles without a warning:

enum Foo[A, B]:
  case Bar[A]() extends Foo[A, A]

def doFoo[A](foo: Foo[A, String]): Foo[A, String] = foo match
  case Foo.Bar() => Foo.Bar()

And this has a rather interesting warning:

enum Foo[A, B]:
  case Bar[A]() extends Foo[A, A]

def doFoo[A](foo: Foo[A, String]): Foo[A, String] = foo match
  case s @ Foo.Bar() => s

[warn] -- [E029] Pattern Match Exhaustivity Warning: /path/torefl/src/main/scala/repro.scala:6:52 
[warn] 6 |def doFoo[A](foo: Foo[A, String]): Foo[A, String] = foo match
[warn]   |                                                    ^^^
[warn]   |                                  match may not be exhaustive.
[warn]   |
[warn]   |                                  It would fail on pattern case: Foo.Bar()
[warn] -- Unchecked Warning: /path/to/refl/src/main/scala/repro.scala:7:7 
[warn] 7 |  case s @ Foo.Bar() => s
[warn]   |       ^
[warn]   |       the type test for repro.Foo.Bar[A] cannot be checked at runtime