Flow analysis. No promotion in case of shared case scope and assignment in `when` part

[sgrekhov]

If switch statement variable is assigned in when part then no promotion occurs if case scope is shared. Why there is no promotion in test2() below?

test1(Object? x) {
  switch (x) {
    case int v when (x = 42) > 0:
      x.expectStaticType<Exactly<int>>(); // Ok, promoted
    case _:
      x.expectStaticType<Exactly<Object?>>();
  }
}

test2(Object? x) {
  switch (x) {
    case int v when (x = 42) > 0:
    case int v:
      x.expectStaticType<Exactly<Object?>>(); // No promotion
    case _:
      x.expectStaticType<Exactly<Object?>>();
  }
}

T expectStaticType<R extends Exactly<T>>() {
  return this;
}

typedef Exactly<T> = T Function(T);

cc @stereotype441

Dart SDK version: 3.9.0-95.0.dev (dev) (Sun May 4 21:03:05 2025 -0700) on "windows_x64"

[stereotype441]

test2(Object? x) {
  switch (x) {
    case int v when (x = 42) > 0:
    case int v:
      x.expectStaticType<Exactly<Object?>>(); // No promotion
    case _:
      x.expectStaticType<Exactly<Object?>>();
  }
}

It's true that at the line marked // No promotion, x must be an int. But proving that this is the case requires more complex reasoning than flow analysis is capable of performing.

See dart-lang/co19#3169 (comment) for an informal description of how flow analysis handles pattern matches and switch statements. In brief, here's what happens in this example:

• After visiting the scrutinee of the switch statement (x), flow analysis creates a shadow variable to represent the matched value. Let's call it $scrutinee.
• Since the scrutinee refers to something promotable, flow analysis makes a note of what the scrutinee refers to (x), as well as the current version of that thing (let's call it x#1).
• Then flow analysis visits the first int v pattern. This causes $scrutinee to be promoted to int. Since the current version of x is still x#1, it causes x to be promoted to int as well.
• Then flow analysis visits the clause when (x = 42) > 0. Since this assigns an integer value to x, x remains promoted to int. But the current version of x is now x#2.
• Then flow analysis considers the control flow paths leading to the second int v pattern. There are two of them:
  • One in which int v matched, but (x = 42) > 0 was false. (Flow analysis doesn't reason about integers, so it doesn't know that (x = 42) > 0 is guaranteed to be true). In this control flow path, both $scrutinee and x are promoted to int, and the current version of x is x#2.
  • One in which int v did not match. In this control flow path, nothing has been promoted, and the current version of x is x#1.
  • When flow analysis joins these two control flow paths, it produces a flow model in which neither $scrutinee nor x is promoted. Since the versions of x are different in the two control flow paths, it assigns a fresh version for x; let's call it x#3.
• Then flow analysis visits the second int v pattern. This causes $scrutinee to be promoted to int. But since the current version of x is now x#3, and that's different from what it was at the top of the switch, x is not promoted.
• Then flow analysis joins the control flow paths from the first two case clauses. In one of them, both $scrutinee and x are promoted; in the other, only $scrutinee is promoted. So it discards the promotion of x.
• This is why x is not promoted in the line marked // No promotion.

To explain it more informally, as soon as flow analysis sees an assignment to x, it considers the connection between x and $scrutinee to be broken, so the second int v doesn't promote x.

[stereotype441]

Closing since the question has been answered.

[sgrekhov]

It's true that at the line marked // No promotion, x must be an int.

Is it Ok to close it if this is an issue? Is there a Github item that covers it?

[stereotype441]

It's true that at the line marked // No promotion, x must be an int.

Is it Ok to close it if this is an issue? Is there a Github item that covers it?

My complete comment was:

It's true that at the line marked // No promotion, x must be an int. But proving that this is the case requires more complex reasoning than flow analysis is capable of performing.

In other words, while a human being can indeed prove that, in this specific example, x is an int, flow analysis can't. I don't intend to add the necessary capabilities to flow analysis to enable it to prove it. I'm not even sure how I would go about doing so. It feels to me like a very hard problem.

Flow analysis is never going to be able to fully match a human's ability to reason about code, so as long as there isn't a soundness problem (and I believe there isn't), I don't consider this a bug per se. If you (or someone else) feel that there is a reasonable user expectation that flow analysis should be able to do this sort of reasoning, I'm open to reconsidering. But since I believe it's a very hard problem, I would either need a pretty compelling use case to convince me that it's worth investing the effort to try to solve the problem, or I would need someone to sketch out a solution in a way that shows me that my intuition about the difficulty is wrong.

Given that, I think it's appropriate to leave the issue closed for now. Flow analysis is behaving as intended, and although the treatment of switches isn't formally specified yet, it's behaving consistently with my informal description in dart-lang/co19#3169 (comment).