Pattern match on GADT not recognizing case as impossible (regression from Scala 2)

[Kazark]

I tried searching around to see if this was a duplicate issue. I found a lot of issues around GADTs and pattern matching but didn't think the code in any of them were as simple as in this one. I hope this is not a duplicate.

Compiler version

3.0.0

Minimized code

Written with Scala 2 syntax for easy 🍎 to 🍏 comparison:

sealed trait Foo[A]
final case class Bar(value: String) extends Foo[String]

object Example {
  def whatthe[A, B]: Foo[A => B] => Unit = {
    case Bar(_) => ()
  }
}

Result

The compilation succeeds in Scala 3.

Expectation

A compilation error similar to the one that I get if I try to compile the same code in Scala 2.13.6:

error: constructor cannot be instantiated to expected type; found : Bar required: Foo[A => B]

[abgruszecki]

/cc @liufengyun could you remind me, did you end up adding support for GADT-aware exhaustivity checks?

[liufengyun]

/cc @liufengyun could you remind me, did you end up adding support for GADT-aware exhaustivity checks?

We do have some support by checking the counter-examples. But I don't think it's bullet-proof.

For the example above, it's exhaustive, because Foo[A => B] has no children. And the unreachable check is not triggered, because there is only one case.

[Kazark]

@liufengyun FWIW this is a simplification of an example where there were multiple cases, some of which matches Foo[A => B], and when I left the case that didn't match it out, it triggered this.

[Kazark]

Any news on where this is on the roadmap? This is a blocker for me to upgrade to Scala 3.

[abgruszecki]

@Kazark I'll see about taking a look. Fengyun's comment suggest that a fix might be relatively simple.

[dwijnand]

That Scala 2 error isn't an exhaustivity error, it's a typer error, because the match doesn't type. And I think it's right (or, rather, I can't think why Scala 3 thinks that's wrong), so I think the fix is in typing the case.

[SethTisue]

SLS 8.5 states unambiguously that the pattern matching anonymous function desugars as follows:

def whatthe[A, B]: Foo[A=>B] => Unit = new (Foo[A => B] => Unit) {
  def apply(x: Foo[A => B]): Unit = x match { case Bar(_) => () }
}

Scala 2 and Scala 3 are both consistent about handling the sugary and desugared versions the same (Scala 2 same error in both cases, Scala 3 no error in both cases). So we can disregard the pattern-matching-anonymous-function aspect of this and deal directly with the raw pattern match.

We can also minimize it further to just:

def whatthe[A, B](x: Foo[A => B]): Unit =
  x match { case Bar(_) => () }

again, Scala 2 gives a type error, Scala 3 accepts it.

And note that Scala 2 isn't only rejecting the code because there's a single case. It still rejects it even if you put a catchall case in:

def whatthe[A, B](x: Foo[A => B]): Unit =
  x match { case Bar(_) => (); case _ => () }

[SethTisue]

The minimized form is governed by SLS 8.4 (Pattern Matching Expressions), which states:

Here the pattern type doesn't conform either to Function1[A, B] (1st clause in quoted passage) or Function1[undefined, undefined] (2nd clause), so as I read it, the spec does require that we issue a hard type error (and not just an unreachable warning) here. So Dale is right and Scala 3 is just wrong here.

(I went down sort of a mental garden path of thinking this ought to be just an unreachable warning, but I was forgetting that "unreachable" refers primarily to a clause being unreachable in reference to previous clauses which have caused a following clause to become impossible to reach.)

[SethTisue]

Minimized even further:

def whatthe(x: Foo[Int]): Unit =
  x match { case Bar(_) => () }

No additional type parameters, no Function1.

So this bug is really quite fundamental.

(Even Scala 2.7 issues an error in this case; I looked in the Scala 2 history and the code for this seems to go all the way back to the initial commit of SOCOS, and perhaps because it's so old, there's no test coverage to speak of.)

[SethTisue]

in Applications.scala, Dale found this relevant comment:

            // We ignore whether constraining the pattern succeeded.
            // Constraining only fails if the pattern cannot possibly match,
            // but useless pattern checks detect more such cases, so we simply rely on them instead.
            withMode(Mode.GadtConstraintInference)(TypeComparer.constrainPatternType(unapplyArgType, selType))

First, this ("ignore whether...") seems like a peculiar choice, because if we've detected early that the pattern cannot possibly match, why wouldn't we report the error right then and there? The comment got reworded later but originally dates back to d25f03c3c188aa23af278fa2d471588e785e2fea (2019); perhaps @abgruszecki could explain his thinking on this...?

Second, we're finding in debugging that constrainPatternType doesn't fail! (We don't know why, yet.)

So one possible fix plan is to address both of those: make constrainPatternType fail, and then don't ignore the failure.

Another possible fix plan would be to leave this stuff alone and catch it downstream in the "useless pattern checks" (redundancy checking) instead. (Though those checks are just warnings and we're supposed to be issuing a hard error here...)