[flow analysis] Rework demotion and type of interest promotion. (#4370)

This formulation is consisent with the behavior of the implementation.

Fixes dart-lang/sdk#60646.

Author: stereotype441

resources/type-system/flow-analysis.md

@@ -110,6 +110,14 @@ that assignment).
     `b`.
   - We use the notation `[...l, a]` where `l` is a list to denote a list
     beginning with all the elements of `l` and followed by `a`.
+  - A list of types `p` is called a _promotion chain_ iff, for all `i < j`,
+    `p[i] <: p[j]`. _Note that since the subtyping relation is transitive, in
+    order to establish that `p` is a promotion chain, it is sufficient to check
+    the `p[i] <: p[j]` relation for each adjacent pair of types._
+  - A promotion chain `p` is said to be _valid for declared type `T`_ iff every
+    type in `p` is a subtype of `T`. _Note that since the subtyping relation is
+    transitive, in order to establish that `p` is valid for declared type `T`,
+    it is sufficient to check that the first type in `p` is a subtype of `T`._
 
 - Stacks
   - We use the notation `push(s, x)` to mean pushing `x` onto the top of the
@@ -123,18 +131,18 @@ that assignment).
 
 ### Models
 
-A *variable model*, denoted `VariableModel(declaredType, promotedTypes,
+A *variable model*, denoted `VariableModel(declaredType, promotionChain,
 tested, assigned, unassigned, writeCaptured)`, represents what is statically
 known to the flow analysis about the state of a variable at a given point in the
 source code.
 
 - `declaredType` is the type assigned to the variable at its declaration site
   (either explicitly or by type inference).
 
-- `promotedTypes` is a list of types that the variable has been promoted to,
-  with the final type in the list being the current promoted type of the
-  variable. Note that each type in the list must be a subtype of all previous
-  types, and of the declared type.
+- `promotionChain` is the variable's promotion chain. This is a list of types
+  that the variable has been promoted to, with the final type in the list being
+  the current promoted type of the variable. It must always be a valid promotion
+  chain for declared type `declaredType`.
 
 - `tested` is a set of types which are considered "of interest" for the purposes
   of promotion, generally because the variable in question has been tested
@@ -397,8 +405,8 @@ We also make use of the following auxiliary functions:
 Promotion policy is defined by the following operations on flow models.
 
 We say that the **current type** of a variable `x` in variable model `VM` is `S` where:
-  - `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
-  - `promoted = [...l, S]` or (`promoted = []` and `declared = S`)
+  - `VM = VariableModel(declared, promotionChain, tested, assigned, unassigned, captured)`
+  - `promotionChain = [...l, S]` or (`promotionChain = []` and `declared = S`)
 
 Policy:
   - We say that at type `T` is a type of interest for a variable `x` in a set of
