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..23c45af326395fcac00133b8517d383eb91e78fc 100644
--- a/docs/language/informal/generalized-void.md
+++ b/docs/language/informal/generalized-void.md
@@ -30,28 +30,30 @@ 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 using the value of an expression of type `void` is not
+technically dangerous, doing so does not violate any constraints at the
+level of the language semantics.  By using the type `void`, developers
+indicate that the value of the corresponding expression evaluation is
+meaningless. 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 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.
+The mechanisms helping developers to avoid using the value of an expression
+of type `void` are divided into **two phases**. This document specifies the
+first phase.
 
 The **first phase** uses restrictions which are based on syntactic criteria
-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.
+in order to ensure that direct usage of the value of an expression 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 for every expression
+of type `void`, its value must be ignored.
 
 The **second phase** will deal with casts and preservation of
 voidness. Some casts will cause derived expressions to switch from having
@@ -62,7 +64,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
@@ -165,43 +167,39 @@ that formal type parameter can be the type void. That case is specified
 explicitly below. Apart from the reserved word `void` and a formal type
 parameter, no other term can denote the type void.*
 
-*Conversely, `void` cannot denote any other entity than the type void:
-`void` cannot occur as the declared name of any declaration (including
-library prefixes, types, variables, parameters, etc.). This implies that
-`void` is not subject to scoped lookup, and the name is not exported by any
-system library. Similarly, it can never be accessed using a prefixed
-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`.
-
-*It is encouraged for an implementation to use a reified representation for
-`void` as a type argument and as a parameter type in a function type which
-is not `identical` to the reified representation of the built-in class
-`Object`, but they must be equal. This allows implementations to produce
-better diagnostic messages, e.g., in case of a runtime error.*
+*There is no way for a Dart program at run time to obtain a reified
+representation of a return type or parameter type of a function type, even
+when the function type as a whole may be obtained (e.g., the function type
+could be passed as a type argument and the corresponding formal type
+parameter could be evaluated as an expression). A reified representation of
+such a return type is therefore not necessary.*
+
+For a composite type (a generic class instantiation or a function type),
+the reified representation at run time must be such that the type void and
+the built-in class `Object` are treated as equal according to `==`, but
+they need not be `identical`.
+
+*For example, with `typedef F<S, T> = S Function(T)`, the `Type` instance
+for `F<Object, void>` at run time is `==` to the one for `F<void, void>`
+and for `F<void, Object>`.*
+
+*In case of a dynamic error, implementations are encouraged to emit an
+error message that includes information about such parts of types being
+`void` rather than `Object`. Developers will then see types which are
+similar to the source code declarations. This may be achieved using
+distinct `Type` objects to represent types such as `F<void, void>` and
+`F<Object, void>`, comparing equal using `==` but not `identical`.*
 
 *This treatment of the reified representation of the type void reinforces
 the understanding that "voidness" is merely a statically known flag on the
-built-in class `Object`, it is not a separate type. However, for backward
-compatibility we need to treat return types differently.*
-
-When `void` is specified as the return type of a function, the reified
-representation of the return type is left unspecified.
-
-*There is no way for a Dart program at run time to obtain a reified
-representation of that return type alone, even when the function type as a
-whole may be obtained (e.g., the function type could be evaluated as an
-expression). It is therefore not necessary to reified representation of
-such a return type.*
+built-in class `Object`. However, for backward compatibility we need to
+treat return types differently in Dart 1.x.*
 
 *It may be possible to use a reflective subsystem (mirrors) to deconstruct
 a function type whose return type is the type void, but the existing design
 of the system library `dart:mirrors` already handles this case by allowing
-for a type mirror that does not have a reflected type.*
+for a type mirror that does not have a reflected type. All in all, the type
+void does not need to be reified at run time, and it is not reified.*
 
 Consider a type _T_ where the type void occurs as an actual type argument
 to a generic class, or as a parameter type in a function type. Dynamically,
@@ -215,16 +213,18 @@ need to specify the the typing relations for generic function types. In
 Dart 2, the subtype relationship for generic function types follows from
 the rule that `void` is treated as `Object`.*
 
-Consider a function type _T_ where the return type is the type void. The
-dynamic more-specific-than relation, `<<`, and the dynamic subtype
-relation, `<:`, are determined by the existing rules in the language
-specification, supplemented by the above rule for handling occurrences of
-the type void other than as a return type.
+Consider a function type _T_ where the return type is the type void. In
+Dart 1.x, the dynamic more-specific-than relation, `<<`, and the dynamic
+subtype relation, `<:`, are determined by the existing rules in the
+language specification, supplemented by the above rule for handling
+occurrences of the type void other than as a return type. In Dart 2 there
+is no exception for return types: the type void is treated as being the
+built-in class `Object`.
 
 *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(...)`,
@@ -251,20 +251,22 @@ class `Object`, or `dynamic`.
 
 For the static analysis, the more-specific-than relation, `<<`, and the
 subtype relation, `<:`, are determined by the same rules as described above
-for the dynamic semantics.
+for the dynamic semantics, for both Dart 1.x and Dart 2.
 
 *That is, the type void is considered to be equivalent to the built-in
-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,14 +278,28 @@ 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 a meaningless value", 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
 `Object`.
 
+In Dart 2, it is a compile-time error when a method declaration _D2_ with
+return type void overrides a method declaration _D1_ whose return type is
+not void.
+
+*This rule is a special case of voidness preservation, which is needed in
+order to maintain the discipline which arises naturally from the function
+type subtype rules in Dart 1.x concerning void as a return type.*
+
 ## Discussion
 
 Expressions derived from typeCast and typeTest do not support `void` as the
@@ -291,8 +307,9 @@ target type. We have omitted support for this situation because we consider
 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.
+`Object` plus a "static voidness flag"), but the value of expressions of
+type void should be 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 +318,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 +328,13 @@ bound as `Object`.
 
 ## Updates
 
-*   August 16h 2017: Removed exceptions allowing `e is T` and `e is! T`.
+*   August 22nd 2017: Reworded specification of reified types to deal with
+    only such values which may be obtained at run time (previously mentioned
+    some entities which may not exist). Added one override rule.
+
+*   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 +342,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.