Update flatten definition (#2713)

Update the definition of the type function `flatten` such that it handles intersection types and type variables in a way that is still sound, but which preserves the type of the operand of `await` much better than the previous approach.

This PR also introduces the notion of 'the future type of a type', which makes it considerably simpler to reason about `flatten` and `await`, because it now consists of two clearly separated simpler steps.

Author: eernstg

specification/dart.sty

@@ -119,7 +119,8 @@
 \newenvironment{commentary}[1]{{\color{commentaryColor}\sf{#1}}}{}
 
 % Auxiliary functions.
-\newcommand{\flatten}[1]{\ensuremath{\mbox{\it flatten}({#1})}}
+\newcommand{\flattenName}{\mbox{\it flatten}}
+\newcommand{\flatten}[1]{\ensuremath{\flattenName({#1})}}
 \newcommand{\futureOrBase}[1]{\ensuremath{\mbox{\it futureOrBase}({#1})}}
 \newcommand{\overrides}[1]{\ensuremath{\mbox{\it overrides}({#1})}}
 \newcommand{\inherited}[1]{\ensuremath{\mbox{\it inherited}({#1})}}

specification/dartLangSpec.tex

@@ -11275,35 +11275,62 @@ \subsection{Function Expressions}
 where inferred types have already been added.%
 }
 
+\LMHash{}%
+We say that $S$ is the
+\IndexCustom{future type of a type}{type!future type of}
+$T$ in the following cases, using the first applicable case:
+
+\begin{itemize}
+\item $T$ implements $S$
+  (\ref{interfaceSuperinterfaces}),
+  and there is a $U$ such that $S$ is \code{Future<$U$>}.
+\item $T$ is $S$ bounded
+  (\ref{bindingActualsToFormals}),
+  and there is a $U$ such that
+  $S$ is \code{FutureOr<$U$>}, \code{Future<$U$>?}, or \code{FutureOr<$U$>?}.
+\end{itemize}
+
+\LMHash{}%
+When none of these cases are applicable,
+we say that $T$ does not have a future type.
+
+\commentary{%
+Note that if $T$ has 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}.%
+}
+
 \LMHash{}%
 We define the auxiliary function
-\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$},
-which is used below and in other sections, as follows:
+\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$}
+as follows, using the first applicable case:
 
 \begin{itemize}
-\item{} If $T$ is \code{$S$?}\ bounded
-  (\ref{bindingActualsToFormals})
-  for some $S$ then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}.
+\item If $T$ is \code{$S$?}\ for some $S$
+  then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}.
 
-\item{} If $T$ is \code{FutureOr<$S$>} bounded
-  then \DefEquals{\flatten{T}}{S}.
+\item If $T$ is \code{$X$\,\&\,$S$}
+  for some type variable $X$ and type $S$ then
+  \begin{itemize}
+  \item if $S$ has future type $U$
+    then \DefEquals{\flatten{T}}{\code{\flatten{U}}}.
+  \item otherwise,
+    \DefEquals{\flatten{T}}{\code{\flatten{X}}}.
+  \end{itemize}
 
-\item{} If $T$ implements \code{Future<$S$>}
-  (\ref{interfaceSuperinterfaces})
+\item If $T$ has future type \code{Future<$S$>}
+  or \code{FutureOr<$S$>}
   then \DefEquals{\flatten{T}}{S}.
 
-\item{} Otherwise, \DefEquals{\flatten{T}}{T}.
+\item If $T$ has future type \code{Future<$S$>?}\ or
+  \code{FutureOr<$S$>?}\ then \DefEquals{\flatten{T}}{\code{$S$?}}.
+
+\item Otherwise, \DefEquals{\flatten{T}}{T}.
 \end{itemize}
 
-\commentary{%
+\rationale{%
 This definition guarantees that for any type $T$,
-\code{$T <:$ FutureOr<$\flatten{T}$>}.
-Note that when $X$ is a type variable with bound $B$,
-it is possible that \flatten{X} is different from $X$:
-$B$ could, for some $S$, be \code{FutureOr<$S$>},
-or a type variable $Y$ with bound \code{FutureOr<$S$>},
-or a class $C$ that implements \code{Future<$S$>},
-or a type variable $X$ with bound $C$.%
+\code{$T <:$ FutureOr<$\flatten{T}$>}.%
 }
 
 \LMHash{}%
@@ -15992,27 +16019,25 @@ \subsection{Await Expressions}
 \end{grammar}
 
 \LMHash{}%
-Evaluation of an await expression $a$ of the form \code{\AWAIT{} $e$}
-where $e$ has static type $S$ proceeds as follows:
-First, the expression $e$ is evaluated to an object $o$.
-Let $T$ be \flatten{S}
-(\flatten{} is defined in section \ref{functionExpressions}).
-It is a dynamic type error if the run-time type of $o$ is not a subtype
-of \code{FutureOr<$T$>} \commentary{(that is, if it is neither a subtype
-of $T$ nor of \code{Future<$T$>})}.
+\BlindDefineSymbol{a, e, S}%
+Let $a$ be an expression of the form \code{\AWAIT\,\,$e$}.
+Let $S$ be the static type of $e$.
+The static type of $a$ is then \flatten{S}
+(\ref{functionExpressions}).
 
 \LMHash{}%
-% NOTICE: Removed the requirement that an error thrown by $e$ is caught in a
-% future. There is no reason $var x = e; await x;$ and $await e$ should behave
-% differently, and no implementation actually implemented it.
+Evaluation of $a$ proceeds as follows:
+First, the expression $e$ is evaluated to an object $o$.
+Let \DefineSymbol{T} be \flatten{S}.
 If the run-time type of $o$ is a subtype of \code{Future<$T$>},
-then let $f$ be $o$;
+then let \DefineSymbol{f} be $o$;
 otherwise let $f$ be the result of creating
 a new object using the constructor \code{Future<$T$>.value()}
 with $o$ as its argument.
 
 \LMHash{}%
-Next, the stream associated with the innermost enclosing asynchronous for loop
+Next, the stream associated with
+the innermost enclosing asynchronous \FOR{} loop
 (\ref{asynchronousFor-in}),
 if any, is paused.
 The current invocation of the function body immediately enclosing $a$
@@ -16023,8 +16048,34 @@ \subsection{Await Expressions}
 (\ref{expressionEvaluation}).
 If $f$ completes with an object $v$, $a$ evaluates to $v$.
 
-% Otherwise, the value of $a$ is the value of $e$. If evaluation of
-% $e$ raises an exception $x$, $a$ raises $x$.
+\rationale{%
+The use of \flattenName{} to find $T$ and hence determine the dynamic type test
+implies that we await a future in every case where this choice is sound.%
+}
+
+\commentary{%
+An interesting case on the edge of this trade-off is when $e$
+has the static type \code{FutureOr<Object>?}.
+You could say that the intention behind this type is that
+the value of $e$ is a \code{Future<Object>},
+or it is an \code{Object} which is not a future,
+or it is \NULL.
+So, presumably, we should await the first kind,
+and we should pass on the second and third kind unchanged.
+However, the second kind could be a \code{Future<Object?>}.
+This object isn't a \code{Future<Object>}, and it isn't \NULL,
+so it \emph{must} be considered to be in the second group.
+Nevertheless, \flatten{\code{FutureOr<Object>?}} is \code{Object?},
+so we \emph{will} await a \code{Future<Object?>}.
+We have chosen this semantics because it was the smallest breaking change
+relative to the semantics in earlier versions of Dart,
+and also because it allows for a simple rule:
+The type of \code{\AWAIT\,\,$e$} is used to decide whether or not
+the future (if any) is awaited, and there are no exceptions---even
+in cases like this example, where the type seems to imply that
+a \code{Future<Object?>} should not be awaited.
+In summary, we await every future that we can soundly await.%
+}
 
 \commentary{%
 An await expression can only occur in a function which is declared
@@ -16047,9 +16098,6 @@ \subsection{Await Expressions}
 Tools may choose to give a hint in such cases.%
 }
 
-\LMHash{}%
-The static type of $a$ is $T$.
-
 
 \subsection{Postfix Expressions}
 \LMLabel{postfixExpressions}