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..a9a9d0600bd47a95d5507f1c01b8a3dde466904e 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`,

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

In my quixotic quest to abolish "it" (which you can ignore because it doesn't
affect correctness), consider rewording to:

Note that using a value of type `void` is not technically dangerous; doing so
does not violate any language semantics contraints.

I'm still concerned because values do not have the type void, so maybe:

Note that using the value of an expression of type `void` is not technically
dangerous; ...

[eernst, 2017/09/01 07:49:45]

Done.

+doing so does not violate any constraints at the level of the language
+semantics.  By using the type `void`, developers just indicate that the

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

Drop "just". It's a word that carries a lot of insinuation, and it rarely makes
anything more precise.

[eernst, 2017/09/01 07:49:45]

Done.

+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

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

values of type `void` -> values of expression of type `void`

[eernst, 2017/09/01 07:49:45]

Done.

 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
@@ -165,43 +166,38 @@ 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 evaluated as an expression). It is therefore not necessary to

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

The function type cannot actually be evaluated as an expression, but it can be
used as a type argument and the corresponding type variable used as an
expression.

[eernst, 2017/09/01 07:49:45]

Right, or it could be defined in a non-parameterized typedef `F` which could be
evaluated as an expression.

Adjusted the text to focus on the type variable example that you gave.

+have a reified representation of such a return type.*

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

A reified representation of such a return type is therefore not necessary.

(Maybe).

[eernst, 2017/09/01 07:49:45]

Done. There goes another `it`. ;-)

+
+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

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

void -> `void`
?

[eernst, 2017/09/01 07:49:45]

I actually have 21 occurrences of '`void`' and 64 occurrences of
'[^`]\bvoid\b[^`]', 10-or-so of which are part of a source code snippet. So
there are significantly more usages of a plain 'void' than '`void`' (hence, this
one isn't a lone typo).

The approach I've tried to maintain is that '`void`' is used when the context
definitely requires that the token `void` occurs in the source code (or when it
refers to a hypothetical example situation where it might as well occur, in
order to keep the example simple), and otherwise a plain non-source 'void' is
used. In particular, it is important to allow for the "semantic void" rather
than the "syntactic void" in cases where we argue that it is a non-problem that
we don't reify void, because the justification should work for "semantic void",
not just syntactic.

I've kept all the occurrences of the plain 'void' for now.

+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.*

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

This is a specification, so is it or is it not reified?
What does mirrors do?

(IOW, don't let this stand by itself, complete it by saying ", and it isn't.")

[eernst, 2017/09/01 07:49:45]

All this commentary stuff is a follow-up on 'There is no value which is the
reified representation of the type void at
run time.' in line 159, so in that sense it's clear. Still added 'and it isn't',
though.

 
 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 +211,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 +249,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 +276,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
@@ -292,7 +306,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

[Lasse Reichstein Nielsen, 2017/08/30 05:29:51]

values of type void -> values with static type void

(the values doesn't have the type void, but it might be the only statically know
type for the value)
Alternatively: values -> expressions.

[eernst, 2017/09/01 07:49:45]

Done.

-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 +316,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 +326,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 +340,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.