Batched small updates

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

@@ -6,6 +6,11 @@ Status: Draft
 
 ## CHANGELOG
 
+2020..06.02
+  - Fix the diff to the spec for potentially constant instance checks
+  - Specify that extensions do not apply to values of type `Never`
+  - Specify the treatment of typedefs from legacy libraries
+
 2020.05.20
   - Turn new references to `CastError` into being dynamic type errors.
 
@@ -702,9 +707,13 @@ class G<T> {
 
 For the purposes of extension method resolution, there is no special treatment
 of nullable types with respect to what members are considered accessible.  That
-is, the only members of a nullable tyhpe that are considered accessible
+is, the only members of a nullable type that are considered accessible
 (and hence which take precedence over extensions) are the members on `Object`.
 
+For the purposes of extension method resolution, the type `Never` is considered
+to implement all members, and hence no extension may apply to an expression of
+type `Never`.
+
 ### Assignability
 
 The definition of assignability is changed as follows.
@@ -756,7 +765,8 @@ We change the following specification text:
 to
 
 ```
-\item An expression of the form \code{$e$\,\,as\,\,$T$} is potentially constant
+\item An expression of the form \code{$e$\,\,as\,\,$T$} or
+  \code{$e$\,\,is\,\,$T$} is potentially constant
   if $e$ is a potentially constant expression
   and $T$ is a potentially constant type expression,
   and it is further constant if $e$ is constant.
@@ -1215,6 +1225,31 @@ all occurrences of `S*` in `T` shall be replaced with `S`.  As a result, legacy
 types will never appear as type annotations in opted-in libraries, nor will they
 appear in reified positions.
 
+### Typedefs defined in legacy libraries used in opted-in libraries
+
+A typedef which is define in a legacy library and used in an opted-in library is
+treated as defining a function type, all of the components of which are
+legacy. The function type itself is treated as non-nullable (and not legacy) at
+the top level.  Hence given the following program, it is an error to assign a
+nullable value to a variable of type `F` in an opted-in library, but any
+function which is compatible with a legacy function of type `int*
+Function(int*)` may be assigned to such a variable.
+
+```dart
+// Opted-out library "opted_out.dart".
+typedef F = int Function(int);
+
+// Opted-in library "main.dart"
+import "opted_out.dart";
+
+int? f1(int x) => x;
+
+void test() {
+    F f = null; // Static error
+    f = f1;  // No error
+}
+```
+
 ### Exports
 
 If a legacy library re-exports an opted-in library, the re-exported symbols

resources/type-system/flow-analysis.md

@@ -9,7 +9,10 @@ https://docs.google.com/document/d/11Xs0b4bzH6DwDlcJMUcbx4BpvEKGz8MVuJWEfo_mirE/
 
 ## CHANGELOG
 
-2019.01.16
+2020.06.02
+  - Specify the interaction between downwards inference and promotion/demotion.
+
+2020.01.16
   - Modify `restrictV` to make a variable definitely assigned in a try block or
     a finally block definitely assigned after the block.
   - Clarify that initialization promotion does not apply to formal parameters.
@@ -432,36 +435,17 @@ Definitions:
   - Else if `T` is `FutureOr<R>` and `R <: S` then `factor(Future<R>, S)`
   - Else `T`
 
-Questions:
- - The interaction between assignment based **promotion** and downwards inference is
-   probably managable.  I think doing downwards inference using the current
-   type, and then promoting the variable afterwards is fine for all reasonable
-   cases.
- - The interaction between assignment based **demotion** and downwards inference is
-   a bit trickier.  In so far as it is manageable, I think it would need to be
-   done as follows, given `x = E` where `x` has current type `S`.
-     - Infer `E` in context `S`
-     - if the inferred type of `E` is `T` and `S <: T` and the demotion policy
-     applies, then instead of treating this as `x = (E as S)` (or an error),
-     then instead treat `x` as promoted to `S` in the scope of the assigment.
-
-   - if a variable is tested before it is initialized, we must choose whether to
-    honor the type test or the assignment.  Above I've chosen to prefer type
-    test based promotion.  Examples:
-    ```
-      test1() {
-        var x;
-        if (x is num) {
-           x = 3; // not an initializing promotion, since it's already promoted
-        }
-      }
-      test2() {
-        var x;
-        if (x is String) {
-           x = 3; // not an initializing promotion, nor an assignment promotion
-        }
-      }
-     ```
+#### Interactions between downwards inference and promotion
+
+Given an assignment (or composite assignment) `x = E` where `x` has current type
+`S` (possibly the result of promotion), inference and promotion interact as
+follows.
+  - Inference for `E` is done as usual, using `S` as the downwards typing
+    context.  All reference to `x` within `E` are treated as having type `S` as
+    usual.
+  - Let `T` be the resulting inferred type of `E`.
+  - The assignment is treated as an assignment of an expression of type `T` to a
+    variable of type `S`, with the usual promotion, demotion and errors applied.
 
 ## Flow analysis
 

resources/type-system/inference.md

@@ -6,6 +6,10 @@ Status: Draft
 
 ## CHANGELOG
 
+2020.06.02
+  - Account for the special treatment of bottom types during function literal
+  inference.
+
 2020.05.27
   - Update function literal return type inference to use
     **futureValueTypeSchema**.
@@ -217,10 +221,17 @@ Inference for each returned expression in the body of the function literal is
 done in an empty typing context (see below).
 
 Function literals which are inferred in an non-empty typing context where the
-context type is a function type are inferred as follows.  Each parameter is
-assumed to have its declared type if present, or the type taken from the
-corresponding parameter (if any) from the typing context if not present.  The
-return type of the context function type is used at several points during
+context type is a function type are inferred as described below.
+
+Each parameter is assumed to have its declared type if present.  If no type is
+declared for a parameter and there is a corresponding parameter in the context
+type schema with type schema `K`, the parameter is given an inferred type `T`
+where `T` is derived from `K` as follows.  If the greatest closure of `K` is `S`
+and `S` is a subtype of `Null`, then `T` is `Object?`.  Otherwise, `T` is `S`.
+If there is no corresponding parameter in the context type schema, the variable
+is treated as having type `dynamic`.
+
+The return type of the context function type is used at several points during
 inference.  We refer to this type as the **imposed return type
 schema**. Inference for each returned or yielded expression in the body of the
 function literal is done using a context type derived from the imposed return