Bounds of a generic type alias ensure the body is regular-bounded

The analyzer enforces the rule that when a generic type alias F has
formal type parameters X1..Xm with bounds B1..Bm, if we assume that
X1..Xm are types satisfying the corresponding bounds then it must be
the case that every type which occurs in the body of F must be
regular-bounded.

In other words, the bounds on the left hand side of `=` must imply
the bounds applicable to every type on the right hand side.

---------- NEW TEXT ----------

I just discovered that it is _not_ possible to skip the check on
every super-bounded parameterized type based on a generic type
alias: It is certainly possible to have a type which is correctly
super-bounded according to the type parameter bounds on the left
hand side of `=` in the type alias declaration, and still have a
right hand side where some types are not well-bounded. Consider the
following declarations:

  class B<Y1 extends Y2, Y2, Y3 extends num> {}
  typedef F<X extends num> = B<num, Object, X> Function();

According to the declarations to the left of `=`, `F<Object>`
is a correct super-bounded type, because it is not
regular-bounded (`Object <\: num`), and `F<Null>` is regular-bounded
(`Null <: num`).

Also, when the declared bound of `X` is satisfied, we are
guaranteed that each type on the right hand side is regular-bounded
(if parameterized, it receives type arguments that satisfy all
the specified bounds).

But consider the result of applying `F` to `Object`:

  B<num, Object, Object> Function();

That's not a type where all subterms which are types are
well-bounded:

  B<num, Object, Object> is not regular-bounded because
  `Object <\: num` (third type argument).

  B<num, Object, Object> is not super-bounded because
  B<num, Null, Null> is not regular-bounded because
  `num <\: Null` (violating `Y1 extends Y2`).

So there is no way we can prove that this check can be skipped,
because we have a pretty simple counter-example!

I'm currently adjusting the text to re-introduce the check.

---------- OLD TEXT, NOT VALID ----------

This must be specified, because it justifies the _removal_ of a
requirement that we had in the feature specification
super-bounded-types.md: It was required for every application of a
generic type alias F to a list of actual type arguments <T1..Tk>
such that the resulting parameterized type F<T1..Tk> was
super-bounded that both the parameterized type F<T1..Tk> and every
type in the resulting type [T1/X1..Tk/Xk]U (where U is the body of
F and X1..Xk are its formal type parameters) be well-bounded.

But when the bounds of F imply satisfaction of the bounds of all
types that occur in the body of F, it's trivially true that all
types in the resulting type are regular-bounded for the result
of substituting Null for covariant top types and Object for
contravariant Null for every super-bounded F<T1..Tk>. I'm looking
into a proof sketch for the result that this implies that any
well-bounded generic type alias application yields a type that
contains only well-bounded types.

This would be a very welcome simplification (because it was an
inconvenient complication that we had to check both the left hand
side and the right hand side of a type alias whenever we
encountered a super-bounded type expressed via a type alias), and
I believe that it will also make the tools run faster (because they
can now skip all those checks of every type that occurs in the body
for every super-bounded usage of a type alias.

Change-Id: Icd70649ebaed41b193aeb0cb6f08d06aed0ee5bd
Reviewed-on: https://dart-review.googlesource.com/c/79743
Reviewed-by: Leaf Petersen <leafp@google.com>
Reviewed-by: Lasse R.H. Nielsen <lrn@google.com>

docs/language/dartLangSpec.tex

@@ -63,6 +63,10 @@
 % - Eliminate all references to checked and production mode, Dart 2 does
 %   not have modes.
 % - Integrate feature specification on noSuchMethod forwarders.
+% - Specify that bound satisfaction in generic type alias type parameters
+%   must imply bound satisfaction everywhere in the body.
+% - Specify that super-bounded generic type alias applications must trigger
+%   a well-boundedness check on all types occurring in the denoted type.
 %
 % 2.0
 % - Don't allow functions as assert test values.
@@ -3538,11 +3542,6 @@ \section{Generics}
 It is a compile-time error if $T$ is not well-bounded
 (\ref{superBoundedTypes}).
 
-\commentary{
-That is, if the number of type arguments is wrong,
-or one or more of the upper bounds has been violated.
-}
-
 \LMHash{}
 Otherwise, said parameterized type \code{C<$T_1, \ldots,\ T_m$>} denotes an application of the generic class declared by $G$ to the type arguments $T_1, \ldots, T_m$.
 This yields a class $C'$ whose members are equivalent to those of a class declaration which is obtained from the declaration of $G$ by replacing each occurrence of $X_j$ by $T_j$.
@@ -3553,22 +3552,35 @@ \section{Generics}
 }
 
 \LMHash{}
