Adjusted spec of For-In to insist on Iterable

specification/dartLangSpec.tex

@@ -24,7 +24,9 @@
 
 % CHANGES
 % =======
+%
 % Significant changes to the specification.
+%
 % 2.2
 % - Specify whether the values of literal expressions override Object.==.
 % - Allow Type objects as case expressions and const map keys.
@@ -36,6 +38,8 @@
 %   Function.
 % - Generalize specification of type aliases such that they can denote any
 %   type, not just function types.
+% - Added requirement that the iterator of a for-in statement must have
+%   type `Iterator`.
 %
 % 2.1
 % - Remove 64-bit constraint on integer literals compiled to JavaScript numbers.
@@ -12287,24 +12291,33 @@ \subsubsection{For-in}
 \LMLabel{for-in}
 
 \LMHash{}%
-Let $D$ be derived from \syntax{<finalConstVarOrType>?}
-and let $n0$ be an identifier that does not occur anywhere in the program.
-A for statement of the form \code{\FOR{} ($D$ \id{} \IN{} $e$) $s$} is equivalent to the following code:
+Let $D$ be derived from \syntax{<finalConstVarOrType>?}.
+A for statement of the form \code{\FOR{} ($D$ \id{} \IN{} $e$)\,\,$S$}
+is then treated as the following code,
+where $\id_1$ and $\id_2$ are fresh identifiers:
 
 \begin{normativeDartCode}
-\VAR{} $n0$ = $e$.iterator;
-\WHILE{} ($n0$.moveNext()) \{
-\ \ $D$ \id{} = $n0$.current;
-\ \ $s$
+$T$ $\id_1$ = $e$;
+\VAR{} $\id_2$ = $id_1$.iterator;
+\WHILE{} ($\id_2$.moveNext()) \{
+\ \ $D$ \id{} = $\id_2$.current;
+\ \ $S$
 \}
 \end{normativeDartCode}
 
-For purposes of static typechecking,
-this code is checked under the assumption that $n0$ is declared to be of type $T$,
-where $T$ is the static type of \code{$e$.iterator}.
-
-\commentary{
-It follows that it is a compile-time error if $D$ is empty and \id{} is a final variable.
+\noindent
+If the static type of $e$ is a top type
+(\ref{superBoundedTypes})
+then $T$ is \code{Iterable<dynamic>},
+otherwise $T$ is the static type of $e$.
+It is a compile-time error if $T$ is not assignable to \code{Iterable<dynamic>}.
+
+\commentary{
+It follows that it is a compile-time error
+if $D$ is empty and \id{} is a final variable;
+and it is a dynamic error if $e$ has a top type,
+but $e$ evaluates to an instance of a type
+which is not a subtype of \code{Iterable<dynamic>}.
 }