[Patterns] Should List and/or Map patterns be considered for exhaustiveness?

[leafpetersen]

The patterns proposal lists a small set of types which are considered for exhaustiveness:

bool
Null
A enum type
A type whose declaration is marked sealed
T? where T is exhaustive
FutureOr<T> for some type T that is exhaustive
A record type whose fields are all exhaustive types

List and Map are not included in this list, which suggests that code like the following will not be considered for exhaustiveness checking:

switch([3]) {
  [] => "Empty",
  [var x, ...] =>  "$x"
}

I believe the code above will be considered an error, since there is no default, and the type in question is not an exhaustive type.

Should we include List and Map as exhaustive types? The code above seems like really good code to allow. On the other hand, List and Map are not sealed types, so we probably (possibly?) don't want to require full exhaustiveness:

class MySpecialList() implements List<int> {...}
switch([3]) {
   case MySpecialList(): print("Special List");
}

Should we treat List (and possibly Map) as types which are exhaustive types only WRT to length? That is, we require that all lengths are covered, but not necessarily all subtypes? And if so, to what extent do we generalize this to explicit calls to the length getter, as opposed to only considering explicit patterns. Does the following get an exhaustiveness error?

switch([3]) {
  List(length: <1) => "Empty",
  [var x, ...] =>  "$x"
}

This would seem to start to require more reasoning about integers than we necessarily want to do.

Perhaps the correct way to think about this is to separate out what we can show to be exhaustive from what we require to be exhaustive? That is, we say:

• A switch statement is required to be exhaustive (and hence is only checked for exhaustiveness) only if the scrutinee has an exhaustive type as defined above.
• A switch expression is always required to be exhaustive, and is always checked for exhaustiveness
• Exhaustiveness checking may take into account more than just the set of exhaustive types, and hence there will be switch expressions which are proved exhaustive which would not be considered for exhaustiveness checking as switch statements.

For flow analysis and type inference, we have proposed that reachability for switch statement be driven entirely based on whether or not the type of the scrutinee is an exhaustive type (or if there is an explicit default). This would imply that there are switch statements which will be assumed to be non-exhaustive, but which are in fact exhaustive, and could be proven so if turned into switch statements.

Example:

class A {
  final bool value;
  A(this.value);
}
void test(A a) {
  int x;
  // A is not an exhaustive type, so this switch is assumed to be non-exhaustive
  switch(a) {
    case A(value:true): x = 0;
    case A(value:false): x = 1;
  }
  x.isEven; // Error, x is not definitely assigned
}
void test(A a) {
  int x;
  (switch(a) {
    A(value:true) => x = 0,
    A(value:false) => x = 1
  })
  x.isEven; // Ok, x is definitely assigned.
}

cc @munificent @eernstg @lrhn @kallentu @natebosch @jakemac53 @stereotype441 @johnniwinther