Generalized void informal spec clarified in several locations.

docs/language/informal/generalized-void.md

Index: docs/language/informal/generalized-void.md
diff --git a/docs/language/informal/generalized-void.md b/docs/language/informal/generalized-void.md
index e18caa5b2494adcf347893b4f46cbcaaca66ab5c..3b816358bcf558641bc59d41c101a3c251727d2a 100644
--- a/docs/language/informal/generalized-void.md
+++ b/docs/language/informal/generalized-void.md
@@ -30,18 +30,19 @@ covariantly. For instance, the class `Future<T>` uses return types
 like `Future<T>` and `Stream<T>`, and it uses `T` as a parameter type of a
 callback in the method `then`.
 
-Note that is not technically dangerous to use a value of type `void`, it
-does not violate any constraints at the level of the language semantics.
-Developers just made the decision to declare that the value is useless,
-based on the program logic. Hence, there is **no requirement** for the
-generalized void mechanism to be strict and **sound**. However, it is the
-intention that the mechanism should be sufficiently strict to make the
-mechanism helpful and non-frustrating in practice.
+Note that it is not technically dangerous to use a value of type `void`,
+doing so does not violate any constraints at the level of the language
+semantics.  By using the type `void`, developers just indicate that the
+value of the corresponding expression evaluation is useless. Hence, there

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Maybe: "useless and unspecified"

[eernst, 2017/08/22 09:09:46]

Adjusted to 'meaningless'.

+is **no requirement** for the generalized void mechanism to be strict and
+**sound**. However, it is the intention that the mechanism should be
+sufficiently sound to make the mechanism helpful and non-frustrating in
+practice.
 
 No constraints are imposed on which values may be given type `void`, so in
 that sense `void` can be considered to be just another name for the type
-`Object`, flagged as useless. Note that this is an approximate rule (in
-Dart 1.x), it fails to hold for function types.
+`Object`, flagged as useless. Note that this is an approximate rule in
+Dart 1.x, it fails to hold for function types; it does hold in Dart 2.
 
 The mechanisms helping developers to avoid using values of type `void` are
 divided into **two phases**. This document specifies the first phase.
@@ -51,7 +52,7 @@ in order to ensure that direct usage of a value of type `void` is a static
 warning (in Dart 2: an error). A few exceptions are allowed, e.g., type
 casts, such that developers can explicitly make the choice to use such a
 value. The general rule is that all values of type `void` must be
-discarded.
+ignored.
 
 The **second phase** will deal with casts and preservation of
 voidness. Some casts will cause derived expressions to switch from having
