Generalize exhaustiveness checking for non-trivial generics

[eernstg]

See dart-lang/sdk#60260 for some background. Thanks to @TekExplorer for bringing this up!

Dart's exhaustiveness analysis recognizes many situations where a switch is guaranteed to cover all possible values of the scrutinee, including having a catch-all case at the end, covering all the values of an enumerated type, or covering each of the classes that are the immediate subtypes of a sealed class.

However, the current analysis only covers a few special cases when it comes to type arguments. For example:

sealed class A<X, Y> {}

class B1<X> implements A<X, Never> {}
class B2<Y> implements A<Never, Y> {}

int f(A<String, Exception> a) => switch (a) { // Error: not exhaustive.
  B1<String>() => 1,
  B2<Exception>() => 2
};

The only situations that may occur at run time are the following:

• a is a B1<T> for some T which is a subtype of String.
• a is a B2<S> for some S which is a subtype of Exception.

This means that the switch is actually exhaustive, but the exhaustiveness analysis is not able to prove it. This issue serves as a reminder that we might be able to generalize the current exhaustiveness analysis in order to cover more cases.

[lrhn]

It's been noticed before: #3633, #3866, #4199

We really should try to fix it, it keeps coming up.

[TekExplorer]

It's been noticed before: #3633, #3866, #4199

We really should try to fix it, it keeps coming up.

yes please! the feature is effectively broken - and the workaround ends up being to include the unused type in the subtypes, which makes the API worse.

[eernstg]

Here's an idea about how this could be done:

Checking the example here and in #3633, #3866, and #4199, it looks like we're only talking about the situation where the scrutinee type is sealed.

It seems likely that we could have similar considerations for FutureOr<T> being split into Future<T> and T, where T is a generic type, but the case where the scrutinee type is sealed is still at the core. So let's focus on that one.

For simplicity, we don't consider the possibility that type parameters could be contravariant or invariant (the approach would need to be generalized a bit in order to handle that, but it should be doable).

The basic idea is that for a switch whose scrutinee type A<...> is sealed, we will check that for each immediate subtype Bj<...> of A<...> that every scrutinees of type A<...> which is also of type Bj<...> is matched by that case.

