Flow analysis. Variable of type `Never` in a `for-in` loop issue

[sgrekhov]

There are two issues in the code below.

1. No error in both CFE and the analyzer in test1
2. No error in CFE in test2

test1() {
  late int i;
  if (2 > 1) {
    for (Never n in <dynamic>[i = 42]) {} // Analyzer warning "The value of the local variable 'n' isn't used."
  }
  i; // Definitely unassigned but no error in either CFE and the analyzer
}

test2(Never n) {
  late int i;
  if (2 > 1) {
    for (n in <dynamic>[i = 42]) {}
  }
  i; // Definitely unassigned. Error in the analyzer, no error in CFE
}

cc @stereotype441

Dart SDK version: 3.8.0-205.0.dev (dev) (Tue Mar 18 21:02:26 2025 -0700) on "windows_x64"

[stereotype441]

Regarding test1:

test1() {
  late int i;
  if (2 > 1) {
    for (Never n in <dynamic>[i = 42]) {} // Analyzer warning "The value of the local variable 'n' isn't used."
  }
  i; // Definitely unassigned but no error in either CFE and the analyzer
}

As discussed in #60376, in order to avoid having to make multiple passes through the code, flow analysis does a conservative analysis of loops that doesn't account for types, using the conservativeJoin relation defined in https://github.com/dart-lang/language/blob/main/resources/type-system/flow-analysis.md#models. So it considers for (Never n in <dynamic>[i = 42]) {} to potentially assign to i, even though based on type analysis one could see that the assignment to n could never possibly succeed. So flow analysis is behaving as specified in this test case.

Edit: even though the iterable expression <dynamic>[i = 42] appears syntactically inside the for construct, it is executed before the top of the loop. So flow analysis considers i to be definitely assigned after evaluation of the iterable expression; then it uses conservativeJoin to handle any assignments inside the loop itself (there aren't any assignments to i, so this has no effect). Therefore i is considered definitely assigned in the "then" branch of the loop and definitely unassigned in the "else" branch of the loop. So it's considered potentially assigned at the site of the final reference to i. Note that a human can see that an assignment to Never n will never succeed, and thus the "then" branch of the loop is dead code, but flow analysis doesn't perform this reasoning step, so it considers the "then" branch to be live.

I'm not sure what's going on in test2 yet. I will look at it in more detail and follow up.

[eernstg]

So it considers for (Never n in <dynamic>[i = 42]) {} to potentially assign to i

I'd actually expect this statement to yield an after flow model where i is 'definitely assigned' because the for-in statement rule treats the evaluation of the iterable as something that occurs as the first step, which is then followed by the conservative join.

'Definitely unassigned' would be disproven by a variant of this example, by the way:

void main() {
  late int i;
  if (2 > 1) {
    for (Never _ in <dynamic>[if ((i = 42) < 0) 1]) {}
  }
  print(i); // OK.
}

[stereotype441]

So it considers for (Never n in <dynamic>[i = 42]) {} to potentially assign to i

I'd actually expect this statement to yield an after flow model where i is 'definitely assigned' because the for-in statement rule treats the evaluation of the iterable as something that occurs as the first step, which is then followed by the conservative join.

You're right, my mistake. I've edited my response. Thanks!

[stereotype441]

Ok, I've dug into test2:

test2(Never n) {
  late int i;
  if (2 > 1) {
    for (n in <dynamic>[i = 42]) {}
  }
  i; // Definitely unassigned. Error in the analyzer, no error in CFE
}

Due to an analyzer bug, before visiting the expression <dynamic>[i = 42], the analyzer marks the code path as unreachable, so it considers the "then" branch of the "if" statement to be dead. So when it joins the "then" and "else" branches at the bottom of the "else", it ignores the dead "then" branch and just uses the data from the live "else" branch (in which i is definitely unassigned), and therefore it considers i to be definitely unassigned, and issues an error.

That's not wrong per se; for this particular example, it happens to be true that if control flow reaches i; then i has definitely not been assigned. But the analyzer is coming to this correct conclusion for the wrong reasons, and furthermore, according to the flow analysis spec, the analyzer should not be classifying this code path as unreachable at all. (There is no rule in the flow analysis spec saying that an assignment to Never is unreachable; the intent is that the control flow path should be marked as unreachable if an expression has a static type of Never, and there are no expressions in this example with a static type of Never). Note that this analyzer bug leads to other, more serious problems; see #60424.

The CFE follows the behavior dictated by the spec, which is:

• The expression <dynamic>[i = 42] puts i in the "definitely assigned" state
• The assignment to n does not cause the control flow path to become unreachable
• Therefore, the "then" control flow path assigns to i and the "else" control flow path doesn't, so after the end of the "if" statement, i is considered to be potentially assigned.
• Therefore, no error is issued.

Since both implementations are behaving as specified for test1, and the only departure from the spec in test2 is covered by #60424, I'm going to close this issue as a duplicate of #60424.