Flow analysis. No promotion to `Never` via type test

[sgrekhov]

Promotion via type test is specified as:

• We say that a variable x is promotable via type test with type T given variable model VM if
  • VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)
  • and captured is false
  • and S is the current type of x in VM
  • and not S <: T
  • and T <: S or (S is X extends R and T <: R) or (S is X & R and T <: R)

According to the above we should be able to promote any type to type Never. But we cannot.

main() {
  String s = "a";
  if (s is Never) {
    s.expectStaticType<Exactly<Never>>(); // Error: 'Exactly<Never>' doesn't conform to the bound 'Exactly<String>' of the type parameter 'R'. 
  }
}

extension StaticType<T> on T {
  T expectStaticType<R extends Exactly<T>>() {
    return this;
  }
}
typedef Exactly<T> = T Function(T);

Yes, s.expectStaticType<...>(...) is dead code, but according to the spec it should work.

Dart SDK version: 3.9.0-74.0.dev (dev) (Tue Apr 29 21:02:55 2025 -0700) on "windows_x64"

[lrhn]

Well .... we only promote on the true branch, and s is Never is never true 😜

(I don't know if that's the actual reason. It could be. If we do recognize that the branch is unreachable, then promotion can't very well flow into it.)

[eernstg]

we only promote on the true branch

Of course, but the invocation of expectStaticType is on the true branch. It is dead code, but that doesn't change the expected outcome because dead code is treated as reachable via every predecessor node in the control flow graph. So we should expect s to have type Never for that invocation of expectStaticType.

[stereotype441]

Flow analysis is behaving as intended (and as specified). Here is the relevant spec text:

• instance check If N is an expression of the form E1 is S where the static type of E1 is T then:
  • Let before(E1) = before(N)
  • If T is a bottom type, then:
    • Let true(N) = unreachable(after(E1)).
    • Let false(N) = after(E1).
  • Otherwise:
    • Let true(N) = promote(E1, S, after(E1))
    • Let false(N) = promote(E1, factor(T, S), after(E1))

Since Never is a bottom type, the test s is Never doesn't invoke promotion via type test. Instead, the body of the if statement is marked as unreachable and no promotion is performed.

Closing as "not planned".