Flow analysis: promotion to Never makes code unreachable. (#1097)

See dart-lang/sdk#41981

Corresponding implementation change is here:
https://dart-review.googlesource.com/c/sdk/+/154624

Author: stereotype441

resources/type-system/flow-analysis.md

@@ -430,13 +430,13 @@ Definitions:
         - otherwise `demoted` is `previous`
 
 - `promote(E, T, M)` where `E` is an expression, `T` is a type which it may be
-  promoted to, and `M = FlowModel(r, VI)` is the flow model in which to promote,
-  is defined as follows:
-  - If `E` is not a promotion target, then `M`
+  promoted to, and `M1 = FlowModel(r, VI)` is the flow model in which to
+  promote, is defined to be `M3`, where:
+  - If `E` is not a promotion target, then `M3` = `M1`
   - If `E` is a promotion target `x`, then
     - Let `VM = VariableModel(declared, promoted, tested, assigned, unassigned,
       captured)` be the variable model for `x` in `VI`
-    - If `x` is not promotable via type test to `T` given `VM`, then return `M`
+    - If `x` is not promotable via type test to `T` given `VM`, then `M3` = `M1`
     - Else
       - Let `S` be the current type of `x` in `VM`
       - If `T <: S` then let `T1` = `T`
@@ -445,7 +445,8 @@ Definitions:
       - Else `x` is not promotable (shouldn't happen since we checked above)
       - Let `VM2 = VariableModel(declared, T1::promoted, T1::tested, assigned,
       unassigned, captured)`
-      - Return `FlowModel(r, VI[x -> VM2])`
+      - Let `M2 = FlowModel(r, VI[x -> VM2])`
+      - If `T1 <: Never` then `M3` = `unreachable(M2)`, otherwise `M3` = `M2`
 - `promoteToNonNull(E, M)` where `E` is an expression and `M` is a flow model is
   defined to be `promote(E, T, M)` where `T0` is the type of `E`, and `T` is
   **NonNull(`T0`)**.