From fb4db075e894e1b01722e138476ee4be3b817d2b Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Dec 2023 15:17:22 +0100
Subject: [PATCH 01/82] Integrate the null-safety subtyping rules into
 dartLangSpec.tex

---
 specification/dartLangSpec.tex | 502 +++++++++++++++++----------------
 1 file changed, 259 insertions(+), 243 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index b598a8bdf2..7d6f92bc42 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -85,6 +85,8 @@
 %   a function literal.
 % - Specify in which situations it is an error to declare an initializing
 %   formal parameter.
+% - Integrate the subtyping rule updates that are needed in order to support
+%   null-safety.
 %
 % Nov 2023
 % - Specify that the dynamic error for calling a function in a deferred and
@@ -21839,128 +21841,188 @@ \subsection{Subtypes}
 }
 
 \LMHash{}%
-%% TODO(eernst): Introduce these specialized intersection types
-%% in a suitable location where type promotion is specified.
-Types of the form
-\IndexCustom{$X \& S$}{type!of the form $X \& S$}%
-\IndexExtraEntry{\&@$X \& S$}
-arise during static analysis due to type promotion
+Intersection types
+(\commentary{types of the form \code{$X$\,\&\,$S$}}),
+may arise during static analysis due to type promotion
 (\ref{typePromotion}).
 They never occur during execution,
-they are never a type argument of another type,
-nor a return type or a formal parameter type,
-and it is always the case that $S$ is a subtype of the bound of $X$.
-\commentary{%
-  The motivation for $X \& S$ is that it represents
-  the type of a local variable $v$
-  whose type is declared to be the type variable $X$,
-  and which is known to have type $S$ due to promotion.
-  Similarly, $X \& S$ may be seen as an intersection type,
-  which is a subtype of $X$ and also a subtype of $S$.
-  Intersection types are \emph{not} supported in general,
-  only in this special case.%
-}
-Every other form of type may occur during static analysis
-as well as during execution,
-and the subtype relationship is always determined in the same way.
+and there are many other restrictions on where they can occur
+(\ref{intersectionTypes}).
+However, their subtype relations are specified without restrictions.
+\commentary{%
+  It causes no problems that these rules will not be used
+  in their full generality.%
+}
 
 % Subtype Rule Numbering
 \newcommand{\SrnReflexivity}{1}
-\newcommand{\SrnTop}{2}
-\newcommand{\SrnBottom}{3}
-\newcommand{\SrnNull}{4}
-\newcommand{\SrnLeftTypeAlias}{5}
-\newcommand{\SrnRightTypeAlias}{6}
-\newcommand{\SrnLeftFutureOr}{7}
-\newcommand{\SrnTypeVariableReflexivityA}{8}
-\newcommand{\SrnRightPromotedVariable}{9}
-\newcommand{\SrnRightFutureOrA}{10}
-\newcommand{\SrnRightFutureOrB}{11}
-\newcommand{\SrnLeftPromotedVariable}{12}
-\newcommand{\SrnLeftVariableBound}{13}
-\newcommand{\SrnRightFunction}{14}
-\newcommand{\SrnPositionalFunctionType}{15}
-\newcommand{\SrnNamedFunctionType}{16}
-\newcommand{\SrnCovariance}{17}
-\newcommand{\SrnSuperinterface}{18}
+\newcommand{\SrnRightTop}{2}
+\newcommand{\SrnLeftTop}{3}
+\newcommand{\SrnBottom}{4}
+%\newcommand{\SrnRightObjectOne}{} Redundant
+%\newcommand{\SrnRightObjectTwo}{} Redundant
+%\newcommand{\SrnRightObjectThree}{} Redundant
+\newcommand{\SrnRightObjectFour}{5}
+\newcommand{\SrnNullOne}{6}
+\newcommand{\SrnNullTwo}{7}
+\newcommand{\SrnLeftFutureOr}{8}
+\newcommand{\SrnLeftNullable}{9}
+\newcommand{\SrnLeftPromotedVariableOne}{10}
+\newcommand{\SrnRightPromotedVariable}{11}
+\newcommand{\SrnRightFutureOrA}{12}
+\newcommand{\SrnRightFutureOrB}{13}
+\newcommand{\SrnRightNullableOne}{14}
+\newcommand{\SrnRightNullableTwo}{15}
+\newcommand{\SrnLeftPromotedVariableTwo}{16}
+\newcommand{\SrnLeftVariableBound}{17}
+\newcommand{\SrnRightFunction}{18}
+\newcommand{\SrnPositionalFunctionType}{19}
+\newcommand{\SrnNamedFunctionType}{20}
+\newcommand{\SrnCovariance}{21}
+\newcommand{\SrnNominal}{22}
 
 \begin{figure}[p]
   \def\VSP{\vspace{4mm}}
   \def\ExtraVSP{\vspace{2mm}}
