#3057. Update instance check tests and add negated instance check ones

TypeSystem/flow-analysis/reachability_A12_t01.dart

@@ -5,10 +5,14 @@
 /// @assertion 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)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - 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))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `R?` and `Null <: S`.

TypeSystem/flow-analysis/reachability_A12_t02.dart

@@ -5,10 +5,14 @@
 /// @assertion 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)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - 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))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `R?` and `S` is not subtype of `Null`.

TypeSystem/flow-analysis/reachability_A12_t03.dart

@@ -5,10 +5,14 @@
 /// @assertion 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)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - 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))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `FutureOr<R>` and `Future<R> <: S`.

TypeSystem/flow-analysis/reachability_A12_t04.dart

@@ -5,10 +5,14 @@
 /// @assertion 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)`
-/// - Let `true(N) = promote(E1, S, after(E1))`
-/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+/// - 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))`
 ///
-/// @description Checks that for expression of the form `E1 is S`
+/// @description Checks that for expression of the form `E1 is S`,
 /// `true(N) = promote(E1, S, after(E1))` and
 /// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
 /// the case `T` is `FutureOr<R>` and `R <: S`.

TypeSystem/flow-analysis/reachability_A12_t05.dart

@@ -0,0 +1,32 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion 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))`
+///
+/// @description Checks that if `T` is a bottom type then
+/// `true(N) = unreachable(after(E1))`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  late int i;
+  if (x is Never) {
+    i = 42;
+  }
+  i; // Definitely unassigned.
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test);
+}

TypeSystem/flow-analysis/reachability_A12_t06.dart

@@ -0,0 +1,29 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion 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))`
+///
+/// @description Checks that if `T` is a bottom type then `false(N) = after(E1)`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  int i;
+  if (x is Never) {
+  } else {
+    i = 42;
+  }
+  i; // Definitely assigned.
+}
+
+main() {
+  test(null);
+}

TypeSystem/flow-analysis/reachability_A23_t01.dart

@@ -0,0 +1,30 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion negated 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) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for the case
+/// `T` is `R?` and `Null <: S`.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+main() {
+  int? i = 2 > 1 ? null : 42;
+  if (i is! Null) {
+    i.expectStaticType<Exactly<int>>();
+  } else {
+    Null n = i;
+  }
+}

TypeSystem/flow-analysis/reachability_A23_t02.dart

@@ -0,0 +1,30 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion negated 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) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for the case
+/// `T` is `R?` and `S` is not subtype of `Null`.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+main() {
+  int? i = 2 > 1 ? null : 42;
+  if (i is! int) {
+    i.expectStaticType<Exactly<Null>>();
+  } else {
+    i.expectStaticType<Exactly<int>>();
+  }
+}

TypeSystem/flow-analysis/reachability_A23_t03.dart

@@ -0,0 +1,37 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion negated 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) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for the case
+/// `T` is `FutureOr<R>` and `Future<R> <: S`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+import '../../Utils/static_type_helper.dart';
+
+class C {}
+
+test(FutureOr<C> foc) async {
+  if (foc is! Future<C>) {
+    foc.expectStaticType<Exactly<C>>();
+  } else {
+    foc.expectStaticType<Exactly<Future<C>>>();
+  }
+}
+
+main() {
+  test(C());
+  test(Future<C>.value(C()));
+}

TypeSystem/flow-analysis/reachability_A23_t04.dart

@@ -0,0 +1,37 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion negated 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) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is! S`,
+/// `true(N) = promote(E1, factor(T, S), after(E1))` and
+/// `false(N) = promote(E1, S, after(E1))`. Test `factor(T, S)` for
+/// the case `T` is `FutureOr<R>` and `R <: S`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+import '../../Utils/static_type_helper.dart';
+
+class C {}
+
+test(FutureOr<C> foc) async {
+  if (foc is! C) {
+    foc.expectStaticType<Exactly<Future<C>>>();
+  } else {
+    foc.expectStaticType<Exactly<C>>();
+  }
+}
+
+main() {
+  test(C());
+  test(Future<C>.value(C()));
+}

TypeSystem/flow-analysis/reachability_A23_t05.dart

@@ -0,0 +1,28 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion negated 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) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that if `T` is a bottom type then `true(N) = after(E1)`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  int i;
+  if (x is! Never) {
+    i = 42;
+  }
+  i; // Definitely assigned.
+}
+
+main() {
+  test(null);
+}

TypeSystem/flow-analysis/reachability_A23_t06.dart

@@ -0,0 +1,33 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion negated 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) = after(E1)`.
+///   - Let `false(N) = unreachable(after(E1))`.
+/// - Otherwise:
+///   - Let `true(N) = promote(E1, factor(T, S), after(E1))`
+///   - Let `false(N) = promote(E1, S, after(E1))`
+///
+/// @description Checks that if `T` is a bottom type then
+/// `false(N) = promote(E1, factor(T, S), after(E1))`.
+/// @author sgrekhov22@gmail.com
+
+test(x) {
+  late int i;
+  if (x is! Never) {
+  } else {
+    i = 42;
+  }
+  i; // Definitely unassigned.
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test);
+}