-A {\em generic type alias} introduces a mapping from actual type argument lists to types.
-Consider a generic type alias declaration $G$ named \code{F} with formal type parameter declarations
+A {\em generic type alias}
+introduces a mapping from actual type argument lists to types.
+Consider a generic type alias declaration $G$ named \code{F}
+with formal type parameter declarations
 $X_1\ \EXTENDS\ B_1, \ldots,\ X_m\ \EXTENDS\ B_m$,
-and right hand side $T$,
-and the parameterized type $S$ of the form \code{F<$T_1, \ldots,\ T_l$>}.
+%% TODO(eernst): 'right hand side' works only for a type alias using `=`.
+%% Explain what "the right hand side" means for an old-style declaration.
+and right hand side $T$.
 
 \LMHash{}
-It is a compile-time error if $m \not= l$.
-It is a compile-time error if $S$ is not well-bounded
-(\ref{superBoundedTypes}).
+Under the assumption that $X_1,\ \ldots,\ X_m$ are types such that
+$X_j <: B_j$, for all $j \in 1 .. m$,
+it is a compile-time error if any type in $T$ is not regular-bounded.
 
 \commentary{
-That is, if the number of type arguments is wrong,
-or one or more of the upper bounds has been violated.
+This means that the bounds declared for
+the formal type parameters of a generic type alias
+must be such that when they are satisfied,
+the bounds that pertain to any type in the body must also be satisfied.
 }
 
+\LMHash{}
+Let $G$, \code{F}, and $X_1,\ \ldots,\ X_m$ be as defined above,
+let $T_1,\ \ldots,\ T_l$ be types,
+and let $S$ be the parameterized type \code{F<$T_1, \ldots,\ T_l$>}.
+It is a compile-time error if $m \not= l$.
+It is a compile-time error if $S$ is not well-bounded
+(\ref{superBoundedTypes}).
+
 \LMHash{}
 Otherwise, said parameterized type
 \code{F<$T_1, \ldots,\ T_m$>}
@@ -3577,10 +3589,38 @@ \section{Generics}
 This yields the type
 $[T_1/X_1, \ldots, T_m/X_m]T$.
 
+\rationale{
+The requirement that satisfaction of the bounds on
+the formal type parameters of a generic type alias $G$
+must imply satisfaction of all bounds pertaining to
+every type that occurs in the body of $G$
+limits the expressive power of generic type aliases.
+However, it would require the constraints on formal type parameters
+to be expressed in a much more powerful language
+if we were to allow a significantly larger set of types
+to be expressed using a generic type alias.
+}
+
 \commentary{
-A generic type alias does not correspond to any entities at run time,
-it is only an alias for an existing type.
-Hence, we may consider it as syntactic sugar which is eliminated before the program runs.
+For example, consider the following code:
+}
+
+\begin{dartCode}
+\CLASS{} A<X \EXTENDS{} \VOID{} \FUNCTION(num)> \{\}
+\TYPEDEF{} F<Y> = A<\VOID{} \FUNCTION(Y)> \FUNCTION(); // \comment{compile-time error}
+\end{dartCode}
+
+\commentary{
+There is no way to specify a bound on \code{Y} in the declaration of \code{F}
+which will ensure that all bounds on the right hand side are respected.
+This is because the actual requirement is that \code{Y} must be
+a \emph{supertype} of \code{num},
+but Dart does not support lower bounds for type parameters.
+The type \code{A<\VOID{} \FUNCTION(U)> \FUNCTION()}
+can still be specified explicitly
+for every \code{U} which satisfies the bounds declared by \code{A}.
+So the types can be expressed,
+they just cannot be abbreviated using a generic type alias.
 }
 
 \LMHash{}
@@ -3768,13 +3808,13 @@ \subsection{Variance}
   for some $j \in 1 .. n$.
 
 \item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
