Update on top of #941: Some review responses got lost, and flatten(S) must be changed in some locations (#948)

Correct `flatten{S}` to `T_v` in several locations. Update commentary to match changes to return rules. Perform smaller corrections based on review of #941.

Author: eernstg

accepted/future-releases/nnbd/feature-specification.md

@@ -11,7 +11,7 @@ Status: Draft
     static rules for return statements, and dynamic semantics of return in
     asynchronous non-generators.
   - Add rule that the use of expressions of type `void*` is restricted in
-    the same way as expressions of type `void`.
+    the same way as the use of expressions of type `void`.
 
 2020.04.30
   - Specify static analysis of `e1 == e2`.
@@ -292,7 +292,8 @@ The function **futureValueType** is defined as follows:
 
 _Note that it is a compile-time error unless the return type of an asynchronous
 non-generator function is a supertype of `Future<Never>`, which means that
-the last case will only be applied when `S` is a non-`void` top type._
+the last case will only be applied when `S` is `Object` or a non-`void` top
+type._
 
 ### Return statements
 
@@ -306,46 +307,54 @@ about synchronous non-generator functions, the text is changed as follows:
 ```
 It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
 $T$ is neither \VOID{} nor \DYNAMIC,
-and $S$ is \VOID{} or \code{\VOID*}.
+and $S$ is \VOID.
 ```
 
 _Comparing to Dart before null-safety, this means that it is no longer allowed
-to "return void to null" in a regular function._
+to return a void expression in a regular function if the return type is
+`Null`._
 
-At [this location](https://github.com/dart-lang/language/blob/65b8267be0ebb9b3f0849e2061e6132021a4827d/specification/dartLangSpec.tex#L15525)
+At [this location](https://github.com/dart-lang/language/blob/65b8267be0ebb9b3f0849e2061e6132021a4827d/specification/dartLangSpec.tex#L15507)
 about an asynchronous non-generator function with future value type `$T_v$`,
 the text is changed as follows:
 
 ```
+It is a compile-time error if $s$ is \code{\RETURN{};},
+unless $T_v$
+is \VOID, \DYNAMIC, or \code{Null}.
+%
+It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
+$T_v$ is \VOID,
+and \flatten{S} is neither \VOID, \DYNAMIC, \code{Null}.
+%
 It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
 $T_v$ is neither \VOID{} nor \DYNAMIC,
-and \flatten{S} is \VOID{} or \code{\VOID*}.
-```
-
-_Comparing to Dart before null-safety, this means that it is no longer allowed
-to "return void to null" in an `async` function, nor to "return a void future
-to null"._
-
-The next sentence is changed as follows:
-
-```
+and \flatten{S} is \VOID.
+%
 It is a compile-time error if $s$ is \code{\RETURN{} $e$;},
 \flatten{S} is not \VOID,
 $S$ is not assignable to $T_v$,
 and flatten{S} is not a subtype of $T_v$.
 ```
 
-_Comparing to Dart before null-safety, this means that it is now allowed
-to return a future when the future value type is a suitable future; for
-instance, we can have `return Future<int>.value(42)` in an `async` function
-with declared return type `Future<Future<int>>`. Conversely, it is no longer
-allowed to return a `Future<dynamic>` or `FutureOr<dynamic>` when the future
-value type is `Future<U>` for some `U` which is not a top type._
+_Comparing to Dart before null-safety, this means that it is no longer allowed
+to return an expression whose flattened static type is `void` in an `async`
+function with future value type `Null`; nor is it allowed, in an `async`
+function with future value type `void`, to return an expression whose flattened
+static type is not `void`, `void*`, `dynamic`, or `Null`. Conversely, it is
+allowed to return a future when the future value type is a suitable future;
+for instance, we can have `return Future<int>.value(42)` in an `async` function
+with declared return type `Future<Future<int>>`. Finally, let `S` be
+`Future<dynamic>` or `FutureOr<dynamic>`; it is then no longer allowed to
+return an expression with static type `S`, unless the future value type is a
+supertype of `S`. This differs from Dart before null-safety in that it was
+allowed to return an expression of these types with a declared return type
+of the form `Future<T>` for any `T`._
 
 The dynamic semantics specified at
 [this location](https://github.com/dart-lang/language/blob/65b8267be0ebb9b3f0849e2061e6132021a4827d/specification/dartLangSpec.tex#L15597)
 is changed as follows, where `$f$` is the enclosing function with declared
-return type `$T$`, and `$e$` is the returned expression with static type `$S$`:
+return type `$T$`, and `$e$` is the returned expression:
 
 ```
 When $f$ is a synchronous non-generator, evaluation proceeds as follows: