Simplify reasoning about await soundness using a lemma about flatten. (#3920)

The lemma is that for all types `T`, `T <: FutureOr<flatten(T)>`. The
lemma was claimed (without proof) in `dartLangSpec.tex`, so I've added
a (non-normative) proof of it to the spec, right after the claim.

This made it possible to significantly simplify the reasoning around
the soundness of `await` in `inference.md`.

Thanks to @lrhn for the core idea behind this.

Author: stereotype441

resources/type-system/inference.md

@@ -1046,22 +1046,33 @@ The elaboration process sometimes introduces new operations that are not easily
 expressible using the syntax of Dart. To allow these operations to be specified
 succintly, the syntax of Dart is extended to allow the following forms:
 
-- `@AWAIT_WITH_TYPE_CHECK<T>(m_1)`, represents the following operation:
+- `@AWAIT_WITH_TYPE_CHECK(m_1)` represents the following operation:
 
-  - Evaluate `m_1`, and let `v` denote the result.
+  - Let `T_1` be the static type of `m_1`.
 
-  - If `v` is an instance satisfying type `Future<T>`, then
-    `@AWAIT_WITH_TYPE_CHECK<T>(m_1)` evaluates to `v`.
+  - Let `T` be `flatten(T_1)`.
 
-  - Otherwise, let `u` be a future satisfying type `Future<T>` that will
-    complete to the value `v` at some later point. Then,
-    `@AWAIT_WITH_TYPE_CHECK<T>(m_1)` evaluates to `u`.
+  - Evaluate `m_1`, and let `v` denote the result. _Note that since `m_1` has
+    static type `T_1`, by soundness, `v` must be an instance satisfying
+    `T_1`. Since `T_1 <: FutureOr<flatten(T_1)>` for all `T_1`, it follows that
+    `v` must be an instance satisfying `FutureOr<flatten(T_1)>`, or
+    equivalently, satisfying `FutureOr<T>`. Therefore, `v` must either be an
+    instance satisfying either `Future<T>` or `T`. We consider the two cases
+    below._
 
-    - _TODO(paulberry): explain why such a future is guaranteed to (soundly)
-      exist, by stipulating that if `T_1` is the static type of `m_1`, then `T`
-      must be `flatten(T_1)`, and then proving a lemma that `T_1 <:
-      FutureOr<flatten(T_1)>`; therefore `T_1 <: FutureOr<T>`, so in this
-      "otherwise" case, `v` must be an instance satisfying `T`._
+  - If `v` is an instance satisfying type `Future<T>`, then let
+    `@AWAIT_WITH_TYPE_CHECK(m_1)` evaluate to `v`.
+
+  - Otherwise, let `@AWAIT_WITH_TYPE_CHECK(m_1)` evaluate to a future satisfying
+    type `Future<T>` that will complete to the value `v` at some later
+    point. _Such a future could, for instance, be created by executing
+    `Future<T>.value(v)` (this is sound because in this case `v` is an instance
+    satisfying `T`). It also could be created using a more efficient
+    implementation-specific mechanism._
+
+  - _Note that these two cases in the abstract correspond concretely to a type
+    check in the implementation; this where the name `@AWAIT_WITH_TYPE_CHECK`
+    comes from._
 
 - `@CONCAT(m_1, m_2, ..., m_n)`, where each `m_i` is an elaborated expression
   whose static type is a subtype of `String`, represents the operation of
@@ -1389,99 +1400,17 @@ are determined as follows:
 
 - Let `T_2` be `flatten(T_1)`.
 
-- Let `m_2` be `@AWAIT_WITH_TYPE_CHECK<T_2>(m_1)`, with static type
-  `Future<T_2>`.
+- Let `m_2` be `@AWAIT_WITH_TYPE_CHECK(m_1)`, with static type
+  `Future<T_2>`. _This is sound because `@AWAIT_WITH_TYPE_CHECK(m_1)` always
+  evaluates to an instance satisfying type `Future<T_2>`._
 
   - _Note that in many circumstances, it will be trivial for the compiler to
     establish that `m_1` always evaluates to an instance `v` that satisfies type
     `Future<T_2>`, in which case `m_2` can be optimized to
     `@PROMOTED_TYPE<Future<T_2>>(m_1)`._
 
-  - _For soundness, we must prove that whenever
-    `@AWAIT_WITH_TYPE_CHECK<T_2>(m_1)` evaluates `m_1` to a value `v` that is
-    __not__ an instance satisfying type `Future<T_2>`, that `v` __is__ an
-    instance satisfying type `T_2`. This is necessary to ensure that the future
-    created by `@AWAIT_WITH_TYPE_CHECK` will complete to a value satisfying its
-    type signature. Note that `v` is guaranteed to be an instance satisfying
-    type `T_1` (because `T_1` is the static type of `m_1`). So we can establish
-    soundness by assuming that `v` is an instance satisfying type `T_1` and not
-    an instance satisfying type `Future<T_2>`, and then considering two cases:_
-
-    - _TODO(paulberry): it should be possible to simplify and clarify this
-      section once we have proven that `T <: FutureOr<flatten(T)>` for all types
-      `T`._
-
-    - _If the runtime value of `v` is `null`, then by soundness, `T_1` must be
-      of the form `Null`, `dynamic`, `S*`, or `S?`. Considering each of these:_
-
-      - _If `T_1` is of the form `Null` or `dynamic`, then by the definition of
-        `flatten`, `T_2` must be the same as `T_1`. Therefore, `v` is an
-        instance satisfying type `T_2`, so soundness is satisfied._
-
-      - _If `T_1` is of the form `S*` or `S?`, then by the definition of
-        `flatten`, `T_2` must be of the form `flatten(S)*` or `flatten(S)?`,
-        respectively. `null` is an instance satisfying all types ending in `*`
-        and `?`, so soudness is satisfied._
-
-    - _Otherwise, we need to show that if `v` is a non-null instance satisfying
-      type `T_1`, but not an instance satisfying type `Future<T_2>`, then `v` is
-      an instance satisfying type `T_2`._
-
-    - _Substituting in the definition of `T_2`, we need to show that if `v` is a
-      non-null instance satisfying type `T_1`, but not an instance satisfying
-      type `Future<flatten(T_1)>`, then `v` is an instance satisfying type
-      `flatten(T_1)`. We can prove this by induction on `T_1`:_
-
-      - _If `T_1` is `S?`, then `flatten(T_1)` is `flatten(S)?`. We need to show
-        that if `v` is a non-null instance satisfying type `S?`, but not an
-        instance satisfying type `Future<flatten(S)?>`, then `v` is an instance
-        satisfying type `flatten(S)?`. Assuming `v` is a non-null instance
-        satisfying type `S?`, it must be a non-null instance satisfying type
-        `S`. Assuming `v` is not an instance satisfying type
-        `Future<flatten(S)?>`, it follows that `v` is not an instance satisfying
-        type `Future<flatten(S)>`. So we have satisfied the premise of the
-        induction hypothesis using `T_1 = S`, and therefore by induction, `v` is
-        an instance satisfying type `flatten(S)`. This in turn implies that `v`
-        is an instance satisfying type `flatten(S)?`._
-
-      - _(Same argument but with `?` replaced by `*`): If `T_1` is `S*`, then
-        `flatten(T_1)` is `flatten(S)*`. We need to show that if `v` is a
-        non-null instance satisfying type `S*`, but not an instance satisfying
-        type `Future<flatten(S)*>`, then `v` is an instance satisfying type
-        `flatten(S)*`. Assuming `v` is a non-null instance satisfying type `S*`,
-        it must be a non-null instance satisfying type `S`. Assuming `v` is not
-        an instance satisfying type `Future<flatten(S)*>`, it follows that `v`
-        is not an instance satisfying type `Future<flatten(S)>`. So we have
-        satisfied the premise of the induction hypothesis using `T_1 = S`, and
-        therefore by induction, `v` is an instance satisfying type
-        `flatten(S)`. This in turn implies that `v` is an instance satisfying
-        type `flatten(S)*`._
-
-      - _If `T_1` is `FutureOr<S>`, then `flatten(T_1)` is `S`. We need to show
-        that if `v` is a non-null instance satisfying type `FutureOr<S>`, but
-        not an instance satisfying type `Future<S>`, then `v` is an instance
-        satisfying type `S`. This is trivially true, because `FutureOr<S>` is
-        the union of types `S` and `Future<S>`._
-
-      - _If `T_1 <: Future`, then `flatten(T_1)` is `S`, where `S` is a type
-        such that `T_1 <: Future<S>` and for all `R`, if `T_1 <: Future<R>` then
-        `S <: R`. We need to show that if `v` is a non-null instance satisfying
-        type `T_1`, but not an instance satisfying type `Future<S>`, then `v` is
-        an instance satisfying type `S`. Assuming `v` is a non-null instance
-        satisfying type `T_1`, it must also be a non-null instance satisfying
-        type `Future<S>` (because `T_1 <: Future<S>`). But this contradicts the
-        assumption that `v` is __not__ an instance satisfying type `Future<S>`,
-        so this case is impossible._
-
-      - _Finally, if none of the above cases are satisfied, then `flatten(T_1)`
-        is `T_1`. We need to show that if `v` is a non-null instance satisfying
-        type `T_1`, but not an instance satisfying type `Future<T_1>`, then `v`
-        is an instance satisfying type `T_1`. This is trivially true, since if
-        `v` is a non-null instance satisfying type `T_1`, it must be an instance
-        satisfying type `T_1`._
-
 - Let `T` be `T_2`, and let `m` be `await m_2`. _Since `m_2` has static type
-  `Future<m_2>`, the value of `await m_2` must necessarily be an instance
+  `Future<T_2>`, the value of `await m_2` must necessarily be an instance
   satisfying type `T_2`, so soundness is satisfied._
 
 <!--

specification/dartLangSpec.tex

@@ -11794,7 +11794,41 @@ \subsection{Function Expressions}
 \commentary{%
 Note that if $T$ derives a future type $F$ then \SubtypeNE{T}{F},
 and $F$ is always of the form \code{$G$<...>} or \code{$G$<...>?},
-where $G$ is \code{Future} or \code{FutureOr}.
+where $G$ is \code{Future} or \code{FutureOr}. The proof is by induction on the
+structure of $T$:
+
+\begin{itemize}
+\item
+  %% TODO(eernst): Come mixin classes and extension types: add them.
+  If $T$ is a type which is introduced by
+  a class, mixin, or enum declaration,
+  and if $T$ or a direct or indirect superinterface
+  (\ref{interfaceSuperinterfaces})
+  of $T$ is \code{Future<$U$>} for some $U$, then, letting
+  \code{$G =$ Future} and \code{$F = G$<$U$>}, $T <: F$.
+\item
+  If $T$ is the type \code{FutureOr<$U$>} for some $U$, then by reflexivity,
+  \code{$T <:$ FutureOr<$U$>}. Letting \code{$G =$ FutureOr} and
+  \code{$F = G$<$U$>}, it follows that $T <: F$.
+\item
+  If $T$ is \code{$S$?} for some $S$, and
+  $S$ derives the future type $F'$,
+  then by the induction hypothesis, \code{$S <: F'$}, where $F'$ is of the form
+  \code{$G'$<$U$>} or \code{$G'$<$U$>?} and $G'$ is \code{Future} or
+  \code{FutureOr}. Therefore, \code{$S$? $<: F'$?}, and by substitution,
+  \code{$T <: F'$?}. Since \code{$T$?? $= T$?} for all $T$, it follows that
+  \code{$T <: G'$<$U$>?}. So, letting $G = G'$ and \code{$F = G$<$U$>?},
+  it follows that $T <: F$.
+\item
+  If $T$ is a type variable with bound $B$, and
+  $B$ derives the future type $F$,
+  then by the induction hypothesis, \code{$B <: F'$}, where $F'$ is of the form
+  \code{$G'$<$U$>} or \code{$G'$<$U$>?} and $G'$ is \code{Future} or
+  \code{FutureOr}. Also, since $B$ is the bound of $T$, $T <: B$, so by
+  transitivity, $T <: F'$. Therefore, letting $G = G'$ and $F = F'$, it
+  follows that $T <: F$.
+\end{itemize}
+
 Also note that 'derives' in this context refers to the computation
 where a type $T$ is given, the supertypes of $T$ are searched,
 and a type $F$ of one of those forms is selected.
@@ -11829,7 +11863,44 @@ \subsection{Function Expressions}
 
 \rationale{%
 This definition guarantees that for any type $T$,
-\code{$T <:$ FutureOr<$\flatten{T}$>}.%
+\code{$T <:$ FutureOr<$\flatten{T}$>}. The proof is by induction on the
+structure of $T$:
+
+\begin{itemize}
+\item If $T$ is \code{$X$\,\&\,$S$} then
+  \begin{itemize}
+  \item if $S$ derives a future type $U$,
+    then \code{$T <: S$} and \code{$S <: U$}, so \code{$T <: U$}.
+    By the induction hypothesis, \code{$U <:$ FutureOr<$\flatten{U}$>}.
+    Since \code{$\flatten{T} = \flatten{U}$} in this case, it follows that
+    \code{$U <:$ FutureOr<$\flatten{T}$>}, and so
+    \code{$T <:$ FutureOr<$\flatten{T}$>}.
+  \item otherwise, \code{$T <: X$}.
+    By the induction hypothesis, \code{$X <:$ FutureOr<$\flatten{X}$>}.
+    Since \code{$\flatten{T} = \flatten{X}$} in this case, it follows that
+    \code{$U <:$ FutureOr<$\flatten{T}$>}, and so
+    \code{$T <:$ FutureOr<$\flatten{T}$>}.
+  \end{itemize}
+
+\item If $T$ derives a future type \code{Future<$S$>}
+  or \code{FutureOr<$S$>}, then, since \code{Future<$S$> $<:$ FutureOr<$S$>},
+  it follows that \code{$T <:$ FutureOr<$S$>}. Since \code{$\flatten{T} = S$}
+  in this case, it follows that \code{$T <:$ FutureOr<$\flatten{T}$>}.
+
+\item If $T$ derives a future type \code{Future<$S$>?} or
+  \code{FutureOr<$S$>?}, then, since \code{Future<$S$>? $<:$ FutureOr<$S$>?},
+  it follows that \code{$T <:$ FutureOr<$S$>?}.
+  \code{FutureOr<$S$>? $<:$ FutureOr<$S$?>} for any type $S$ (this can be shown
+  using the union type subtype rules and from
+  \code{Future<$S$> $<:$ Future<$S$?>} by covariance), so by transivitity,
+  \code{$T <:$ FutureOr<$S$?>}. Since \code{$\flatten{T} = S$?} in this case,
+  it follows that \code{$T <:$ FutureOr<$\flatten{T}$>}.
+
+\item Otherwise, \code{$\flatten{T} = T$}, so
+  \code{FutureOr<$\flatten{T}$> $=$ FutureOr<$T$>}. Since
+  \code{$T <:$ FutureOr<$T$>}, it follows that
+  \code{$T <:$ FutureOr<$\flatten{T}$>}.
+\end{itemize}
 }
 
 \LMHash{}%