Constant types; type variable elimination in constants

Author: eernstg

specification/dartLangSpec.tex

@@ -8665,8 +8665,8 @@ \subsection{Constants}
   If generic function instantiation does apply to $e$
   and the provided actual type arguments are \List{T}{1}{s}
   then $e$ is a potentially constant and constant expression
-  if{}f each $T_j, j \in 1 .. s$, is a constant type expression
-  (\ref{constants}).
+  if{}f each $T_j, j \in 1 .. s$, is a constant type
+  (\ref{constantTypes}).
 \item
   An identifier expression denoting a parameter of a constant constructor
   (\ref{constantConstructors})
@@ -8690,7 +8690,8 @@ \subsection{Constants}
   \code{\CONST{} <$T$>[$e_1$, \ldots, $e_n$]}, or
   \code{<$T$>[$e_1$, \ldots, $e_n$]}
   that occurs in a constant context,
-  is a potentially constant expression if $T$ is a constant type expression,
+  is a potentially constant expression if $T$ is a constant type
+  (\ref{constantTypes}),
   and $e_1$, \ldots{} , $e_n$ are constant expressions.
   It is further a constant expression
   if the list literal evaluates to an object.
@@ -8700,7 +8701,8 @@ \subsection{Constants}
   \code{<$T$>\{$e_1$, \ldots, $e_n$\}}
   that occurs in a constant context,
   is a potentially constant expression
-  if $T$ is a constant type expression,
+  if $T$ is a constant type
+  (\ref{constantTypes}),
   and $e_1$, \ldots{} , $e_n$ are constant expressions.
   It is further a constant expression
   if the list literal evaluates to an object.
@@ -8843,7 +8845,8 @@ \subsection{Constants}
 \item
   An expression of the form \code{$e$\,\,\AS\,\,$T$} is potentially constant
   if $e$ is a potentially constant expression