@@ -62,7 +63,7 @@ example:
 ```dart
 class A<T> { T foo(); }
 A<Object> a = new A<void>(); // Violates voidness preservation.
-var x = a.foo(); // Use a "void value", with static type Object.
+var x = a.foo(); // Use a "void value", now with static type Object.
 ```
 
 We intend to introduce a **voidness preservation analysis** (which is
@@ -174,9 +175,9 @@ expression (`p.void`). Hence, `void` has a fixed meaning everywhere in all
 Dart programs, and it can only occur as a stand-alone word.*
 
 When `void` is passed as an actual type argument to a generic class or a
-generic function, and when the type void occurs as a parameter type in a
-function type, the reified representation is equal (according to `==`) to
-the reified representation of the built-in class `Object`.
+generic function invocation, and when the type void occurs as a parameter
+type in a function type, the reified representation is equal (according to

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Consider: equal -> equivalent
We use "equivalent" below.

[Lasse Reichstein Nielsen, 2017/08/22 05:31:07]

What does it mean to "occur as a parameter type" in a function type? I'd say
"Function(void)", but there is nothing reified about that one, so I'm not sure
what this is saying.

[eernst, 2017/08/22 09:09:46]

Done.

+`==`) to the reified representation of the built-in class `Object`.
 
 *It is encouraged for an implementation to use a reified representation for

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Wording, consider: "An implementation is encouraged to .."
(Shorter and more direct, I'm trying to avoid using "it" too much myself :).

 `void` as a type argument and as a parameter type in a function type which
@@ -224,7 +225,7 @@ the type void other than as a return type.
 *This ensures backward compatibility for the cases where the type void can
 be used already today. It follows that it will be a breaking change to
 switch to a ruleset where the type void even as a return type is treated
-like the built-in class Object, i.e. when switching to Dart 2.0. However,
+like the built-in class Object, i.e. when switching to Dart 2. However,
 the only situation where the semantics differs is as follows: Consider a
 situation where a value of type `void Function(...)` is assigned to a
 variable or parameter `x` whose type annotation is `Object Function(...)`,
@@ -254,17 +255,19 @@ subtype relation, `<:`, are determined by the same rules as described above
 for the dynamic semantics.
 
 *That is, the type void is considered to be equivalent to the built-in

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Here we use "equivalent".

-class `Object`, except when used as a return type, in which case it is
-effectively considered to be a proper supertype of `Object`. As mentioned,
-voidness preservation is a separate analysis which is not specified by this
-document, but it is intended to be used in the future to track "voidness"
-in types and flag implicit casts wherein information about voidness may
-indirectly be lost. With voidness preservation in place, we expect to be
-able to treat the type void as `Object` in all cases during subtype
-checks.*
-
-It is a static warning for an expression to have type void, except for the
-following situations:
+class `Object` in Dart 1.x, except when used as a return type, in which
+case it is effectively considered to be a proper supertype of `Object`. In
+Dart 2 subtyping, the type void is consistently considered to be equivalent
+to the built-in class `Object`. As mentioned, this document does not
+specify voidness preservation; however, when voidness preservation checks
+are added we get an effect in Dart 2 which is similar to the special
+treatment of void as a return type in Dart 1.x: The function type downcast
+which will be rejected in Dart 1.x (at run time, with a static warning at
+compile time) will become a voidness preservation violation, i.e., a
+compile-time error.*
+
+It is a static warning for an expression to have type void (in Dart 2: a
+compile-time error), except for the following situations:
 
 *   In an expressionStatement `e;`, e may have type void.
 *   In the initialization and increment expressions of a for-loop,
@@ -276,9 +279,15 @@ following situations:
 
 *Note that the parenthesized expression itself has type void, so it is
 again subject to the same constraints. Also note that we may not allow
-return statements returning an expression of type void in the future, but
+return statements returning an expression of type void in Dart 2, but
 it is allowed here for backward compatibility.*
 
+*The value yielded by an expression of type void must be discarded (and
+hence ignored), except when explicitly subjected to a type cast. This
+"makes it hard to use useless values", but leaves a small escape hatch open
+for the cases where the developer knows that the typing misrepresents the
+actual situation.*
+
 During bounds checking, it is possible that a bound of a formal type
 parameter of a generic class or function is statically known to be the type
 void. In this case, the bound is considered to be the built-in class
@@ -292,7 +301,8 @@ it to be useless. If void is passed indirectly via a type variable `T` then
 `e as T`, `e is T`, and `e is! T` will treat `T` like `Object`. In general,
 the rationale is that the type void admits all values (because it is just
 `Object` plus a "static voidness flag"), but values of type void should be
-discarded.
+discarded. So there is no point in *obtaining* the type void for a given
+expression which already has a different type.
 
 The treatment of bounds is delicate. We syntactically prohibit `void` as a
 bound of a formal type parameter of a generic class or function. It is
@@ -301,8 +311,8 @@ class, and that type argument might in turn be used as the bound of another
 formal type parameter of the class, or of a generic function in the
 class. It would be possible to make it a compile-time error to pass `void`
 as a type argument to a generic class where it will be used as a bound, but
-this would presumably require a transitive traversal of all generic classes
-and functions where the corresponding formal type parameter is passed on to
+this would require a transitive traversal of all generic classes and
+functions where the corresponding formal type parameter is passed on to
 other generic classes or functions, which would be highly brittle: A tiny
 change to a generic class or function could break code far away. So we do
 not wish to prevent formal type parameter bounds from indirectly becoming
@@ -311,7 +321,9 @@ bound as `Object`.
 
 ## Updates
 
-*   August 16h 2017: Removed exceptions allowing `e is T` and `e is! T`.
+*   August 17th 2017: Several parts clarified.
+
+*   August 16th 2017: Removed exceptions allowing `e is T` and `e is! T`.
 
 *   August 9th 2017: Transferred to SDK repo, docs/language/informal.
 
@@ -319,9 +331,9 @@ bound as `Object`.
 
 *   June 13th 2017: Compile-time error for using a void value was changed to
     static warning.
-*   June 12th 2017: Grammar changed extensively, to use
-    `typeNotVoid` rather than
-    `voidOrType`.
-*   June 5th 2017: Added `typeCast` and
-    `typeTest` to the locations where void
-    expressions may occur.
+
+*   June 12th 2017: Grammar changed extensively, to use `typeNotVoid`
+    rather than `voidOrType`.
+
+*   June 5th 2017: Added `typeCast` and `typeTest` to the locations where
+    void expressions may occur.