Skip to content

Exhaustiveness checking says a non-subtype is unhandled. #53486

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lrhn opened this issue Sep 11, 2023 · 3 comments
Open

Exhaustiveness checking says a non-subtype is unhandled. #53486

lrhn opened this issue Sep 11, 2023 · 3 comments
Assignees
Labels
area-dart-model For issues related to conformance to the language spec in the parser, compilers or the CLI analyzer. model-exhaustiveness Implementation of exhaustiveness checking

Comments

@lrhn
Copy link
Member

lrhn commented Sep 11, 2023

Example (inspired by from dart-lang/language#3337):

sealed class Result<T, E> {
  const factory Result.value(T value) = ValueResult<T>._;
  const factory Result.error(E error) = ErrorResult<E>._;
}

final class ValueResult<T> implements Result<T, Never> {
  final T value;
  const ValueResult._(this.value);
}

final class ErrorResult<E> implements Result<Never, E> {
  final E error;
  const ErrorResult._(this.error);
}

void main() {
  test(const Result.value(1));
  test(const Result.error("e"));
}

void test(Result<int, String> r, [bool b = false]){
  switch (r) { // Result<int, String>' not exhausted, doesn't match 'ValueResult<dynamic>()'
    case ValueResult<int> v: print(v.value);
    case ErrorResult<String> e: print(e.error);
  }
}

The error message given by both the analyzer and dart2js (using DartPad, master channel) is:

The type 'Result<int, String>' is not exhaustively matched by the switch cases since it doesn't match 'ValueResult<dynamic>()'.

However, ValueResult<dynamic> is not a subtype of the matched element type of Result<int, String>, so that type should not need to be matched.
(If I do match it, I get told to also match ErrorResult<dynamic>.)

If I forward both type arguments to the subclasses:

sealed class Result<T, E> {
  const factory Result.value(T value) = ValueResult<T, E>._;
  const factory Result.error(E error) = ErrorResult<T, E>._;
}

final class ValueResult<T, E> implements Result<T, E> {
  final T value;
  const ValueResult._(this.value);
}

final class ErrorResult<T, E> implements Result<T, E> {
  final E error;
  const ErrorResult._(this.error);
}

void main() {
  test(const Result.value(1));
  test(const Result.error("e"));
}

void test(Result<int, String> r, [bool b = false]){
  switch (r) {
    case ValueResult<int, String> v: print(v.value);
    case ErrorResult<int, String> e: print(e.error);
  }
}

then the error goes away, so it's something about the Never which makes the exhaustiveness algorithm think that ValueResult<int> doesn't exhaust the ValueResult-subtypes of Result<int, *>.

I can see how ValueResult<int> might only seem to match Result<int, Never>, not all of Result<int, String>, but it exhausts all ValueResults that are actually subtypes of Result<int, *>, no matter the second operand, and exhausting ValueResult<int> by itself should exhaust it as a subtype of Result<int, *> too.

Maybe it's the "spaces" computation which gets confused.

In any case, saying that I should match ValueResult<dynamic>, which is not related to the second type argument of Result either, doesn't provoke confidence.

@munificent
Copy link
Member

Maybe it's the "spaces" computation which gets confused.

Ah, yeah. I've had this in the back of my mind for a while. Take a look at this part of the exhaustiveness spec:


To expand a space s with type T, we create a new set of spaces that share
the same properties as s but with possibly different types and restrictions.
The resulting spaces are:

  • The declaration D of T is a sealed type:

    1. For each declaration C in the library of D that has D in an
      implements, extends, or with clause:

      1. If every type parameter in C forwards to a corresponding type
        parameter in D, then C is a trivial substitution for D.
        Let S be C instantiated with the type arguments of T.

        For example:

        sealed class A<T1, T2> {}
        class B<R1, R2> extends A<R1, R2> {}
      2. Else (not a trivial substitution) let S be an overapproximation
        (see below) of C.

        TODO: Is the overapproximation part here correct?

      3. If S exists and is a subtype of the overapproximation of T:

        1. A space with type S.

        Type S might not be a subtype if it constrains its supertype in
        a way that is incompatible with the specific instantiation of the
        sealed super type that we're matching against. For example:

        sealed class A<T> {}
        class B<T> extends A<T> {}
        class C extends A<int> {}

        Here, if we are matching on A<String>, then B<String> is a
        subtype, but C is not and won't be included. That means that this
        is exhaustive:

        test(A<String> a) => switch (a) {
          B _ => 'B'
        };

In cases where the relationship between a sealed supertype and its subtypes isn't just simple forwarding, the algorithm kind of gives up and takes a simpler conservative approach ("over-approximation").

@johnniwinther figured this all out on his own when implementing it since I didn't have anything approaching a complete design at the time (and what I had didn't cover generics at all). The approach is much better than I would have been able to come up with, but there might still be room to make it a little more sophisticated in cases like this.

