Review response

Author: eernstg

specification/dartLangSpec.tex

@@ -13717,7 +13717,7 @@ \subsubsection{Ordinary Invocation}
 Otherwise, let $d$ be the result of getter lookup
 for $m$ in $T$ with respect to $L$,
 and let $F$ be the return type of $d$.
-(\commentary{
+(\commentary{%
 Since \code{$T$.$m$} exists we cannot have a failure in both lookups.%
 })
 If the getter return type $F$ is an interface type
@@ -13741,7 +13741,7 @@ \subsubsection{Ordinary Invocation}
 \LMHash{}%
 It is a compile-time error to invoke an instance method on a type literal
 that is immediately followed by the token `.' (a period).
-\commentary{
+\commentary{%
 For instance, \code{int.toString()} is an error.%
 }
 
@@ -20337,13 +20337,13 @@ \subsection{Type Aliases}
 it is a compile-time error if $T$ is not regular-bounded,
 and it is a compile-time error if any type occurring in $T$ is not well-bounded.
 
-\commentary{
+\commentary{%
 This means that the bounds declared for
 the formal type parameters of a generic type alias
 must be such that when they are satisfied,
 the bounds that pertain to the body are also satisfied,
 and a type occurring as a subterm of the body can violate its bounds,
-but only if it is a correct super-bounded type.
+but only if it is a correct super-bounded type.%
 }
 
 \LMHash{}%
@@ -22384,7 +22384,7 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds}
   \DefEquals{\UpperBoundType{$T_1$}{$T_2$}}{T_2},
   if \SubtypeNE{T_1}{T_2}.
 
-  \commentary{
+  \commentary{%
     In this and in the following cases, both types must be interface types.%
   }
 \item
@@ -22641,7 +22641,7 @@ \subsection{Standard Upper Bounds and Standard Lower Bounds}
   \DefEquals{\LowerBoundType{$T_1$}{$T_2$}}{\code{Never}}, otherwise.
 \end{itemize}
 
-\rationale{
+\rationale{%
 The rules defining \UpperBoundTypeName{} and \LowerBoundTypeName{}
 are somewhat redundant in that they explicitly specify
 a lot of pairs of symmetric cases.
@@ -24433,6 +24433,7 @@ \subsection{Type Promotion}
 }
 
 \LMHash{}%
+\BlindDefineSymbol{\ell, v}%
 Let $\ell$ be a location,
 and let $v$ be a local variable which is in scope at $\ell$.
 Assume that $\ell$ occurs after the declaration of $v$.
@@ -24456,34 +24457,33 @@ \subsection{Type Promotion}
 
 \LMHash{}%
 In particular,
-a check of the form \code{$v$\,\,==\,\,\NULL},
-\code{\NULL\,\,==\,\,$v$},
-or \code{$v$\,\,\IS\,\,Null}
+an expression of the form \code{$v$\,\,==\,\,\NULL} or
+\code{\NULL\,\,==\,\,$v$}
 where $v$ has type $T$ at $\ell$
 promotes the type of $v$
-to \code{Null} in the \TRUE{} continuation,
-and to \NonNullType{$T$} in the \FALSE{} continuation.
-
-%% TODO(eernst), for review: The null safety spec says that `T?` is
-%% promoted to `T`, but implementations _do_ promote `X extends int?` to
-%% `X & int`. So we may be able to specify something which will yield
-%% slightly more precise types, and which is more precisely the implemented
-%% behavior.
-\LMHash{}%
-A check of the form \code{$v$\,\,!=\,\,\NULL},
-\code{\NULL\,\,!=\,\,$v$},
-or \code{$v$\,\,\IS\,\,$T$}
-where $v$ has static type $T?$ at $\ell$
+to \NonNullType{$T$} in the \FALSE{} continuation;
+and an expression of the form \code{$v$\,\,!=\,\,\NULL} or
+\code{\NULL\,\,!=\,\,$v$}
+where $v$ has static type $T$ at $\ell$
+promotes the type of $v$
+to \NonNullType{$T$} in the \TRUE{} continuation.
+
+\LMHash{}%
+Similarly, a type test of the form \code{$v$\,\,\IS\,\,$T$}
 promotes the type of $v$
 to $T$ in the \TRUE{} continuation,
-and to \code{Null} in the \FALSE{} continuation.
+and a type check of the form \code{$v$\,\,\AS\,\,$T$}
+promotes the type of $v$
+to $T$ in the continuation where the expression evaluated to an object
+(\commentary{that is, it did not throw}).
 
 \commentary{%
 The resulting type of $v$ may be the obvious one, e.g.,
 \code{$v$\,\,=\,\,1} may promote $v$ to \code{int},
 but it may also give rise to a demotion
-(changing the type of $v$ to a supertype of the type of $v$ at $\ell$),
-and it may have no effect on the type of $v$
+(changing the type of $v$ to a supertype of the type of $v$ at $\ell$
+and potentially promoting it to some other type of interest).
+It may also have no effect on the type of $v$
 (e.g., when the static type of $e$ is not a type of interest).
 These details will be specified in a future version of this specification.
 
@@ -24655,15 +24655,20 @@ \section*{Appendix: Algorithmic Subtyping}
 the one which is specified in Fig.~\ref{fig:subtypeRules}.
 It shows that Dart subtyping relationships can be decided
 with good performance.
+This section is not normative.
 
 \LMHash{}%
 In this algorithm, types are considered to be the same when they have
 the same canonical syntax
 (\ref{theCanonicalSyntaxOfTypes}).
+\commentary{%
+For example, \SubtypeStd{\code{C}}{\code{C}} does not hold if
+the two occurrences of \code{C} refer to declarations in different libraries.%
+}
 The algorithm must be performed such that the first case that matches
 is always the case which is performed.
 The algorithm produces results which are both positive and negative
-(\commentary{
+(\commentary{%
   that is, in some situations the subtype relation is determined to be false%
 }),
 which is important for performance because
@@ -24675,16 +24680,18 @@ \section*{Appendix: Algorithmic Subtyping}
 \begin{itemize}
 \item
   \textbf{Reflexivity:}
-  if $T_0$ and $T_1$ are the same type then \SubtypeNE{T_0}{T_1}
+  if $T_0$ and $T_1$ are the same atomic type then \SubtypeNE{T_0}{T_1}.
 
   \commentary{%
-    Note that this check is necessary as the base case for primitive types,
+    This check is necessary as the base case for primitive types,
     and type variables, but not for composite types.
     In particular, a structural equality check is admissible,
     but not required here.
-    Pragmatically, non-constant time identity checks here are
-    counter-productive.
-    So this rule should only be used when $T$ is atomic.%
+    Non-constant time identity checks here are counter-productive
+    because the following rules will yield the same result anyway,
+    so we may just perform a full traversal of a large structure twice
+    for no reason.
+    Hence, this rule is only used when the given type is atomic.%
   }
 \item
   \textbf{Right Top:}
@@ -24694,7 +24701,7 @@ \section*{Appendix: Algorithmic Subtyping}
   if $T_0$ is \DYNAMIC{} or \VOID{}
   then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{\code{Object?}}{T_1}.
 \item
-  \textbf{Left Bottom:}
+  \textbf{Bottom:}
   if $T_0$ is \code{Never} then \SubtypeNE{T_0}{T_1}.
 \item
   \textbf{Right Object:}
@@ -24747,7 +24754,7 @@ \section*{Appendix: Algorithmic Subtyping}
   or a promoted type variables \code{$X_0$\,\&\,$S_0$} and $T_1$ is $X_0$
   then \SubtypeNE{T_0}{T_1}.
 
-  \commentary{
+  \commentary{%
     Note that this rule is admissible, and can be safely elided if desired.%
     }
 \item
@@ -24830,7 +24837,7 @@ \section*{Appendix: Algorithmic Subtyping}
     for $i \in 0 .. q$.
   \item \SubtypeNE{U_0[Z_0/X_0, \ldots, Z_k/X_k]}{U_1[Z_0/Y_0, \ldots, Z_k/Y_k]}.
   \item $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i}[Z_0/Y_0, \ldots, Z_k/Y_k]$
-    have the same canonical syntax, for $i \in 0 .. k$.
+    are subtypes of each other, for $i \in 0 .. k$.
   \end{itemize}
 \item
   \textbf{Named Function Types:}
@@ -24871,8 +24878,7 @@ \section*{Appendix: Algorithmic Subtyping}
     \SubtypeNE{U_0[Z_0/X_0, \ldots, Z_k/X_k]}{U_1[Z_0/Y_0, \ldots, Z_k/Y_k]}.
   \item
     $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i}[Z_0/Y_0, \ldots, Z_k/Y_k]$
-    have the same canonical syntax,
-    for each $i \in 0 .. k$.
+    are subtypes of each other, for each $i \in 0 .. k$.
   \end{itemize}
 
   \commentary{%