-  where $G$ denotes a parameterized type alias such that
+  where $G$ denotes a generic type alias such that
   $j \in 1 .. n$,
   the formal type parameter corresponding to $S_j$ is covariant,
   and $S$ occurs in a covariant position in $S_j$.
 
 \item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
-  where $G$ denotes a parameterized type alias such that
+  where $G$ denotes a generic type alias such that
   $j \in 1 .. n$,
   the formal type parameter corresponding to $S_j$ is contravariant,
   and $S$ occurs in a contravariant position in $S_j$.
@@ -3816,13 +3856,13 @@ \subsection{Variance}
   for some $j \in 1 .. n$.
 
 \item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
-  where $G$ denotes a parameterized type alias such that
+  where $G$ denotes a generic type alias such that
   $j \in 1 .. n$,
   the formal type parameter corresponding to $S_j$ is covariant,
   and $S$ occurs in a contravariant position in $S_j$.
 
 \item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
-  where $G$ denotes a parameterized type alias such that
+  where $G$ denotes a generic type alias such that
   $j \in 1 .. n$,
   the formal type parameter corresponding to $S_j$ is contravariant,
   and $S$ occurs in a covariant position in $S_j$.
@@ -3834,7 +3874,7 @@ \subsection{Variance}
 
 \begin{itemize}
 \item $T$ is of the form \code{$G$<$S_1,\ \ldots,\ S_n$>}
-  where $G$ denotes a generic class or a parameterized type alias,
+  where $G$ denotes a generic class or a generic type alias,
   and $S$ occurs in an invariant position in $S_j$ for some $j \in 1 .. n$.
 
 \item $T$ is of the form
@@ -3860,7 +3900,7 @@ \subsection{Variance}
   for some $i \in 1 .. m$.
 
 \item $T$ is of the form \code{$G$<$S_1, \ldots,\ S_n$>}
-  where $G$ denotes a parameterized type alias,
+  where $G$ denotes a generic type alias,
   $j \in 1 .. n$,
   the formal type parameter corresponding to $S_j$ is invariant,
   and $S$ occurs in $S_j$.
@@ -3919,9 +3959,16 @@ \subsection{Super-Bounded Types}
 
 \LMHash{}
 Every type which is not a parameterized type is {\em regular-bounded}.
+
+\commentary{
+In particular, every non-generic class and every function type
+is a regular-bounded type.
+}
+
+\LMHash{}
 Let $T$ be a parameterized type of the form
 \code{$G$<$S_1, \ldots,\ S_n$>}
-where $G$ denotes a generic class or a parameterized type alias.
+where $G$ denotes a generic class or a generic type alias.
 Let
 \code{$X_1\ \EXTENDS\ B_1, \ldots,\ X_n\ \EXTENDS\ B_n$}
 be the formal type parameter declarations of $G$.
@@ -3931,14 +3978,14 @@ \subsection{Super-Bounded Types}
 for all $j \in 1 .. n$.
 
 \commentary{
-This means that each actual type argument satisfies the declared upper
-bound for the corresponding formal type parameter.
+This means that regular-bounded types are those types
+that do not violate their type parameter bounds.
 }
 
 \LMHash{}
 Let $T$ be a parameterized type of the form
 \code{$G$<$S_1, \ldots,\ S_n$>}
-where $G$ denotes a generic class or a parameterized type alias.
+where $G$ denotes a generic class or a generic type alias.
 $T$ is {\em super-bounded} if{}f the following conditions are both true:
 
 \begin{itemize}
@@ -3953,6 +4000,11 @@ \subsection{Super-Bounded Types}
   It is then required that
   \code{$G$<$S'_1, \ldots,\ S'_n$>}
   is regular-bounded.
+  %
+  Moreover, if $G$ denotes a generic type alias with body $U$,
+  it is required that every type that occurs as a subterm of
+  $[S_1/X_1, \ldots,\ S_n/X_n]U$
+  is well-bounded (defined below).
 \end{itemize}
 
 \commentary{
@@ -3979,7 +4031,7 @@ \subsection{Super-Bounded Types}
 \item $T$ is an immediate subterm of a redirecting factory constructor
   signature
  (\ref{redirectingFactoryConstructors}).
-\item $T$ is an immediate subterm of an \EXTENDS{} clause
+\item $T$ is an immediate subterm of an \EXTENDS{} clause of a class
   (\ref{superclasses}),
   or it occurs as an element in the type list of an \IMPLEMENTS{} clause
   (\ref{superinterfaces}),
@@ -4017,6 +4069,9 @@ \subsection{Super-Bounded Types}
 \rationale{
 Super-bounded types enable the expression of informative common supertypes
 of some sets of types whose common supertypes would otherwise be much less informative.
+}
+
+\commentary{
 For example, consider the following class:
 }
 
@@ -4026,7 +4081,7 @@ \subsection{Super-Bounded Types}
 \}
 \end{dartCode}
 