-  \def\Axiom#1#2#3#4{\centerline{\inference[#1]{}{\SubtypeStd{#3}{#4}}}\VSP}
-  \def\Rule#1#2#3#4#5#6{\centerline{\inference[#1]{\SubtypeStd{#3}{#4}}{\SubtypeStd{#5}{#6}}}\VSP}
-  \def\RuleTwo#1#2#3#4#5#6#7#8{%
-    \centerline{\inference[#1]{\SubtypeStd{#3}{#4} & \SubtypeStd{#5}{#6}}{\SubtypeStd{#7}{#8}}}\VSP}
-  \def\RuleRaw#1#2#3#4#5{%
-    \centerline{\inference[#1]{#3}{\SubtypeStd{#4}{#5}}}\VSP}
-  \def\RuleRawRaw#1#2#3#4{\centerline{\inference[#1]{#3}{#4}}\VSP}
+  \def\Axiom#1#2#3{\centerline{\inference[#1]{}{\SubtypeStd{#2}{#3}}}\VSP}
+  \def\Rule#1#2#3#4#5{%
+    \centerline{\inference[#1]{\SubtypeStd{#2}{#3}}{\SubtypeStd{#4}{#5}}}\VSP}
+  \def\RuleTwo#1#2#3#4#5#6#7{%
+    \centerline{\inference[#1]{\SubtypeStd{#2}{#3} & %
+        \SubtypeStd{#4}{#5}}{\SubtypeStd{#6}{#7}}}\VSP}
+  \def\RuleRaw#1#2#3#4{%
+    \centerline{\inference[#1]{#2}{\SubtypeStd{#3}{#4}}}\VSP}
+  \def\RuleRawRaw#1#2#3{\centerline{\inference[#1]{#2}{#3}}\VSP}
   %
+  % ----------------------------------------------------------------------
+  % Omitted rules stated here, with justification for
+  % the omission.
+  % ------------------------------------------------ Right Object 1
+  % Not needed unless algorithmic: Instance of
+  % \SrnLeftVariableBound.
+  %   \RuleRaw{\SrnRightObjectOne}{%
+  %     \code{$X$\,\EXTENDS\,$B$} & \SubtypeStd{B}{\code{Object}}%
+  %   }{X}{\code{Object}}
+  % ------------------------------------------------ Right Object 2
+  % Not needed unless algorithmic: Instance of
+  % \SrnLeftPromotedVariableTwo.
+  %   \RuleRaw{\SrnRightObjectTwo}{%
+  %     \SubtypeStd{S}{\code{Object}}}{%
+  %       \code{$X$\,\&\,$S$}}{\code{Object}}
+  % ------------------------------------------------ Right Object 3
+  % Not needed unless algorithmic: Derivable from
+  % \SrnLeftFutureOr{} and \SrnRightObjectFour{} (to get
+  % Future<S> <: Object).
+  %   \RuleRaw{\SrnRightObjectThree}{%
+  %     \SubtypeStd{S}{\code{Object}}}{%
+  %       \code{FutureOr<$S$>}}{\code{Object}}
+  % ----------------------------------------------------------------------
   \begin{minipage}[c]{0.49\textwidth}
-    \Axiom{\SrnReflexivity}{Reflexivity}{S}{S}
-    \Axiom{\SrnBottom}{Left Bottom}{\bot}{T}
+    % ------------------------------------------------ Reflexivity
+    \Axiom{\SrnReflexivity}{T}{T}
+    % ------------------------------------------------ Left Top
+    % Non-algorithmic justification for this rule: Needed
+    % to prove dynamic/void <: FutureOr<Object>?.
+    \RuleRaw{\SrnLeftTop}{%
+      S \in \{\DYNAMIC, \VOID\}\\
+      \SubtypeStd{\code{Object?}}{T}}{S}{T}
+    % ------------------------------------------------ Left Bottom
+    \Axiom{\SrnBottom}{\code{Never}}{T}
+    % ------------------------------------------------ Left Null 1
+    \Axiom{\SrnNullOne}{\code{Null}}{\code{$T$?}}
   \end{minipage}
   \begin{minipage}[c]{0.49\textwidth}
-    \RuleRaw{\SrnTop}{Right Top}{T \in \{\code{Object}, \DYNAMIC, \VOID\}}{S}{T}
-    \RuleRaw{\SrnNull}{Left Null}{T \not= \bot}{\code{Null}}{T}
+    % ------------------------------------------------ Right Top
+    \RuleRaw{\SrnRightTop}{%
+      T \in \{\code{Object?}, \DYNAMIC, \VOID\}}{S}{T}
+    % ------------------------------------------------ Right Object
+    % TODO(eernst): Comment out this rule as redundant and
+    % renumber, it is an instance of \SrnRightFutureOrB.
+    \RuleRaw{\SrnRightObjectFour}{%
+      \mbox{$S$ is an interface type or \FUNCTION}}{S}{\code{Object}}
+    % ------------------------------------------------ Left Null 2
+    \Rule{\SrnNullTwo}{\code{Null}}{T}{%
+      \code{Null}}{\code{FutureOr<$T$>}}
   \end{minipage}
 
-  \ExtraVSP
-  \RuleRaw{\SrnLeftTypeAlias}{Type Alias Left}{%
-    \code{\TYPEDEF{} $F$<\TypeParametersNoBounds{X}{s}> = U} &
-    \SubtypeStd{[S_1/X_1,\ldots,S_s/X_s]U}{T}}{\code{$F$<\List{S}{1}{s}>}}{T}
-  \RuleRaw{\SrnRightTypeAlias}{Type Alias Right}{%
-    \code{\TYPEDEF{} $F$<\TypeParametersNoBounds{X}{s}> = U} &
-    \SubtypeStd{S}{[T_1/X_1,\ldots,T_s/X_s]U}}{S}{\code{$F$<\List{T}{1}{s}>}}
-
   \begin{minipage}[c]{0.49\textwidth}
-    \RuleTwo{\SrnLeftFutureOr}{Left FutureOr}{S}{T}{%
-      \code{Future<$S$>}}{T}{\code{FutureOr<$S$>}}{T}
-    \RuleTwo{\SrnRightPromotedVariable}{Right Promoted Variable}{S}{X}{S}{T}{%
+    % ------------------------------------------------ Left FutureOr
+    \RuleTwo{\SrnLeftFutureOr}{%
+      \code{Future<$S$>}}{T}{S}{T}{%
+      \code{FutureOr<$S$>}}{T}
+    % ------------------------------------------------ Right Promoted Variable
+    \RuleTwo{\SrnRightPromotedVariable}{S}{X}{S}{T}{%
       S}{X \& T}
-    \Rule{\SrnRightFutureOrB}{Right FutureOr B}{S}{T}{S}{\code{FutureOr<$T$>}}
-    \Rule{\SrnLeftVariableBound}{Left Variable Bound}{\Delta(X)}{T}{X}{T}
+    % ------------------------------------------------ Right FutureOr B
+    \Rule{\SrnRightFutureOrB}{S}{T}{S}{%
+      \code{FutureOr<$T$>}}
+    % ------------------------------------------------ Right Nullable 2
+    \Rule{\SrnRightNullableTwo}{S}{\code{Null}}{S}{%
+      \code{$T$?}}
+    % ------------------------------------------------ Left Variable Bound
+    \Rule{\SrnLeftVariableBound}{\Delta(X)}{T}{X}{T}
   \end{minipage}
   \begin{minipage}[c]{0.49\textwidth}
-    \Axiom{\SrnTypeVariableReflexivityA}{Left Promoted Variable A}{X \& S}{X}
-    \Rule{\SrnRightFutureOrA}{Right FutureOr A}{S}{\code{Future<$T$>}}{%
-      S}{\code{FutureOr<$T$>}}
-    \Rule{\SrnLeftPromotedVariable}{Left Promoted Variable B}{S}{T}{X \& S}{T}
-    \RuleRaw{\SrnRightFunction}{Right Function}{T\mbox{ is a function type}}{%
-      T}{\FUNCTION}
+    % ------------------------------------------------ Left Nullable
+    \RuleTwo{\SrnLeftNullable}{S}{T}{\code{Null}}{T}{%
+      \code{$S$?}}{T}
+    % ------------------------------------------------ Left Promoted Variable A
+    \Axiom{\SrnLeftPromotedVariableOne}{X \& S}{X}
+    % ------------------------------------------------ Right FutureOr A
+    \Rule{\SrnRightFutureOrA}{S}{%
+      \code{Future<$T$>}}{S}{\code{FutureOr<$T$>}}
+    % ------------------------------------------------ Right Nullable 1
+    \Rule{\SrnRightNullableOne}{S}{T}{S}{\code{$T$?}}
+    % ------------------------------------------------ Left Promoted Variable B
+    \Rule{\SrnLeftPromotedVariableTwo}{S}{T}{X \& S}{T}
+    % ------------------------------------------------ Right Function
+    \RuleRaw{\SrnRightFunction}{%
+      T\mbox{ is a function type}}{T}{\FUNCTION}
   \end{minipage}
   %
   \ExtraVSP
-  \RuleRawRaw{\SrnPositionalFunctionType}{Positional Function Types}{%
+  % ------------------------------------------------ Positional Function Type
+  \RuleRawRaw{\SrnPositionalFunctionType}{%
     \Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
+    \forall i \in 1..s\!:\;\MutualSubtype{\Delta'}{B_i}{B'\!_i} &
     \Subtype{\Delta'}{S_0}{T_0} \\
     n_1 \leq n_2 &
     n_1 + k_1 \geq n_2 + k_2 &
     \forall j \in 1 .. n_2 + k_2\!:\;\Subtype{\Delta'}{T_j}{S_j}}{%
     \begin{array}{c}
       \Delta\vdash\RawFunctionTypePositional{S_0}{X}{B}{s}{S}{n_1}{k_1}\;<:\;\\
-      \RawFunctionTypePositional{T_0}{X}{B}{s}{T}{n_2}{k_2}
+      \RawFunctionTypePositional{T_0}{X}{B'\!}{s}{T}{n_2}{k_2}
     \end{array}}
   \ExtraVSP\ExtraVSP
-  \RuleRawRaw{\SrnNamedFunctionType}{Named Function Types}{%
+  % ------------------------------------------------ Named Function Type
+  \RuleRawRaw{\SrnNamedFunctionType}{%
     \Delta' = \Delta\uplus\{X_i\mapsto{}B_i\,|\,1 \leq i \leq s\} &
+    \forall i \in 1..s\!:\;\MutualSubtype{\Delta'}{B_i}{B'\!_i} &
     \Subtype{\Delta'}{S_0}{T_0} &
-    \forall j \in 1 .. n\!:\;\Subtype{\Delta'}{T_j}{S_j} \\
-    \{\,\List{y}{n+1}{n+k_2}\,\} \subseteq \{\,\List{x}{n+1}{n+k_1}\,\} \\
-    \forall p \in 1 .. k_2, q \in 1 .. k_1:\quad
-    y_{n+p} = x_{n+q}\quad\Rightarrow\quad\Subtype{\Delta'}{T_{n+p}}{S_{n+q}}}{%
+    \forall j \in 1 .. n\!:\;\Subtype{\Delta'}{T_j}{S_j}\\
+    \{\,\List{y}{n+1}{n+k_2}\,\} \subseteq \{\,\List{x}{n+1}{n+k_1}\,\}\\
+    \forall p \in 1 .. k_2, q \in 1 .. k_1:\quad%
+    y_{n+p} = x_{n+q}\quad\Rightarrow\quad%
+    (\Subtype{\Delta'}{T_{n+p}}{S_{n+q}})\;\wedge\;%
+    (r_{n+q} = \REQUIRED{} \Rightarrow r'_{n+p} = \REQUIRED)}{%
     \begin{array}{c}
       \Delta\vdash\RawFunctionTypeNamed{S_0}{X}{B}{s}{S}{n}{x}{k_1}{r}\;<:\;\\
-      \RawFunctionTypeNamed{T_0}{X}{B}{s}{T}{n}{y}{k_2}{r}
+      \RawFunctionTypeNamed{T_0}{X}{B'\!}{s}{T}{n}{y}{k_2}{r'}
     \end{array}}
   %
   \ExtraVSP
-  \RuleRaw{\SrnCovariance}{Covariance}{%
-    \code{\CLASS{} $C$<\TypeParametersNoBounds{X}{s}>\,\ldots\,\{\}} &
-    \forall j \in 1 .. s\!:\;\SubtypeStd{S_j}{T_j}}{%
+  % ------------------------------------------------ Covariance
+  %% TODO(eernst): Type aliases have been expanded so there is no other
+  %% variance than covariance, but there will be in/out/inout in classes,
+  %% and then we'll need to handle variance here.
+  \RuleRaw{\SrnCovariance}{%
+    \mbox{$C$ is an interface type with $s$ type parameters.} &
+    \SubtypeStd{S_j}{T_j}\mbox{, for each $j \in 1..s$}}{%
     \code{$C$<\List{S}{1}{s}>}}{\code{$C$<\List{T}{1}{s}>}}
   \ExtraVSP
-  \RuleRaw{\SrnSuperinterface}{Superinterface}{%
-    \code{\CLASS{} $C$<\TypeParametersNoBounds{X}{s}>\,\ldots\,\{\}}\\
+  % ------------------------------------------------ Superinterface
+  \RuleRaw{\SrnNominal}{%
+    \mbox{$C$ is an interface type with type parameters \List{X}{1}{s}}\\
     \Superinterface{\code{$D$<\List{T}{1}{m}>}}{C} &
     \SubtypeStd{[S_1/X_1,\ldots,S_s/X_s]\code{$D$<\List{T}{1}{m}>}}{T}}{%
     \code{$C$<\List{S}{1}{s}>}\;}{\;T}
@@ -21999,6 +22061,9 @@ \subsubsection{Meta-Variables}
 \item $T$ and $S$ range over types, possibly with an index like $T_1$ or $S_j$.
 \item $B$ ranges over types, again possibly with an index;
   it is only used as a type variable bound.
+\item $r$ and $r'$ range over \REQUIRED{} or empty;
+  it is used to enable the specification of a named parameter
+  which may or may not have the modifier \REQUIRED.
 \end{itemize}
 
 
@@ -22010,9 +22075,9 @@ \subsubsection{Subtype Rules}
 Whenever a rule contains one or more meta-variables,
 that rule can be used by
 \IndexCustom{instantiating}{instantiation!subtype rule}
-it, that is, by consistently replacing
-each occurrence of a given meta-variable by
-concrete syntax denoting the same type.
+it, that is, by choosing a specific type $T$ and metavariable $\cal V$,
+and then consistently replacing all occurrences of $\cal V$ by
+concrete syntax denoting $T$.
 
 \commentary{%
   In general, this means that two or more occurrences of
@@ -22025,41 +22090,35 @@ \subsubsection{Subtype Rules}
   can be used to conclude
   \Subtype{\emptyset}{\code{int}}{\code{int}},
   where $\emptyset$ denotes the empty environment
-  (any environment would suffice because no type variables occur).
-
-  However, the wording `denoting the same type' above covers
-  additional situations as well:
-  For instance, we may use rule~\SrnReflexivity{}
-  to show that \code{p1.C} is a subtype of
-  \code{p2.C} when \code{C} is a class declared in a
-  library $L$ which is imported by libraries $L_1$ and $L_2$ and
-  used in declarations there,
-  when $L_1$ and $L_2$ are imported with prefixes
-  \code{p1} respectively \code{p2} by the current library.
-  The important point is that all occurrences of the same meta-variable
-  in a given rule instantiation stands for the same type,
-  even in the case where that type is not denoted by
-  the same syntax in both cases.
-
-  Conversely, we can \emph{not} use the same rule to conclude
-  that \code{C} is a subtype of \code{C}
-  in the case where the former denotes a class declared in library $L_1$
-  and the latter denotes a class declared in $L_2$, with $L_1 \not= L_2$.
-  This situation can arise without compile-time errors, e.g.,
-  if $L_1$ and $L_2$ are imported indirectly into the current library
-  and the two ``meanings'' of \code{C} are used
-  as type annotations on variables or formal parameters of functions
-  declared in intermediate libraries importing $L_1$ respectively $L_2$.
-  The failure to prove
-  ``\Subtype{\emptyset}{\code{C}}{\code{C}}''
-  will then occur, e.g., in a situation where we check whether
-  such a variable can be passed as an actual argument to such a function,
-  because the two occurrences of \code{C} do not denote the same type.%
-}
-
-\LMHash{}%
-Every \synt{typeName} used in a type mentioned in this section is assumed to
-have no compile-time error and denote a type.
+  (any environment would suffice because no type variables occur).%
+
+  However, we must eliminate the difficulties associated with
+  different syntax denoting the same type,
+  and different types denoted by the same syntax.
+  We do this by assuming that every type in the program has been expressed
+  in a manner where those situations never occur,
+  because each type is denoted by the same globally unique syntax everywhere.%
+}
+
+\LMHash{}%
+In section~\ref{subtypes} and its subsections,
+all designations of types are considered to be the same
+if{}f they have the same canonical syntax
+(\ref{theCanonicalSyntaxOfTypes}).
+
+\commentary{%
+  Note that the canonical syntax also implies
+  transitive expansion of all type aliases
+  (\ref{typedef}).
+  In other words, subtyping rules do not need to consider type aliases,
+  because all type aliases have been expanded.%
+}
+
+\LMHash{}%
+Every \synt{typeName} used in a type mentioned
+in section~\ref{subtypes} and its subsections
+is assumed to have no compile-time error,
+and it is assumed to denote a type.
 
 \commentary{%
   That is, no subtyping relationship can be proven for
@@ -22109,9 +22168,11 @@ \subsubsection{Subtype Rules}
   So
   $\{ \code{X} \mapsto \code{int}, \code{Y} \mapsto \code{double} \} \uplus
   \{ \code{Z} \mapsto \code{Object} \} =
-  \{ \code{X} \mapsto \code{int}, \code{Y} \mapsto \code{double}, \code{Z} \mapsto \code{Object} \}$
+  \{ \code{X} \mapsto \code{int}, \code{Y} \mapsto \code{double}, %
+  \code{Z} \mapsto \code{Object} \}$
   and
-  $\{ \code{X} \mapsto \code{int}, \code{Y} \mapsto \code{FutureOr<List<double>{}>} \} \uplus
+  $\{ \code{X} \mapsto \code{int}, \code{Y} \mapsto %
+  \code{FutureOr<List<double>{}>} \} \uplus
   \{ \code{Y} \mapsto \code{int} \} =
   \{ \code{X} \mapsto \code{int}, \code{Y} \mapsto \code{int} \}$.
   Note that operator $\uplus$ is concerned with scopes and shadowing,
@@ -22122,7 +22183,8 @@ \subsubsection{Subtype Rules}
 In this specification we frequently refer to
 subtype relationships and assignability
 without mentioning the environment explicitly,
-as in \Index{\SubtypeNE{S}{T}}.
+as in
+\IndexCustom{\SubtypeNE{S}{T}}{$<:$@\SubtypeNE{S}{T}}.
 This is only done when a specific location in code is in focus,
 and it means that the environment is that which is obtained
 by mapping each type variable in scope at that location
@@ -22149,48 +22211,18 @@ \subsubsection{Subtype Rules}
 }
 
 
-\subsubsection{Being a subtype}
+\subsubsection{Being a Subtype}
 \LMLabel{beingASubtype}
 
 \LMHash{}%
 A type $S$ is shown to be a \Index{subtype} of another type $T$
 in an environment $\Delta$ by providing
 an instantiation of a rule $R$ whose conclusion is
-\IndexCustom{\SubtypeStd{S}{T}}{$\Delta$@\SubtypeStd{S}{T}},
+\IndexCustom{\SubtypeStd{S}{T}}{$\Delta<:$@\SubtypeStd{S}{T}},
 along with rule instantiations showing
 each of the premises of $R$,
 continuing until a rule with no premises is reached.
 
-\commentary{%
-  For rule \SrnNull, note that the \code{Null} type
-  is a subtype of all non-$\bot$ types,
-  even though it doesn't actually extend or implement those types.
-  The other types are effectively treated as if they were nullable,
-  which makes the null object (\ref{null}) assignable to them.%
-}
-
-\LMHash{}%
-The first premise in the
-rules~\SrnLeftTypeAlias{} and~\SrnRightTypeAlias{}
-is a type alias declaration.
-This premise is satisfied in each of the following situations:
-
-\begin{itemize}
-\item A non-generic type alias named $F$ is declared.
-  In this case $s$ is zero,
-  no assumptions are made about the existence
-  of any formal type parameters,
-  and actual type argument lists are omitted everywhere in the rule.
-\item We may choose $s$ and \List{X}{1}{s} such that the following holds:
-  A generic type alias named $F$ is declared,
-  with formal type parameters \List{X}{1}{s}.
-  \commentary{%
-    Each formal type parameter $X_j$ may have a bound,
-    but the bounds are never used in this context,
-    so we do not introduce metavariables for them.%
-  }
-\end{itemize}
-
 \LMHash{}%
 Rule~\SrnRightFunction{} has as a premise that `$T$ is a function type'.
 This means that $T$ is a type of one of the forms introduced in
@@ -22203,28 +22235,14 @@ \subsubsection{Being a subtype}
 }
 
 \LMHash{}%
-In rules~\SrnCovariance{} and~\SrnSuperinterface,
-the first premise is a class declaration.
-This premise is satisfied in each of the following situations:
-
-\begin{itemize}
-\item A non-generic class named $C$ is declared.
-  In this case $s$ is zero,
-  no assumptions are made about the existence
-  of any formal type parameters,
-  and actual type argument lists are omitted everywhere in the rule.
-\item We may choose $s$ and \List{X}{1}{s} such that the following holds:
-  A generic class named $C$ is declared,
-  with formal type parameters \List{X}{1}{s}.
-  \commentary{%
-    Each formal type parameter $X_j$ may have a bound,
-    but the bounds are never used in this context,
-    so we do not introduce metavariables for them.%
-  }
-\end{itemize}
+In rules~\SrnCovariance{} and~\SrnNominal,
+the first premise is that the given name denotes an interface type
+(\ref{interfaceTypes})
+with the specified type parameters.
+The non-generic case is covered by having zero type parameters.
 
 \LMHash{}%
-The second premise of rule~\SrnSuperinterface{} specifies that
+The second premise of rule~\SrnNominal{} specifies that
 a parameterized type \code{$D$<\ldots{}>} belongs to
 \IndexCustom{\Superinterfaces{C}}{superinterfaces(C)@\Superinterfaces{C}}.
 The semantic function \Superinterfaces{\_} applied to a generic class $C$ yields
@@ -22242,23 +22260,12 @@ \subsubsection{Being a subtype}
 }
 
 \commentary{%
-  The last premise of rule~\SrnSuperinterface{}
+  The last premise of rule~\SrnNominal{}
   substitutes the actual type arguments \List{S}{1}{s} for the
   formal type parameters \List{X}{1}{s},
   because \List{T}{1}{m} may contain those formal type parameters.%
 }
 
-\commentary{%
-  The rules~\SrnCovariance{} and~\SrnSuperinterface{}
-  are applicable to interfaces,
-  but they can be used with classes as well,
-  because a non-generic class $C$ which is used as a type
-  denotes the interface of $C$,
-  and similarly for a parameterized type
-  \code{$C$<\List{T}{1}{k}>}
-  where $C$ denotes a generic class.%
-}
-
 
 \subsubsection{Informal Subtype Rule Descriptions}
 \LMLabel{informalSubtypeRuleDescriptions}
@@ -22299,8 +22306,8 @@ \subsubsection{Informal Subtype Rule Descriptions}
     the rule is also valid in any environment
     and the environment is never used explicitly,
     so we will not repeat that.
-  \Item{\SrnTop}{Top}
-    Every type is a subtype of \code{Object},
+  \Item{\SrnRightTop}{Right Top}
+    Every type is a subtype of \code{Object?},
     every type is a subtype of \DYNAMIC,
     and every type is a subtype of \VOID.
     Note that this implies that these types are equivalent
@@ -22309,42 +22316,48 @@ \subsubsection{Informal Subtype Rule Descriptions}
     and others with the same property (such as \code{FutureOr<Object>}),
     as top types
     (\ref{superBoundedTypes}).
+  \Item{\SrnLeftTop}{Left Top}
+    If \code{Object?} is a subtype of any given type $T$,
+    then \DYNAMIC{} and \VOID{} are subtypes of $T$, too.
   \Item{\SrnBottom}{Bottom}
-    Every type is a supertype of $\bot$.
-  \Item{\SrnNull}{Null}
-    Every type other than $\bot$ is a supertype of \code{Null}.
-  \Item{\SrnLeftTypeAlias}{Type Alias Left}
-    An application of a type alias to some actual type arguments is
-    a subtype of another type $T$
-    if the expansion of the type alias to the type that it denotes
-    is a subtype of $T$.
-    Note that a non-generic type alias is handled by letting $s = 0$.
-  \Item{\SrnRightTypeAlias}{Type Alias Right}
-    A type $S$ is a subtype of an application of a type alias
-    if $S$ is a subtype of
-    the expansion of the type alias to the type that it denotes.
-    Note that a non-generic type alias is handled by letting $s = 0$.
+    \code{Never} is a subtype of every type.
+  \Item{\SrnRightObjectFour}{Right Object}
+    Interface types and \FUNCTION{} are subtypes of \code{Object}.
+  \Item{\SrnNullOne}{Null Nullable}
+    \code{Null} is a subtype of every type of the form \code{$T$?}.
+  \Item{\SrnNullTwo}{Null FutureOr}
+    \code{Null} is a subtype of \code{FutureOr<$T$>}
+    if \code{Null} is a subtype of $T$.
   \Item{\SrnLeftFutureOr}{Left FutureOr}
     The type \code{FutureOr<$S$>} is a subtype of a given type $T$
-    if $S$ is a subtype of $T$ and \code{Future<$S$>} is a subtype of $T$,
+    if \code{Future<$S$>} is a subtype of $T$ and $S$ is a subtype of $T$,
     for every type $S$ and $T$.
-  \Item{\SrnTypeVariableReflexivityA}{Left Promoted Variable}
-    The type $X \& S$ is a subtype of $X$.
-  \Item{\SrnRightPromotedVariable}{Right Promoted Variable A}
-    The type $S$ is a subtype of $X \& T$ if
-    $S$ is a subtype of both $X$ and $T$.
+  \Item{\SrnLeftNullable}{Left Nullable}
+    A nullable type \code{$S$?} is a subtype of a given type $T$
+    if \code{$S$} is a subtype of $T$ and \code{Null} is a subtype of $T$.
+  \Item{\SrnLeftPromotedVariableOne}{Left Promoted Variable A}
+    The type \code{$X$\,\&\,$S$} is a subtype of $X$.
+  \Item{\SrnRightPromotedVariable}{Right Promoted Variable}
+    The type $S$ is a subtype of \code{$X$\,\&\,$T$}
+    if $S$ is a subtype of both $X$ and $T$.
   \Item{\SrnRightFutureOrA}{Right FutureOr A}
-    The type $S$ is a subtype of \code{FutureOr<$T$>} if
-    $S$ is a subtype of \code{Future<$T$>}.
+    The type $S$ is a subtype of \code{FutureOr<$T$>}
+    if $S$ is a subtype of \code{Future<$T$>}.
   \Item{\SrnRightFutureOrB}{Right FutureOr B}
-    The type $S$ is a subtype of \code{FutureOr<$T$>} if
-    $S$ is a subtype of $T$.
-  \Item{\SrnLeftPromotedVariable}{Left Promoted Variable B}
-    The type $X \& S$ is a subtype of $T$ if
-    $S$ is a subtype of $T$.
+    The type $S$ is a subtype of \code{FutureOr<$T$>}
+    if $S$ is a subtype of $T$.
+  \Item{\SrnRightNullableOne}{Right Nullable A}
+    The type $S$ is a subtype of \code{$T$?}
+    if $S$ is a subtype of $T$.
+  \Item{\SrnRightNullableTwo}{Right Nullable B}
+    The type $S$ is a subtype of \code{$T$?}
+    if $S$ is a subtype of \code{Null}.
+  \Item{\SrnLeftPromotedVariableTwo}{Left Promoted Variable B}
+    The type \code{$X$\,\&\,$S$} is a subtype of $T$
+    if $S$ is a subtype of $T$.
   \Item{\SrnLeftVariableBound}{Left Variable Bound}
-    The type variable $X$ is a subtype of a type $T$ if
-    the bound of $X$
+    The type variable $X$ is a subtype of a type $T$
+    if the bound of $X$
     (as specified in the current environment $\Delta$)
     is a subtype of $T$.
   \Item{\SrnRightFunction}{Right Function}
@@ -22381,8 +22394,9 @@ \subsubsection{Informal Subtype Rule Descriptions}
     and the set of names of named parameters for the latter is a subset
     of that for the former;
     the return type of $F_1$ is a subtype of that of $F_2$;
-    and each parameter type of $F_1$ is a \emph{supertype} of
-    the corresponding parameter type of $F_2$, if any.
+    each parameter type of $F_1$ is a \emph{supertype} of
+    the corresponding parameter type of $F_2$, if any;
+    and each required named parameter in $F_1$ is also required in $F_2$.
     Note that the relationship to function types with no optional parameters,
     and the relationship between function types with no optional parameters,
     is covered by letting $k_2 = 0$ respectively $k_1 = k_2 = 0$,
@@ -22401,11 +22415,13 @@ \subsubsection{Informal Subtype Rule Descriptions}
     This rule may have $s = 0$ and cover a non-generic class as well,
     but that is redundant because this is already covered by
     rule~\SrnReflexivity.
-  \Item{\SrnSuperinterface}{Superinterface}
+  \Item{\SrnNominal}{Nominal Subtyping}
     Considering the case where $s = 0$ and $m = 0$ first,
     a parameterized type based on a non-generic class $C$ is a subtype of
     a parameterized type based on a different non-generic class $D$ if
     $D$ is a direct superinterface of $C$.
+    Subtyping relations with indirect superinterfaces are shown by
+    using this rule repeatedly.
     When $s > 0$ or $m > 0$, this rule describes a subtype relationship
     which includes one or more generic classes,
     in which case we need to give names to the formal type parameters of $C$,
@@ -22415,7 +22431,7 @@ \subsubsection{Informal Subtype Rule Descriptions}
     that exists between two parameterized types based on $C$ and $D$.
     %
     %% TODO(eernst): Note that the specification of how to pass type arguments
-    %% in \ref{mixinApplication} is incorrect, and also that it will need to be
+    %% \in ref{mixinApplication} is incorrect, and also that it will need to be
     %% rewritten completely for the integration of the new mixin construct.
     The case where the superclass is a mixin application is covered via
     the equivalence with a declaration of
@@ -22423,7 +22439,7 @@ \subsubsection{Informal Subtype Rule Descriptions}
     (\ref{mixinApplication}),
     and this means that there may be multiple subtype steps from
     a given class declaration to the class specified in an \EXTENDS{} clause.
-  \end{itemize}%
+\end{itemize}%
 }
 
 
@@ -22432,33 +22448,33 @@ \subsubsection{Additional Subtyping Concepts}
 
 \LMHash{}%
 $S$ is a \Index{supertype} of $T$ in a given environment $\Delta$,
-written \SupertypeStd{S}{T},
+written
+\IndexCustom{\SupertypeStd{S}{T}}{$\Delta:>$@\SupertypeStd{S}{T}},
 if{}f \SubtypeStd{T}{S}.
 
+\LMHash{}%
+$S$ and $T$ are \Index{mutual subtypes} of each other
+in a given environment $\Delta$,
+written
+\IndexCustom{\MutualSubtypeStd{S}{T}}{$\Delta<:>$@\MutualSubtypeStd{S}{T}},
+if{}f both \SubtypeStd{T}{S} and \SubtypeStd{S}{T}.
+
 \LMHash{}%
 A type $T$
 \Index{may be assigned}
-to a type $S$ in an environment $\Delta$,
-written \AssignableStd{S}{T},
-if{}f either \SubtypeStd{S}{T} or \SubtypeStd{T}{S}.
-In this case we say that the types $S$ and $T$ are
-\Index{assignable}.
+to a type $S$ in an environment $\Delta$
+if{}f $T$ is \DYNAMIC, or \SubtypeStd{T}{S}.
+In this case we also say that the type $T$ is \Index{assignable} to $S$.
 
 \rationale{%
-  This rule may surprise readers accustomed to conventional typechecking.
-  The intent of the \AssignableRelationSymbol{} relation
-  is not to ensure that an assignment is guaranteed to succeed dynamically.
-  Instead, it aims to only flag assignments
-  that are almost certain to be erroneous,
-  without precluding assignments that may work.
-
-  For example, assigning an object of static type \code{Object}
-  to a variable with static type \code{String},
-  while not guaranteed to be correct,
-  might be fine if the run-time value happens to be a string.
-
-  A static analyzer or compiler
-  may support more strict static checks as an option.%
+  The use of the type \DYNAMIC{} is intended to shift type checks from
+  compile time to run time,
+  thus allowing operations that are not statically safe,
+  but which may succeed or fail at run time.
+  This treatment of \DYNAMIC{} ensures that
+  expressions of type \DYNAMIC{} are treated
+  as if the compiler would implicitly insert a downcast whenever needed,
+  in order to make the program type correct.%
 }
 
 

From e9ea0fde657d58d4578512a09f561bdecd4eac57 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Dec 2023 15:40:06 +0100
Subject: [PATCH 02/82] Integrated null-safety into the appendix about
 subtyping

---
 specification/dart.sty         |  27 +--
 specification/dartLangSpec.tex | 369 ++++++++++++++++++++-------------
 2 files changed, 240 insertions(+), 156 deletions(-)

diff --git a/specification/dart.sty b/specification/dart.sty
index 6c856874b5..73c41f65c8 100644
--- a/specification/dart.sty
+++ b/specification/dart.sty
@@ -124,11 +124,11 @@
 \newenvironment{commentary}[1]{{\color{commentaryColor}\sf{#1}}}{}
 
 % Auxiliary functions.
-\newcommand{\flattenName}{\mbox{\it flatten}}
+\newcommand{\flattenName}{\metavar{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})}}
+\newcommand{\futureOrBase}[1]{\ensuremath{\metavar{futureOrBase}({#1})}}
+\newcommand{\overrides}[1]{\ensuremath{\metavar{overrides}({#1})}}
+\newcommand{\inherited}[1]{\ensuremath{\metavar{inherited}({#1})}}
 
 % Used as a mini-section marker, indicating visibly that a range of
 % text (usually just a couple of paragraphs) are concerned with one
@@ -200,7 +200,11 @@
 
 % Mark a compile-time error in the margin.
 \newcommand{\Error}[1]{%
-  \leavevmode\marginpar{\ensuremath{_{^\ominus}}}{#1}}
+  \leavevmode\marginpar{\ensuremath{_{\textcolor{red}{^\ominus}}}}{#1}}
+
+% Mark a dynamic error in the margin.
+\newcommand{\DynamicError}[1]{%
+  \leavevmode\marginpar{\textcolor{red}{\Lightning}}{#1}}
 
 % Used to specify comma separated lists of similar symbols.
 \newcommand{\List}[3]{\ensuremath{{#1}_{#2},\,\ldots,\ {#1}_{#3}}}
@@ -402,9 +406,9 @@
 
 % Same as \FunctionTypeNamed except suitable for inline usage, hence omitting
 % the spacer argument.
-\newcommand{\RawFunctionTypeNamed}[8]{%
+\newcommand{\RawFunctionTypeNamed}[9]{%
   \RawFunctionType{#1}{#2}{#3}{#4}{%
-    \FunctionTypeNamedParameters{#5}{#6}{#7}{#8}{r}}}
+    \FunctionTypeNamedParameters{#5}{#6}{#7}{#8}{#9}}}
 
 % A variant of \FunctionTypeNamed that uses the standard symbols,
 % that is, a function type with positional optional parameters which
@@ -471,11 +475,10 @@
 \newcommand{\Supertype}[3]{\ensuremath{{#1}\vdash{#2}\,:>\,{#3}}}
 \newcommand{\SupertypeStd}[2]{\Supertype{\Delta}{#1}{#2}}
 
-% Judgment expressing that an assignability relation exists.
-\newcommand{\AssignableRelationSymbol}{\ensuremath{\Longleftrightarrow}}
-\newcommand{\Assignable}[3]{%
-  \ensuremath{{#1}\vdash{#2}\,\AssignableRelationSymbol\,{#3}}}
-\newcommand{\AssignableStd}[2]{\Assignable{\Gamma}{#1}{#2}}
+% Judgment expressing that a subtype and a supertype relation exist.
+\newcommand{\MutualSubtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:>\,{#3}}}
+\newcommand{\MutualSubtypeStd}[2]{\MutualSubtype{\Delta}{#1}{#2}}
+\newcommand{\MutualSubtypeNE}[2]{\ensuremath{{#1}\,<:>\,{#2}}}
 
 % Semantic function delivering the superinterfaces of a class.
 \newcommand{\Superinterfaces}[1]{\ensuremath{\metavar{Superinterfaces}({#1})}}
diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 7d6f92bc42..ccbbcf17db 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23545,157 +23545,238 @@ \subsection{Operator Precedence}
 \section*{Appendix: Algorithmic Subtyping}
 \LMLabel{algorithmicSubtyping}
 
-% Subtype Rule Numbering
-\newcommand{\AppSrnReflexivity}{\ensuremath{1_{\scriptsize\mbox{algo}}}}
-\newcommand{\AppSrnTypeVariableReflexivityB}{\SrnTypeVariableReflexivityA.1}
-\newcommand{\AppSrnTypeVariableReflexivityC}{\SrnTypeVariableReflexivityA.2}
-\newcommand{\AppSrnTypeVariableReflexivityD}{\SrnTypeVariableReflexivityA.3}
-\newcommand{\AppSrnRightFutureOrC}{\SrnRightFutureOrB.1}
-\newcommand{\AppSrnRightFutureOrD}{\SrnRightFutureOrB.2}
-
-\begin{figure}[h!]
-  \def\VSP{\vspace{3mm}}
-  \def\ExtraVSP{\vspace{1mm}}
-  \def\Axiom#1#2#3#4{\centerline{\inference[#1]{}{\SubtypeStd{#3}{#4}}}\VSP}
-  \def\Rule#1#2#3#4#5#6{\centerline{\inference[#1]{\SubtypeStd{#3}{#4}}{\SubtypeStd{#5}{#6}}}\VSP}
-  \def\RuleTwo#1#2#3#4#5#6#7#8{%
-    \centerline{\inference[#1]{\SubtypeStd{#3}{#4} & \SubtypeStd{#5}{#6}}{\SubtypeStd{#7}{#8}}}\VSP}
-  \def\RuleRaw#1#2#3#4#5{%
-    \centerline{\inference[#1]{#3}{\SubtypeStd{#4}{#5}}}\VSP}
-  \def\RuleRawRaw#1#2#3#4{\centerline{\inference[#1]{#3}{#4}}\VSP}
-  %
-  \begin{minipage}[c]{0.49\textwidth}
-    \RuleRaw{\AppSrnReflexivity}{Reflexivity}{S\mbox{ not composite}}{S}{S}
-    \Rule{\AppSrnTypeVariableReflexivityC}{Type Variable Reflexivity B}{X}{T}{X}{X \& T}
-    \Rule{\AppSrnRightFutureOrC}{Right FutureOr C}{\Delta(X)}{\code{FutureOr<$T$>}}{X}{\code{FutureOr<$T$>}}
-  \end{minipage}
-  \begin{minipage}[c]{0.49\textwidth}
-    \Axiom{\AppSrnTypeVariableReflexivityB}{Type Variable Reflexivity}{X}{X}
-    \Rule{\AppSrnTypeVariableReflexivityD}{Type Variable Reflexivity C}{X \& S}{T}{X \& S}{X \& T}
-    \Rule{\AppSrnRightFutureOrD}{Right FutureOr D}{S}{\code{FutureOr<$T$>}}{X \& S}{\code{FutureOr<$T$>}}
-  \end{minipage}
-  %
-  \caption{Algorithmic subtype rules.
-    Rules \SrnTop--\SrnSuperinterface{} are unchanged and hence omitted here.}
-  \label{fig:algorithmicSubtypeRules}
-\end{figure}
+\LMHash{}%
+The following algorithm computes the same relation as
+the one which is specified in Fig.~\ref{fig:subtypeRules}.
+It shows that Dart subtyping relationships can be decided
+with good performance.
 
 \LMHash{}%
-The text in this appendix is not part of the specification of the Dart language.
-However, we still use the notation where precise information
-uses the style associated with normative text in the specification (this style),
-\commentary{whereas examples and explanations use commentary style (like this)}.
+In this algorithm, types are considered to be the same when they have
+the same canonical syntax
+(\ref{theCanonicalSyntaxOfTypes}).
+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{%
+  that is, in some situations the subtype relation is determined to be false%
+}),
+which is important for performance because
+it is then unnecessary to consider any subsequent cases.
 
 \LMHash{}%
-This appendix presents a variant of the subtype rules given
-in Figure~\ref{fig:subtypeRules} on page~\pageref{fig:subtypeRules}.
+A type $T_0$ is a subtype of a type $T_1$ (written \SubtypeNE{T_0}{T_1}) when:
 
-\commentary{%
-  The rules will prove the same set of subtype relationships,
-  but the rules given here show that there is an efficient implementation
-  that will determine whether \SubtypeStd{S}{T} holds,
-  for any given types $S$ and $T$.
-  It is easy to see that the algorithmic rules will prove at most
-  the same subtype relationships,
-  because all rules given here can be proven
-  by means of rules in Figure~\ref{fig:subtypeRules}.
-  It is also relatively straightforward to sketch out proofs
-  that the algorithmic rules can prove at least the same subtype relationships,
-  also when the following ordering and termination constraints are observed.%
-}
+\begin{itemize}
+\item
+  \textbf{Reflexivity:}
+  if $T_0$ and $T_1$ are the same type then \SubtypeNE{T_0}{T_1}
 
-\LMHash{}%
-The only rule which is modified is number~\SrnReflexivity,
-which is modified to \AppSrnReflexivity.
-This only changes the applicability of the rule:
-This rule is only used for types which are not atomic.
-An \IndexCustom{atomic type}{type!atomic}
-is a type which is not a type variable,
-not a promoted type variable,
-not a function type,
-and not a parameterized type.
+  \commentary{%
+    Note that 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.%
+  }
+\item
+  \textbf{Right Top:}
+  if $T_1$ is \DYNAMIC, \VOID, or \code{Object?} then \SubtypeNE{T_0}{T_1}.
+\item
+  \textbf{Left Top:}
+  if $T_0$ is \DYNAMIC{} or \VOID{}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{\code{Object?}}{T_1}.
+\item
+  \textbf{Left Bottom:}
+  if $T_0$ is \code{Never} then \SubtypeNE{T_0}{T_1}.
+\item
+  \textbf{Right Object:}
+  if $T_1$ is \code{Object} then:
+  \begin{itemize}
+  \item
+    if $T_0$ is an unpromoted type variable with bound $B$
+    then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B}{\code{Object}}.
+  \item
+    if $T_0$ is a promoted type variable \code{$X$\,\&\,$S$}
+    then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S}{\code{Object}}.
+  \item
+    if $T_0$ is \code{FutureOr<$S$>} for some $S$,
+    then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S}{\code{Object}}.
+  \item
+    if $T_0$ is \code{Null}, \DYNAMIC, \VOID, or \code{$S$?} for any $S$,
+    then the subtyping does not hold
+    (\commentary{%
+      i.e., the result of the subtyping query is known to be false%
+    }).
+  \item
+    Otherwise \SubtypeNE{T_0}{T_1} is true.
+  \end{itemize}
+\item
+  \textbf{Left Null:}
+  if $T_0$ is \code{Null} then:
+  \begin{itemize}
+  \item
+    if $T_1$ is a type variable (promoted or not) the query is false.
+  \item
+    if $T_1$ is \code{FutureOr<$S$>} for some $S$,
+    then the query is true if{}f \SubtypeNE{\code{Null}}{S}.
+  \item
+    if $T_1$ is \code{$S$?} for some $S$ then the query is true.
+  \item
+    Otherwise, the query is false.
+  \end{itemize}
+\item
+  \textbf{Left FutureOr:}
+  if $T_0$ is \code{FutureOr<$S_0$>}
+  then \SubtypeNE{T_0}{T_1} if{}f
+  \SubtypeNE{\code{Future<$S_0$>}}{T_1} and \SubtypeNE{S_0}{T_1}.
+\item
+  \textbf{Left Nullable:}
+  if $T_0$ is \code{$S_0$?} then \SubtypeNE{T_0}{T_1} if{}f
+  \SubtypeNE{S_0}{T_1} and \SubtypeNE{\code{Null}}{T_1}.
+\item
+  \textbf{Type Variable Reflexivity 1:}
+  if $T_0$ is a type variable $X_0$
+  or a promoted type variables \code{$X_0$\,\&\,$S_0$} and $T_1$ is $X_0$
+  then \SubtypeNE{T_0}{T_1}.
 
-\commentary{%
-  In other words, rule \AppSrnReflexivity{} is used for
-  special types like \DYNAMIC, \VOID, and \FUNCTION,
-  and it is used for non-generic classes,
-  but it is not used for any type where it is an operation
-  that takes more than one comparison to detect whether
-  it is the same as some other type.
-  %
-  The point is that the remaining rules will force
-  a structural traversal anyway, as far as needed,
-  and we may hence just as well omit the initial structural traversal
-  which might take many steps only to report that two large type terms
-  are not quite identical.%
-}
-
-\LMHash{}%
-The rules are ordered by means of their rule numbers:
-A rule given here numbered $N.1$ is inserted immediately after rule $N$,
-followed by rule $N.2$, and so on,
-followed by the rule whose number is $N+1$.
-\commentary{%
-  So the order is
-  \AppSrnReflexivity, \SrnTop--\SrnTypeVariableReflexivityA,
-  \AppSrnTypeVariableReflexivityB, \AppSrnTypeVariableReflexivityC,
-  \AppSrnTypeVariableReflexivityD,
-  \SrnRightPromotedVariable, and so on.%
-}
-
-\LMHash{}%
-We now specify the procedure which is used to determine whether
-\SubtypeStd{S}{T} holds,
-for some specific types $S$ and $T$:
-Select the first rule $R$ whose syntactic constraints are satisfied
-by the given types $S$ and $T$,
-and proceed to show that its premises hold.
-If so, we terminate and conclude that the subtype relationship holds.
-Otherwise we terminate and conclude
-that the subtype relationship does not hold,
-except if $R$ is
-\SrnRightFutureOrA, \SrnRightFutureOrB,
-\AppSrnRightFutureOrC, or \AppSrnRightFutureOrD.
-\commentary{%
-  In particular, for the original query \SubtypeStd{S}{T},
-  we do not backtrack into trying to use a rule that has
-  a higher rule number than that of $R$,
-  except that we may try all of
-  the rules with \code{FutureOr<$T$>} to the right.%
-}
-
-\commentary{%
-  Apart from the fact that the full complexity of subtyping
-  is potentially incurred each time it is checked whether a premise holds,
-  the checks applied for each rule is associated with an amount of work
-  which is constant for all rules except the following:
-  First, the group of rules
-  \SrnRightFutureOrA, \SrnRightFutureOrB,
-  \AppSrnRightFutureOrC, and \AppSrnRightFutureOrD{}
-  may cause backtracking to take place.
-  Next, rules \SrnPositionalFunctionType--\SrnCovariance{}
-  require work proportional to the size of $S$ and $T$,
-  due to the number of premises that must be checked.
-  Finally, rule~\SrnSuperinterface{} requires work
-  proportional to the size of $S$,
-  and it may also incur the cost of searching up to the entire set of
-  direct and indirect superinterfaces of the candidate subtype $S$,
-  until the corresponding premise for one of them is shown to hold,
-  if any.
-
-  Additional optimizations are applicable.
-  For instance,
-  we can immediately conclude that the subtype relationship does not hold
-  when we are about to check rule~\SrnSuperinterface{}
-  if $T$ is a type variable or a function type.
-  For several other forms of type, e.g.,
-  a promoted type variable,
-  \code{Object}, \DYNAMIC, \VOID,
-  \code{FutureOr<$T$>} for any $T$, or \FUNCTION,
-  it is known that it will never occur as $T$ for rule~\SrnSuperinterface,
-  which means that this seemingly expensive step
-  can be confined to some extent.%
-}
+  \commentary{%
+    Note that this rule is admissible, and can be safely elided if desired.%
+  }
+\item
+  \textbf{Type Variable Reflexivity 2:}
+  if $T_0$ is a type variable $X_0$
+  or a promoted type variable \code{$X_0$\,\&\,$S_0$}
+  and $T_1$ is \code{$X_0$\,\&\,$S_1$}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{T_0}{S_1}.
+
+  \commentary{%
+    Note that this rule is admissible, and can be safely elided if desired.%
+  }
+\item
+  \textbf{Right Promoted Variable:}
+  if $T_1$ is a promoted type variable \code{$X_1$\,\&\,$S_1$}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{T_0}{X_1} and \SubtypeNE{T_0}{S_1}.
+\item
+  \textbf{Right FutureOr:}
+  if $T_1$ is \code{FutureOr<$S_1$>}
+  then \SubtypeNE{T_0}{T_1} if{}f any of the following hold:
+  \begin{itemize}
+  \item either \SubtypeNE{T_0}{\code{Future<$S_1$>}}.
+  \item or \SubtypeNE{T_0}{S_1}.
+  \item or $T_0$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T_1}.
+  \item or $T_0$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T_1}.
+  \end{itemize}
+\item
+  \textbf{Right Nullable:}
+  if $T_1$ is \code{$S_1$?}
+  then \SubtypeNE{T_0}{T_1} if{}f any of the following hold:
+  \begin{itemize}
+  \item either \SubtypeNE{T_0}{S_1}.
+  \item or \SubtypeNE{T_0}{\code{Null}}.
+  \item or $T_0$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T_1}.
+  \item or $T_0$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T_1}.
+  \end{itemize}
+\item
+  \textbf{Left Promoted Variable:}
+  $T_0$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
+  and \SubtypeNE{S_0}{T_1}.
+\item
+  \textbf{Left Type Variable Bound:}
+  $T_0$ is a type variable $X_0$ with bound $B_0$
+  and \SubtypeNE{B_0}{T_1}.
+\item
+  \textbf{Function Type/Function:}
+  $T_0$ is a function type and $T_1$ is \FUNCTION.
+\item
+  \textbf{Interface Compositionality:}
+  $T_0$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
+  and $T_1$ is \code{$C_0$<$U_0$, \ldots, $U_k$>} and each \SubtypeNE{S_i}{U_i}.
+\item
+  \textbf{Super-Interface:}
+  $T_0$ is an interface type with super-interfaces \List{S}{0}{n}
+  and \SubtypeNE{S_i}{T_1} for some $i$.
+\item
+  \textbf{Positional Function Types:}
+  $T_0$ is
+
+  \code{$U_0$ \FUNCTION<%
+    $X_0$\,\EXTENDS\,$B_{00}$, \ldots, $X_k$\,\EXTENDS\,$B_{0k}$>(%
+    $V_0$\,$x_0$, \ldots, $V_n$ $x_n$, %
+    [$V_{n+1}$\,\,$x_{n+1}$, \ldots, $V_m$\,\,$x_m$])}
+
+  and $T_1$ is
+
+  \code{$U_1$ \FUNCTION<%
+    $Y_0$\,\EXTENDS\,$B_{10}$, \ldots, $Y_k$\,\EXTENDS\,$B_{1k}$>(%
+    $S_0$\,$y_0$, \ldots, $S_p$\,$y_p$, %
+    [$S_{p+1}$\,$y_{p+1}$, \ldots, $S_q$\,$y_q$])}
+
+  such that each of the following criteria is satisfied,
+  where the $Z_i$ are fresh type variables with bounds
+  $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$:
+
+  \begin{itemize}
+  \item $p \geq n$.
+  \item $m \geq q$.
+  \item \SubtypeNE{S_i[Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i[Z_0/X_0, \ldots, Z_k/X_k]}
+    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$.
+  \end{itemize}
+\item
+  \textbf{Named Function Types:}
+  $T_0$ is
+
+  \code{%
+    $U_0$ \FUNCTION<$X_0$\,\EXTENDS\,$B_{00}$, \ldots, %
+      $X_k$\,\EXTENDS\,$B_{0k}$>(%
+        $V_0$\,$x_0$, \ldots, $V_n$\,$x_n$, %
+          \{$r_{0,n+1}$\,$V_{n+1}$\,$x_{n+1}$, \ldots, $r_{0m}$\,$V_m$\,$x_m$\})}
+
+  where $r_{0j}$ is empty or \REQUIRED{} for $j \in n+1 .. m$
+  and $T_1$ is
+
+  \code{%
+    $U_1$ \FUNCTION<$Y_0$\,\EXTENDS\,$B_{10}$, \ldots, %
+      $Y_k$\,\EXTENDS\,$B_{1k}$>(%
+        $S_0$\,$y_0$, \ldots, $S_n$\,$y_n$, %
+          \{$r_{1,n+1}$\,$S_{n+1}$\,$y_{n+1}$, \ldots, $r_{1q}$\,$S_q$\,$y_q$\})}
+
+  where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
+  and the following criteria are all satisfied,
+  where \List{Z}{1}{k} are fresh type variables with bounds
+  $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$:
+
+  \begin{itemize}
+  \item
+    $\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
+  \item
+    \SubtypeNE{S_i[Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i[Z_0/X_0, \ldots, Z_k/X_k]}
+    for $i \in 0 .. n$.
+  \item \SubtypeNE{S_i[Z_0/Y_0, \ldots, Z_k/Y_k]}{V_j[Z_0/X_0, \ldots, Z_k/X_k]}
+    for $i \in n+1 .. q$, and $y_j = x_i$.
+  \item
+    for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
+    $i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
+  \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 each $i \in 0 .. k$.
+  \end{itemize}
+
+  \commentary{%
+    The requirement that \List{Z}{1}{k} are fresh names is as usual required
+    such that type variable names do not get captured.
+    It is valid to choose $Z_i$ to be $X_i$ or $Y_i$,
+    so long as capture is avoided.%
+  }
+\end{itemize}
 
 
 \section*{Appendix: Integer Implementations}

From d5a65f9e5bf8a153ae6ee3a40578a62c7663bddc Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Dec 2023 18:43:33 +0100
Subject: [PATCH 03/82] Fix a couple of typos

---
 specification/dartLangSpec.tex | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index ccbbcf17db..c0be8129df 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -22052,15 +22052,15 @@ \subsubsection{Meta-Variables}
 }
 
 \LMHash{}%
-In this section we use the following meta-variables:
+In this section (\ref{subtypes}) we use the following meta-variables,
+possibly with an index like $X_1$ or $S_j$:
 
 \begin{itemize}
 \item $X$ ranges over type variables.
 \item $C$ ranges over classes,
 \item $F$ ranges over type aliases.
-\item $T$ and $S$ range over types, possibly with an index like $T_1$ or $S_j$.
-\item $B$ ranges over types, again possibly with an index;
-  it is only used as a type variable bound.
+\item $T$ and $S$ range over types.
+\item $B$ ranges over types; it is only used as a type variable bound.
 \item $r$ and $r'$ range over \REQUIRED{} or empty;
   it is used to enable the specification of a named parameter
   which may or may not have the modifier \REQUIRED.
@@ -22285,8 +22285,8 @@ \subsubsection{Informal Subtype Rule Descriptions}
   For example, rule~\SrnRightFutureOrA{} says that
   ``The type $S$ is a \ldots{} of \code{FutureOr<$T$>} \ldots'',
   and this is taken to mean that for any arbitrary types $S$ and $T$,
-  showing that $S$ is a subtype of $T$ is sufficient to show that $S$ is
-  a subtype of \code{FutureOr<$T$>}.
+  in order to show that $S$ is a subtype of \code{FutureOr<$T$>},
+  it is sufficient to show that $S$ is a subtype of $T$.
 
   Another example is the wording in rule~\SrnReflexivity{}:
   ``\ldots{} in any environment $\Delta$'',
@@ -22313,7 +22313,7 @@ \subsubsection{Informal Subtype Rule Descriptions}
     Note that this implies that these types are equivalent
     according to the subtype relation.
     We denote these types,
-    and others with the same property (such as \code{FutureOr<Object>}),
+    and others with the same property (such as \code{FutureOr<Object>?}),
     as top types
     (\ref{superBoundedTypes}).
   \Item{\SrnLeftTop}{Left Top}
@@ -22431,7 +22431,7 @@ \subsubsection{Informal Subtype Rule Descriptions}
     that exists between two parameterized types based on $C$ and $D$.
     %
     %% TODO(eernst): Note that the specification of how to pass type arguments
-    %% \in ref{mixinApplication} is incorrect, and also that it will need to be
+    %% in \ref{mixinApplication} is incorrect, and also that it will need to be
     %% rewritten completely for the integration of the new mixin construct.
     The case where the superclass is a mixin application is covered via
     the equivalence with a declaration of

From 757a33c7b0137ba9ca66f1c5a535627f52b7a3a1 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 17 Oct 2024 13:56:53 +0200
Subject: [PATCH 04/82] Adjust dart.sty to change like
 specify_null_safety_sep21

---
 specification/dart.sty | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/specification/dart.sty b/specification/dart.sty
index 73c41f65c8..32609abc6d 100644
--- a/specification/dart.sty
+++ b/specification/dart.sty
@@ -173,9 +173,12 @@
 \newcommand{\id}{\metavar{id}}
 \newcommand{\op}{\metavar{op}}
 
+% Used in margin to indicate that a term is being defined here.
+\newcommand{\IndexMarker}{\ensuremath{^\vartriangle}}
+
 % Used for defining occurrence of phrase, with customized index entry.
 \newcommand{\IndexCustom}[2]{%
-  \leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}\index{#2}}
+  \leavevmode\marginpar{\IndexMarker}\emph{#1}\index{#2}}
 
 % Used for the defining occurrence of a local symbol.
 \newcommand{\DefineSymbol}[1]{%
@@ -196,7 +199,7 @@
 
 % Same appearance, but not adding an entry to the index.
 \newcommand{\NoIndex}[1]{%
-  \leavevmode\marginpar{\ensuremath{_{^\vartriangle}}}\emph{#1}}
+  \leavevmode\marginpar{\IndexMarker}\emph{#1}}
 
 % Mark a compile-time error in the margin.
 \newcommand{\Error}[1]{%
@@ -470,16 +473,14 @@
 \newcommand{\SubtypeStd}[2]{\Subtype{\Delta}{#1}{#2}}
 % Subtype judgment where the environment is omitted (NE: "no environment").
 \newcommand{\SubtypeNE}[2]{\ensuremath{{#1}\,<:\,{#2}}}
+\newcommand{\MutualSubtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:>\,{#3}}}
+\newcommand{\MutualSubtypeStd}[2]{\MutualSubtype{\Delta}{#1}{#2}}
+\newcommand{\MutualSubtypeNE}[2]{\ensuremath{{#1}\,<:>\,{#2}}}
 
 % Judgment expressing that a supertype relation exists.
 \newcommand{\Supertype}[3]{\ensuremath{{#1}\vdash{#2}\,:>\,{#3}}}
 \newcommand{\SupertypeStd}[2]{\Supertype{\Delta}{#1}{#2}}
 
-% Judgment expressing that a subtype and a supertype relation exist.
-\newcommand{\MutualSubtype}[3]{\ensuremath{{#1}\vdash{#2}\,<:>\,{#3}}}
-\newcommand{\MutualSubtypeStd}[2]{\MutualSubtype{\Delta}{#1}{#2}}
-\newcommand{\MutualSubtypeNE}[2]{\ensuremath{{#1}\,<:>\,{#2}}}
-
 % Semantic function delivering the superinterfaces of a class.
 \newcommand{\Superinterfaces}[1]{\ensuremath{\metavar{Superinterfaces}({#1})}}
 \newcommand{\Superinterface}[2]{{#1}\in\Superinterfaces{#2}}

From 5336f3b73900988650fe345831d525a834144e55 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 17 Oct 2024 14:03:15 +0200
Subject: [PATCH 05/82] WIP

---
 specification/dart.sty | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dart.sty b/specification/dart.sty
index 32609abc6d..086e2420f8 100644
--- a/specification/dart.sty
+++ b/specification/dart.sty
@@ -203,7 +203,7 @@
 
 % Mark a compile-time error in the margin.
 \newcommand{\Error}[1]{%
-  \leavevmode\marginpar{\ensuremath{_{\textcolor{red}{^\ominus}}}}{#1}}
+  \leavevmode\marginpar{\ensuremath{\textcolor{red}{\ominus}}}{#1}}
 
 % Mark a dynamic error in the margin.
 \newcommand{\DynamicError}[1]{%

From 5e37cd63f347522da03148c02d2e2cb7202815d1 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 17 Oct 2024 14:44:54 +0200
Subject: [PATCH 06/82] Align this PR with specify_null_safety_sep21

---
 specification/dartLangSpec.tex | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index c0be8129df..538907b42b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -24,13 +24,7 @@
 % CHANGES
 % =======
 %
-% Significant changes to the specification. Note that the versions specified
-% below indicate the current tool chain version when those changes were made.
-% In practice, new features have always been integrated into the language
-% specification (this document) a while after the change was accepted into
-% the language and implemented. As of September 2022, the upcoming version of
-% the language which is being specified is indicated by a version number in
-% parentheses after the tool chain version.
+% Significant changes to the specification.
 %
 % Note that the version numbers used below (up to 2.15) were associated with
 % the currently released language and tools at the time of the spec change,
@@ -53,6 +47,8 @@
 % Jul 2025
 % - Clarify that operator `[]` and `[]=` are included in the `void` allowlist
 %   rule about formal parameters of type `void`, and so are setters.
+% - Integrate the subtyping rule updates that are needed in order to support
+%   null-safety.
 %
 % May 2025
 % - Add `s?.length` as a constant expression in the case where `s` satisfies
@@ -85,8 +81,6 @@
 %   a function literal.
 % - Specify in which situations it is an error to declare an initializing
 %   formal parameter.
-% - Integrate the subtyping rule updates that are needed in order to support
-%   null-safety.
 %
 % Nov 2023
 % - Specify that the dynamic error for calling a function in a deferred and

From 5c2fb659df6eff1ef17b158663102ce35be628d1 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 17 Oct 2024 15:43:48 +0200
Subject: [PATCH 07/82] WIP

---
 specification/dartLangSpec.tex | 80 ++++++++++++++++------------------
 1 file changed, 38 insertions(+), 42 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 538907b42b..27192d7ac4 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -22516,16 +22516,17 @@ \subsection{Function Types}
 
 \LMHash{}%
 A function object is always an instance of some class $C$ that implements
-the class \FUNCTION{} (\ref{functionType}),
-and which has a method named \CALL,
-whose signature is the function type $C$ itself.
+a function type $F$ which is a subtype of the class \FUNCTION{}
+(\ref{functionType}).
+The function object has a method named \CALL,
+whose signature is said function type $F$.
 \commentary{%
   Consequently, all function types are subtypes of \FUNCTION{}
   (\ref{subtypes}).%
 }
 
 
-\subsection{Type \FUNCTION}
+\subsection{Type Function}
 \LMLabel{functionType}
 
 \LMHash{}%
@@ -22547,13 +22548,13 @@ \subsection{Type \FUNCTION}
 \LMHash{}%
 If a mixin application mixes \FUNCTION{} onto a superclass, it follows the
 normal rules for mixin-application, but since the result of that mixin
-application is equivalent to a class with \code{implements Function}, and
+application is equivalent to a class with \code{implements \FUNCTION}, and
 that clause has no effect, the resulting class also does not
 implement \FUNCTION.
 \commentary{%
   The \FUNCTION{} class declares no concrete instance members,
-  so the mixin application creates a sub-class of
-  the superclass with no new members and no new interfaces.%
+  so the mixin application creates a sub-class
+  of the superclass with no new members and no new interfaces.%
 }
 
 \rationale{%
@@ -22566,7 +22567,7 @@ \subsection{Type \FUNCTION}
 }
 
 
-\subsection{Type \DYNAMIC}
+\subsection{Type dynamic}
 \LMLabel{typeDynamic}
 
 \LMHash{}%
@@ -22707,7 +22708,7 @@ \subsection{Type \DYNAMIC}
   \metavar{typeArguments} is a list of actual
   type arguments derived from \synt{typeArguments}, and
   \metavar{arguments} is an actual argument list derived from \synt{arguments}.
-  It is a compile-time error if \id{} is the name of
+  It is a \Error{compile-time error} if \id{} is the name of
   a non-generic method declared in \code{Object}.
   \commentary{%
     No generic methods are declared in \code{Object}.
@@ -22782,7 +22783,7 @@ \subsection{Type FutureOr}
   That is, \code{FutureOr} is in a sense
   the union of $T$ and the corresponding future type.
   The last point guarantees that
-  \code{FutureOr<$T$>} <: \code{Object},
+  \code{FutureOr<$T$>} <: \code{Object?},
   and also that \code{FutureOr} is covariant in its type parameter,
   just like class types:
   if $S$ <: $T$ then \code{FutureOr<$S$>} <: \code{FutureOr<$T$>}.%
@@ -22791,7 +22792,7 @@ \subsection{Type FutureOr}
 \LMHash{}%
 If the type arguments passed to \code{FutureOr} would incur compile-time errors
 if applied to a normal generic class with one type parameter,
-the same compile-time errors are issued for \code{FutureOr}.
+the same \Error{compile-time errors} are issued for \code{FutureOr}.
 The name \code{FutureOr} as an expression
 denotes a \code{Type} object representing the type \code{FutureOr<dynamic>}.
 
@@ -22836,7 +22837,7 @@ \subsection{Type FutureOr}
 \end{itemize}
 
 
-\subsection{Type Void}
+\subsection{Type void}
 \LMLabel{typeVoid}
 
 \LMHash{}%
@@ -22866,16 +22867,16 @@ \subsection{Type Void}
 \commentary{%
   The type \VOID{} is a top type
   (\ref{superBoundedTypes}),
-  so \VOID{} and \code{Object} are subtypes of each other
+  so \VOID{} and \code{Object?} are subtypes of each other
   (\ref{subtypes}),
   which also implies that any object can be
   the value of an expression of type \VOID.
   %
   Consequently, any instance of type \code{Type} which reifies the type \VOID{}
   must compare equal (according to the \lit{==} operator \ref{equality})
-  to any instance of \code{Type} which reifies the type \code{Object}
+  to any instance of \code{Type} which reifies the type \code{Object?}
   (\ref{dynamicTypeSystem}).
-  It is not guaranteed that \code{identical(\VOID, Object)} evaluates to true.
+  It is not guaranteed that those two reified types are identical.
   In fact, it is not recommended that implementations strive to achieve this,
   because it may be more important to ensure that diagnostic messages
   (including stack traces and dynamic error messages)
@@ -22887,7 +22888,7 @@ \subsection{Type Void}
 In support of the notion
 that the value of an expression with static type \VOID{} should be discarded,
 such objects can only be used in specific situations:
-The occurrence of an expression of type \VOID{} is a compile-time error
+The occurrence of an expression of type \VOID{} is a \Error{compile-time error}
 unless it is permitted according to one of the following rules.
 
 \begin{itemize}
@@ -22917,6 +22918,7 @@ \subsection{Type Void}
     where it is not an error to have it.%
   }
 \item
+  %% This relies on \IsMoreTopType{\VOID}{$T$} = \VOID.
   In a conditional expression \code{$e$\,?\,$e_1$\,:\,$e_2$},
   $e_1$ and $e_2$ may have type \VOID.
   \rationale{%
@@ -22926,20 +22928,13 @@ \subsection{Type Void}
     in some context where it is not an error to have it.%
   }
 \item
+  %% This relies on \IsMoreTopType{\VOID}{$T$} = \VOID.
   In a null coalescing expression \code{$e_1$\,??\,$e_2$},
   $e_2$ may have type \VOID.
   \rationale{%
     The static type of the null coalescing expression is then \VOID,
     which in turn restricts where it can occur.%
   }
-\item
-  In an expression of the form \code{\AWAIT\,\,$e$}, $e$ may have type \VOID.
-  \rationale{%
-    This rule was adopted because it was a substantial breaking change
-    to turn this situation into an error
-    at the time where the treatment of \VOID{} was changed.
-    Tools may choose to give a hint in such cases.%
-  }
 \item
   \commentary{%
     In a return statement \code{\RETURN\,$e$;},
@@ -23021,13 +23016,13 @@ \subsection{Type Void}
 Finally, we need to address situations involving implicit usage of
 an object whose static type can be \VOID.
 %
-It is a compile-time error for a for-in statement to have an iterator
+It is a \Error{compile-time error} for a for-in statement to have an iterator
 expression of type $T$ such that \code{Iterator<\VOID{}>}
 is the most specific instantiation of \code{Iterator}
 that is a superinterface of $T$, unless the
 iteration variable has type \VOID.
 %
-It is a compile-time error for an asynchronous for-in statement
+It is a \Error{compile-time error} for an asynchronous for-in statement
 to have a stream expression of type $T$
 such that \code{Stream<\VOID{}>} is the most specific
 instantiation of \code{Stream} that is a superinterface of $T$,
@@ -23036,7 +23031,7 @@ \subsection{Type Void}
 \commentary{Here are some examples:}
 
 \begin{dartCode}
-\FOR{} (Object x in <\VOID>[]) \{\} // \comment{Error.}
+\FOR{} (Object? x in <\VOID>[]) \{\} // \comment{Error.}
 \AWAIT{} \FOR{} (int x \IN{} new Stream<\VOID{}>.empty()) \{\} // \comment{Error.}
 \FOR{} (\VOID{} x \IN{} <\VOID{}>[]) \{\ldots\} // \comment{OK.}
 \FOR (\VAR{} x \IN{} <\VOID{}>[]) \{\ldots\} // \comment{OK, type of x inferred.}
@@ -23084,22 +23079,22 @@ \subsubsection{Void Soundness}
 \ABSTRACT{} \CLASS A<X> \{
   final X x;
   A(this.x);
-  Object foo(X x);
+  Object? foo(X x);
 \}
 \\
 \CLASS{} B<X> \EXTENDS{} A<X> \{
   B(X x): super(x);
-  Object foo(Object x) => x;
+  Object? foo(Object? x) => x;
 \}
 \\
-Object f<X>(X x) => x;
+Object? f<X>(X x) => x;
 \\
 \VOID{} main() \{
   \VOID x = 42;
   print(f(x)); // \comment{(1)}
   \\
   A<\VOID{}> a = B<\VOID{}>(x);
-  A<Object> aObject = a;
+  A<Object?> aObject = a;
   print(aObject.x); // \comment{(2)}
   print(a.foo(x)); // \comment{(3)}
 \}
@@ -23116,25 +23111,25 @@ \subsubsection{Void Soundness}
   which is or contains a type variable whose value could be \VOID,
   so we are allowed to return \code{x} in the body of \code{f},
   even though this means that we indirectly get access to the value
-  of an expression of type \VOID, under the static type \code{Object}.
+  of an expression of type \VOID, under the static type \code{Object?}.
 
   At (2), we indirectly obtain access to the value of
   the variable \code{x} with type \VOID,
   because we use an assignment to get access to the instance of \code{B}
   which was created with type argument \VOID{} under the type
-  \code{A<Object>}.
-  Note that \code{A<Object>} and \code{A<\VOID{}>} are subtypes of each other,
+  \code{A<Object?>}.
+  Note that \code{A<Object?>} and \code{A<\VOID{}>} are subtypes of each other,
   that is, they are equivalent according to the subtype rules,
   so neither static nor dynamic type checks will fail.
 
   At (3), we indirectly obtain access to the value of
   the variable \code{x} with type \VOID{}
-  under the static type \code{Object},
+  under the static type \code{Object?},
   because the statically known method signature of \code{foo}
   has parameter type \VOID,
   but the actual implementation of \code{foo} which is invoked
-  is an override whose parameter type is \code{Object},
-  which is allowed because \code{Object} and \VOID{} are both top types.%
+  is an override whose parameter type is \code{Object?},
+  which is allowed because \code{Object?} and \VOID{} are both top types.%
 }
 
 \rationale{%
@@ -23155,7 +23150,7 @@ \subsubsection{Void Soundness}
   from one variable or parameter to the next one, all with type \VOID,
   explicitly, or as the value of a type parameter.
   In particular, we could require that method overrides should
-  never override return type \code{Object} by return type \VOID,
+  never override return type \code{Object?} by return type \VOID,
   or parameter types in the opposite direction;
   parameterized types with type argument \VOID{} could not be assigned
   to variables where the corresponding type argument is anything other than
@@ -23203,7 +23198,7 @@ \subsection{Parameterized Types}
 Let $T$ be a parameterized type \code{$G$<$S_1, \ldots,\ S_n$>}.
 
 \LMHash{}%
-It is a compile-time error if $G$ is not a generic type,
+It is a \Error{compile-time error} if $G$ is not a generic type,
 or $G$ is a generic type,
 but the number of formal type parameters in the declaration of $G$ is not $n$.
 Otherwise, let
@@ -23218,7 +23213,7 @@ \subsection{Parameterized Types}
 or $T$ is not well-bounded (\ref{superBoundedTypes}).
 
 \LMHash{}%
-It is a compile-time error if $T$ is malbounded.
+It is a \Error{compile-time error} if $T$ is malbounded.
 
 \LMHash{}%
 $T$ is evaluated as follows.
@@ -23242,7 +23237,8 @@ \subsection{Parameterized Types}
 %% replaced by the bottom type (`Null`, for now) in locations of the member
 %% type where it occurs contravariantly. For instance, `c.f` should have
 %% static type `void Function(Null)` when `c` has static type `C<T>` for any
-%% `T`, and we have `class C<X> { void Function(X) f; }`.
+%% `T`, and we have `class C<X> { void Function(X) f; }`. Cf. issue
+%% https://github.com/dart-lang/language/issues/297.
 
 
 \subsubsection{Actual Types}
@@ -23423,7 +23419,7 @@ \subsubsection{Reserved Words}
 \LMHash{}%
 A \Index{reserved word} can only be used in the syntactic positions
 specified by the grammar.
-In particular, a compile-time error occurs if a reserved word is used
+In particular, a \Error{compile-time error} occurs if a reserved word is used
 where an identifier is expected.
 
 \commentary{%

From e179aa8777d10f0d44487f1526cbfce9534594dd Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 13:58:58 +0200
Subject: [PATCH 08/82] WIP

---
 specification/dartLangSpec.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 27192d7ac4..f06b36f5ed 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23629,7 +23629,7 @@ \section*{Appendix: Algorithmic Subtyping}
 \item
   \textbf{Type Variable Reflexivity 1:}
   if $T_0$ is a type variable $X_0$
-  or a promoted type variables \code{$X_0$\,\&\,$S_0$} and $T_1$ is $X_0$
+  or a promoted type variable \code{$X_0$\,\&\,$S_0$} and $T_1$ is $X_0$
   then \SubtypeNE{T_0}{T_1}.
 
   \commentary{%
@@ -23671,12 +23671,12 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Left Promoted Variable:}
-  $T_0$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
-  and \SubtypeNE{S_0}{T_1}.
+  If $T_0$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_0}{T_1}.
 \item
   \textbf{Left Type Variable Bound:}
   $T_0$ is a type variable $X_0$ with bound $B_0$
-  and \SubtypeNE{B_0}{T_1}.
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B_0}{T_1}.
 \item
   \textbf{Function Type/Function:}
   $T_0$ is a function type and $T_1$ is \FUNCTION.

From 6635a69782c36fab2489ec4e376b3e6c9ed6594f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:04:46 +0200
Subject: [PATCH 09/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index f06b36f5ed..6d9e30bf63 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23675,7 +23675,7 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_0}{T_1}.
 \item
   \textbf{Left Type Variable Bound:}
-  $T_0$ is a type variable $X_0$ with bound $B_0$
+  If $T_0$ is a type variable $X_0$ with bound $B_0$
   then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B_0}{T_1}.
 \item
   \textbf{Function Type/Function:}

From 4ee98d5d395f2cf1eb9e359aaf4720062e9fa217 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:07:26 +0200
Subject: [PATCH 10/82] WIP

---
 specification/dart.sty         | 1 +
 specification/dartLangSpec.tex | 3 +++
 2 files changed, 4 insertions(+)

diff --git a/specification/dart.sty b/specification/dart.sty
index 086e2420f8..db1a0f8dbf 100644
--- a/specification/dart.sty
+++ b/specification/dart.sty
@@ -20,6 +20,7 @@
 \def\MIXIN{\builtinId{mixin}}
 \def\OPERATOR{\builtinId{operator}}
 \def\PART{\builtinId{part}}
+\def\RECORD{\builtinId{Record}}
 \def\REQUIRED{\builtinId{required}}
 \def\SET{\builtinId{set}}
 \def\STATIC{\builtinId{static}}
diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 6d9e30bf63..db56cbdc25 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23680,6 +23680,9 @@ \section*{Appendix: Algorithmic Subtyping}
 \item
   \textbf{Function Type/Function:}
   $T_0$ is a function type and $T_1$ is \FUNCTION.
+\item
+  \textbf{Record Type/Record:}
+  $T_0$ is a record type and $T_1$ is \RECORD.
 \item
   \textbf{Interface Compositionality:}
   $T_0$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}

From 08f20f43d3be1286364f061baf5c5804508ecd30 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:11:16 +0200
Subject: [PATCH 11/82] WIP

---
 specification/dartLangSpec.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index db56cbdc25..15b37e1ef7 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23685,8 +23685,9 @@ \section*{Appendix: Algorithmic Subtyping}
   $T_0$ is a record type and $T_1$ is \RECORD.
 \item
   \textbf{Interface Compositionality:}
-  $T_0$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
-  and $T_1$ is \code{$C_0$<$U_0$, \ldots, $U_k$>} and each \SubtypeNE{S_i}{U_i}.
+  If $T_0$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
+  and $T_1$ is \code{$C_0$<$U_0$, \ldots, $U_k$>}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
 \item
   \textbf{Super-Interface:}
   $T_0$ is an interface type with super-interfaces \List{S}{0}{n}

From 144a83e405d5763ec7bad7b9584028145bf14e4f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:14:07 +0200
Subject: [PATCH 12/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 15b37e1ef7..02f9639989 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23690,8 +23690,8 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
 \item
   \textbf{Super-Interface:}
-  $T_0$ is an interface type with super-interfaces \List{S}{0}{n}
-  and \SubtypeNE{S_i}{T_1} for some $i$.
+  If $T_0$ is an interface type with super-interfaces \List{S}{0}{n}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_i}{T_1} for some $i$.
 \item
   \textbf{Positional Function Types:}
   $T_0$ is

From 3f1f8ea0bdf44464252667f313b9658969085a9a Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:19:18 +0200
Subject: [PATCH 13/82] WIP

---
 specification/dartLangSpec.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 02f9639989..e96a5c076e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23694,7 +23694,7 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_i}{T_1} for some $i$.
 \item
   \textbf{Positional Function Types:}
-  $T_0$ is
+  If $T_0$ is
 
   \code{$U_0$ \FUNCTION<%
     $X_0$\,\EXTENDS\,$B_{00}$, \ldots, $X_k$\,\EXTENDS\,$B_{0k}$>(%
@@ -23708,7 +23708,7 @@ \section*{Appendix: Algorithmic Subtyping}
     $S_0$\,$y_0$, \ldots, $S_p$\,$y_p$, %
     [$S_{p+1}$\,$y_{p+1}$, \ldots, $S_q$\,$y_q$])}
 
-  such that each of the following criteria is satisfied,
+  then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
   where the $Z_i$ are fresh type variables with bounds
   $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$:
 
@@ -23723,7 +23723,7 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Named Function Types:}
-  $T_0$ is
+  If $T_0$ is
 
   \code{%
     $U_0$ \FUNCTION<$X_0$\,\EXTENDS\,$B_{00}$, \ldots, %
@@ -23741,7 +23741,7 @@ \section*{Appendix: Algorithmic Subtyping}
           \{$r_{1,n+1}$\,$S_{n+1}$\,$y_{n+1}$, \ldots, $r_{1q}$\,$S_q$\,$y_q$\})}
 
   where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
-  and the following criteria are all satisfied,
+  then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
   where \List{Z}{1}{k} are fresh type variables with bounds
   $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$:
 

From 0150fef4ff7d8afcea5b84707628890777432e32 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:23:13 +0200
Subject: [PATCH 14/82] WIP

---
 specification/dartLangSpec.tex | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index e96a5c076e..c02ec5d630 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23710,15 +23710,15 @@ \section*{Appendix: Algorithmic Subtyping}
 
   then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
   where the $Z_i$ are fresh type variables with bounds
-  $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$:
+  $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$:
 
   \begin{itemize}
   \item $p \geq n$.
   \item $m \geq q$.
-  \item \SubtypeNE{S_i[Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i[Z_0/X_0, \ldots, Z_k/X_k]}
+  \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{[Z_0/X_0, \ldots, Z_k/X_k]V_i}
     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]$
+  \item \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{[Z_0/Y_0, \ldots, Z_k/Y_k]U_1}.
+  \item $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i}$
     have the same canonical syntax, for $i \in 0 .. k$.
   \end{itemize}
 \item
@@ -23743,23 +23743,23 @@ \section*{Appendix: Algorithmic Subtyping}
   where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
   then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
   where \List{Z}{1}{k} are fresh type variables with bounds
-  $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$:
+  $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$:
 
   \begin{itemize}
   \item
     $\{ y_{n+1}, \ldots, y_q \} \subseteq \{ x_{n+1}, \ldots , x_m \}$.
   \item
-    \SubtypeNE{S_i[Z_0/Y_0, \ldots, Z_k/Y_k]}{V_i[Z_0/X_0, \ldots, Z_k/X_k]}
+    \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{[Z_0/X_0, \ldots, Z_k/X_k]V_i}
     for $i \in 0 .. n$.
-  \item \SubtypeNE{S_i[Z_0/Y_0, \ldots, Z_k/Y_k]}{V_j[Z_0/X_0, \ldots, Z_k/X_k]}
+  \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{[Z_0/X_0, \ldots, Z_k/X_k]V_j}
     for $i \in n+1 .. q$, and $y_j = x_i$.
   \item
     for each $j$ such that $r_{0j}$ is \REQUIRED, there exists an
     $i \in n+1 .. q$ such that $x_j = y_i$, and $r_{1i}$ is \REQUIRED.
   \item
-    \SubtypeNE{U_0[Z_0/X_0, \ldots, Z_k/X_k]}{U_1[Z_0/Y_0, \ldots, Z_k/Y_k]}.
+    \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{[Z_0/Y_0, \ldots, Z_k/Y_k]U_1}.
   \item
-    $B_{0i}[Z_0/X_0, \ldots, Z_k/X_k]$ and $B_{1i}[Z_0/Y_0, \ldots, Z_k/Y_k]$
+    $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i}$
     have the same canonical syntax,
     for each $i \in 0 .. k$.
   \end{itemize}

From 0f9e019f8257d48a4faeea9224fc2e43c9d490f5 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 14:36:46 +0200
Subject: [PATCH 15/82] WIP

---
 specification/dartLangSpec.tex | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index c02ec5d630..ebf0cdf72b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23770,6 +23770,11 @@ \section*{Appendix: Algorithmic Subtyping}
     It is valid to choose $Z_i$ to be $X_i$ or $Y_i$,
     so long as capture is avoided.%
   }
+
+\item
+  If $T_0$ is \code{($V_0$, \ldots, $V_n$, \{$V_{n+1} d_{n+1}$, \ldots, $V_m d_m$\})}
+  and $T_1$ is \code{($S_0$, \ldots, $S_n$, \{$S_{n+1} d_{n+1}$, \ldots, $S_m d_m$\})}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.  
 \end{itemize}
 
 

From e93ac8f294bf4411650f4774143b15e80c754d84 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 16:34:49 +0200
Subject: [PATCH 16/82] WIP

---
 specification/dartLangSpec.tex | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index ebf0cdf72b..e627aa5cd3 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -21840,7 +21840,7 @@ \subsection{Subtypes}
 may arise during static analysis due to type promotion
 (\ref{typePromotion}).
 They never occur during execution,
-and there are many other restrictions on where they can occur
+and there are several other restrictions on where they can occur
 (\ref{intersectionTypes}).
 However, their subtype relations are specified without restrictions.
 \commentary{%
@@ -23542,9 +23542,6 @@ \section*{Appendix: Algorithmic Subtyping}
 with good performance.
 
 \LMHash{}%
-In this algorithm, types are considered to be the same when they have
-the same canonical syntax
-(\ref{theCanonicalSyntaxOfTypes}).
 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
@@ -23718,8 +23715,11 @@ \section*{Appendix: Algorithmic Subtyping}
   \item \SubtypeNE{[Z_0/Y_0, \ldots, Z_k/Y_k]S_i}{[Z_0/X_0, \ldots, Z_k/X_k]V_i}
     for $i \in 0 .. q$.
   \item \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{[Z_0/Y_0, \ldots, Z_k/Y_k]U_1}.
-  \item $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i}$
-    have the same canonical syntax, for $i \in 0 .. k$.
+  \item
+    \MutualSubtypeNE{%
+      [Z_0/X_0, \ldots, Z_k/X_k]B_{0i}}{%
+      [Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i}},
+    for $i \in 0 .. k$.
   \end{itemize}
 \item
   \textbf{Named Function Types:}
@@ -23759,8 +23759,9 @@ \section*{Appendix: Algorithmic Subtyping}
   \item
     \SubtypeNE{[Z_0/X_0, \ldots, Z_k/X_k]U_0}{[Z_0/Y_0, \ldots, Z_k/Y_k]U_1}.
   \item
-    $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$ and $[Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i}$
-    have the same canonical syntax,
+    \MutualSubtypeNE{%
+      [Z_0/X_0, \ldots, Z_k/X_k]B_{0i}}{%
+      [Z_0/Y_0, \ldots, Z_k/Y_k]B_{1i}},
     for each $i \in 0 .. k$.
   \end{itemize}
 

From afbb0ab1d2fdd753f516cdb6bd896026c9875a23 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 16:38:45 +0200
Subject: [PATCH 17/82] WIP

---
 specification/dartLangSpec.tex | 1 -
 1 file changed, 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index e627aa5cd3..b729d3cf5b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -22052,7 +22052,6 @@ \subsubsection{Meta-Variables}
 \begin{itemize}
 \item $X$ ranges over type variables.
 \item $C$ ranges over classes,
-\item $F$ ranges over type aliases.
 \item $T$ and $S$ range over types.
 \item $B$ ranges over types; it is only used as a type variable bound.
 \item $r$ and $r'$ range over \REQUIRED{} or empty;

From ea679d1e44d5650959d90e37fab58f5160a069e2 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 16:51:34 +0200
Subject: [PATCH 18/82] WIP

---
 specification/dartLangSpec.tex | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index b729d3cf5b..ad08191e0f 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -22196,13 +22196,6 @@ \subsubsection{Subtype Rules}
 When that is not the case for a given premise,
 we specify the meaning explicitly.
 
-\commentary{%
-  Instantiation of a rule, mentioned above,
-  denotes the consistent replacement of meta-variables
-  by actual syntactic terms denoting types everywhere in the rule,
-  that is, in the premises as well as in the conclusion, simultaneously.%
-}
-
 
 \subsubsection{Being a Subtype}
 \LMLabel{beingASubtype}

From 2fa96300d601c65dfd3bf27b354ed75c63975df2 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 18 Oct 2024 17:12:41 +0200
Subject: [PATCH 19/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index ad08191e0f..6ecfb0bf0b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -22511,7 +22511,7 @@ \subsection{Function Types}
 a function type $F$ which is a subtype of the class \FUNCTION{}
 (\ref{functionType}).
 The function object has a method named \CALL,
-whose signature is said function type $F$.
+whose signature has $F$ as its function type.
 \commentary{%
   Consequently, all function types are subtypes of \FUNCTION{}
   (\ref{subtypes}).%

From 7ca13def08dc6ec756c2c01180bed7e0354f60b0 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 1 Nov 2024 18:28:23 +0100
Subject: [PATCH 20/82] Added section about explicitly resolved (fka canonical)
 syntax

---
 specification/dartLangSpec.tex | 240 +++++++++++++++++++++++++++++----
 1 file changed, 215 insertions(+), 25 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 6ecfb0bf0b..89d6a72adb 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -2686,7 +2686,7 @@ \subsection{Type of a Function}
   different type parameters, F-bounds, and the types of formal parameters.
   However, we do not wish to distinguish between two function types
   if they have the same structure and only differ in the choice of names.
-  This treatment of names is also known as alpha-equivalence.%
+  This treatment of names is also known as alpha equivalence.%
 }
 
 \LMHash{}%
@@ -22088,24 +22088,18 @@ \subsubsection{Subtype Rules}
   However, we must eliminate the difficulties associated with
   different syntax denoting the same type,
   and different types denoted by the same syntax.
-  We do this by assuming that every type in the program has been expressed
-  in a manner where those situations never occur,
-  because each type is denoted by the same globally unique syntax everywhere.%
+  We do this by defining in detail what it means to be the same type
+  (\ref{sameStaticType}).%
 }
 
 \LMHash{}%
 In section~\ref{subtypes} and its subsections,
 all designations of types are considered to be the same
-if{}f they have the same canonical syntax
-(\ref{theCanonicalSyntaxOfTypes}).
+type if{}f they satisfy the criteria in
+Section~\ref{sameStaticType}.
 
-\commentary{%
-  Note that the canonical syntax also implies
-  transitive expansion of all type aliases
-  (\ref{typedef}).
-  In other words, subtyping rules do not need to consider type aliases,
-  because all type aliases have been expanded.%
-}
+\LMHash{}%
+The subtype rules assume that all type aliases have been transitively expanded.
 
 \LMHash{}%
 Every \synt{typeName} used in a type mentioned
@@ -22491,19 +22485,13 @@ \subsection{Function Types}
   coincide in this case.%
 }
 
-\LMHash{}%
-Two function types are considered equal if consistent renaming of type
-parameters can make them identical.
-
 \commentary{%
-  A common way to say this is that we do not distinguish
-  function types which are alpha-equivalent.
-  For the subtyping rule below this means we can assume that
-  a suitable renaming has already taken place.
-  In cases where this is not possible
-  because the number of type parameters in the two types differ
-  or the bounds are different,
-  no subtype relationship exists.%
+  Two function types are the same type
+  if, roughly, consistent renaming of type
+  parameters can make them identical.
+  This is also known as alpha equivalence.
+  The detailed rules are described in
+  Section~\ref{sameStaticType}.%
 }
 
 \LMHash{}%
@@ -23390,6 +23378,208 @@ \subsubsection{Least Upper Bounds}
 }
 
 
+\subsection{Same Static Type}
+\LMLabel{sameStaticType}
+
+\LMHash{}%
+This section specifies how to soundly determine whether or not two types
+that are encountered during static analysis are the same type.
+
+\LMHash{}%
+Concrete syntax denoting types gives rise to several difficulties
+when used to determine static semantic properties,
+like subtyping relationships
+(\ref{subtypes})
+or upper and lower bounds
+(\ref{standardUpperBoundsAndStandardLowerBounds}).
+
+\commentary{%
+Note that the notion of being the same type at run time is different from
+the notion of being the same type during static analysis.
+For example, two distinct type variables \code{X} and \code{Y}
+might at run time be bound to the same type, e.g.,
+\code{List<int>}.
+However, during static analysis we must maintain that
+\code{X} and \code{Y} are different types
+because there is no guarantee that they are always bound to
+the same type at run time.%
+}
+
+\commentary{%
+The phrases `same type' and `identical syntax' deserves some extra scrutiny.
+If a library $L$ imports the libraries $L_1$ and $L_2$
+(where $L_1$ and $L_2$ are not the same library),
+and both $L_1$ and $L_2$ declare a class \code{C},
+then the syntax \code{C} may occur as a type during static analysis of $L$
+in situations where it refers to two distinct types.
+
+For instance, $L_1$ could declare a variable \code{v}
+of type \code{C}-in-$L_1$,
+and $L_2$ could declare a function
+\code{\VOID\,foo(C\,\,c)\,\,\{\}}
+which uses the type \code{C}-in-$L_2$,
+and $L$ could contain the expression \code{foo(v)}.
+
+Note that even though it would be a compile-time error to use \code{C} in $L$
+(because it is ambiguous),
+it is not an error to have an expression like \code{foo(v)},
+and the static analysis of this expression \emph{must}
+be able to determine that the two types whose name is \code{C} are
+not the same type. The invocation may or may not be an error,
+depending on the subtyping relations.%
+}
+
+\rationale{%
+This shows that concrete syntax behaves in such a manner that it is
+unsafe to consider two types to be the same type,
+based on the fact that they are denoted by the same syntax,
+even during the static analysis of a single expression.
+
+Similarly, it is incorrect to consider two terms derived from \synt{type}
+as different types based on the fact that they are syntactically different.
+For example, they could be the same type imported with different import
+prefixes.
+
+We could say that two identifiers
+(possibly qualified, e.g., \code{myPrefix.C} and \code{C})
+denote the same type
+if they have been resolved to the same declaration.
+
+However, we introduce \emph{the explicitly resolved syntax for a type},
+which is basically an explicit representation of this idea,
+in order to make the underlying issues more explicit.
+The explicitly resolved syntax has the property that
+each type has a unique syntactic form
+(except for alpha equivalence, which is defined below).
+We may then consider this unique syntactic form as a static semantic value,
+rather than just a syntactic form which is dependent on
+its location in the program.%
+}
+
+\LMHash{}%
+The
+\IndexCustom{explicitly resolved syntax}{type!explicitly resolved syntax of}
+of the types in a given library $L_1$
+and all libraries \List{L}{2}{n} reachable from $L_1$ via
+one or more import links
+is determined as follows.
+First, choose a set of distinct, globally fresh identifiers
+\List{\metavar{prefix}}{1}{n}.
+Then transform each library $L_i$, $i \in 1 .. n$ as follows:
+
+\begin{enumerate}
+\item
+  For each type variable declared in $L_i$, consistently rename
+  it to a globally fresh name.
+\item
+  If $D_T$ is a declaration of a class, mixin, or type alias in $L_i$
+  whose name $n$ is private,
+  and an occurrence of $n$ that resolves to $D$
+  exists in a type alias declaration $D_A$ whose name is non-private,
+  then perform a consistent renaming of
+  all occurrences of $n$ in $L_i$ that resolve to $D_T$
+  to a fresh, non-private identifier.
+  \commentary{%
+    We make $D_T$ public, because it is being leaked anyway.%
+  }
+\item
+  Add a set of import directives to $L_i$ that imports
+  each of the libraries \List{L}{1}{n} with
+  the corresponding prefix $\metavar{prefix}_j$, $j \in 1 .. n$.
+
+  \commentary{%
+    This means that every library in the set
+    $\{\,\List{L}{1}{n}\,\}$
+    imports every other library in that set,
+    even itself and system libraries like \code{dart:core}.%
+  }
+\item
+  Let \id{} be an occurrence of
+  a non-private type identifier derived from \synt{typeName}
+  that resolves to a library declaration in the library $L_j$
+  in the original program;
+  \id{} is then transformed to \code{$\metavar{prefix}_j$.\id}.
+  Let \code{$p$.\id} be derived from \synt{typeName} such that $p$ is
+  an import prefix in the original program
+  and \id{} is a non-private identifier,
+  and consider the case where \code{$p$.\id} resolves to
+  a library declaration in the library $L_j$ in the original program,
+  for some $j$;
+  \code{$p$.\id} is then transformed to \code{$\metavar{prefix}_j$.\id}.
+\item
+  Replace every type in $L_i$ that denotes a type alias
+  along with its actual type arguments, if any,
+  by its transitive alias expansion
+  (\ref{typedef}).
+  \commentary{%
+    Note that the bodies of type alias declarations
+    already use the new prefixes,
+    so the results of the alias expansion will also use
+    the new prefixes consistently.%
+  }
+\end{enumerate}
+
+\commentary{%
+In short, this transformation adds a unique prefix to every type name
+which is resolved to a top-level declaration
+(in the same library or in an imported library).
+  
+This transformation does not change any occurrence of \VOID,
+and does not need to;
+\VOID{} is a reserved word, not a type identifier.
+Also, \code{$\metavar{prefix}_j$.\VOID} would be a syntax error.
+
+Note that the transformation changes terms derived from \synt{type},
+but it does not change expressions, or any other program element
+(except that a \synt{type} can occur in an expression, e.g., \code{<int>[]}).
+In particular, it does not change type literals
+(that is, expressions denoting types).%
+}
+
+\LMHash{}%
+Every \synt{type} in the resulting set of libraries
+is now expressed in a globally unique syntactic form,
+which is the form that we call the
+\IndexCustom{explicitly resolved syntax of}{type!explicitly resolved syntax of}
+said types.
+
+\LMHash{}%
+When we say that two types $T_1$ and $T_2$ have the
+\IndexCustom{same explicitly resolved syntax}{type!same explicitly resolved syntax},
+it refers to the situation where the current library
+and all libraries which are reachable via one or more imports
+have been transformed as described above,
+and the resulting explicitly resolved syntaxes are textually identical.
+
+\LMHash{}%
+We need to introduce one more concept:
+An \Index{alpha conversion} of a type is a consistent renaming
+of the type variables declared in that type.
+
+\commentary{%
+In Dart, only function types can be subject to an alpha conversion:
+A function type is the only kind of type that declares type variables.
+For example,
+\code{List<X>\,\,\FUNCTION<X>({X\,\,arg})}
+can be turned into 
+\code{List<Y>\,\,\FUNCTION<Y>({Y\,\,arg})}
+by alpha conversion.%
+}
+
+\LMHash{}%
+Two function types are \Index{alpha equivalent} if{}f
+there exists an alpha conversion that makes them textually identical.
+
+\LMHash{}%
+Finally, we define that two type denotations $T_1$ and $T_2$ are the
+\IndexCustom{same static type}{type!same static}
+if there exist alpha conversions
+that can be applied to the function types
+that occur as subterms of $T_1$ and $T_2$, if any,
+such that the resulting terms $T'_1$ and $T'_2$ have
+the same explicitly resolved syntax.
+
+
 \section{Reference}
 \LMLabel{reference}
 

From b2881a01487a72c8bf542db43acfd5c195b2603e Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Mon, 7 Jul 2025 17:40:16 +0200
Subject: [PATCH 21/82] Clean up whitespace

---
 specification/dartLangSpec.tex | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 89d6a72adb..64ed729fea 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23523,7 +23523,7 @@ \subsection{Same Static Type}
 In short, this transformation adds a unique prefix to every type name
 which is resolved to a top-level declaration
 (in the same library or in an imported library).
-  
+
 This transformation does not change any occurrence of \VOID,
 and does not need to;
 \VOID{} is a reserved word, not a type identifier.
@@ -23545,7 +23545,8 @@ \subsection{Same Static Type}
 
 \LMHash{}%
 When we say that two types $T_1$ and $T_2$ have the
-\IndexCustom{same explicitly resolved syntax}{type!same explicitly resolved syntax},
+\IndexCustom{same explicitly resolved syntax}{%
+  type!same explicitly resolved syntax},
 it refers to the situation where the current library
 and all libraries which are reachable via one or more imports
 have been transformed as described above,
@@ -23561,7 +23562,7 @@ \subsection{Same Static Type}
 A function type is the only kind of type that declares type variables.
 For example,
 \code{List<X>\,\,\FUNCTION<X>({X\,\,arg})}
-can be turned into 
+can be turned into
 \code{List<Y>\,\,\FUNCTION<Y>({Y\,\,arg})}
 by alpha conversion.%
 }
@@ -23957,7 +23958,7 @@ \section*{Appendix: Algorithmic Subtyping}
 \item
   If $T_0$ is \code{($V_0$, \ldots, $V_n$, \{$V_{n+1} d_{n+1}$, \ldots, $V_m d_m$\})}
   and $T_1$ is \code{($S_0$, \ldots, $S_n$, \{$S_{n+1} d_{n+1}$, \ldots, $S_m d_m$\})}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.  
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.
 \end{itemize}
 
 

From 295064055c1ef0b1bc8cf9dff0d950d0aca41be8 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 14:24:00 +0200
Subject: [PATCH 22/82] Whitespace

---
 specification/dartLangSpec.tex | 102 ++++++++++++++++-----------------
 1 file changed, 51 insertions(+), 51 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 64ed729fea..8cebdc859b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -17502,10 +17502,10 @@ \subsection{Identifier Reference}
 as the name of a type declaration.
 
 \commentary{%
-A \synt{qualifiedName} is not an identifier expression,
-but we specify its syntax here because it is used in several different contexts,
-and it is more closely related to the plain identifier
-than it is to any single one of those grammar rules where it is used.%
+  A \synt{qualifiedName} is not an identifier expression,
+  but we specify its syntax here because it is used in several different contexts,
+  and it is more closely related to the plain identifier
+  than it is to any single one of those grammar rules where it is used.%
 }
 
 \begin{grammar}
@@ -23394,39 +23394,39 @@ \subsection{Same Static Type}
 (\ref{standardUpperBoundsAndStandardLowerBounds}).
 
 \commentary{%
-Note that the notion of being the same type at run time is different from
-the notion of being the same type during static analysis.
-For example, two distinct type variables \code{X} and \code{Y}
-might at run time be bound to the same type, e.g.,
-\code{List<int>}.
-However, during static analysis we must maintain that
-\code{X} and \code{Y} are different types
-because there is no guarantee that they are always bound to
-the same type at run time.%
+  Note that the notion of being the same type at run time is different from
+  the notion of being the same type during static analysis.
+  For example, two distinct type variables \code{X} and \code{Y}
+  might at run time be bound to the same type, e.g.,
+  \code{List<int>}.
+  However, during static analysis we must maintain that
+  \code{X} and \code{Y} are different types
+  because there is no guarantee that they are always bound to
+  the same type at run time.%
 }
 
 \commentary{%
-The phrases `same type' and `identical syntax' deserves some extra scrutiny.
-If a library $L$ imports the libraries $L_1$ and $L_2$
-(where $L_1$ and $L_2$ are not the same library),
-and both $L_1$ and $L_2$ declare a class \code{C},
-then the syntax \code{C} may occur as a type during static analysis of $L$
-in situations where it refers to two distinct types.
+  The phrases `same type' and `identical syntax' deserves some extra scrutiny.
+  If a library $L$ imports the libraries $L_1$ and $L_2$
+  (where $L_1$ and $L_2$ are not the same library),
+  and both $L_1$ and $L_2$ declare a class \code{C},
+  then the syntax \code{C} may occur as a type during static analysis of $L$
+  in situations where it refers to two distinct types.
 
-For instance, $L_1$ could declare a variable \code{v}
-of type \code{C}-in-$L_1$,
-and $L_2$ could declare a function
-\code{\VOID\,foo(C\,\,c)\,\,\{\}}
-which uses the type \code{C}-in-$L_2$,
-and $L$ could contain the expression \code{foo(v)}.
+  For instance, $L_1$ could declare a variable \code{v}
+  of type \code{C}-in-$L_1$,
+  and $L_2$ could declare a function
+  \code{\VOID\,foo(C\,\,c)\,\,\{\}}
+  which uses the type \code{C}-in-$L_2$,
+  and $L$ could contain the expression \code{foo(v)}.
 
-Note that even though it would be a compile-time error to use \code{C} in $L$
-(because it is ambiguous),
-it is not an error to have an expression like \code{foo(v)},
-and the static analysis of this expression \emph{must}
-be able to determine that the two types whose name is \code{C} are
-not the same type. The invocation may or may not be an error,
-depending on the subtyping relations.%
+  Note that even though it would be a compile-time error to use \code{C} in $L$
+  (because it is ambiguous),
+  it is not an error to have an expression like \code{foo(v)},
+  and the static analysis of this expression \emph{must}
+  be able to determine that the two types whose name is \code{C} are
+  not the same type. The invocation may or may not be an error,
+  depending on the subtyping relations.%
 }
 
 \rationale{%
@@ -23520,20 +23520,20 @@ \subsection{Same Static Type}
 \end{enumerate}
 
 \commentary{%
-In short, this transformation adds a unique prefix to every type name
-which is resolved to a top-level declaration
-(in the same library or in an imported library).
+  In short, this transformation adds a unique prefix to every type name
+  which is resolved to a top-level declaration
+  (in the same library or in an imported library).
 
-This transformation does not change any occurrence of \VOID,
-and does not need to;
-\VOID{} is a reserved word, not a type identifier.
-Also, \code{$\metavar{prefix}_j$.\VOID} would be a syntax error.
+  This transformation does not change any occurrence of \VOID,
+  and does not need to;
+  \VOID{} is a reserved word, not a type identifier.
+  Also, \code{$\metavar{prefix}_j$.\VOID} would be a syntax error.
 
-Note that the transformation changes terms derived from \synt{type},
-but it does not change expressions, or any other program element
-(except that a \synt{type} can occur in an expression, e.g., \code{<int>[]}).
-In particular, it does not change type literals
-(that is, expressions denoting types).%
+  Note that the transformation changes terms derived from \synt{type},
+  but it does not change expressions, or any other program element
+  (except that a \synt{type} can occur in an expression, e.g., \code{<int>[]}).
+  In particular, it does not change type literals
+  (that is, expressions denoting types).%
 }
 
 \LMHash{}%
@@ -23558,13 +23558,13 @@ \subsection{Same Static Type}
 of the type variables declared in that type.
 
 \commentary{%
-In Dart, only function types can be subject to an alpha conversion:
-A function type is the only kind of type that declares type variables.
-For example,
-\code{List<X>\,\,\FUNCTION<X>({X\,\,arg})}
-can be turned into
-\code{List<Y>\,\,\FUNCTION<Y>({Y\,\,arg})}
-by alpha conversion.%
+  In Dart, only function types can be subject to an alpha conversion:
+  A function type is the only kind of type that declares type variables.
+  For example,
+  \code{List<X>\,\,\FUNCTION<X>({X\,\,arg})}
+  can be turned into
+  \code{List<Y>\,\,\FUNCTION<Y>({Y\,\,arg})}
+  by alpha conversion.%
 }
 
 \LMHash{}%

From c6c964c1ee9e2b553283c3a24b6e9d1337f4274d Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 14:55:38 +0200
Subject: [PATCH 23/82] Whitespace

---
 specification/dartLangSpec.tex | 109 +++++++++++++++++----------------
 1 file changed, 55 insertions(+), 54 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 8cebdc859b..163ada527b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -2108,29 +2108,29 @@ \section{Functions}
 the body of a setter or constructor.
 
 \rationale{%
-An asynchronous setter would be of little use,
-since setters can only be used in the context of an assignment
-(\ref{assignment}),
-and an assignment expression always evaluates to
-the value of the assignment's right hand side.
-If the setter actually did its work asynchronously,
-one might imagine that one would return a future that resolved to
-the assignment's right hand side after the setter did its work.
-
-An asynchronous constructor would, by definition, never return
-an instance of the class it purports to construct,
-but instead return a future.
-Calling such a beast via \NEW{} would be very confusing.
-If you need to produce an object asynchronously, use a method.
-
-One could allow modifiers for factories.
-A factory for \code{Future} could be modified by \ASYNC,
-a factory for \code{Stream} could be modified by \code{\ASYNC*},
-and a factory for \code{Iterable} could be modified by \code{\SYNC*}.
-No other scenario makes sense because
-the object returned by the factory would be of the wrong type.
-This situation is very unusual so it is not worth making an exception
-to the general rule for constructors in order to allow it.%
+  An asynchronous setter would be of little use,
+  since setters can only be used in the context of an assignment
+  (\ref{assignment}),
+  and an assignment expression always evaluates to
+  the value of the assignment's right hand side.
+  If the setter actually did its work asynchronously,
+  one might imagine that one would return a future that resolved to
+  the assignment's right hand side after the setter did its work.
+
+  An asynchronous constructor would, by definition, never return
+  an instance of the class it purports to construct,
+  but instead return a future.
+  Calling such a beast via \NEW{} would be very confusing.
+  If you need to produce an object asynchronously, use a method.
+
+  One could allow modifiers for factories.
+  A factory for \code{Future} could be modified by \ASYNC,
+  a factory for \code{Stream} could be modified by \code{\ASYNC*},
+  and a factory for \code{Iterable} could be modified by \code{\SYNC*}.
+  No other scenario makes sense because
+  the object returned by the factory would be of the wrong type.
+  This situation is very unusual so it is not worth making an exception
+  to the general rule for constructors in order to allow it.%
 }
 
 \LMHash{}%
@@ -22520,7 +22520,7 @@ \subsection{Type Function}
 
 \LMHash{}%
 If a class or mixin declaration implements \FUNCTION, it has no effect.
-It is as if the \FUNCTION{} was removed from the \code{implements} clause
+It is as if the \FUNCTION{} was removed from the \IMPLEMENTS{} clause
 (and if it's the only implemented interface, the entire clause is removed).
 The resulting class or mixin interface
 does not have \FUNCTION{} as a superinterface.
@@ -22528,13 +22528,13 @@ \subsection{Type Function}
 \LMHash{}%
 If a mixin application mixes \FUNCTION{} onto a superclass, it follows the
 normal rules for mixin-application, but since the result of that mixin
-application is equivalent to a class with \code{implements \FUNCTION}, and
+application is equivalent to a class with \code{\IMPLEMENTS\,\,\FUNCTION}, and
 that clause has no effect, the resulting class also does not
 implement \FUNCTION.
 \commentary{%
   The \FUNCTION{} class declares no concrete instance members,
-  so the mixin application creates a sub-class
-  of the superclass with no new members and no new interfaces.%
+  so the mixin application creates a sub-class of
+  the superclass with no new members and no new interfaces.%
 }
 
 \rationale{%
@@ -22763,10 +22763,11 @@ \subsection{Type FutureOr}
   That is, \code{FutureOr} is in a sense
   the union of $T$ and the corresponding future type.
   The last point guarantees that
-  \code{FutureOr<$T$>} <: \code{Object?},
+  \SubtypeNE{\code{FutureOr<$T$>}}{\code{Object?}},
   and also that \code{FutureOr} is covariant in its type parameter,
   just like class types:
-  if $S$ <: $T$ then \code{FutureOr<$S$>} <: \code{FutureOr<$T$>}.%
+  if \SubtypeNE{S}{T} then
+  \SubtypeNE{\code{FutureOr<$S$>}}{\code{FutureOr<$T$>}}.%
 }
 
 \LMHash{}%
@@ -22817,7 +22818,7 @@ \subsection{Type FutureOr}
 \end{itemize}
 
 
-\subsection{Type void}
+\subsection{Type Void}
 \LMLabel{typeVoid}
 
 \LMHash{}%
@@ -23430,30 +23431,30 @@ \subsection{Same Static Type}
 }
 
 \rationale{%
-This shows that concrete syntax behaves in such a manner that it is
-unsafe to consider two types to be the same type,
-based on the fact that they are denoted by the same syntax,
-even during the static analysis of a single expression.
-
-Similarly, it is incorrect to consider two terms derived from \synt{type}
-as different types based on the fact that they are syntactically different.
-For example, they could be the same type imported with different import
-prefixes.
-
-We could say that two identifiers
-(possibly qualified, e.g., \code{myPrefix.C} and \code{C})
-denote the same type
-if they have been resolved to the same declaration.
-
-However, we introduce \emph{the explicitly resolved syntax for a type},
-which is basically an explicit representation of this idea,
-in order to make the underlying issues more explicit.
-The explicitly resolved syntax has the property that
-each type has a unique syntactic form
-(except for alpha equivalence, which is defined below).
-We may then consider this unique syntactic form as a static semantic value,
-rather than just a syntactic form which is dependent on
-its location in the program.%
+  This shows that concrete syntax behaves in such a manner that it is
+  unsafe to consider two types to be the same type,
+  based on the fact that they are denoted by the same syntax,
+  even during the static analysis of a single expression.
+
+  Similarly, it is incorrect to consider two terms derived from \synt{type}
+  as different types based on the fact that they are syntactically different.
+  For example, they could be the same type imported with different import
+  prefixes.
+
+  We could say that two identifiers
+  (possibly qualified, e.g., \code{myPrefix.C} and \code{C})
+  denote the same type
+  if they have been resolved to the same declaration.
+
+  However, we introduce \emph{the explicitly resolved syntax for a type},
+  which is basically an explicit representation of this idea,
+  in order to make the underlying issues more explicit.
+  The explicitly resolved syntax has the property that
+  each type has a unique syntactic form
+  (except for alpha equivalence, which is defined below).
+  We may then consider this unique syntactic form as a static semantic value,
+  rather than just a syntactic form which is dependent on
+  its location in the program.%
 }
 
 \LMHash{}%

From 8d89ebbc2fdbaf238c975cb60b69a950a24e0e81 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:06:42 +0200
Subject: [PATCH 24/82] WIP

---
 specification/dartLangSpec.tex | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 163ada527b..396529f6d0 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -22089,14 +22089,14 @@ \subsubsection{Subtype Rules}
   different syntax denoting the same type,
   and different types denoted by the same syntax.
   We do this by defining in detail what it means to be the same type
-  (\ref{sameStaticType}).%
+  (\ref{sameType}).%
 }
 
 \LMHash{}%
 In section~\ref{subtypes} and its subsections,
 all designations of types are considered to be the same
 type if{}f they satisfy the criteria in
-Section~\ref{sameStaticType}.
+Section~\ref{sameType}.
 
 \LMHash{}%
 The subtype rules assume that all type aliases have been transitively expanded.
@@ -22491,7 +22491,7 @@ \subsection{Function Types}
   parameters can make them identical.
   This is also known as alpha equivalence.
   The detailed rules are described in
-  Section~\ref{sameStaticType}.%
+  Section~\ref{sameType}.%
 }
 
 \LMHash{}%
@@ -23379,8 +23379,8 @@ \subsubsection{Least Upper Bounds}
 }
 
 
-\subsection{Same Static Type}
-\LMLabel{sameStaticType}
+\subsection{Same Type}
+\LMLabel{sameType}
 
 \LMHash{}%
 This section specifies how to soundly determine whether or not two types
@@ -23741,16 +23741,17 @@ \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 type (\ref{sameType})
+  then \SubtypeNE{T_0}{T_1}.
 
   \commentary{%
-    Note that this check is necessary as the base case for primitive types,
-    and type variables, but not for composite types.
+    Note that this check is necessary as the base case for atomic types
+    and for 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
+    Pragmatically, non-constant time equality checks here are
     counter-productive.
-    So this rule should only be used when $T$ is atomic.%
+    Hence, this rule is only used when $T$ is atomic.%
   }
 \item
   \textbf{Right Top:}

From 0d5885fc837f4ad1ab9ac4bcf375882c57e5dbcb Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:15:11 +0200
Subject: [PATCH 25/82] Rename type variables

---
 specification/dartLangSpec.tex | 124 ++++++++++++++++-----------------
 1 file changed, 62 insertions(+), 62 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 396529f6d0..ac130f5ef8 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23755,142 +23755,142 @@ \section*{Appendix: Algorithmic Subtyping}
   }
 \item
   \textbf{Right Top:}
-  if $T_1$ is \DYNAMIC, \VOID, or \code{Object?} then \SubtypeNE{T_0}{T_1}.
+  if $T$ is \DYNAMIC, \VOID, or \code{Object?} then \SubtypeNE{S}{T}.
 \item
   \textbf{Left Top:}
-  if $T_0$ is \DYNAMIC{} or \VOID{}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{\code{Object?}}{T_1}.
+  if $S$ is \DYNAMIC{} or \VOID{}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{\code{Object?}}{T}.
 \item
   \textbf{Left Bottom:}
-  if $T_0$ is \code{Never} then \SubtypeNE{T_0}{T_1}.
+  if $S$ is \code{Never} then \SubtypeNE{S}{T}.
 \item
   \textbf{Right Object:}
-  if $T_1$ is \code{Object} then:
+  if $T$ is \code{Object} then:
   \begin{itemize}
   \item
-    if $T_0$ is an unpromoted type variable with bound $B$
-    then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B}{\code{Object}}.
+    if $S$ is an unpromoted type variable with bound $B$
+    then \SubtypeNE{S}{T} if{}f \SubtypeNE{B}{\code{Object}}.
   \item
-    if $T_0$ is a promoted type variable \code{$X$\,\&\,$S$}
-    then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S}{\code{Object}}.
+    if $S$ is a promoted type variable \code{$X$\,\&\,$S$}
+    then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{\code{Object}}.
   \item
-    if $T_0$ is \code{FutureOr<$S$>} for some $S$,
-    then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S}{\code{Object}}.
+    if $S$ is \code{FutureOr<$S$>} for some $S$,
+    then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{\code{Object}}.
   \item
-    if $T_0$ is \code{Null}, \DYNAMIC, \VOID, or \code{$S$?} for any $S$,
+    if $S$ is \code{Null}, \DYNAMIC, \VOID, or \code{$S$?} for any $S$,
     then the subtyping does not hold
     (\commentary{%
       i.e., the result of the subtyping query is known to be false%
     }).
   \item
-    Otherwise \SubtypeNE{T_0}{T_1} is true.
+    Otherwise \SubtypeNE{S}{T} is true.
   \end{itemize}
 \item
   \textbf{Left Null:}
-  if $T_0$ is \code{Null} then:
+  if $S$ is \code{Null} then:
   \begin{itemize}
   \item
-    if $T_1$ is a type variable (promoted or not) the query is false.
+    if $T$ is a type variable (promoted or not) the query is false.
   \item
-    if $T_1$ is \code{FutureOr<$S$>} for some $S$,
+    if $T$ is \code{FutureOr<$S$>} for some $S$,
     then the query is true if{}f \SubtypeNE{\code{Null}}{S}.
   \item
-    if $T_1$ is \code{$S$?} for some $S$ then the query is true.
+    if $T$ is \code{$S$?} for some $S$ then the query is true.
   \item
     Otherwise, the query is false.
   \end{itemize}
 \item
   \textbf{Left FutureOr:}
-  if $T_0$ is \code{FutureOr<$S_0$>}
-  then \SubtypeNE{T_0}{T_1} if{}f
-  \SubtypeNE{\code{Future<$S_0$>}}{T_1} and \SubtypeNE{S_0}{T_1}.
+  if $S$ is \code{FutureOr<$S_0$>}
+  then \SubtypeNE{S}{T} if{}f
+  \SubtypeNE{\code{Future<$S_0$>}}{T} and \SubtypeNE{S_0}{T}.
 \item
   \textbf{Left Nullable:}
-  if $T_0$ is \code{$S_0$?} then \SubtypeNE{T_0}{T_1} if{}f
-  \SubtypeNE{S_0}{T_1} and \SubtypeNE{\code{Null}}{T_1}.
+  if $S$ is \code{$S_0$?} then \SubtypeNE{S}{T} if{}f
+  \SubtypeNE{S_0}{T} and \SubtypeNE{\code{Null}}{T}.
 \item
   \textbf{Type Variable Reflexivity 1:}
-  if $T_0$ is a type variable $X_0$
-  or a promoted type variable \code{$X_0$\,\&\,$S_0$} and $T_1$ is $X_0$
-  then \SubtypeNE{T_0}{T_1}.
+  if $S$ is a type variable $X_0$
+  or a promoted type variable \code{$X_0$\,\&\,$S_0$} and $T$ is $X_0$
+  then \SubtypeNE{S}{T}.
 
   \commentary{%
     Note that this rule is admissible, and can be safely elided if desired.%
   }
 \item
   \textbf{Type Variable Reflexivity 2:}
-  if $T_0$ is a type variable $X_0$
+  if $S$ is a type variable $X_0$
   or a promoted type variable \code{$X_0$\,\&\,$S_0$}
-  and $T_1$ is \code{$X_0$\,\&\,$S_1$}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{T_0}{S_1}.
+  and $T$ is \code{$X_0$\,\&\,$S_1$}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{S_1}.
 
   \commentary{%
     Note that this rule is admissible, and can be safely elided if desired.%
   }
 \item
   \textbf{Right Promoted Variable:}
-  if $T_1$ is a promoted type variable \code{$X_1$\,\&\,$S_1$}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{T_0}{X_1} and \SubtypeNE{T_0}{S_1}.
+  if $T$ is a promoted type variable \code{$X_1$\,\&\,$S_1$}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X_1} and \SubtypeNE{S}{S_1}.
 \item
   \textbf{Right FutureOr:}
-  if $T_1$ is \code{FutureOr<$S_1$>}
-  then \SubtypeNE{T_0}{T_1} if{}f any of the following hold:
+  if $T$ is \code{FutureOr<$S_1$>}
+  then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}
-  \item either \SubtypeNE{T_0}{\code{Future<$S_1$>}}.
-  \item or \SubtypeNE{T_0}{S_1}.
-  \item or $T_0$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T_1}.
-  \item or $T_0$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T_1}.
+  \item either \SubtypeNE{S}{\code{Future<$S_1$>}}.
+  \item or \SubtypeNE{S}{S_1}.
+  \item or $S$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T}.
+  \item or $S$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T}.
   \end{itemize}
 \item
   \textbf{Right Nullable:}
-  if $T_1$ is \code{$S_1$?}
-  then \SubtypeNE{T_0}{T_1} if{}f any of the following hold:
+  if $T$ is \code{$S_1$?}
+  then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}
-  \item either \SubtypeNE{T_0}{S_1}.
-  \item or \SubtypeNE{T_0}{\code{Null}}.
-  \item or $T_0$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T_1}.
-  \item or $T_0$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T_1}.
+  \item either \SubtypeNE{S}{S_1}.
+  \item or \SubtypeNE{S}{\code{Null}}.
+  \item or $S$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T}.
+  \item or $S$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T}.
   \end{itemize}
 \item
   \textbf{Left Promoted Variable:}
-  If $T_0$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_0}{T_1}.
+  If $S$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_0}{T}.
 \item
   \textbf{Left Type Variable Bound:}
-  If $T_0$ is a type variable $X_0$ with bound $B_0$
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B_0}{T_1}.
+  If $S$ is a type variable $X_0$ with bound $B_0$
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{B_0}{T}.
 \item
   \textbf{Function Type/Function:}
-  $T_0$ is a function type and $T_1$ is \FUNCTION.
+  $S$ is a function type and $T$ is \FUNCTION.
 \item
   \textbf{Record Type/Record:}
-  $T_0$ is a record type and $T_1$ is \RECORD.
+  $S$ is a record type and $T$ is \RECORD.
 \item
   \textbf{Interface Compositionality:}
-  If $T_0$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
-  and $T_1$ is \code{$C_0$<$U_0$, \ldots, $U_k$>}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
+  If $S$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
+  and $T$ is \code{$C_0$<$U_0$, \ldots, $U_k$>}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
 \item
   \textbf{Super-Interface:}
-  If $T_0$ is an interface type with super-interfaces \List{S}{0}{n}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_i}{T_1} for some $i$.
+  If $S$ is an interface type with super-interfaces \List{S}{0}{n}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{T} for some $i$.
 \item
   \textbf{Positional Function Types:}
-  If $T_0$ is
+  If $S$ is
 
   \code{$U_0$ \FUNCTION<%
     $X_0$\,\EXTENDS\,$B_{00}$, \ldots, $X_k$\,\EXTENDS\,$B_{0k}$>(%
     $V_0$\,$x_0$, \ldots, $V_n$ $x_n$, %
     [$V_{n+1}$\,\,$x_{n+1}$, \ldots, $V_m$\,\,$x_m$])}
 
-  and $T_1$ is
+  and $T$ is
 
   \code{$U_1$ \FUNCTION<%
     $Y_0$\,\EXTENDS\,$B_{10}$, \ldots, $Y_k$\,\EXTENDS\,$B_{1k}$>(%
     $S_0$\,$y_0$, \ldots, $S_p$\,$y_p$, %
     [$S_{p+1}$\,$y_{p+1}$, \ldots, $S_q$\,$y_q$])}
 
-  then \SubtypeNE{T_0}{T_1} if{}f each of the following criteria is satisfied,
+  then \SubtypeNE{S}{T} if{}f each of the following criteria is satisfied,
   where the $Z_i$ are fresh type variables with bounds
   $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$:
 
@@ -23908,7 +23908,7 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Named Function Types:}
-  If $T_0$ is
+  If $S$ is
 
   \code{%
     $U_0$ \FUNCTION<$X_0$\,\EXTENDS\,$B_{00}$, \ldots, %
@@ -23917,7 +23917,7 @@ \section*{Appendix: Algorithmic Subtyping}
           \{$r_{0,n+1}$\,$V_{n+1}$\,$x_{n+1}$, \ldots, $r_{0m}$\,$V_m$\,$x_m$\})}
 
   where $r_{0j}$ is empty or \REQUIRED{} for $j \in n+1 .. m$
-  and $T_1$ is
+  and $T$ is
 
   \code{%
     $U_1$ \FUNCTION<$Y_0$\,\EXTENDS\,$B_{10}$, \ldots, %
@@ -23926,7 +23926,7 @@ \section*{Appendix: Algorithmic Subtyping}
           \{$r_{1,n+1}$\,$S_{n+1}$\,$y_{n+1}$, \ldots, $r_{1q}$\,$S_q$\,$y_q$\})}
 
   where $r_{1j}$ is empty or \REQUIRED{} for $j \in n+1 .. q$
-  then \SubtypeNE{T_0}{T_1} if{}f the following criteria are all satisfied,
+  then \SubtypeNE{S}{T} if{}f the following criteria are all satisfied,
   where \List{Z}{1}{k} are fresh type variables with bounds
   $[Z_0/X_0, \ldots, Z_k/X_k]B_{0i}$:
 
@@ -23958,9 +23958,9 @@ \section*{Appendix: Algorithmic Subtyping}
   }
 
 \item
-  If $T_0$ is \code{($V_0$, \ldots, $V_n$, \{$V_{n+1} d_{n+1}$, \ldots, $V_m d_m$\})}
-  and $T_1$ is \code{($S_0$, \ldots, $S_n$, \{$S_{n+1} d_{n+1}$, \ldots, $S_m d_m$\})}
-  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.
+  If $S$ is \code{($V_0$, \ldots, $V_n$, \{$V_{n+1} d_{n+1}$, \ldots, $V_m d_m$\})}
+  and $T$ is \code{($S_0$, \ldots, $S_n$, \{$S_{n+1} d_{n+1}$, \ldots, $S_m d_m$\})}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.
 \end{itemize}
 
 

From 9f9e661fcfc4cfd9d8ce4f6c108118b9374b0d0c Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:16:25 +0200
Subject: [PATCH 26/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index ac130f5ef8..c1c744cc22 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23736,7 +23736,7 @@ \section*{Appendix: Algorithmic Subtyping}
 it is then unnecessary to consider any subsequent cases.
 
 \LMHash{}%
-A type $T_0$ is a subtype of a type $T_1$ (written \SubtypeNE{T_0}{T_1}) when:
+A type $S$ is a subtype of a type $T$ (written \SubtypeNE{S}{T}) when:
 
 \begin{itemize}
 \item

From 70a4cb58f682f94c2ba6313d6997bd98ef240511 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:17:49 +0200
Subject: [PATCH 27/82] WIP

---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index c1c744cc22..c8dd5fb397 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23736,7 +23736,8 @@ \section*{Appendix: Algorithmic Subtyping}
 it is then unnecessary to consider any subsequent cases.
 
 \LMHash{}%
-A type $S$ is a subtype of a type $T$ (written \SubtypeNE{S}{T}) when:
+A type $S$ is a subtype of a type $T$ in the environment $\Delta$
+(written \SubtypeStd{S}{T}) when:
 
 \begin{itemize}
 \item

From b65c7fde67b695559ceb71c576052e98af1ed006 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:25:38 +0200
Subject: [PATCH 28/82] WIP

---
 specification/dartLangSpec.tex | 42 +++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index c8dd5fb397..5f57bbcf35 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23741,7 +23741,7 @@ \section*{Appendix: Algorithmic Subtyping}
 
 \begin{itemize}
 \item
-  \textbf{Reflexivity:}
+  \textbf{Reflexivity (\SrnReflexivity):}
   if $T_0$ and $T_1$ are the same type (\ref{sameType})
   then \SubtypeNE{T_0}{T_1}.
 
@@ -23755,17 +23755,17 @@ \section*{Appendix: Algorithmic Subtyping}
     Hence, this rule is only used when $T$ is atomic.%
   }
 \item
-  \textbf{Right Top:}
+  \textbf{Right Top (\SrnRightTop):}
   if $T$ is \DYNAMIC, \VOID, or \code{Object?} then \SubtypeNE{S}{T}.
 \item
-  \textbf{Left Top:}
+  \textbf{Left Top (\SrnLeftTop):}
   if $S$ is \DYNAMIC{} or \VOID{}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{\code{Object?}}{T}.
 \item
-  \textbf{Left Bottom:}
+  \textbf{Left Bottom (\SrnBottom):}
   if $S$ is \code{Never} then \SubtypeNE{S}{T}.
 \item
-  \textbf{Right Object:}
+  \textbf{Right Object (\SrnRightObjectFour):}
   if $T$ is \code{Object} then:
   \begin{itemize}
   \item
@@ -23787,7 +23787,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Otherwise \SubtypeNE{S}{T} is true.
   \end{itemize}
 \item
-  \textbf{Left Null:}
+  \textbf{Left Null (\SrnNullOne):}
   if $S$ is \code{Null} then:
   \begin{itemize}
   \item
@@ -23801,16 +23801,16 @@ \section*{Appendix: Algorithmic Subtyping}
     Otherwise, the query is false.
   \end{itemize}
 \item
-  \textbf{Left FutureOr:}
+  \textbf{Left FutureOr (\SrnLeftFutureOr, \SrnNullTwo):}
   if $S$ is \code{FutureOr<$S_0$>}
   then \SubtypeNE{S}{T} if{}f
   \SubtypeNE{\code{Future<$S_0$>}}{T} and \SubtypeNE{S_0}{T}.
 \item
-  \textbf{Left Nullable:}
+  \textbf{Left Nullable (\SrnLeftNullable):}
   if $S$ is \code{$S_0$?} then \SubtypeNE{S}{T} if{}f
   \SubtypeNE{S_0}{T} and \SubtypeNE{\code{Null}}{T}.
 \item
-  \textbf{Type Variable Reflexivity 1:}
+  \textbf{Type Variable Reflexivity 1 (\SrnLeftPromotedVariableOne):}
   if $S$ is a type variable $X_0$
   or a promoted type variable \code{$X_0$\,\&\,$S_0$} and $T$ is $X_0$
   then \SubtypeNE{S}{T}.
@@ -23819,7 +23819,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Note that this rule is admissible, and can be safely elided if desired.%
   }
 \item
-  \textbf{Type Variable Reflexivity 2:}
+  \textbf{Type Variable Reflexivity 2 (?):}
   if $S$ is a type variable $X_0$
   or a promoted type variable \code{$X_0$\,\&\,$S_0$}
   and $T$ is \code{$X_0$\,\&\,$S_1$}
@@ -23829,11 +23829,11 @@ \section*{Appendix: Algorithmic Subtyping}
     Note that this rule is admissible, and can be safely elided if desired.%
   }
 \item
-  \textbf{Right Promoted Variable:}
+  \textbf{Right Promoted Variable (\SrnRightPromotedVariable):}
   if $T$ is a promoted type variable \code{$X_1$\,\&\,$S_1$}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X_1} and \SubtypeNE{S}{S_1}.
 \item
-  \textbf{Right FutureOr:}
+  \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB):}
   if $T$ is \code{FutureOr<$S_1$>}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}
@@ -23843,7 +23843,7 @@ \section*{Appendix: Algorithmic Subtyping}
   \item or $S$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T}.
   \end{itemize}
 \item
-  \textbf{Right Nullable:}
+  \textbf{Right Nullable (\SrnRightNullableOne, \SrnRightNullableTwo):}
   if $T$ is \code{$S_1$?}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}
@@ -23853,30 +23853,30 @@ \section*{Appendix: Algorithmic Subtyping}
   \item or $S$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T}.
   \end{itemize}
 \item
-  \textbf{Left Promoted Variable:}
+  \textbf{Left Promoted Variable (\SrnLeftPromotedVariableTwo):}
   If $S$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_0}{T}.
 \item
-  \textbf{Left Type Variable Bound:}
+  \textbf{Left Type Variable Bound (\SrnLeftVariableBound):}
   If $S$ is a type variable $X_0$ with bound $B_0$
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{B_0}{T}.
 \item
-  \textbf{Function Type/Function:}
+  \textbf{Function Type/Function (\SrnRightFunction):}
   $S$ is a function type and $T$ is \FUNCTION.
 \item
-  \textbf{Record Type/Record:}
+  \textbf{Record Type/Record (\SrnPositionalFunctionType):}
   $S$ is a record type and $T$ is \RECORD.
 \item
-  \textbf{Interface Compositionality:}
+  \textbf{Interface Compositionality (\SrnNamedFunctionType):}
   If $S$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
   and $T$ is \code{$C_0$<$U_0$, \ldots, $U_k$>}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
 \item
-  \textbf{Super-Interface:}
+  \textbf{Super-Interface (\SrnNominal):}
   If $S$ is an interface type with super-interfaces \List{S}{0}{n}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{T} for some $i$.
 \item
-  \textbf{Positional Function Types:}
+  \textbf{Positional Function Types (\SrnPositionalFunctionType):}
   If $S$ is
 
   \code{$U_0$ \FUNCTION<%
@@ -23908,7 +23908,7 @@ \section*{Appendix: Algorithmic Subtyping}
     for $i \in 0 .. k$.
   \end{itemize}
 \item
-  \textbf{Named Function Types:}
+  \textbf{Named Function Types (\SrnNamedFunctionType):}
   If $S$ is
 
   \code{%

From dfe943f2bca73554d5950b9186e334a1c14a353f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:26:42 +0200
Subject: [PATCH 29/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 5f57bbcf35..73f4becc42 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23756,7 +23756,7 @@ \section*{Appendix: Algorithmic Subtyping}
   }
 \item
   \textbf{Right Top (\SrnRightTop):}
-  if $T$ is \DYNAMIC, \VOID, or \code{Object?} then \SubtypeNE{S}{T}.
+  if $T$ is \code{Object?}, \DYNAMIC, or \VOID then \SubtypeNE{S}{T}.
 \item
   \textbf{Left Top (\SrnLeftTop):}
   if $S$ is \DYNAMIC{} or \VOID{}

From e3d0a7974a73ca82b020402b7688b0a654738c8a Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:28:35 +0200
Subject: [PATCH 30/82] WIP

---
 specification/dartLangSpec.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 73f4becc42..7debe05ffa 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23737,7 +23737,8 @@ \section*{Appendix: Algorithmic Subtyping}
 
 \LMHash{}%
 A type $S$ is a subtype of a type $T$ in the environment $\Delta$
-(written \SubtypeStd{S}{T}) when:
+(written \SubtypeStd{S}{T} and
+abbreviated to \SubtypeNE{S}{T} when the environment is unused) when:
 
 \begin{itemize}
 \item
@@ -23756,7 +23757,7 @@ \section*{Appendix: Algorithmic Subtyping}
   }
 \item
   \textbf{Right Top (\SrnRightTop):}
-  if $T$ is \code{Object?}, \DYNAMIC, or \VOID then \SubtypeNE{S}{T}.
+  if $T$ is \code{Object?}, \DYNAMIC, or \VOID{} then \SubtypeNE{S}{T}.
 \item
   \textbf{Left Top (\SrnLeftTop):}
   if $S$ is \DYNAMIC{} or \VOID{}

From 24eea6ab278c4e731a7141896583e42b4a7c85a9 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:36:27 +0200
Subject: [PATCH 31/82] WIP

---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 7debe05ffa..358f664fbd 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23766,7 +23766,8 @@ \section*{Appendix: Algorithmic Subtyping}
   \textbf{Left Bottom (\SrnBottom):}
   if $S$ is \code{Never} then \SubtypeNE{S}{T}.
 \item
-  \textbf{Right Object (\SrnRightObjectFour):}
+  \textbf{Right Object (\SrnLeftVariableBound*, \SrnLeftPromotedVariableTwo*, %
+    \SrnLeftFutureOr*, \SrnRightObjectFour):}
   if $T$ is \code{Object} then:
   \begin{itemize}
   \item

From 3f24aee16c1454f9d72299072612fa9466c4474f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:41:03 +0200
Subject: [PATCH 32/82] WIP

---
 specification/dartLangSpec.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 358f664fbd..f57597badd 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23795,10 +23795,10 @@ \section*{Appendix: Algorithmic Subtyping}
   \item
     if $T$ is a type variable (promoted or not) the query is false.
   \item
-    if $T$ is \code{FutureOr<$S$>} for some $S$,
-    then the query is true if{}f \SubtypeNE{\code{Null}}{S}.
+    if $T$ is \code{FutureOr<$U$>} for some $U$,
+    then the query is true if{}f \SubtypeNE{\code{Null}}{U}.
   \item
-    if $T$ is \code{$S$?} for some $S$ then the query is true.
+    if $T$ is \code{$U$?} for some $U$ then the query is true.
   \item
     Otherwise, the query is false.
   \end{itemize}

From 37fb0e11bc3bbcdb504346ba77b7a4d4187f12a4 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:44:22 +0200
Subject: [PATCH 33/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index f57597badd..27c31574f5 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23777,8 +23777,8 @@ \section*{Appendix: Algorithmic Subtyping}
     if $S$ is a promoted type variable \code{$X$\,\&\,$S$}
     then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{\code{Object}}.
   \item
-    if $S$ is \code{FutureOr<$S$>} for some $S$,
-    then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{\code{Object}}.
+    if $S$ is \code{FutureOr<$U$>} for some $U$,
+    then \SubtypeNE{S}{T} if{}f \SubtypeNE{U}{\code{Object}}.
   \item
     if $S$ is \code{Null}, \DYNAMIC, \VOID, or \code{$S$?} for any $S$,
     then the subtyping does not hold

From 87ac87f425cd6b4e32bb81675093785ab2096829 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:49:19 +0200
Subject: [PATCH 34/82] WIP

---
 specification/dartLangSpec.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 27c31574f5..b00d9304ab 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23789,7 +23789,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Otherwise \SubtypeNE{S}{T} is true.
   \end{itemize}
 \item
-  \textbf{Left Null (\SrnNullOne):}
+  \textbf{Left Null (\SrnRightFutureOrB*, \SrnNullOne):}
   if $S$ is \code{Null} then:
   \begin{itemize}
   \item
@@ -23804,9 +23804,9 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Left FutureOr (\SrnLeftFutureOr, \SrnNullTwo):}
-  if $S$ is \code{FutureOr<$S_0$>}
+  if $S$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f
-  \SubtypeNE{\code{Future<$S_0$>}}{T} and \SubtypeNE{S_0}{T}.
+  \SubtypeNE{\code{Future<$U$>}}{T} and \SubtypeNE{U}{T}.
 \item
   \textbf{Left Nullable (\SrnLeftNullable):}
   if $S$ is \code{$S_0$?} then \SubtypeNE{S}{T} if{}f

From 1916562e077ad97ec67c00fe4ecfe53600eb423f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:50:33 +0200
Subject: [PATCH 35/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index b00d9304ab..8876c9175f 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23803,7 +23803,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Otherwise, the query is false.
   \end{itemize}
 \item
-  \textbf{Left FutureOr (\SrnLeftFutureOr, \SrnNullTwo):}
+  \textbf{Left FutureOr (\SrnLeftFutureOr):}
   if $S$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f
   \SubtypeNE{\code{Future<$U$>}}{T} and \SubtypeNE{U}{T}.

From b5ec605f223cffd398518eca42a352649cdaa989 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:51:20 +0200
Subject: [PATCH 36/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 8876c9175f..91dd2d8de1 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23809,8 +23809,8 @@ \section*{Appendix: Algorithmic Subtyping}
   \SubtypeNE{\code{Future<$U$>}}{T} and \SubtypeNE{U}{T}.
 \item
   \textbf{Left Nullable (\SrnLeftNullable):}
-  if $S$ is \code{$S_0$?} then \SubtypeNE{S}{T} if{}f
-  \SubtypeNE{S_0}{T} and \SubtypeNE{\code{Null}}{T}.
+  if $S$ is \code{$U$?} then \SubtypeNE{S}{T} if{}f
+  \SubtypeNE{U}{T} and \SubtypeNE{\code{Null}}{T}.
 \item
   \textbf{Type Variable Reflexivity 1 (\SrnLeftPromotedVariableOne):}
   if $S$ is a type variable $X_0$

From c230889131ce2e0383994dcc74236f5ebf3b834b Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:53:54 +0200
Subject: [PATCH 37/82] WIP

---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 91dd2d8de1..878325651d 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23812,7 +23812,8 @@ \section*{Appendix: Algorithmic Subtyping}
   if $S$ is \code{$U$?} then \SubtypeNE{S}{T} if{}f
   \SubtypeNE{U}{T} and \SubtypeNE{\code{Null}}{T}.
 \item
-  \textbf{Type Variable Reflexivity 1 (\SrnLeftPromotedVariableOne):}
+  \textbf{Type Variable Reflexivity 1 %
+    (\SrnLeftPromotedVariableOne, \SrnReflexivity*):}
   if $S$ is a type variable $X_0$
   or a promoted type variable \code{$X_0$\,\&\,$S_0$} and $T$ is $X_0$
   then \SubtypeNE{S}{T}.

From ced80e2e78ba910baad42f4b7159a42cab453424 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:55:41 +0200
Subject: [PATCH 38/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 878325651d..1dd2dc2211 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23814,8 +23814,8 @@ \section*{Appendix: Algorithmic Subtyping}
 \item
   \textbf{Type Variable Reflexivity 1 %
     (\SrnLeftPromotedVariableOne, \SrnReflexivity*):}
-  if $S$ is a type variable $X_0$
-  or a promoted type variable \code{$X_0$\,\&\,$S_0$} and $T$ is $X_0$
+  if $S$ is a type variable $X$
+  or a promoted type variable \code{$X$\,\&\,$U$} and $T$ is $X$
   then \SubtypeNE{S}{T}.
 
   \commentary{%

From dcd2c568a68b4a89c600cfd42b41bcc258f30c64 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 15:57:41 +0200
Subject: [PATCH 39/82] WIP

---
 specification/dartLangSpec.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 1dd2dc2211..7c1188c0a1 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23823,10 +23823,10 @@ \section*{Appendix: Algorithmic Subtyping}
   }
 \item
   \textbf{Type Variable Reflexivity 2 (?):}
-  if $S$ is a type variable $X_0$
-  or a promoted type variable \code{$X_0$\,\&\,$S_0$}
-  and $T$ is \code{$X_0$\,\&\,$S_1$}
-  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{S_1}.
+  if $S$ is a type variable $X$
+  or a promoted type variable \code{$X$\,\&\,$U$}
+  and $T$ is \code{$X$\,\&\,$V$}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{U}{V}.
 
   \commentary{%
     Note that this rule is admissible, and can be safely elided if desired.%

From b46282fad3e10a6113146f21a2f3c397e8b35d12 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:02:07 +0200
Subject: [PATCH 40/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 7c1188c0a1..01d2a8e0b2 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23822,11 +23822,11 @@ \section*{Appendix: Algorithmic Subtyping}
     Note that this rule is admissible, and can be safely elided if desired.%
   }
 \item
-  \textbf{Type Variable Reflexivity 2 (?):}
+  \textbf{Type Variable Reflexivity 2 (\Srn):}
   if $S$ is a type variable $X$
   or a promoted type variable \code{$X$\,\&\,$U$}
   and $T$ is \code{$X$\,\&\,$V$}
-  then \SubtypeNE{S}{T} if{}f \SubtypeNE{U}{V}.
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{V}.
 
   \commentary{%
     Note that this rule is admissible, and can be safely elided if desired.%

From 8c7566019a8e5bf836743b4d1fba7f658fdd4ccd Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:05:10 +0200
Subject: [PATCH 41/82] WIP

---
 specification/dartLangSpec.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 01d2a8e0b2..cd7534900e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23822,7 +23822,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Note that this rule is admissible, and can be safely elided if desired.%
   }
 \item
-  \textbf{Type Variable Reflexivity 2 (\Srn):}
+  \textbf{Type Variable Reflexivity 2 (\SrnRightPromotedVariable*):}
   if $S$ is a type variable $X$
   or a promoted type variable \code{$X$\,\&\,$U$}
   and $T$ is \code{$X$\,\&\,$V$}
@@ -23833,8 +23833,8 @@ \section*{Appendix: Algorithmic Subtyping}
   }
 \item
   \textbf{Right Promoted Variable (\SrnRightPromotedVariable):}
-  if $T$ is a promoted type variable \code{$X_1$\,\&\,$S_1$}
-  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X_1} and \SubtypeNE{S}{S_1}.
+  if $T$ is a promoted type variable \code{$X$\,\&\,$U$}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X} and \SubtypeNE{S}{U}.
 \item
   \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB):}
   if $T$ is \code{FutureOr<$S_1$>}

From 42524d1bb69f29bb1ed26da18d8397bdc6bd351e Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:07:41 +0200
Subject: [PATCH 42/82] WIP

---
 specification/dartLangSpec.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index cd7534900e..758554c9f3 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23837,13 +23837,13 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X} and \SubtypeNE{S}{U}.
 \item
   \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB):}
-  if $T$ is \code{FutureOr<$S_1$>}
+  if $T$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}
-  \item either \SubtypeNE{S}{\code{Future<$S_1$>}}.
-  \item or \SubtypeNE{S}{S_1}.
-  \item or $S$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T}.
-  \item or $S$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T}.
+  \item either \SubtypeNE{S}{\code{Future<$U$>}}.
+  \item or \SubtypeNE{S}{U}.
+  \item or $S$ is $X$ and $X$ has bound $B$ and \SubtypeNE{B}{T}.
+  \item or $S$ is \code{$X$\,\&\,$V$} and \SubtypeNE{V}{T}.
   \end{itemize}
 \item
   \textbf{Right Nullable (\SrnRightNullableOne, \SrnRightNullableTwo):}

From 9329b995011fbc1fbd5cae56a9810351d130fd15 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:09:08 +0200
Subject: [PATCH 43/82] WIP

---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 758554c9f3..0404698004 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23836,7 +23836,8 @@ \section*{Appendix: Algorithmic Subtyping}
   if $T$ is a promoted type variable \code{$X$\,\&\,$U$}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X} and \SubtypeNE{S}{U}.
 \item
-  \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB):}
+  \textbf{Right FutureOr %
+    (\SrnRightFutureOrA, \SrnRightFutureOrB, \SrnLeftVariableBound):}
   if $T$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}

From 7dbf36a5e48f88cf0ce52f6e0d7224d06d4df540 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:10:44 +0200
Subject: [PATCH 44/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 0404698004..cf98c0c73b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23836,8 +23836,8 @@ \section*{Appendix: Algorithmic Subtyping}
   if $T$ is a promoted type variable \code{$X$\,\&\,$U$}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X} and \SubtypeNE{S}{U}.
 \item
-  \textbf{Right FutureOr %
-    (\SrnRightFutureOrA, \SrnRightFutureOrB, \SrnLeftVariableBound):}
+  \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB, %
+    \SrnLeftVariableBound, SrnLeftPromotedVariableTwo*):}
   if $T$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}

From c52e27bd307e2c8bf86b3b39f2b00c85fc7db9be Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:11:34 +0200
Subject: [PATCH 45/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index cf98c0c73b..4766a0057c 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23837,7 +23837,7 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X} and \SubtypeNE{S}{U}.
 \item
   \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB, %
-    \SrnLeftVariableBound, SrnLeftPromotedVariableTwo*):}
+    \SrnLeftVariableBound, \SrnLeftPromotedVariableTwo*):}
   if $T$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}

From f28af42edd59964e2925096f5b6dc844309457b6 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:13:12 +0200
Subject: [PATCH 46/82] WIP

---
 specification/dartLangSpec.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 4766a0057c..862b57b807 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23848,13 +23848,13 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Right Nullable (\SrnRightNullableOne, \SrnRightNullableTwo):}
-  if $T$ is \code{$S_1$?}
+  if $T$ is \code{$U$?}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}
-  \item either \SubtypeNE{S}{S_1}.
+  \item either \SubtypeNE{S}{U}.
   \item or \SubtypeNE{S}{\code{Null}}.
-  \item or $S$ is $X_0$ and $X_0$ has bound $B_0$ and \SubtypeNE{B_0}{T}.
-  \item or $S$ is \code{$X_0$\,\&\,$S_0$} and \SubtypeNE{S_0}{T}.
+  \item or $S$ is $X$ and $X$ has bound $B$ and \SubtypeNE{B}{T}.
+  \item or $S$ is \code{$X$\,\&\,$V$} and \SubtypeNE{V}{T}.
   \end{itemize}
 \item
   \textbf{Left Promoted Variable (\SrnLeftPromotedVariableTwo):}

From f7a0669565272f975eb5be05bd77e25382504acc Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:14:46 +0200
Subject: [PATCH 47/82] WIP

---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 862b57b807..602974f90a 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23847,7 +23847,8 @@ \section*{Appendix: Algorithmic Subtyping}
   \item or $S$ is \code{$X$\,\&\,$V$} and \SubtypeNE{V}{T}.
   \end{itemize}
 \item
-  \textbf{Right Nullable (\SrnRightNullableOne, \SrnRightNullableTwo):}
+  \textbf{Right Nullable (\SrnRightNullableOne, \SrnRightNullableTwo, %
+    \SrnLeftVariableBound*):}
   if $T$ is \code{$U$?}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}

From 81eaa1c9810a782ce1308607d7b4b716598bd6ce Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:16:14 +0200
Subject: [PATCH 48/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 602974f90a..5feeb1aa5e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23859,8 +23859,8 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Left Promoted Variable (\SrnLeftPromotedVariableTwo):}
-  If $S$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
-  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_0}{T}.
+  If $S$ is a promoted type variable \code{$X$\,\&\,$U$}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{U}{T}.
 \item
   \textbf{Left Type Variable Bound (\SrnLeftVariableBound):}
   If $S$ is a type variable $X_0$ with bound $B_0$

From e348f55c9ef0c08d4c5af753e9036599cc919f1d Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:17:09 +0200
Subject: [PATCH 49/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 5feeb1aa5e..61569e6a05 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23863,8 +23863,8 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{U}{T}.
 \item
   \textbf{Left Type Variable Bound (\SrnLeftVariableBound):}
-  If $S$ is a type variable $X_0$ with bound $B_0$
-  then \SubtypeNE{S}{T} if{}f \SubtypeNE{B_0}{T}.
+  If $S$ is a type variable $X$ with bound $B$
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{B}{T}.
 \item
   \textbf{Function Type/Function (\SrnRightFunction):}
   $S$ is a function type and $T$ is \FUNCTION.

From 0543c564d7146925b2b96d522febe602fdcec34f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:20:39 +0200
Subject: [PATCH 50/82] WIP

---
 specification/dartLangSpec.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 61569e6a05..21dae0fdb0 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23869,15 +23869,17 @@ \section*{Appendix: Algorithmic Subtyping}
   \textbf{Function Type/Function (\SrnRightFunction):}
   $S$ is a function type and $T$ is \FUNCTION.
 \item
-  \textbf{Record Type/Record (\SrnPositionalFunctionType):}
+  %% TODO(eernst): Come records, we must add an inference rule for this
+  %% in the 'Subtype rules' figure.
+  \textbf{Record Type/Record ():}
   $S$ is a record type and $T$ is \RECORD.
 \item
-  \textbf{Interface Compositionality (\SrnNamedFunctionType):}
+  \textbf{Covariance (\SrnCovariance):}
   If $S$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
   and $T$ is \code{$C_0$<$U_0$, \ldots, $U_k$>}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
 \item
-  \textbf{Super-Interface (\SrnNominal):}
+  \textbf{Nominal subtyping (\SrnNominal):}
   If $S$ is an interface type with super-interfaces \List{S}{0}{n}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{T} for some $i$.
 \item

From 5082e647c0e555f5785f64a4ab77025db05d5be2 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 16:25:53 +0200
Subject: [PATCH 51/82] WIP

---
 specification/dartLangSpec.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 21dae0fdb0..43d304279e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23868,11 +23868,11 @@ \section*{Appendix: Algorithmic Subtyping}
 \item
   \textbf{Function Type/Function (\SrnRightFunction):}
   $S$ is a function type and $T$ is \FUNCTION.
-\item
-  %% TODO(eernst): Come records, we must add an inference rule for this
-  %% in the 'Subtype rules' figure.
-  \textbf{Record Type/Record ():}
-  $S$ is a record type and $T$ is \RECORD.
+%% TODO(eernst): Come records, include this rule, and add an
+%% inference rule for this in the 'Subtype rules' figure:
+%% \item
+%%   \textbf{Record Type/Record ():}
+%%   $S$ is a record type and $T$ is \RECORD.
 \item
   \textbf{Covariance (\SrnCovariance):}
   If $S$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}

From e695900017b8e1b37982034726805ee43fecff05 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 17:56:36 +0200
Subject: [PATCH 52/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 43d304279e..c348bae2bd 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23789,7 +23789,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Otherwise \SubtypeNE{S}{T} is true.
   \end{itemize}
 \item
-  \textbf{Left Null (\SrnRightFutureOrB*, \SrnNullOne):}
+  \textbf{Left Null (\SrnRightFutureOrB*, \SrnNullTwo):}
   if $S$ is \code{Null} then:
   \begin{itemize}
   \item

From bd7d51c8b73891476e917930997de1d746e26ae9 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 17:58:23 +0200
Subject: [PATCH 53/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index c348bae2bd..5645e5a249 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23789,7 +23789,7 @@ \section*{Appendix: Algorithmic Subtyping}
     Otherwise \SubtypeNE{S}{T} is true.
   \end{itemize}
 \item
-  \textbf{Left Null (\SrnRightFutureOrB*, \SrnNullTwo):}
+  \textbf{Left Null (\SrnRightFutureOrB*, \SrnNullTwo, \SrnNullOne):}
   if $S$ is \code{Null} then:
   \begin{itemize}
   \item

From 5da7f691356d5d2930823f53c9bbbf7cee8dc88c Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 18:04:59 +0200
Subject: [PATCH 54/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 5645e5a249..d4e29d45a8 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23837,7 +23837,7 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S}{X} and \SubtypeNE{S}{U}.
 \item
   \textbf{Right FutureOr (\SrnRightFutureOrA, \SrnRightFutureOrB, %
-    \SrnLeftVariableBound, \SrnLeftPromotedVariableTwo*):}
+    \SrnLeftVariableBound*, \SrnLeftPromotedVariableTwo*):}
   if $T$ is \code{FutureOr<$U$>}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}

From 92f3ca66b4240cef21c2d1883c67db17af14d944 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 18:07:19 +0200
Subject: [PATCH 55/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index d4e29d45a8..cc032539d4 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23848,7 +23848,7 @@ \section*{Appendix: Algorithmic Subtyping}
   \end{itemize}
 \item
   \textbf{Right Nullable (\SrnRightNullableOne, \SrnRightNullableTwo, %
-    \SrnLeftVariableBound*):}
+    \SrnLeftVariableBound*, \SrnLeftPromotedVariableTwo*):}
   if $T$ is \code{$U$?}
   then \SubtypeNE{S}{T} if{}f any of the following hold:
   \begin{itemize}

From c6d0f9bc4c3d73b765cf5ad1c46b630ac4b85d1f Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 18:09:37 +0200
Subject: [PATCH 56/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index cc032539d4..c788d68cd9 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23875,8 +23875,8 @@ \section*{Appendix: Algorithmic Subtyping}
 %%   $S$ is a record type and $T$ is \RECORD.
 \item
   \textbf{Covariance (\SrnCovariance):}
-  If $S$ is an interface type \code{$C_0$<$S_0$, \ldots, $S_k$>}
-  and $T$ is \code{$C_0$<$U_0$, \ldots, $U_k$>}
+  If $S$ is an interface type \code{$C$<$S_1$, \ldots, $S_s$>}
+  and $T$ is \code{$C$<$U_1$, \ldots, $U_s$>}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
 \item
   \textbf{Nominal subtyping (\SrnNominal):}

From b9b703e4852940d6899a5e8b52e1fccd507342d1 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 18:10:42 +0200
Subject: [PATCH 57/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index c788d68cd9..3e1daade89 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23876,8 +23876,8 @@ \section*{Appendix: Algorithmic Subtyping}
 \item
   \textbf{Covariance (\SrnCovariance):}
   If $S$ is an interface type \code{$C$<$S_1$, \ldots, $S_s$>}
-  and $T$ is \code{$C$<$U_1$, \ldots, $U_s$>}
-  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{U_i} for each $i$.
+  and $T$ is \code{$C$<$T_1$, \ldots, $T_s$>}
+  then \SubtypeNE{S}{T} if{}f \SubtypeNE{S_i}{T_i} for each $i$.
 \item
   \textbf{Nominal subtyping (\SrnNominal):}
   If $S$ is an interface type with super-interfaces \List{S}{0}{n}

From 6164426c211c36768393426bed976e30c4b35c6d Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 14 Aug 2025 18:34:07 +0200
Subject: [PATCH 58/82] WIP

---
 specification/dartLangSpec.tex | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 3e1daade89..ee88416187 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23737,7 +23737,7 @@ \section*{Appendix: Algorithmic Subtyping}
 
 \LMHash{}%
 A type $S$ is a subtype of a type $T$ in the environment $\Delta$
-(written \SubtypeStd{S}{T} and
+(written \SubtypeStd{S}{T},
 abbreviated to \SubtypeNE{S}{T} when the environment is unused) when:
 
 \begin{itemize}
@@ -23971,6 +23971,15 @@ \section*{Appendix: Algorithmic Subtyping}
   then \SubtypeNE{S}{T} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.
 \end{itemize}
 
+\LMHash{}%
+In these rules, the numbers in parentheses refer to the derivation rules in
+Fig.~\ref{fig:subtypeRules} with the given number.
+A number with an asterisk indicates that
+a special case of said derivation rule is used.
+A number with no asterisk indicates that the textual rule above
+(or part of it) corresponds more directly to
+the derivation rule with the specified number.
+
 
 \section*{Appendix: Integer Implementations}
 \LMLabel{integerImplementations}

From bcf7b4a27dd97828ecc92d4c33232818189820e8 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 10:01:46 +0200
Subject: [PATCH 59/82] WIP

---
 specification/dartLangSpec.tex | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index ee88416187..f6ea6a5b3e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -11,6 +11,7 @@
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \usepackage{makeidx}
+\usepackage{tocloft}
 \makeindex
 \title{Dart Programming Language Specification\\
 {6th edition draft}\\
@@ -460,6 +461,9 @@
 
 \begin{document}
 \maketitle
+% Adjust the horizontal offset of section titles in the table of contents.
+\setlength{\cftsubsecnumwidth}{2.7em}
+\setlength{\cftsubsubsecnumwidth}{3.4em}
 \tableofcontents
 
 \newpage

From ce5094d99a34982f7baa4c48a014f55c18434a71 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 15:47:28 +0200
Subject: [PATCH 60/82] WIP

---
 specification/dartLangSpec.tex | 193 ++++++++-------------------------
 1 file changed, 47 insertions(+), 146 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index f6ea6a5b3e..4c2152bfc5 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23387,11 +23387,11 @@ \subsection{Same Type}
 \LMLabel{sameType}
 
 \LMHash{}%
-This section specifies how to soundly determine whether or not two types
+This section specifies how to determine whether or not two types
 that are encountered during static analysis are the same type.
 
 \LMHash{}%
-Concrete syntax denoting types gives rise to several difficulties
+Concrete syntax denoting types gives rise to difficulties
 when used to determine static semantic properties,
 like subtyping relationships
 (\ref{subtypes})
@@ -23399,7 +23399,7 @@ \subsection{Same Type}
 (\ref{standardUpperBoundsAndStandardLowerBounds}).
 
 \commentary{%
-  Note that the notion of being the same type at run time is different from
+  The notion of being the same type at run time is different from
   the notion of being the same type during static analysis.
   For example, two distinct type variables \code{X} and \code{Y}
   might at run time be bound to the same type, e.g.,
@@ -23408,12 +23408,9 @@ \subsection{Same Type}
   \code{X} and \code{Y} are different types
   because there is no guarantee that they are always bound to
   the same type at run time.%
-}
 
-\commentary{%
-  The phrases `same type' and `identical syntax' deserves some extra scrutiny.
-  If a library $L$ imports the libraries $L_1$ and $L_2$
-  (where $L_1$ and $L_2$ are not the same library),
+  The phrase `same type' deserves some extra scrutiny.
+  If a library $L$ imports the libraries $L_1$ and $L_2$,
   and both $L_1$ and $L_2$ declare a class \code{C},
   then the syntax \code{C} may occur as a type during static analysis of $L$
   in situations where it refers to two distinct types.
@@ -23421,8 +23418,8 @@ \subsection{Same Type}
   For instance, $L_1$ could declare a variable \code{v}
   of type \code{C}-in-$L_1$,
   and $L_2$ could declare a function
-  \code{\VOID\,foo(C\,\,c)\,\,\{\}}
-  which uses the type \code{C}-in-$L_2$,
+  \code{\VOID\,foo(C\,\,c)\,\,\{\ldots\}}
+  which refers to the type \code{C}-in-$L_2$,
   and $L$ could contain the expression \code{foo(v)}.
 
   Note that even though it would be a compile-time error to use \code{C} in $L$
@@ -23434,137 +23431,25 @@ \subsection{Same Type}
   depending on the subtyping relations.%
 }
 
-\rationale{%
-  This shows that concrete syntax behaves in such a manner that it is
-  unsafe to consider two types to be the same type,
-  based on the fact that they are denoted by the same syntax,
-  even during the static analysis of a single expression.
-
-  Similarly, it is incorrect to consider two terms derived from \synt{type}
-  as different types based on the fact that they are syntactically different.
-  For example, they could be the same type imported with different import
-  prefixes.
-
-  We could say that two identifiers
-  (possibly qualified, e.g., \code{myPrefix.C} and \code{C})
-  denote the same type
-  if they have been resolved to the same declaration.
-
-  However, we introduce \emph{the explicitly resolved syntax for a type},
-  which is basically an explicit representation of this idea,
-  in order to make the underlying issues more explicit.
-  The explicitly resolved syntax has the property that
-  each type has a unique syntactic form
-  (except for alpha equivalence, which is defined below).
-  We may then consider this unique syntactic form as a static semantic value,
-  rather than just a syntactic form which is dependent on
-  its location in the program.%
-}
-
-\LMHash{}%
-The
-\IndexCustom{explicitly resolved syntax}{type!explicitly resolved syntax of}
-of the types in a given library $L_1$
-and all libraries \List{L}{2}{n} reachable from $L_1$ via
-one or more import links
-is determined as follows.
-First, choose a set of distinct, globally fresh identifiers
-\List{\metavar{prefix}}{1}{n}.
-Then transform each library $L_i$, $i \in 1 .. n$ as follows:
-
-\begin{enumerate}
-\item
-  For each type variable declared in $L_i$, consistently rename
-  it to a globally fresh name.
-\item
-  If $D_T$ is a declaration of a class, mixin, or type alias in $L_i$
-  whose name $n$ is private,
-  and an occurrence of $n$ that resolves to $D$
-  exists in a type alias declaration $D_A$ whose name is non-private,
-  then perform a consistent renaming of
-  all occurrences of $n$ in $L_i$ that resolve to $D_T$
-  to a fresh, non-private identifier.
-  \commentary{%
-    We make $D_T$ public, because it is being leaked anyway.%
-  }
-\item
-  Add a set of import directives to $L_i$ that imports
-  each of the libraries \List{L}{1}{n} with
-  the corresponding prefix $\metavar{prefix}_j$, $j \in 1 .. n$.
-
-  \commentary{%
-    This means that every library in the set
-    $\{\,\List{L}{1}{n}\,\}$
-    imports every other library in that set,
-    even itself and system libraries like \code{dart:core}.%
-  }
-\item
-  Let \id{} be an occurrence of
-  a non-private type identifier derived from \synt{typeName}
-  that resolves to a library declaration in the library $L_j$
-  in the original program;
-  \id{} is then transformed to \code{$\metavar{prefix}_j$.\id}.
-  Let \code{$p$.\id} be derived from \synt{typeName} such that $p$ is
-  an import prefix in the original program
-  and \id{} is a non-private identifier,
-  and consider the case where \code{$p$.\id} resolves to
-  a library declaration in the library $L_j$ in the original program,
-  for some $j$;
-  \code{$p$.\id} is then transformed to \code{$\metavar{prefix}_j$.\id}.
-\item
-  Replace every type in $L_i$ that denotes a type alias
-  along with its actual type arguments, if any,
-  by its transitive alias expansion
-  (\ref{typedef}).
-  \commentary{%
-    Note that the bodies of type alias declarations
-    already use the new prefixes,
-    so the results of the alias expansion will also use
-    the new prefixes consistently.%
-  }
-\end{enumerate}
-
-\commentary{%
-  In short, this transformation adds a unique prefix to every type name
-  which is resolved to a top-level declaration
-  (in the same library or in an imported library).
-
-  This transformation does not change any occurrence of \VOID,
-  and does not need to;
-  \VOID{} is a reserved word, not a type identifier.
-  Also, \code{$\metavar{prefix}_j$.\VOID} would be a syntax error.
-
-  Note that the transformation changes terms derived from \synt{type},
-  but it does not change expressions, or any other program element
-  (except that a \synt{type} can occur in an expression, e.g., \code{<int>[]}).
-  In particular, it does not change type literals
-  (that is, expressions denoting types).%
-}
-
 \LMHash{}%
-Every \synt{type} in the resulting set of libraries
-is now expressed in a globally unique syntactic form,
-which is the form that we call the
-\IndexCustom{explicitly resolved syntax of}{type!explicitly resolved syntax of}
-said types.
+Hence, when this specification refers to
+a type designated by a term
+that may seem to stand for concrete syntax,
+it is actually using \Index{resolved syntax}.
+Resolved syntax is syntax which is enhanced such that
+every \emph{applied} occurrence of an identifier
+(as opposed to a declaring occurrence)
+carries information about the declaration
+that it has been resolved to denote.
 
 \LMHash{}%
-When we say that two types $T_1$ and $T_2$ have the
-\IndexCustom{same explicitly resolved syntax}{%
-  type!same explicitly resolved syntax},
-it refers to the situation where the current library
-and all libraries which are reachable via one or more imports
-have been transformed as described above,
-and the resulting explicitly resolved syntaxes are textually identical.
-
-\LMHash{}%
-We need to introduce one more concept:
-An \Index{alpha conversion} of a type is a consistent renaming
-of the type variables declared in that type.
+An \Index{alpha conversion} of a type is a consistent, non-capturing renaming
+of type variables declared in that type.
 
 \commentary{%
-  In Dart, only function types can be subject to an alpha conversion:
-  A function type is the only kind of type that declares type variables.
+  In Dart, a function type is
+  the only kind of type which can declare type variables,
+  so only a generic function type can be subjected to an alpha conversion.
   For example,
   \code{List<X>\,\,\FUNCTION<X>({X\,\,arg})}
   can be turned into
@@ -23573,17 +23458,33 @@ \subsection{Same Type}
 }
 
 \LMHash{}%
-Two function types are \Index{alpha equivalent} if{}f
-there exists an alpha conversion that makes them textually identical.
+We can now define what it means to be the same type.
+Two types $S$ and $T$ are the same type when
+at least one of the following criteria holds:
 
-\LMHash{}%
-Finally, we define that two type denotations $T_1$ and $T_2$ are the
-\IndexCustom{same static type}{type!same static}
-if there exist alpha conversions
-that can be applied to the function types
-that occur as subterms of $T_1$ and $T_2$, if any,
-such that the resulting terms $T'_1$ and $T'_2$ have
-the same explicitly resolved syntax.
+\begin{itemize}
+\item $S$ is \VOID{} and $T$ is \VOID.
+  \commentary{This is a reserved word and cannot be shadowed.}
+\item $S$ is an identifier or a prefixed identifier which is resolved
+  to denote a type-introducing declaration $D_S$,
+  and $T$ is an identifier or a prefixed identifier which is resolved
+  to denote a type-introducing declaration $D_T$,
+  and $D_S$ is the same declaration as  $D_T$.
+\item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},
+  and $T$ is of the form \code{$D$<$V_1$, \ldots\ $V_s$>},
+  where $C$ and $D$ have been resolved to denote the same declaration,
+  or they are both \code{FutureOr},
+  and $U_j$ is the same type as $V_j$ for all $j \in 1 .. s$.
+\item $S$ and $T$ are both positional function types with the same
+  number of mandatory parameters and the same number of optional parameters,
+  the same return type, and the same type for each of the parameters.
+\item $S$ and $T$ are both named function types with the same
+  number of mandatory parameters and the same set of named parameters,
+  the same return type, and the same type for each of the parameters,
+  and the same subset of the named parameters marked as \REQUIRED.
+\item There exists an alpha conversion of $S$ yielding $S'$, and
+  $S'$ and $T$ are the same type.
+\end{itemize}
 
 
 \section{Reference}

From b154532b0ba65b3519a570252bd01726c59fa178 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 15:56:17 +0200
Subject: [PATCH 61/82] WIP

---
 specification/dartLangSpec.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 4c2152bfc5..309c592299 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23482,6 +23482,14 @@ \subsection{Same Type}
   number of mandatory parameters and the same set of named parameters,
   the same return type, and the same type for each of the parameters,
   and the same subset of the named parameters marked as \REQUIRED.
+\item $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
+  denotes a type alias declaration,
+  the unfolding of the type alias yields $S'$,
+  and $S'$ is the same type as $T$.
+\item $T$ is of the form \code{$G$<$V_1$, \ldots\ $V_s$>} where $G$
+  denotes a type alias declaration,
+  the unfolding of the type alias yields $T'$,
+  and $S$ is the same type as $T'$.
 \item There exists an alpha conversion of $S$ yielding $S'$, and
   $S'$ and $T$ are the same type.
 \end{itemize}

From 98bb53f5d30aba1762a81d9405b3c78feb269acc Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 15:58:56 +0200
Subject: [PATCH 62/82] WIP

---
 specification/dartLangSpec.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 309c592299..903ad64a89 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23396,7 +23396,9 @@ \subsection{Same Type}
 like subtyping relationships
 (\ref{subtypes})
 or upper and lower bounds
-(\ref{standardUpperBoundsAndStandardLowerBounds}).
+(\ref{standardUpperBoundsAndStandardLowerBounds}),
+because it is concerned with relationships among program elements
+that occur in different binding environments.
 
 \commentary{%
   The notion of being the same type at run time is different from

From bb12639f6209a00babb96b68989c5d026cc8ed67 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:00:31 +0200
Subject: [PATCH 63/82] WIP

---
 specification/dartLangSpec.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 903ad64a89..937ad27d03 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23445,6 +23445,7 @@ \subsection{Same Type}
 that it has been resolved to denote.
 
 \LMHash{}%
+We need one more mechanism:
 An \Index{alpha conversion} of a type is a consistent, non-capturing renaming
 of type variables declared in that type.
 

From 55f584113f26ef8caa39c2a0c1ae9047c565d283 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:01:32 +0200
Subject: [PATCH 64/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 937ad27d03..d6c9d90510 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23454,9 +23454,9 @@ \subsection{Same Type}
   the only kind of type which can declare type variables,
   so only a generic function type can be subjected to an alpha conversion.
   For example,
-  \code{List<X>\,\,\FUNCTION<X>({X\,\,arg})}
+  \code{List<X>\,\,\FUNCTION<X>({X})}
   can be turned into
-  \code{List<Y>\,\,\FUNCTION<Y>({Y\,\,arg})}
+  \code{List<Y>\,\,\FUNCTION<Y>({Y})}
   by alpha conversion.%
 }
 

From d3145f2732683f39712eebdde69df3fa1ca9bd70 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:02:26 +0200
Subject: [PATCH 65/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index d6c9d90510..25bbe92737 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23467,7 +23467,7 @@ \subsection{Same Type}
 
 \begin{itemize}
 \item $S$ is \VOID{} and $T$ is \VOID.
-  \commentary{This is a reserved word and cannot be shadowed.}
+  \commentary{This is a reserved word and cannot be redefined.}
 \item $S$ is an identifier or a prefixed identifier which is resolved
   to denote a type-introducing declaration $D_S$,
   and $T$ is an identifier or a prefixed identifier which is resolved

From 7f21129fa77fcdc03852cf508a85450aa8403e1e Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:05:25 +0200
Subject: [PATCH 66/82] WIP

---
 specification/dartLangSpec.tex | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 25bbe92737..a4ab6a461e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23444,6 +23444,11 @@ \subsection{Same Type}
 carries information about the declaration
 that it has been resolved to denote.
 
+\LMHash{}%
+Moreover, it is assumed that
+type inference and instantiation to bound has taken place 
+such that none of the types enountered are raw.
+
 \LMHash{}%
 We need one more mechanism:
 An \Index{alpha conversion} of a type is a consistent, non-capturing renaming

From 4838676c8b2f9ab9a2c1b54dbca71841c8cdf56b Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:16:08 +0200
Subject: [PATCH 67/82] WIP

---
 specification/dartLangSpec.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index a4ab6a461e..934c6646a7 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23483,6 +23483,9 @@ \subsection{Same Type}
   where $C$ and $D$ have been resolved to denote the same declaration,
   or they are both \code{FutureOr},
   and $U_j$ is the same type as $V_j$ for all $j \in 1 .. s$.
+\item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
+  and $S'$ is the same type as $T'$.
+%% TODO(eernst): When records are added, add a record type case here.
 \item $S$ and $T$ are both positional function types with the same
   number of mandatory parameters and the same number of optional parameters,
   the same return type, and the same type for each of the parameters.
@@ -23502,6 +23505,13 @@ \subsection{Same Type}
   $S'$ and $T$ are the same type.
 \end{itemize}
 
+\LMHash{}%
+For the purpose of the above test, \code{Object}, \code{dynamic},
+\code{Null}, \code{Never}, \code{Function},
+%% TODO(eernst): Add \code{Record},
+and \code{Future} are considered to be introduced by a declaration in
+\code{dart:core}.
+
 
 \section{Reference}
 \LMLabel{reference}

From e9eb451d838281231ed3be116148aa4bdedadddd Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:17:52 +0200
Subject: [PATCH 68/82] WIP

---
 specification/dartLangSpec.tex | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 934c6646a7..aea006e341 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23481,7 +23481,6 @@ \subsection{Same Type}
 \item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},
   and $T$ is of the form \code{$D$<$V_1$, \ldots\ $V_s$>},
   where $C$ and $D$ have been resolved to denote the same declaration,
-  or they are both \code{FutureOr},
   and $U_j$ is the same type as $V_j$ for all $j \in 1 .. s$.
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.
@@ -23509,8 +23508,8 @@ \subsection{Same Type}
 For the purpose of the above test, \code{Object}, \code{dynamic},
 \code{Null}, \code{Never}, \code{Function},
 %% TODO(eernst): Add \code{Record},
-and \code{Future} are considered to be introduced by a declaration in
-\code{dart:core}.
+\code{Future}, and \code{FutureOr}
+are considered to be introduced by a declaration in \code{dart:core}.
 
 
 \section{Reference}

From d4905c0af6fea166ebf292c520cbca5cf89b5186 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:19:14 +0200
Subject: [PATCH 69/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index aea006e341..6168a86466 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23478,12 +23478,12 @@ \subsection{Same Type}
   and $T$ is an identifier or a prefixed identifier which is resolved
   to denote a type-introducing declaration $D_T$,
   and $D_S$ is the same declaration as  $D_T$.
+\item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
+  and $S'$ is the same type as $T'$.
 \item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},
   and $T$ is of the form \code{$D$<$V_1$, \ldots\ $V_s$>},
   where $C$ and $D$ have been resolved to denote the same declaration,
   and $U_j$ is the same type as $V_j$ for all $j \in 1 .. s$.
-\item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
-  and $S'$ is the same type as $T'$.
 %% TODO(eernst): When records are added, add a record type case here.
 \item $S$ and $T$ are both positional function types with the same
   number of mandatory parameters and the same number of optional parameters,

From 62c25e0fa1dbc42cdc8734ba3669a37eb377832d Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:20:06 +0200
Subject: [PATCH 70/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 6168a86466..497e3e0c3a 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23474,9 +23474,9 @@ \subsection{Same Type}
 \item $S$ is \VOID{} and $T$ is \VOID.
   \commentary{This is a reserved word and cannot be redefined.}
 \item $S$ is an identifier or a prefixed identifier which is resolved
-  to denote a type-introducing declaration $D_S$,
+  to denote a declaration $D_S$,
   and $T$ is an identifier or a prefixed identifier which is resolved
-  to denote a type-introducing declaration $D_T$,
+  to denote a declaration $D_T$,
   and $D_S$ is the same declaration as  $D_T$.
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.

From 68e02af20e21ec7a9bf8b8dcc94a4fcf4f2f8198 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:23:07 +0200
Subject: [PATCH 71/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 497e3e0c3a..e7de55133e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23505,7 +23505,7 @@ \subsection{Same Type}
 \end{itemize}
 
 \LMHash{}%
-For the purpose of the above test, \code{Object}, \code{dynamic},
+For the purpose of the above ruleset, \code{Object}, \code{dynamic},
 \code{Null}, \code{Never}, \code{Function},
 %% TODO(eernst): Add \code{Record},
 \code{Future}, and \code{FutureOr}

From 102d5619d3384f35b8ad2586ab63affd97a707c5 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:24:21 +0200
Subject: [PATCH 72/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index e7de55133e..f37ac74e6e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23398,7 +23398,7 @@ \subsection{Same Type}
 or upper and lower bounds
 (\ref{standardUpperBoundsAndStandardLowerBounds}),
 because it is concerned with relationships among program elements
-that occur in different binding environments.
+that may occur in different binding environments.
 
 \commentary{%
   The notion of being the same type at run time is different from

From 05bfb2c9e8f15dc91d093f40d4b4606e7c360298 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:30:49 +0200
Subject: [PATCH 73/82] WIP

---
 specification/dartLangSpec.tex | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index f37ac74e6e..fe0df74acb 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23478,6 +23478,10 @@ \subsection{Same Type}
   and $T$ is an identifier or a prefixed identifier which is resolved
   to denote a declaration $D_T$,
   and $D_S$ is the same declaration as  $D_T$.
+  \commentary{%
+    This covers references to classes and other type-introducing declarations,
+    and it also covers type parameters.%
+  }
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.
 \item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},

From 780dddb1bba06016be2cbd7d2e9ebb28c50f4595 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:36:19 +0200
Subject: [PATCH 74/82] WIP

---
 specification/dartLangSpec.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index fe0df74acb..55d098fcd6 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23492,10 +23492,16 @@ \subsection{Same Type}
 \item $S$ and $T$ are both positional function types with the same
   number of mandatory parameters and the same number of optional parameters,
   the same return type, and the same type for each of the parameters.
+  If at least one of the function types is generic
+  then they must both be generic,
+  and they must have textually identical type parameter declaration lists.
 \item $S$ and $T$ are both named function types with the same
   number of mandatory parameters and the same set of named parameters,
   the same return type, and the same type for each of the parameters,
   and the same subset of the named parameters marked as \REQUIRED.
+  If at least one of the function types is generic
+  then they must both be generic,
+  and they must have textually identical type parameter declaration lists.
 \item $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
   denotes a type alias declaration,
   the unfolding of the type alias yields $S'$,
@@ -23506,6 +23512,11 @@ \subsection{Same Type}
   and $S$ is the same type as $T'$.
 \item There exists an alpha conversion of $S$ yielding $S'$, and
   $S'$ and $T$ are the same type.
+  \commentary{%
+    This rule can be used to obtain
+    textually identical type parameter declaration lists,
+    if they only differ in the choice of naming.%
+  }
 \end{itemize}
 
 \LMHash{}%

From 3aec5a6ac5f11fc614accecfeb1db9e37ca9995b Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:43:15 +0200
Subject: [PATCH 75/82] WIP

---
 specification/dartLangSpec.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 55d098fcd6..893b63d56e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23489,19 +23489,19 @@ \subsection{Same Type}
   where $C$ and $D$ have been resolved to denote the same declaration,
   and $U_j$ is the same type as $V_j$ for all $j \in 1 .. s$.
 %% TODO(eernst): When records are added, add a record type case here.
-\item $S$ and $T$ are both positional function types with the same
+\item (1) $S$ and $T$ are both positional function types with the same
   number of mandatory parameters and the same number of optional parameters,
   the same return type, and the same type for each of the parameters.
-  If at least one of the function types is generic
-  then they must both be generic,
-  and they must have textually identical type parameter declaration lists.
-\item $S$ and $T$ are both named function types with the same
+  Otherwise (2), $S$ and $T$ are both named function types with the same
   number of mandatory parameters and the same set of named parameters,
   the same return type, and the same type for each of the parameters,
   and the same subset of the named parameters marked as \REQUIRED.
-  If at least one of the function types is generic
+  %
+  For both (1) and (2), if at least one of the function types is generic
   then they must both be generic,
   and they must have textually identical type parameter declaration lists.
+  With this, the $j$th type parameter declaration from $S$ and from $T$
+  are considered to be the same declaration, for all $j \in 1 .. s$.
 \item $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
   denotes a type alias declaration,
   the unfolding of the type alias yields $S'$,

From 573ff1950b1fa01bed9aa0e1897d52eaeab6f9c5 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:46:22 +0200
Subject: [PATCH 76/82] WIP

---
 specification/dartLangSpec.tex | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 893b63d56e..d80c44b165 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23502,6 +23502,13 @@ \subsection{Same Type}
   and they must have textually identical type parameter declaration lists.
   With this, the $j$th type parameter declaration from $S$ and from $T$
   are considered to be the same declaration, for all $j \in 1 .. s$.
+\item There exists an alpha conversion of $S$ yielding $S'$, and
+  $S'$ and $T$ are the same type.
+  \commentary{%
+    This rule can be used to obtain
+    textually identical type parameter declaration lists,
+    if they only differ in the choice of naming.%
+  }
 \item $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
   denotes a type alias declaration,
   the unfolding of the type alias yields $S'$,
@@ -23510,13 +23517,6 @@ \subsection{Same Type}
   denotes a type alias declaration,
   the unfolding of the type alias yields $T'$,
   and $S$ is the same type as $T'$.
-\item There exists an alpha conversion of $S$ yielding $S'$, and
-  $S'$ and $T$ are the same type.
-  \commentary{%
-    This rule can be used to obtain
-    textually identical type parameter declaration lists,
-    if they only differ in the choice of naming.%
-  }
 \end{itemize}
 
 \LMHash{}%

From e2d031a6f6a266f68746ed69af206cf23b38dc1c Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:47:00 +0200
Subject: [PATCH 77/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index d80c44b165..6276324b2e 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23509,11 +23509,11 @@ \subsection{Same Type}
     textually identical type parameter declaration lists,
     if they only differ in the choice of naming.%
   }
-\item $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
+\item (1) $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
   denotes a type alias declaration,
   the unfolding of the type alias yields $S'$,
   and $S'$ is the same type as $T$.
-\item $T$ is of the form \code{$G$<$V_1$, \ldots\ $V_s$>} where $G$
+  Otherwise (2), $T$ is of the form \code{$G$<$V_1$, \ldots\ $V_s$>} where $G$
   denotes a type alias declaration,
   the unfolding of the type alias yields $T'$,
   and $S$ is the same type as $T'$.

From 01d61d7b68e1bf47609ca517976e67748a08026c Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:47:37 +0200
Subject: [PATCH 78/82] WIP

---
 specification/dartLangSpec.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 6276324b2e..fd552a483f 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23480,7 +23480,7 @@ \subsection{Same Type}
   and $D_S$ is the same declaration as  $D_T$.
   \commentary{%
     This covers references to classes and other type-introducing declarations,
-    and it also covers type parameters.%
+    and it also covers type variables.%
   }
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.

From da845bff86fb09b99a3f4504f645820f1f8b1c31 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:49:17 +0200
Subject: [PATCH 79/82] WIP

---
 specification/dartLangSpec.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index fd552a483f..5bdfdc2638 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23484,6 +23484,8 @@ \subsection{Same Type}
   }
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.
+\item $S$ is of the form \code{$X$\&$U$} and $T$ is of the form \code{$X$\&$V$},
+  and $U$ is the same type as $V$.
 \item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},
   and $T$ is of the form \code{$D$<$V_1$, \ldots\ $V_s$>},
   where $C$ and $D$ have been resolved to denote the same declaration,

From 38d2201b8c7ed565016445356fee828e5cc0c2e8 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:49:49 +0200
Subject: [PATCH 80/82] WIP

---
 specification/dartLangSpec.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 5bdfdc2638..f922f2f24b 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23484,7 +23484,8 @@ \subsection{Same Type}
   }
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.
-\item $S$ is of the form \code{$X$\&$U$} and $T$ is of the form \code{$X$\&$V$},
+\item $S$ is of the form \code{$X$\,\,\&\,\,$U$}
+  and $T$ is of the form \code{$X$\,\,\&\,\,$V$},
   and $U$ is the same type as $V$.
 \item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},
   and $T$ is of the form \code{$D$<$V_1$, \ldots\ $V_s$>},

From 7f310f88f443ce89897fd8c8e458225a94732890 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:50:45 +0200
Subject: [PATCH 81/82] WIP

---
 specification/dartLangSpec.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index f922f2f24b..e1f8f82245 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23484,8 +23484,8 @@ \subsection{Same Type}
   }
 \item $S$ is of the form $S'?$ and $T$ is of the form $T'?$,
   and $S'$ is the same type as $T'$.
-\item $S$ is of the form \code{$X$\,\,\&\,\,$U$}
-  and $T$ is of the form \code{$X$\,\,\&\,\,$V$},
+\item $S$ is of the form \code{$X$\,\&\,$U$}
+  and $T$ is of the form \code{$X$\,\&\,$V$},
   and $U$ is the same type as $V$.
 \item $S$ is of the form \code{$C$<$U_1$, \ldots\ $U_s$>},
   and $T$ is of the form \code{$D$<$V_1$, \ldots\ $V_s$>},

From 69ebb092cc2eefac4b17345c72229d2983009aa8 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Fri, 15 Aug 2025 16:59:19 +0200
Subject: [PATCH 82/82] WIP

---
 specification/dartLangSpec.tex | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index e1f8f82245..73d8e46881 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -23502,15 +23502,16 @@ \subsection{Same Type}
   %
   For both (1) and (2), if at least one of the function types is generic
   then they must both be generic,
-  and they must have textually identical type parameter declaration lists.
-  With this, the $j$th type parameter declaration from $S$ and from $T$
+  and they must have the same names of type parameters in the same order,
+  and with the same types as bounds.
+  When satisfying these requirements,
+  the $j$th type parameter declaration from $S$ and from $T$
   are considered to be the same declaration, for all $j \in 1 .. s$.
 \item There exists an alpha conversion of $S$ yielding $S'$, and
   $S'$ and $T$ are the same type.
   \commentary{%
-    This rule can be used to obtain
-    textually identical type parameter declaration lists,
-    if they only differ in the choice of naming.%
+    This rule can be used to obtain type parameter declaration lists
+    with the same names in the same order, as required in the previous item.%
   }
 \item (1) $S$ is of the form \code{$F$<$U_1$, \ldots\ $U_s$>} where $F$
   denotes a type alias declaration,