Subtype constraint solving is incomplete, so GADT exhaustiveness checking could be unsound

[Blaisorblade]

While trying to explain why #3645 is fixed by #3646, I've found a potential loophole in the proof I've sketched.

Consider checking exhaustiveness of the match in f. Since there's no case for C3, the match is exhaustive if and only if v: Root[Foo] cannot be an instance of C3 <: Root[C].
So, we must check if we can instantiate Foo such that Root[Foo] can be an instance of C3 (that is, if Root[Foo] <:< Root[C]); the match is exhaustive if such an instantiation is impossible. That's the logic of #3646.

However, Dotty's constraint solver is not complete, so it cannot show in general that an instantiation is impossible, as documented in

https://github.com/lampepfl/dotty/blob/2a85106974ce5620eabbf4658810ddb917465145/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L966, https://github.com/lampepfl/dotty/blob/2a85106974ce5620eabbf4658810ddb917465145/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L507

However, to trigger incompleteness, we need the constraint solver to run into a disjunction D1 where both branches give satisfiable constraint, choose the first branch, then run into another constraint which is unsatisfiable under the first branch of D1, but satisfiable under the second branch of D1.

If the issue can be triggered, an "easy" fix would be to have constraint solving detect when it runs into potential incompleteness, and signal that to the caller somehow. But details are tricky.

Action items:

• try to construct such examples (for me).
• if found, decide a course of action.

It could get a new checking mode (where we only want to get false if we're sure), or return Option[Boolean] so that if we detect incompleteness we fail. Some details are open, since a success is supposed to also give a substitution usually — luckily, that's not needed for checking missing branches, but it's needed in the converse case, when checking that present branches are reachable; if a branch is reachable we want to refine type variables correctly. Maybe in the incomplete cases we should just not refine type variables at all, to be safe.

/cc @alexknvl @liufengyun .

[Blaisorblade]

I expect such an example would require at least two pattern matches. But while trying to construct an issue I run into #4030.

Using nested pattern matches might also cause trouble. Even before this issue, we could see if what is deduced by <:< is used to refine type variables; that's unsound in the presence of disjunctions/incompleteness because the constraints from <:< aren't necessarily implied by it.

[Blaisorblade]

It could get a new checking mode (where we only want to get false if we're sure), or return Option[Boolean] so that if we detect incompleteness we fail.

To be sure, if you implemented this Option[Boolean] is too slow but you'd realize it as a 3-value type without boxing. But you still want the same basic semantics of "yes/no/dunno", for which Option[Boolean] is a good conceptual model.