-\rationale{
+\commentary{
 Without super-bounded types,
 there is no type $T$ which makes \code{C<$T$>} a common supertype of
 all types of the form \code{C<$S$>}
@@ -4037,12 +4092,14 @@ \subsection{Super-Bounded Types}
 as its type annotation,
 which means that a member like \code{next} is not known to exist
 (which is what we mean by saying that the type is `less informative').
+}
 
+\rationale{
 We could introduce a notion of recursive (infinite) types, and express
 the least upper bound of all types of the form \code{C<$S$>} as
 some syntax whose meaning could be approximated by
 \code{C<C<C<C<$\ldots$>$\!$>$\!$>$\!$>}.
-
+%
 However, we expect that any such concept in Dart would incur a significant cost
 on developers and implementations in terms of added complexity and subtlety,
 so we have chosen not to do that.
@@ -4063,7 +4120,7 @@ \subsection{Super-Bounded Types}
 If \code{c} has type \code{C<C<\DYNAMIC>{}>}
 then \code{c.next.next} has type \DYNAMIC{}
 and \code{c.next.next.whatever} has no compile-time error,
-but if \code{c} has type \code{C<C<\VOID>{}>} then
+but if \code{c} has type \code{C<C<\VOID>{}>} then already
 \code{Object x = c.next.next;} is a compile-time error.
 It is thus possible for developers to get a more or less strict treatment
 of expressions whose type proceeds beyond the given finite unfolding.

docs/language/informal/super-bounded-types.md

@@ -2,10 +2,14 @@
 
 **Author**: eernst@.
 
-**Version**: 0.7 (2018-06-01).
+**Version**: 0.8 (2018-10-16).
 
 **Status**: Background material.
 The language specification has the normative text on this topic.
+Note that the rules have changed, which means that
+**this document cannot be used as a reference**, it can only be
+used to get an overview of the ideas; please refer to the language
+specification for all technical details.
 
 **This document** is an informal specification of the support in Dart 2 for
 using certain generic types where the declared bounds are violated. The
@@ -31,9 +35,9 @@ void foo<X extends List<num>>(X x) {
   ...
 }
 ```
-cannot be invoked with `foo<List<dynamic>>('Hello!')`, nor can the type
+cannot be invoked with `foo<List<dynamic>>([])`, nor can the type
 argument be inferred to `List<dynamic>` in an invocation like
-`foo('Hello!')`. But `C<void> x = new C<int>();` is OK, and so is
+`foo([])`. But `C<void> x = new C<int>();` is OK, and so is
 `x is C<Object>`.
 
 
@@ -194,9 +198,11 @@ a `C<S>` (where `S` can be anything), but we could also pass it where a
 
 Finally, if we choose to use `C<void>` and so on then we will not even be
 able to access the object where the type information ends: we cannot use
-the value of an expression like `c0.next` at all without an explicit
-cast. This means that we cannot pass `c0.next` as an argument to a function
-that accepts a `C<S>` (for any `S`) without an explicit cast.
+the value of an expression like `c0.next` without an explicit
+cast (OK, `void v = c0.next;` is accepted, but it is mostly impossible to
+use the value of an expression of type `void`). This means that we cannot
+pass `c0.next` as an argument to a function that accepts a `C<S>`
+(for any `S`) without an explicit cast.
 
 In summary, the choice of `dynamic`, `Object`, and `void` offers a range of
 approaches to the lack of typing information, but the amount of information
@@ -581,6 +587,9 @@ class types like `C<C<dynamic>>` that we have already argued are useful.
 
 ## Updates
 
+*   Version 0.8 (2018-10-16), emphasized that this document is no longer
+    specifying the current rules, it is for background info only.
+
 *   Version 0.7 (2018-06-01), marked as background material: The normative
     text on variance and on super-bounded types is now part of the language
     specification.