Specify that a void return type doesn't cause errors in checked mode.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification  \\
@@ skipping 6435 matching lines @@
 
 \LMHash{}
 Let $T$ be the static type of $e$ and let $f$ be the immediately enclosing function.
 
 \LMHash{}
 It is a static type warning if the body of $f$ is marked \ASYNC{} and the type \code{Future<flatten(T)>} (\ref{functionExpressions}) may not be assigned to the declared return type of $f$.    Otherwise, it is a static type warning if $T$ may not be assigned to the declared return type of $f$.
 
 \LMHash{}
 Let $S$ be the runtime type of $o$. In checked mode:
 \begin{itemize}
-\item  If the body of $f$ is marked \ASYNC{} (\ref{functions}) it is a dynamic type error if $o$ is not \NULL{} (\ref{null}) and \code{Future<flatten(S)>} is not a subtype of the actual return type  (\ref{actualTypeOfADeclaration}) of $f$.
-\item Otherwise, it is a dynamic type error if $o$ is not \NULL{} and the runtime type of $o$ is not a subtype of the actual return type of $f$.
+\item  If the body of $f$ is marked \ASYNC{} (\ref{functions})
+it is a dynamic type error if $o$ is not \NULL{} (\ref{null}),
+the actual return type (\ref{actualTypeOfADeclaration}) of $f$ is not \VOID,

[eernst, 2017/05/10 14:38:48]

At this point we have assumed that (the body of) $f$ is marked \ASYNC{}, in
which case it is a static warning if the declared return type of $f$ is not a
supertype of Future<T> for some T, which would be the case if it's \VOID.

So this is a very special case exemplified by declarations like `void f(..)
async { return e; }`, incurring a static warning but still runnable. We plan to
make `return e;` in a void function a compile-time error, so this will need to
be adjusted again very soon.

Maybe add a comment like "%% TODO: Remove this line when we make `return e;` in
a void function a compile-time error."

[Lasse Reichstein Nielsen, 2017/05/11 06:09:59]

The change to make `return e;` an error, not just a warning, in a void function,
is something I don't expect to happen until Dart 2.0.
It's a breaking change with not real advantage in Dart 1, but in Dart 2, we will
generally make warnings into errors, so that would be the "right time" for this
change too.
I don't plan to add "TODO"s for everything we'll do in Dart 2.0, but I guess a
comment can't hurt.

It's true that a `void foo(a) async => bar(await a.baz());` would cause a
warning for now because Future<whatever bar returns> isn't assignable to `void`
(it's not a supertype requirement, just assignability). We haven't changed
assignability wrt. void, we've just changed this rule to avoid the runtime error
that can happen in well-typed programs.
Maybe it's not necessary to allow this case, I just thought it would be
consistent.

[eernst, 2017/05/11 09:56:13]

I recommended the comment because I suspect that it will be non-obvious 
when adding the rule that "`return e;` is an error in a void function"
that this particular situation will no longer occur, so the line should be
deleted. I agree that we shouldn't presage all of 2.0 with TODOs, but we
might help ourselves getting it right if we note tricky corners like this
one (`void foo(a) async ..` is weird).
Right.
I think it is consistent to let arbitrary values pass that `void` return type
test.  Weird and wrong code, of course, but we shouldn't add an exception to
the common rules to that.

+and \code{Future<flatten(S)>} is not a subtype of the actual return type of $f$.
+\item Otherwise, it is a dynamic type error if $o$ is not \NULL{},
+the actual return type of $f$ is not \VOID{},
+and the runtime type of $o$ is not a subtype of the actual return type of $f$.
 \end{itemize}
 
 \LMHash{}
 It is a compile-time error if a return statement of the form \code{\RETURN{} $e$;} appears in a generative constructor (\ref{generativeConstructors}).
 
 \rationale{
 It is quite easy to forget to add the factory prefix for a constructor, accidentally converting a factory into a generative constructor. The static checker may detect a type mismatch in some, but not all, of these cases. The rule above helps catch such errors, which can otherwise be very hard to recognize. There is no real downside to it, as returning a value from a generative constructor is meaningless.
 }
 
 \LMHash{}
@@ skipping 1681 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------