At the time, I figured sealed classes hierarchies that (a) were also generic and (b) used the type parameters in non-simple-forwarding ways would be so obscure and rare as to not be worth worrying about. Unfortunately, I didn't realize that the obvious way to implement Option and Either types—probably the most common use of sum types!—happens to fall right into that set. :(

@johnniwinther
Copy link
Member

The real solution is to perform a constraint-solving. Given that I couldn't share that code between the analyzer and CFE, I chose the approximation to be able to implement a working solution in time for the feature release.

@lrhn
Copy link
Member Author

lrhn commented Sep 18, 2023

Let me see if I can read this. Take:

sealed class Result<R, E> {}
final class ValueResult<R> implements Result<R, Never> {}
final class ErrorResult<E> implements Result<Never, E> {}
void main() {
  Result<int, Error> r = null as dynamic; // Only here for the static errors.
  switch (r) { case ValueResult<int> _: ...; case ErrorResult<Error> _: ...}
}

When switching on (the type T) Result<int, Error>, we do:

  • Let D be the declaration of T, aka. sealed class Result<R, E>{}.
  • D is a sealed type.
  • For each declaration C which ... implements D (aka class ValueResult and class ErrorResult):
    • Not a trivial forwarding.
    • Let S be the overapproximation of C.
      • Those are ValueResult<Object?> and ErrorResult<Object?>
    • If S exists, which it does. (Is F-bounds why it can possibly not exist?)
    • And is a subtype of the overapproximation of T
      • That's undefined, overapproximation is defined on declarations, T is a type, should probably say D.
      • In which case its Result<Object?, Object?>.
      • And both are subtypes of that. (Again, is it F-bounds which can possilby make that fail?)
    • Then the space S (for the static types Value<Object?> and Result<Object?>).

Those spaces are, I think, the ones to exhaust in order to exhaust T.
So the switch (r) should exhaust ValueResult<Object?> and ErrorResult<Object?>, which it doesn't.
That explains the error message of not exhausting ValueResult<dynamic>.

And to solve that, we do need some kind of constraint solving, to know for which X, ValueResult<X> is enough to cover all instances of the intersection Result<int, Error> & ValueResult<Object?>.
This one looks easy (and we can possibly extend the "trivial forwarding" to trivally forwarding some parameters, and only overapproximate the rest), but that doesn't handle something more complicated, like:

sealed class Json<T> {
  T get value;
}
abstract final class JsonList<T> extends Json<List<T>> {
  final List<T> value;
  T operator[](int index) => value[index];
}
abstract final class JsonMap<T> extends Json<Map<String, T>> {
  final Map<String, T> value;
  T? operator[](String key) => value[key];
}
abstract final class JsonLiteral<T> extends Json<T> {
  final T value;
}

where we might need to solve Json<Iterable<int>> & JsonList <: JsonList<T> for T. (T = int is the optimal solution, and even this is in the easy end of complicated cases.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area-dart-model For issues related to conformance to the language spec in the parser, compilers or the CLI analyzer. model-exhaustiveness Implementation of exhaustiveness checking
Projects
None yet
Development

No branches or pull requests

4 participants