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

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index f643ef1b4c525783671578723d7bb4eb0c3ac4ee..1eaea8d53273d6c51c9846bee0892f629d82e920 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -6453,8 +6453,13 @@ It is a static type warning if the body of $f$ is marked \ASYNC{} and the type \
 \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{}