Assume the following hierarchy, where the kind of the subtype relationship from the sealed type to each of its immediate subtypes can vary freely (that is, it could be implements, extends, or on for a mixin, but I'm using extends everywhere here, just to avoid some verbosity):

sealed class A<X1 extends Bx1 .. Xk extends Bxk> .../*superinterfaces: not important*/... {}

class B1<Y1 extends By1 .. Yn extends Byn> extends A<T1 .. Tk> {}
class B2<Z1 extends Bz1 .. Zm extends Bzm> extends A<S1 .. Sk> {}

Consider the following switch expression:

int example(A<U1 .. Uk> a) => switch (a) {
  B1<V1 .. Vn>() => 0,
  B2<W1 .. Wm>() => 0,
};

In order to decide whether or not this switch expression is exhaustive, we could do the following:

Perform the matching Uj <# Tj [Y1 .. Yn] -> Cj for j in 1 .. k where Tj contains one or more type variables. If the match fails then the B1 case does not cover all the possible scrutinee values of type B1, and if there are no other B1 cases then we know that the switch is non-exhaustive.

For all type variables Yj that do not have a constraint, we add the constraint that it must be a supertype of its bound (that is, if the scrutinee type doesn't give us a lower bound then the given type variable must "cover everything"). Let C1 .. Cp be all the constraints after those constraints have been added.

Otherwise (when the match succeeds), we know that any binding of Y1 .. Yn that satisfies C1 .. Cp is guaranteed to ensure that the matched subtype relationships hold. In particular, we can substitute Vj for Yj in C1 .. Cp, and if this turns the constraints into provable subtype relationships then it is guaranteed that every scrutinee of type B1<...> will be matched by B1<V1 .. Vn>().

The same approach determines whether B2<W1 .. Wm>() is guaranteed to match every scrutinee whose type is B2, and similarly for each further case if we're dealing with a bigger sealed family of classes.

Because of the definition of sealed, this is sufficient to conclude that the switch as a whole is exhaustive.

It is worth noting that the match is kind of upside down, in the sense that we make sure the pattern B1<V1 .. Vn>() uses type arguments such that B1<V1 .. Vn> has a superinterface A<R1 .. Rk> such that A<U1 .. Uk> <: A<R1 .. Rk>. That is, we're requiring that the pattern on the subtype B1 is broad enough to include all possible scrutinees (whose type is a subtype of A<U1 .. Uk>) . It is much more common that we wish to check something like B1<V1 .. Vn> <: A<U1 .. Uk>, but in that case the match has the opposite direction (if B1<V1 .. Vn> has superinterface A<R1 .. Rk> then we need to check that A<R1 .. Rk> <: A<U1 .. Uk>). So it's unusual, but it makes sense when one thinks about it. Twice, perhaps. ;-)

@johnniwinther, WDYT?

[Correction, Mar 18: Add the constraint that we don't match Uj with Tj when Tj does not contain any type variables.]

[eernstg]

Let me try to unfold the idea I mentioned on the concrete example:

sealed class A<X, Y> {}

class B1<X> implements A<X, Never> {}
class B2<Y> implements A<Never, Y> {}

int f(A<String, Exception> a) => switch (a) {
  B1<String>() => 1,
  B2<Exception>() => 2
};

We have exactly one case for B1 and one case for B2, so we just need to check that the B1 case covers all the possible scrutinees of type B1<...>, and similarly for B2<...>.

We need to match String <# X [X] -> C1 which is satisfied with the constraint set C1 == {String <: X <: _}. For B2<...>, we match Exception <# Y [Y] -> C2 yielding C2 == {Exception <: Y <: _}.

So the set of all constraints is {String <: X <: _, Exception <: Y <: _}. Next, we check that the actual type arguments in the cases yield subtype relationships that hold: String <: String and Exception <: Exception, so that's OK.

This implies that if o is a scrutinee (hence, of type A<String, Exception>) and o is also of type B1<...> then o must have a type which is a subtype of B1<String>. Similarly for the case where o has type B2.

Hence, the switch is exhaustive.

If we consider switch (a) { B1<Object>() => 1, B2<Object>() => 2} then the subtype relationships will also hold: String <: Object and Exception <: Object, so that's also an exhaustive switch. However, with switch (a) { B1<int>() => 1, B2<Object>() => 2} we fail to satisfy String <: int which means that the switch isn't exhaustive for B1.

---

Note that this is not a complete solution (we don't have any guarantees that such a solution exists, or that it can be built using matching).

One case which is not covered is the case where some type arguments are involved, but the subtype still restricts the possible actual type arguments to a proper subset:

sealed class C<X, Y> {}
class D1<X, Z> extends C<X, List<Z>> {}
class D2<U extends num, Y> extends C<List<U>, Y> {}

int g(C<Iterable<Comparable<num>>, Iterable<String>> c) => switch (c) {
  D1<Iterable<Object>, String>() => 1,
  D2<num, Iterable<String>>() => 2,
};

For D1, we need to match Iterable<Comparable<num>> <# X [X] -> C1 yielding C1 == {Iterable<Comparable<num>> <: X <: _} and Iterable<String> <# List<Z> [Z] -> C2 which has no solution. The point is that we can't choose a value for Z such that it is guaranteed that Iterable<String> <: List<Z>. This isn't necessary because we know that the second type argument must be List<...> when the scrutinee has type D1, but we'd need another step (a recursive one) which would transform the match into List<String> <# List<Z> [Z] -> C2b, yielding C2b == {String <: Z <: _}.

This means that we can't use this technique when the dependency structure among the type variables and superinterfaces is too complex, unless we generalize the approach with this recursive step.

For D2, we need to match Iterable<Comparable<num> <# List<U> [U] -> C3, possibly transformed into List<Comparable<num>> <# List<U> [U] -> C3b yielding C3b == {Comparable<num> <: U <: _}. Similarly, Iterable<String> <# Y [Y] -> C4 yielding Iterable<String> <: Y <: _.

Inserting the actual type arguments of the cases we get Iterable<Comparable<num>> <: Iterable<Object>, String <: String, and Comparable<num> <: num <: _. Again, we need to generalize the technique in order to handle this kind of switch.

[johnniwinther]

cc @chloestefantsova

[eernstg]

Here's another perspective on the task. It's directly derived from the mathematical structure of the task which means that it doesn't say much about a solution. However, it can still be useful as a backstop: If you think you have a solution then you can use this as a sanity check: Every solution must belong to the set of solutions that are implied by this characterization:

For any given scrutinee e with static type S<T1 .. Tk> where S is a sealed class, we can derive a space Space(S<T1 .. Tk>) that describes all the possible scrutinees.

For each immediate subtype of S, let's call them A1 .. Ak, we can derive a space Space(Aj<Object?, ... Object?>) that includes every object of type Aj (no matter which actual type arguments it has).

(Note that Aj may be able to use the specified bounds rather than Object? for some actual type arguments, but Object? for all type arguments is a super-bounded type which is a safe bet because it also works with F-bounded type parameters.)

For each j, we want to find the intersection SPj = Space(S<T1 .. Tk>) ∩ Space(Aj<Object?, .. Object?>), and then we want to confirm that the union of all cases in the switch for the case Aj covers all of it: SPj ⊆ Space(AjCase1) ⋃ .. ⋃ Space(AjCaseN).

The switch is exhaustive if and only if this subset relation holds. The algorithm I've hinted at in the previous comments covers some special cases of this relation (in particular, I assumed exactly one case per subtype).

Another important special case arises when there is a case for Aj that covers all possible type arguments of Aj. This means that we will match every scrutinee of type Aj<...>, which is of course enough to ensure that we will match every scrutinee which belongs to an intersection of Aj instances with any other set. In other words, we can always fall back on Aj<Object?, .. Object?>() and similar patterns that are known to match all objects of type Aj.

Conversely, if there is an element o in SPj which is not in said union Space(AjCase1) ⋃ .. ⋃ Space(AjCaseN) then o could be a scrutinee, but o is not matched by any of the cases AjCase1 .. AjCaseN, which is a soundness violation. In other words, there's no way we can find an even better solution than the ones that satisfy SPj ⊆ Space(AjCase1) ⋃ .. ⋃ Space(AjCaseN).