Fixed the "SUB issues" section

Author: eernstg

specification/dartLangSpec.tex

@@ -23339,7 +23339,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
     \FUNCTION}.
 \item
   Let $U_1$ and $U_2$ be, respectively,
-  
+
   \noindent
   \code{$T_1$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{11}$,\,\ldots,\,$X_m$\,%
     \EXTENDS\,$B_{1m}$>($P_{11}$,\,\ldots,\,$P_{1k}$)}
@@ -23372,7 +23372,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
   \noindent
   \code{$T_2$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{21}$,\,\ldots,\,$X_m$\,%
     \EXTENDS\,$B_{2m}$>($P_{21}$,\,\ldots,\,$P_{2k}$,\,$\metavar{Named}_2$)}
-  
+
   \noindent
   where $\metavar{Named}_j$ declares a non-empty set of named parameters
   with names $\metavar{NamesOfNamed}_j$, $j \in 1 .. 2$,
@@ -23386,7 +23386,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
   \item For each required entry named $n$ in $\metavar{Named}_2$,
     $\metavar{Named}_1$ contains an entry named $n$
     (\commentary{which may or may not be required}).
-  \end{itemize}  
+  \end{itemize}
 
   Then \DefEqualsNewline{\UpperBoundType{$U_1$}{$U_2$}}{%
     \code{$T_3$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{31}$,\,\ldots,\,$X_m$\,%
@@ -23431,7 +23431,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
 \item
   \DefEqualsNewline{\UpperBoundType{$T_1$}{$S$ \FUNCTION<\ldots>(\ldots)}}{%
     \UpperBoundType{$T_1$}{Object}}.
-\item 
+\item
   \DefEquals{\UpperBoundType{FutureOr<$T_1$>}{FutureOr<$T_2$>}}{%
     \code{FutureOr<$T_3$>}},
   where $T_3$ = \UpperBoundType{$T_1$}{$T_2$}.
@@ -23447,7 +23447,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
   \DefEquals{\UpperBoundType{$T_1$}{FutureOr<$T_2$>}}{%
     \code{FutureOr<$T_3$>}},
   where $T_3$ = \UpperBoundType{$T_1$}{$T_2$}.
-\item 
+\item
   \DefEquals{\UpperBoundType{FutureOr<$T_1$>}{$T_2$}}{%
     \code{FutureOr<$T_3$>}},
   where $T_3$ = \UpperBoundType{$T_1$}{$T_2$}.
@@ -23594,7 +23594,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
 %%
 \item
   Let $U_1$ and $U_2$ be, respectively,
-  
+
   \noindent
   \code{$T_1$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{11}$,\,\ldots,\,$X_m$\,%
     \EXTENDS\,$B_{1m}$>($P_{11}$,\,\ldots,\,$P_{1k}$)}
@@ -23609,7 +23609,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
   let $T_3$ be \LowerBoundType{$T_1$}{$T_2$},
   let $B_{3i}$ be $B_{1i}$, and
   let $P_{3i}$ be determined as follows:
-  
+
   \begin{itemize}
   \item $P_{3i}$ is \UpperBoundType{$P_{1i}$}{$P_{2i}$} for
     $i \leq \metavar{min}(k, l)$.
@@ -23618,7 +23618,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
   \item $P_{3i}$ is optional if $P_{1i}$ or $P_{2i}$ is optional,
     or if $\metavar{min}(k, l) < i \leq q$.
   \end{itemize}
-  
+
   Then \DefEqualsNewline{\LowerBoundType{$U_1$}{$U_2$}}{%
     \code{$T_3$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{31}$,\,\ldots,\,$X_m$\,%
       \EXTENDS\,$B_{3m}$>($P_{31}$,\,\ldots,\,$P_{3q}$)}}.
@@ -23636,7 +23636,7 @@ \subsubsection{Standard Upper Bounds and Standard Lower Bounds}
   \noindent
   \code{$T_2$\,\FUNCTION<$X_1$\,\EXTENDS\,$B_{21}$,\,\ldots,\,$X_m$\,%
     \EXTENDS\,$B_{2m}$>($P_{21}$,\,\ldots,\,$P_{2k}$,\,$\metavar{Named}_2$)}
-  
+
   \noindent
   where $\metavar{Named}_j$ declares a non-empty set of named parameters
   with names $\metavar{NamesOfNamed}_j$, $j \in 1 .. 2$,
@@ -23743,7 +23743,7 @@ \subsubsection{The Standard Upper Bound of Distinct Interface Types}
 \commentary{%
 For example, the algorithm yields \code{Object} as the standard upper bound of
 \code{List<Comparable<int>{}>} and \code{Iterable<int>},
-but it is easy to see that a tighter upper bound exists, e.g., 
+but it is easy to see that a tighter upper bound exists, e.g.,
 \code{Iterable<Comparable<num>{}>}.%
 }
 
@@ -23789,18 +23789,16 @@ \subsubsection{The Standard Upper Bound of Distinct Interface Types}
 The least upper bound of $I$ and $J$ is then the sole element of $M_q$.
 
 
-\subsubsection{Standard Upper Bound Termination}
-\LMLabel{standardUpperBoundTermination}
+\subsubsection{Standard Upper Bound Issues}
+\LMLabel{standardUpperBoundIssues}
 
-%% TODO(eernst), for review: This section could be turned into a few github
-%% issues, but it seems reasonable to let the user of Dart know about it.
-%% So do we include it, or do we delete the whole section (and create those
-%% github issues)?
-%%
-%% Note that I omitted the symmetry issue: The given example does not
-%% demonstrate any asymmetry (both results have type `List<dynamic>`).
-%% So we should study the symmetry properties a bit more if we keep this
-%% section.
+%% TODO(eernst), for review: I kept this here (and updated some parts of it)
+%% in order to ensure that this information is preserved. However, it should
+%% perhaps not be in the specification. Should it actually be turned into
+%% a couple of github issues? In any case, it makes sense to communicate
+%% these properties of the algoritm to anyone who needs to know the language
+%% in full detail, which could justify keeping it here, or including a
+%% reference to some other location where the information is available.
 
 \commentary{%
 The definition of the standard upper bound for type variables
@@ -23809,9 +23807,7 @@ \subsubsection{Standard Upper Bound Termination}
 }
 
 \begin{dartCode}
-\VOID{} foo<T \EXTENDS{} List<S>, S \EXTENDS{} List<T>>() \{
-  T x;
-  S y;
+\VOID{} foo<T \EXTENDS{} List<S>, S \EXTENDS{} List<T>>(T x, S y) \{
   \VAR{} a = (x == y) ? x : y;
 \}
 \end{dartCode}
@@ -23828,6 +23824,43 @@ \subsubsection{Standard Upper Bound Termination}
 with the current algorithm.%
 }
 
+\commentary{%
+The current algorithm is asymmetric.
+There is an equivalence class of top types,
+and we correctly choose a canonical representative for bare top types
+using the \IsMoreTopTypeName{} predicate.
+However, when two different top types are embedded in two mutual subtypes,
+we don't correctly choose a canonical representative.%
+}
+
+\begin{dartCode}
+\IMPORT{} 'dart:async';
+\\
+\VOID{} main() \{
+  List<FutureOr<Object?>{}> x;
+  List<\DYNAMIC> y;
+
+  var a = (x == y) ? x : y; // List<\DYNAMIC>.
+  var b = (x == y) ? y : x; // List<FutureOr<Object?>{}>.
+\}
+\end{dartCode}
+
+\commentary{%
+The best solution for this is probably to normalize the types.
+This is fairly straightforward:
+We just normalize \code{FutureOr<$T$>} to the normal form of $T$
+when $T$ is a top type.
+We can then inductively apply this across the rest of the types.
+Then, whenever we have mutual subtypes, we just return the normal form.
+This would be breaking, albeit hopefully only in a minor way.
+
+A similar treatment would need to be done for the bottom types as well,
+since there are two equivalences there:
+A type variable $X$ with bound $T$ is equivalent to \code{Never}
+if $T$ is equivalent to \code{Never},
+and \code{FutureOr<Never>} is equivalent to \code{Future<Never>}.%
+}
+
 
 \subsection{Least and Greatest Closure of Types}
 \LMLabel{leastAndGreatestClosureOfTypes}