@@ -407,46 +415,91 @@ Policy:
 
   - 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)`
+    - `VM = VariableModel(declared, promotionChain, 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`)
 
-  - We say that a variable `x` is promotable via assignment of an expression of
-    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 `T <: S` and not `S <: T`
-    - and `T` is a type of interest for `x` in `tested`
-
-  - We say that a variable `x` is demotable via assignment of an expression of
-    type `T` given variable model `VM` if
-    - `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
-    - and `captured` is false
-    - and [...promoted, declared] contains a type `S` such that `T` is `S` or
-      `T` is **NonNull(`S`)**.
-
 Definitions:
 
+- `demote(promotionChain, written)`, is a promotion chain obtained by deleting
+  any elements from `promotionChain` that do not satisfy `written <: T`. _In
+  effect, this removes any type promotions that are no longer valid after the
+  assignment of a value of type `written`._
+  - _Note that if `promotionChain` is valid for declared type `T`, it follows
+    that `demote(promotionChain, written)` is also valid for declared type `T`._
+
+- `toi_promote(declared, promotionChain, tested, written)`, where `declared` and
+  `written` are types satisfying `written <: declared`, `promotionChain` is
+  valid for declared type `declared`, and all types `T` in `promotionChain`
+  satisfy `written <: T`, is the promotion chain `newPromotionChain`, defined as
+  follows. _("toi" stands for "type of interest".)_
+  - Let `provisionalType` be the last type in `promotionChain`, or `declared` if
+    `promotionChain` is empty. _(This is the type of the variable after
+    demotions, but before type of interest promotion.)_
+    - _Since the last type in a promotion chain is a subtype of all the others,
+      it follows that all types `T` in `promotionChain` satisfy `provisionalType
+      <: T`._
+  - If `written` and `provisionalType` are the same type, then
+    `newPromotionChain` is `promotionChain`. _(No type of interest promotion is
+    necessary in this case.)_
+  - Otherwise _(when `written` is not `provisionalType`)_, let `p1` be a set
+    containing the following types:
+    - **NonNull**(`declared`), if it is not the same as `declared`.
+    - For each type `T` in the `tested` list:
+      - `T`
+      - **NonNull**(`T`)
+
+    _The types in `p1` are known as the types of interest._
+  - Let `p2` be the set `p1 \ { provisionalType }` _(where `\` denotes set
+    difference)_.
+  - If the `written` type is in `p2`, and `written <: provisionalType`, then
+    `newPromotionChain` is `[...promotionChain, written]`. _Writing a value
+    whose static type is a type of interest promotes to that type._
+    - _By precondition, `written <: declared` and `written <: T` for all types
+      in `promotionChain`. Therefore, `newPromotionChain` satisfies the
+      definition of a promotion chain, and is valid for declared type
+      `declared`._
+  - Otherwise _(when `written` is not in `p2`)_:
+    - Let `p3` be the set of all types `T` in `p2` such that `written <: T <:
+      provisionalType`.
+    - If `p3` contains exactly one type `T` that is a subtype of all the others,
+      then `promoted` is `[...promotionChain, T]`. _Writing a value whose static
+      type is a subtype of a type of interest promotes to that type of interest,
+      provided there is a single "best" type of interest available to promote
+      to._
+      - _Since `T <: provisionalType <: declared`, and all types `U` in
+        `promotionChain` satisfy `provisionalType <: U`, it follows that all
+        types `U` in `promotionChain` satisfy `T <: U`. Therefore
+        `newPromotionChain` satisfies the definition of a promotion chain, and
+        is valid for declared type `declared`._
+    - Otherwise, `newPromotionChain` is `promotionChain`. _If there is no single
+      "best" type of interest to promote to, then no type of interest promotion
+      is done._
+
 - `assign(x, E, M)` where `x` is a local variable, `E` is an expression of
-  inferred type `T`, and `M = FlowModel(r, VI)` is the flow model for `E` is
-  defined to be `FlowModel(r, VI[x -> VM])` where:
-    - `VI(x) = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
-    - if `captured` is true then:
-      - `VM = VariableModel(declared, promoted, tested, true, false, captured)`.
-    - otherwise if `x` is promotable via assignment of `E` given `VM`
-      - `VM = VariableModel(declared, [...promoted, T], tested, true, false,
-        captured)`.
-    - otherwise if `x` is demotable via assignment of `E` given `VM`
-      - `VM = VariableModel(declared, demoted, tested, true, false, captured)`.
-      - where `previous` is the prefix of `promoted` ending with the first type
-        `S` such that `T <: S`, and:
-        - if `S` is nullable and if `T <: Q` where `Q` is **NonNull(`S`)** then
-          `demoted` is `[...previous, Q]`
-        - otherwise `demoted` is `previous`
+  inferred type `T` (which must be a subtype of `x`'s declared type), and `M =
+  FlowModel(r, VI)` is the flow model for `E` is defined to be `FlowModel(r,
+  VI[x -> VM])` where:
+  - `VI(x) = VariableModel(declared, promoted, tested, assigned, unassigned,
+    captured)`
+  - If `captured` is true then:
+    - `VM = VariableModel(declared, promotionChain, tested, true, false, captured)`.
+  - Otherwise:
+    - Let `written = T`.
+    - Let `promotionChain' = demote(promotionChain, written)`.
+    - Let `promotionChain'' = toi_promote(declared, promotionChain', tested,
+      written)`.
+      - _The preconditions for `toi_promote` are satisfied because:_
+        - _`demote` deletes any elements from `promotionChain` that do not
+          satisfy `written <: T`, therefore every element of `promotionChain'`
+          satisfies `written <: T`._
+        - _`written = T` and `T` is a subtype of `x`'s declared type, therefore
+          `written <: declared`._
+    - Then `VM = VariableModel(declared, promotionChain'', tested, true, false,
+      captured)`.
 
 - `stripParens(E1)`, where `E1` is an expression, is the result of stripping
   outer parentheses from the expression `E1`.  It is defined to be the
@@ -551,7 +604,12 @@ then they are all assigned the same value as `after(N)`.
 - **Local-variable assignment**: If `N` is an expression of the form `x = E1`
   where `x` is a local variable, then:
   - Let `before(E1) = before(N)`.
-  - Let `after(N) = assign(x, E1, after(E1))`.
+  - Let `E1'` be the result of applying type coercion to `E1`, to coerce it to
+    the declared type of `x`.
+  - Let `after(N) = assign(x, E1', after(E1))`.
+    - _Since type coercion to type `T` produces an expression whose static type
+      is a subtype of `T`, the precondition of `assign` is satisfied, namely
+      that the static type of `E1'` must be a subtype of `x`'s declared type._
 
 - **operator==** If `N` is an expression of the form `E1 == E2`, where the
   static type of `E1` is `T1` and the static type of `E2` is `T2`, then:
@@ -617,7 +675,12 @@ then they are all assigned the same value as `after(N)`.
 - **Local variable conditional assignment**: If `N` is an expression of the form
   `x ??= E1` where `x` is a local variable, then:
   - Let `before(E1) = split(promote(x, Null, before(N)))`.
-  - Let `M1 = assign(x, E1, after(E1))`
+  - Let `E1'` be the result of applying type coercion to `E1`, to coerce it to
+    the declared type of `x`.
+  - Let `M1 = assign(x, E1', after(E1))`
+    - _Since type coercion to type `T` produces an expression whose static type
+      is a subtype of `T`, the precondition of `assign` is satisfied, namely
+      that the static type of `E1'` must be a subtype of `x`'s declared type._
   - Let `M2 = split(promoteToNonNull(x, before(N)))`
   - Let `after(N) = merge(M1, M2)`