-  and $T$ is a potentially constant type expression,
+  and $T$ is a potentially constant type
+  (\ref{constantTypes}),
   and it is further constant if $e$ is constant.
   \commentary{%
     It is a \Error{compile-time error} to evaluate this constant expression
@@ -8853,18 +8856,57 @@ \subsection{Constants}
 \item
   An expression of the form \code{$e$\,\,\IS\,\,$T$} is potentially constant
   if $e$ is a potentially constant expression
-  and $T$ is a constant type expression,
+  and $T$ is a constant type
+  (\ref{constantTypes}),
   and it is further constant if $e$ is constant.
 \item
   An expression of the form \code{$e$\,\,is!\,\,$T$}
   is equivalent to \code{!($e$\,\,is\,\,$T$)} in every way,
   including whether it's potentially constant or constant.
 \end{itemize}
 
+% Being potentially constant is entirely structural, not type based,
+% but the program still has to satisfy strong-mode typing.
+
+% Constant expressions (like "const Foo(42)") always evaluate to the
+% same value, with at most one value per source location.
+% Potentially constant expressions that are not constant only
+% allow simple operations on basic types (num, String, bool, Null). These can
+% be computed statically without running user code.
+
 \LMHash{}%
-We introduce \Index{constant type expressions} and
-\Index{potentially constant type expressions}
-as follows:
+It is a \Error{compile-time error} if an expression is required to be
+a constant expression,
+but its evaluation would throw an exception.
+It is a \Error{compile-time error} if an assertion is evaluated as part of
+a constant object expression evaluation,
+and the assertion would throw an exception.
+
+\LMHash{}%
+It is a \Error{compile-time error} if the value of a constant expression
+depends on itself.
+
+\commentary{%
+As an example, consider:%
+}
+
+\begin{dartCode}
+\CLASS{} CircularConsts \{
+  // \comment{Illegal program - mutually recursive compile-time constants}
+  \STATIC{} \CONST{} i = j; // \comment{a compile-time constant}
+  \STATIC{} \CONST{} j = i; // \comment{a compile-time constant}
+\}
+\end{dartCode}
+
+
+\subsubsection{Constant Types}
+\LMLabel{constantTypes}
+
+\LMHash{}%
+A \Index{potentially constant type} respectively \Index{constant type}
+is a term derived from \synt{type} which is used as a type
+(\commentary{not as an expression that yields an instance of \code{Type}})
+that satisfy the following criteria:
 \begin{itemize}
 \item
   Consider a type $T$
@@ -8873,70 +8915,105 @@ \subsection{Constants}
   which is not qualified by a deferred prefix,
   and which is optionally followed by
   type arguments of the form \code{<\List{T}{1}{r}>}.
-  $T$ is a potentially constant type expression
-  respectively a constant type expression
-  if{}f $T_j$ is a potentially constant respectively constant type expression
+  $T$ is a potentially constant type respectively a constant type
+  if{}f $T_j$ is a potentially constant respectively constant type
   for each $j \in 1 .. r$.
 \item
   A type of the form \code{FutureOr<$T$>}
-  is a potentially constant type expression
-  respectively a constant type expression
-  if{}f $T$ is a potentially constant type expression
-  respectively a constant type expression.
+  is a potentially constant type
+  respectively a constant type
+  if{}f $T$ is a potentially constant type
+  respectively a constant type.
 \item
   %% TODO(eernst): This does not allow for type variables introduced by
-  %% the type itself. `Function<X>(X)` could be a constant type expression,
+  %% the type itself. `Function<X>(X)` could be a constant type,
   %% but that is not covered by the current rules: `X` is a type variable,
-  %% and they are never constant type expressions.
+  %% and they are never constant type.
   A function type
   \code{$R$ Function<\metavar{typeParameters}>(\metavar{parameterTypes})}
   (where $R$ and \code{<\metavar{typeParameters}>} may be omitted)
-  is a is a potentially constant type expression
-  respectively a constant type expression
+  is a is a potentially constant type
+  respectively a constant type
   if $R$, \metavar{typeParameters}, and \metavar{parameterTypes}
-  (if present) contain only potentially constant type expressions
-  respectively constant type expressions.
+  (if present) contain only potentially constant types
+  respectively constant types.
 \item
-  The type \VOID{} is a potentially constant and a constant type expression.
+  The type \VOID{} is a potentially constant and constant type.
 \item
-  The type \DYNAMIC{} is a potentially constant and a constant type expression.
+  The type \DYNAMIC{} is a potentially constant and constant type.
 \item
-  A type variable is a potentially constant type expression.
+  A type variable is a potentially constant type.
 \end{itemize}
 
-% Being potentially constant is entirely structural, not type based,
-% but the program still has to satisfy strong-mode typing.
 
-% Constant expressions (like "const Foo(42)") always evaluate to the
-% same value, with at most one value per source location.
-% Potentially constant expressions that are not constant only
-% allow simple operations on basic types (num, String, bool, Null). These can
-% be computed statically without running user code.
+\subsubsection{Type Variable Elimination in Constants}
+\LMLabel{typeVariableEliminationInConstants}
 
 \LMHash{}%
-It is a \Error{compile-time error} if an expression is required to be
-a constant expression,
-but its evaluation would throw an exception.
-It is a \Error{compile-time error} if an assertion is evaluated as part of
-a constant object expression evaluation,
-and the assertion would throw an exception.
+\BlindDefineSymbol{e, e'}%
+Let $e$ be an expression that occurs in a constant context
+or whose first token is \CONST,
+and $e'$ be the expression yielded by type inference
+(\ref{typeInference})
+applied to $e$.
+In this case an additional transformation is applied:
 
 \LMHash{}%
-It is a \Error{compile-time error} if the value of a constant expression
-depends on itself.
+Let \List{X}{1}{r} be the free type variables declared by
+a class, mixin, extension, or method that contains $e$,
+such that for each $j \in 1 .. r$, each $X_j$
+occurs in a list of actual type arguments
+which was added by type inference
+(\commentary{%
+so $X_j$ has one or more occurrences in $e'$,
+but not all of those occurrences exist in $e$%
+}).
+For each $j \in 1 .. r$,
+if a specific occurrence of $X_j$ in $e'$ was added by type inference,
+the outermost enclosing type argument which was added by type inference
+and which contains this occurrence
+is replaced by its least closure with respect to \List{X}{1}{r}
+(\ref{leastAndGreatestClosureOfTypes}).
 
 \commentary{%
-As an example, consider:%
+Note that a free type variable which is explicitly used
+as or in a type argument in a constant expression
+is still a compile-time error.
+For example:%
 }
 
 \begin{dartCode}
-\CLASS{} CircularConsts \{
-  // \comment{Illegal program - mutually recursive compile-time constants}
-  \STATIC{} \CONST{} i = j; // \comment{a compile-time constant}
-  \STATIC{} \CONST{} j = i; // \comment{a compile-time constant}
+\CLASS\ G<X> \{
+  \VOID\ foo() \{
+    \CONST\ List<X> c = <X>[]; // \comment{Compile-time error.}
+    \CONST\ List<X> d = []; // \comment{Infers \code{<X>[]}, then becomes \code{<Never>[]}.}
+  \}
 \}
 \end{dartCode}
 
+\rationale{%
+The type variable is not a constant type
+(\ref{constantTypes}),
+which implies that the inferred expression $e'$ is a compile-time error.
+The additional transformation yields a subtype of the inferred type.
+It typically replaces the type variable by \code{Never},
+but it may also replace the type variable by a top type
+(if the type variable occurs contravariantly),
+or the type may be changed more radically
+(e.g., a generic function type using $X_j$ as a type parameter bound
+may be changed to \FUNCTION{} or \code{Never}).
+In any case, the chosen subtype often yields
+a constant which has no errors and is useful.%
+}
+
+\commentary{%
+For example, \code{\CONST\,\,<Never>[]} is actually usable as
+a list of any type,
+and it is not a problem that every invocation of \code{add}
+on this list will fail (statically or dynamically),
+because that is already true for every constant list.%
+}
+
 
 \subsubsection{Further Remarks on Constants and Potential Constants}
 \LMLabel{furtherCommentsOnConstantsAndPotentiallyConstants}
@@ -10697,8 +10774,8 @@ \subsubsection{Lists}
 if an element of a constant list literal is not constant.
 It is a \Error{compile-time error} if the type argument of a constant list literal
 (\commentary{no matter whether it is explicit or inferred})
-is not a constant type expression
-(\ref{constants}).
+is not a constant type
+(\ref{constantTypes}).
 
 \rationale{%
 The binding of a formal type parameter of an enclosing class or function
@@ -11510,8 +11587,8 @@ \subsubsection{Sets}
 (\ref{equality}).
 It is a \Error{compile-time error} if the type argument of a constant set literal
 (\commentary{no matter whether it is explicit or inferred})
-is not a constant type expression
-(\ref{constants}).
+is not a constant type
+(\ref{constantTypes}).
 
 \rationale{%
 The binding of a formal type parameter of an enclosing class or function
@@ -11715,8 +11792,8 @@ \subsubsection{Maps}
 (\ref{equality}).
 It is a \Error{compile-time error} if a type argument of a constant map literal
 (\commentary{no matter whether it is explicit or inferred})
-is not a constant type expression
-(\ref{constants}).
+is not a constant type
+(\ref{constantTypes}).
 
 \rationale{%
 The binding of a formal type parameter of an enclosing class or function
@@ -12466,7 +12543,7 @@ \subsubsection{Const}
 \LMHash{}%
 If $T$ is a parameterized type,
 it is a
-\Error{compile-time error} if $U_j$ is not a constant type expression for any
+\Error{compile-time error} if $U_j$ is not a constant type for any
 $j \in 1 .. m$.
 
 \begin{itemize}
@@ -24993,28 +25070,11 @@ \section{Null safety} %% !!!TODO!!!
 %% !!!At the end: Search Null, change to Never where appropriate
 %% !!!Search all `TODO`.*null
 
-\subsubsection{Const type variable elimination}
-\LMLabel{}
-
-If performing inference on a constant value of a generic class results in
-inferred type arguments to the generic class which contain free type variables
-from an enclosing generic class or method, the free type variables shall be
-eliminated by taking the least closure of the inferred type with respect to the
-free type variables.  Note that free type variables which are explicitly used as
-type arguments in constant generic instances are still considered erroneous.
-
-\begin{dartCode}
-\CLASS\ G<T> \{
-  \VOID\ foo() \{
-    \CONST\ List<T> c = <T>[]; // Error
-    \CONST\ List<T> d = []; // The list literal is inferred as <Never>[]
-  \}
-\}
-\end{dartCode}
-
 \subsubsection{Null promotion}
 \LMLabel{}
 
+!!!
+
 The machinery of type promotion is extended to promote the type of
 variables based on nullability checks subject to the same set of
 restrictions as normal promotion.  The relevant checks and the types