Consider expanding flow analysis' ability to prove that a pattern "always matches"

[stereotype441]

Today I spent some time writing some toy analysis code using patterns. I was building up a switch statement on an as-needed basis, so I had a default clause to handle the cases I hadn't written yet. The code looked like this:

  ir.CodeReference lowerElement(ExecutableElement element) {
    switch (element.enclosingElement) {
      case ClassElement class_:
        return ir.ClassMemberReference(
            Uri.parse(element.library.definingCompilationUnit.uri!),
            class_.name,
            element.name);
      default:
        throw 'TODO(paulberry): ${element.enclosingElement.runtimeType}';
    }
  }

Then I got the bright idea that instead of a default clause, I ought to be able to use an object pattern, i.e.:

  ir.CodeReference lowerElement(ExecutableElement element) { // (1)
    switch (element.enclosingElement) {
      case ClassElement class_:
        return ir.ClassMemberReference(
            Uri.parse(element.library.definingCompilationUnit.uri!),
            class_.name,
            element.name);
      case Object(:var runtimeType):
        throw 'TODO(paulberry): $runtimeType';
    }
  }

But this didn't work. The analyzer produced an error at (1): "The body might complete normally, causing 'null' to be returned, but the return type, 'CodeReference', is a potentially non-nullable type." But in truth, the switch statement is exhaustive (because the type of element.enclosingElement is non-nullable). Flow analysis just wasn't smart enough to see that it was.

In the general case, it's not possible for flow analysis to be as smart as the exhaustiveness algorithm. This is a known limitation of the design of the compilation pipeline, and we have discussed it elsewhere (for example, dart-lang/sdk#51926 (comment)).

However, flow analysis does understand that variable and wildcard patterns might always match (because the type of the pattern is a supertype of the matched value type), and in those cases it considers the switch to be exhaustive. I think it would be worth expanding the set of patterns that flow analysis recognizes as "always matching" to include:

• A cast pattern, if the subpattern is always matching
• A list pattern of the form [...], if the required type is a supertype of the matched value type
• A logical and pattern, if both subpatterns are always matching
• A logical or pattern, if either of the subpatterns is always matching
• A null check pattern, if the matched value type is non-nullable and the subpattern is always matching
• A null assert pattern, if the subpattern is always matching
• An object pattern, if the required type is a supertype of the matched value type and all subpatterns are always matching
• A record pattern, if the required type is a supertype of the matched value type and all subpatterns are always matching

That would allow the example above to work. It would also reduce the number of situations where flow analysis and the exhaustiveness algorithm disagree about whether a switch is exhaustive, which should reduce user pain (see #2977).

(Note that if we were to implement this functionality prior to removing support for mixed-mode null safety, we would have to be careful to make sure that this didn't lead to unsoundness escalation (see #1143).

[stereotype441]

After further experimentation, it appears that flow analysis can't even tell that case var x, or case _ are always matching.

[stereotype441]

I've got a fix out for review that addresses nearly all of the above: https://dart-review.googlesource.com/c/sdk/+/293860. I'll see if I can get it reviewed and landed before the beta cut.

[lrhn]

I think we can elaborate the rules a little, based on the matched value type.

A pattern always matches a matched value type M, when it's:

• A variable pattern with no type, var _, _, etc.
• A variable pattern with type T, T x or T _, where M <: T
  • (Is that the same as "M is a subtype of the the required type"?)
• A cast pattern, p as T, if the subpattern p is always matching T (or matching M, but probably only check T?)
• A list pattern of the form [...], if M implements List
• A list pattern of the form [...], if M implements List<Y> and Y <: X
• A logical and pattern, if both subpatterns are always matching M
• A logical or pattern, if either of the subpatterns is always matching M
• A null check pattern p?, if the M is definitely not nullable p is always matching M
• A null assert pattern, p!, if p is always matching NON_NULL(M)
• An object pattern, if the required type is a supertype of the M and all subpatterns are always matching the static type of the corresponding getters of M.
• A record pattern, if the required type is a supertype of the matched value type (aka. has the same shape) and all subpatterns are always matching the corresponding static field types of M
• A relational pattern == null if M is Null.
• A relational pattern != null if M is definitely not nullable.

The only real change is the NON_NULL for p! and using the type T for p as T, and including [!=]= null. The rest are just "M is subtype of required type for type checks, and sub-patterns always match static type of the property they check".
(I assume _ and T x were already covered by the existing type checking.)

[stereotype441]

This was fully implemented in time for the beta branch, except for two things:

• some list patterns (e.g. [...]) weren't recognized as trivially exhaustive (Flow analysis detection of trivial exhaustiveness fails to understand [...]. sdk#52017)
• null-check patterns aren't currently recognized as trivially exhaustive when the matched value type is non-nullable (Flow analysis doesn't recognize that null check patterns always match a non-nullable type sdk#52084)

The first of these was fixed and cherry-picked to the beta branch. The second is still outstanding.

Since the feature now works as intended except for one bug, I'm going to close this issue and track the remaining work in dart-lang/sdk#52084.