From f5cb6da87938c02e23034575fe7f23b7ee52ffc0 Mon Sep 17 00:00:00 2001
From: Erik Ernst <eernst@google.com>
Date: Thu, 6 Jan 2022 18:16:42 +0100
Subject: [PATCH] Interface type and subtype rule fixes

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

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index d372245fa2..29c7fa5635 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -19947,7 +19947,8 @@ \section{Types}
 \LMLabel{types}
 
 \LMHash{}%
-Dart supports optional typing based on interface types.
+Dart supports optional typing based on interface types
+(\ref{interfaceTypes}).
 
 \rationale{%
 The type system is unsound, due to the covariance of generic classes.
@@ -20747,8 +20748,7 @@ \subsection{Subtypes}
       T \in \{\code{Object?}, \DYNAMIC, \VOID\}}{S}{T}
     % ------------------------------------------------ Right Object
     \RuleRaw{\SrnRightObjectFour}{%
-      \mbox{$S$ is an interface type,}\\
-      \mbox{a function type, or \FUNCTION}}{S}{\code{Object}}
+      \mbox{$S$ is an interface type or \FUNCTION}}{S}{\code{Object}}
     % ------------------------------------------------ Left Null 2
     \Rule{\SrnNullTwo}{\code{Null}}{T}{%
       \code{Null}}{\code{FutureOr<$T$>}}
@@ -21123,8 +21123,7 @@ \subsubsection{Informal Subtype Rule Descriptions}
 \Item{\SrnBottom}{Bottom}
   \code{Never} is a subtype of every type.
 \Item{\SrnRightObjectFour}{Right Object}
-  Interface types, function types, and \FUNCTION{}
-  are subtypes of \code{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}
@@ -21312,7 +21311,7 @@ \subsection{Type Nullability}
 \item \code{Never}.
 \item Any function type.
 \item The type \FUNCTION.
-\item Any interface type except \code{Null}.
+\item Any interface type.
 \item \code{FutureOr<$S$>}, for any non-nullable type $S$.
 \item Any type variable $X$ whose bound is non-nullable.
 \item Any type of the form \code{$X$\,\&\,$S$}, where
@@ -22631,15 +22630,13 @@ \subsubsection{The Standard Upper Bound of Distinct Interface Types}
 
 \LMHash{}%
 We define the auxiliary function \NominalTypeDepthName{}
-on interface types and \code{Object?} as follows:
+on interface types as follows:
 
 \begin{itemize}
 \item
-  \DefEquals{\NominalTypeDepth{Object?}}{0}.
-\item
-  \DefEquals{\NominalTypeDepth{Object}}{1}.
-\item
-  \DefEquals{\NominalTypeDepth{Null}}{1}.
+  % We could make it 1 rather than 0, to "reserve space" for `Object?`,
+  % but this function is never used with `Object?` anyway.
+  \DefEquals{\NominalTypeDepth{Object}}{0}.
 \item
   Let $T$ be a class or a mixin,
   and let $M$ be the set of immediate superinterfaces of $T$.
@@ -22648,10 +22645,6 @@ \subsubsection{The Standard Upper Bound of Distinct Interface Types}
   $\metavar{max}\,\{\;\NominalTypeDepth{$S$}\;|\;S\;\in M\;\}$.
 \end{itemize}
 
-\commentary{%
-
-}
-
 \LMHash{}%
 \BlindDefineSymbol{I, J, M}%
 The algorithm that determines
@@ -23040,7 +23033,7 @@ \subsection{Interface Types}
 (\ref{typedef}).
 We say that $T$ is an \Index{interface type} if{}f
 $T'$ is of the form \code{$C$<\List{T}{1}{k}>},
-where $C$ denotes a class different from \code{Never},
+where $C$ denotes a class different from \code{Never} and \code{Null},
 or $C$ denotes a mixin.
 
 \commentary{%
@@ -23048,13 +23041,14 @@ \subsection{Interface Types}
 Non-generic classes are included because we can have $k = 0$.
 
 In particular, the following types are \emph{not} interface types:
-\VOID, \DYNAMIC, \FUNCTION, \code{FutureOr<$T$>} for any $T$, \code{Never},
+\VOID, \DYNAMIC, \FUNCTION, \code{FutureOr<$T$>} for any $T$,
+\code{Never}, \code{Null},
 any function type, any type variable, any intersection type,
 and any type of the form \code{$T$?}.
 
-Conversely, built-in classes
-like \code{Object}, \code{Null}, \code{num}, \code{int},
-\code{String}, and \code{Exception} are interface types,
+Conversely, built-in classes like, e.g.,
+\code{Object}, \code{num}, \code{int}, \code{String}, and \code{Exception}
+are interface types,
 and so are
 \code{Future<$T$>}, \code{Stream<$T$>}, \code{Iterable<$T$>},
 \code{List<$T$>}, \code{Map<$S$,\,\,$T$}, and \code{Set<$T$>},