Untyped variable and wildcard patterns are not guaranteed to match

[stereotype441]

Consider the following code:

f(int i) {
  if (i case _) {
    print('matched');
  } else {
    print('unreachable');
  }
}

Can this code ever print unreachable? It seems like it should be impossible. But based on my reading of the spec, I think it could. _ is considered by type inference to be equivalent to int _, which means that the match will fail if the runtime type of i is not a subtype of int. In a program that's not fully migrated to null safety, it's possible that i will have the value null.

This is really unfortunate, because even though this is unlikely to arise very often in practice, flow analysis has to reflect the semantics precisely (to avoid unsoundness escalalation), and therefore the else branch can't be flagged as unreachable code.

We could fix this by changing this line from the spec (from Runtime semantics > Matching > Variable):

2. If the runtime type of v is not a subtype of T then the match fails.

To something like:

2. If the matched value type M is not a subtype of T, and the runtime type of c is not a subtype of T, then the match fails.

In other words, if the variable pattern looked like it was guaranteed to match based on static analysis, then it would be guaranteed to match. And therefore all untyped variable and wildcard patterns would be guaranteed to match.

Note: there would be a negative consequence to that. A program like this could print i = null in a program that's not fully migrated:

f(int i) {
  if (i case int x) {
    print('i = $x');
  }
}

I personally think that's ok. IMHO it's no worse than the other examples of mixed mode unsoundness we have in Dart today, and it's way less bad than allowing _ to sometimes fail to match.

[stereotype441]

CC @munificent @leafpetersen @jakemac53 @lrhn @mit-mit @natebosch @eernstg @kallentu

[stereotype441]

We discussed this in the language team meeting today. We considered several possible courses of action:

1. Stick with the spec as it is (i.e. do a type check, and if it doesn't match it doesn't match). Therefore, flow analysis has to consider the "unreachable" code above to actually be reachable.
2. Do a type check, but if it doesn't match then throw an exception. That way flow analysis can correctly classify the "unreachable" code above as unreachable, and null can never flow into a pattern in an unexpected way, even in a mixed mode program.
3. Specify _ as something different from a variable pattern, and specify that it always matches regardless of the types involved and whether the program is a mixed mode program. That way flow analysis can correctly classify the "unreachable" code above as unreachable.
4. Specify that if the static type of the matched value is a subtype of the pattern type, there is no check implied. I believe this is equivalent to my proposal above.

There seemed to be a general consensus that:

• bare _ should never imply a type check, even in mixed mode programs
• it would be nice if we didn't have to bake a bunch of invisible if (v == null) throw checks into mixed mode programs, because that would bloat executable size and affect runtime performance.
• It would be nice if a user could say case var x: as the last case of a case statement, and have it behave the same as default: (in other words, it would be nice for case var x: to match everything, even an unsound null arising from a mixed mode program).

We decided to go with option 4, which meets all these requirements.

We also briefly discussed whether we should adopt a similar rule for other kinds of patterns, e.g. object patterns. I believe the consensus was that yes, we should. So for instance, this code would compile to a no-op (null passes through and the throw is unreachable):

f(int i) {
  if (i case int()) {
    // Do nothing
  } else {
    throw 'unreachable';
  }
}

Similar for this:

f(List l) {
  if (l case [...]) {
    // Do nothing
  } else {
    throw 'unreachable';
  }
}