Add null-safety specification of super-bounded types

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

@@ -6,6 +6,9 @@ Status: Draft
 
 ## CHANGELOG
 
+2020.09.10
+  - Specify updates to super-bounded type rules for null safety.
+
 2020.08.12
   - Specify constraints on the `main` function.
 
@@ -15,7 +18,7 @@ Status: Draft
 
 2020.07.09
   - Specify combined member signature and spread element typing
-    with null-safety.
+    with null safety.
 
 2020.06.02
   - Fix the diff to the spec for potentially constant instance checks
@@ -802,11 +805,32 @@ the element, key, and value type of `...e` and `...?e` is `Never`.
 *When the static type _S_ of `e` is strictly non-nullable, such as when _S_
 is `Never`, `...?e` is a warning, but it may still occur.*
 
-### Instantiate to bounds
+### Instantiation to bound
 
-The computation of instantiation to bounds is changed to substitute `Never` for
+The computation of instantiation to bound is changed to substitute `Never` for
 type variables appearing in contravariant positions instead of `Null`.
 
+### Super-bounded types
+
+Null safety requires three changes to the section 'Super-Bounded Types' in
+the language specification.
+
+The definition of a top type is changed: _T_ is a top type if and only if
+`Object?` is a subtype of _T_. Note that the helper predicate **TOP**
+provides a syntactic characterization of the same concept.
+
+The definition of a super-bounded type is changed such that occurrences of
+`Null` are replaced by types involving `Never`, and `Object` is replaced by
+`Object?`. Moreover, top types in invariant positions and in positions that
+have no variance (*unused type parameters in a type alias*) are given the
+same treatment as top types in covariant positions. This causes one
+sentence to change, with the following result:
+
+Let _T'_ be the result of replacing every occurrence in _T_ of a type _S_
+in a contravariant position where _S <: Never_ by `Object?`, and every
+occurrence in _T_ of a top type in a position which is not contravariant by
+`Never`.
+
 ### Least and greatest closure
 
 The definitions of least and greatest closure are changed in null safe libraries
@@ -1001,6 +1025,87 @@ These are extended as
 per
 [separate proposal](https://github.com/dart-lang/language/blob/master/resources/type-system/flow-analysis.md).
 
+## Helper predicates
+
+The following helper predicates are used to classify types. They are syntactic
+in nature such that termination is obvious. In particular, they do not rely on
+subtyping.
+
+The **TOP** predicate is true for any type which is in the equivalence class of
+top types.
+
+- **TOP**(`T?`) is true iff **TOP**(`T`) or **OBJECT**(`T`)
+- **TOP**(`T*`) is true iff **TOP**(`T`) or **OBJECT**(`T`)
+- **TOP**(`dynamic`) is true
+- **TOP**(`void`) is true
+- **TOP**(`FutureOr<T>`) is **TOP**(T)
+- **TOP**(T) is false otherwise
+
+**TOP**(`T`) is true if and only if `T` is a supertype of `Object?`.
+
+The **OBJECT** predicate is true for any type which is in the equivalence class
+of `Object`.
+
+- **OBJECT**(`Object`) is true
+- **OBJECT**(`FutureOr<T>`) is **OBJECT**(T)
+- **OBJECT**(`T`) is false otherwise
+
+**OBJECT**(`T`) is true if and only if `T` is a subtype and a supertype of
+`Object`.
+
+The **BOTTOM** predicate is true for things in the equivalence class of `Never`.
+
+- **BOTTOM**(`Never`) is true
+- **BOTTOM**(`X&T`) is true iff **BOTTOM**(`T`)
+- **BOTTOM**(`X extends T`) is true iff **BOTTOM**(`T`)
+- **BOTTOM**(`T`) is false otherwise
+
+**BOTTOM**(`T`) is true if and only if `T` is a subtype of `Never`.
+
+The **NULL** predicate is true for things in the equivalence class of `Null`
+
+- **NULL**(`Null`) is true
+- **NULL**(`T?`) is true iff **NULL**(`T`) or **BOTTOM**(`T`)
+- **NULL**(`T*`) is true iff **NULL**(`T`) or **BOTTOM**(`T`)
+- **NULL**(`T`) is false otherwise
+
+**NULL**(`T`) is true if and only if `T` is a subtype and a supertype of `Null`.
+
+The **MORETOP** predicate defines a total order on top and `Object` types.
+
+- **MORETOP**(`void`, `T`) = true
+- **MORETOP**(`T`, `void`) = false
+- **MORETOP**(`dynamic`, `T`) = true
+- **MORETOP**(`T`, `dynamic`) = false
+- **MORETOP**(`Object`, `T`) = true
+- **MORETOP**(`T`, `Object`) = false
+- **MORETOP**(`T*`, `S*`) = **MORETOP**(`T`, `S`)
+- **MORETOP**(`T`, `S*`) = true
+- **MORETOP**(`T*`, `S`) = false
+- **MORETOP**(`T?`, `S?`) = **MORETOP**(`T`, `S`)
+- **MORETOP**(`T`, `S?`) = true
+- **MORETOP**(`T?`, `S`) = false
+- **MORETOP**(`FutureOr<T>`, `FutureOr<S>`) = **MORETOP**(T, S)
+
+The **MOREBOTTOM** predicate defines an (almost) total order on bottom and
+`Null` types.  This does not currently consistently order two different type
+variables with the same bound.
+
+- **MOREBOTTOM**(`Never`, `T`) = true
+- **MOREBOTTOM**(`T`, `Never`) = false
+- **MOREBOTTOM**(`Null`, `T`) = true
+- **MOREBOTTOM**(`T`, `Null`) = false
+- **MOREBOTTOM**(`T?`, `S?`) = **MOREBOTTOM**(`T`, `S`)
+- **MOREBOTTOM**(`T`, `S?`) = true
+- **MOREBOTTOM**(`T?`, `S`) = false
+- **MOREBOTTOM**(`T*`, `S*`) = **MOREBOTTOM**(`T`, `S`)
+- **MOREBOTTOM**(`T`, `S*`) = true
+- **MOREBOTTOM**(`T*`, `S`) = false
+- **MOREBOTTOM**(`X&T`, `Y&S`) = **MOREBOTTOM**(`T`, `S`)
+- **MOREBOTTOM**(`X&T`, `S`) = true
+- **MOREBOTTOM**(`S`, `X&T`) = false
+- **MOREBOTTOM**(`X extends T`, `Y extends S`) = **MOREBOTTOM**(`T`, `S`)
+
 ### The main function
 
 The section 'Scripts' in the language specification is replaced by the

resources/type-system/upper-lower-bounds.md

@@ -4,6 +4,9 @@ leafp@google.com
 
 ## CHANGELOG
 
+2020.08.13
+  - Move helper predicates to the null safety specification.
+
 2020.07.21
   - **CHANGE** Specify treatment of mixed hierarchies.
 
@@ -14,7 +17,7 @@ This documents the currently implemented upper and lower bound computation,
 modified to account for explicit nullability and the accompanying type system
 changes (including the legacy types).  In the interest of backwards
 compatibility, it does not try to fix the various issues with the existing
-algorithm.  
+algorithm.
 
 ## Types
 
@@ -36,72 +39,15 @@ We assume that type aliases have been expanded, and that all types are named
 
 ## Helper predicates
 
-The **TOP** predicate is true for any type which is in the equivalence class of
-top types.
-
-- **TOP**(`T?`) is true iff **TOP**(`T`) or **OBJECT**(`T`)
-- **TOP**(`T*`) is true iff **TOP**(`T`) or **OBJECT**(`T`)
-- **TOP**(`dynamic`) is true
-- **TOP**(`void`) is true
-- **TOP**(`FutureOr<T>`) is **TOP**(T)
-- **TOP**(T) is false otherwise
-
-The **OBJECT** predicate is true for any type which is in the equivalence class
-of `Object`.
-
-- **OBJECT**(`Object`) is true
-- **OBJECT**(`FutureOr<T>`) is **OBJECT**(T)
-- **OBJECT**(T) is false otherwise
-
-The **BOTTOM** predicate is true for things in the equivalence class of `Never`.
-
-- **BOTTOM**(`Never`) is true
-- **BOTTOM**(`X&T`) is true iff **BOTTOM**(`T`)
-- **BOTTOM**(`X extends T`) is true iff **BOTTOM**(`T`)
-- **BOTTOM**(`T`) is false otherwise
-
-The **NULL** predicate is true for things in the equivalence class of `Null`
-
-- **NULL**(`Null`) is true
-- **NULL**(`T?`) is true iff **NULL**(`T`) or **BOTTOM**(`T`)
-- **NULL**(`T*`) is true iff **NULL**(`T`) or **BOTTOM**(`T`)
-- **NULL**(`T`) is false otherwise
-
-The **MORETOP** predicate defines a total order on top and `Object` types.
-
-- **MORETOP**(`void`, `T`) = true
-- **MORETOP**(`T`, `void`) = false
-- **MORETOP**(`dynamic`, `T`) = true
-- **MORETOP**(`T`, `dynamic`) = false
-- **MORETOP**(`Object`, `T`) = true
-- **MORETOP**(`T`, `Object`) = false
-- **MORETOP**(`T*`, `S*`) = **MORETOP**(`T`, `S`)
-- **MORETOP**(`T`, `S*`) = true
-- **MORETOP**(`T*`, `S`) = false
-- **MORETOP**(`T?`, `S?`) = **MORETOP**(`T`, `S`)
-- **MORETOP**(`T`, `S?`) = true
-- **MORETOP**(`T?`, `S`) = false
-- **MORETOP**(`FutureOr<T>`, `FutureOr<S>`) = **MORETOP**(T, S)
-
-The **MOREBOTTOM** predicate defines an (almost) total order on bottom and
-`Null` types.  This does not currently consistently order two different type
-variables with the same bound.
-
-- **MOREBOTTOM**(`Never`, `T`) = true
-- **MOREBOTTOM**(`T`, `Never`) = false
-- **MOREBOTTOM**(`Null`, `T`) = true
-- **MOREBOTTOM**(`T`, `Null`) = false
-- **MOREBOTTOM**(`T?`, `S?`) = **MOREBOTTOM**(`T`, `S`)
-- **MOREBOTTOM**(`T`, `S?`) = true
-- **MOREBOTTOM**(`T?`, `S`) = false
-- **MOREBOTTOM**(`T*`, `S*`) = **MOREBOTTOM**(`T`, `S`)
-- **MOREBOTTOM**(`T`, `S*`) = true
-- **MOREBOTTOM**(`T*`, `S`) = false
-- **MOREBOTTOM**(`X&T`, `Y&S`) = **MOREBOTTOM**(`T`, `S`)
-- **MOREBOTTOM**(`X&T`, `S`) = true
-- **MOREBOTTOM**(`S`, `X&T`) = false
-- **MOREBOTTOM**(`X extends T`, `Y extends S`) = **MOREBOTTOM**(`T`, `S`)
-
+This document relies on several type classification helper predicates
+which are specified in the
+[null safety specification](https://github.com/dart-lang/language/blob/master/accepted/future-releases/nnbd/feature-specification.md):
+**TOP**, which is true for all top types;
+**OBJECT**, which is true for types equivalent to `Object`;
+**BOTTOM**, which is true for types equivalent to `Never`;
+**NULL**, which is true for types equivalent to `Null`;
+**MORETOP**, which is a total order on top and `Object` types; and
+**MOREBOTTOM**, which is an (almost) total order on bottom and `Null` types.
 
 ## Upper bounds
 
@@ -420,7 +366,7 @@ that are not identical are `T0` and `S0` respectively, and **MORETOP**(`T0`,
 `S0`).
 
 A similar treatment would need to be done for the bottom types as well, since
-there are two equivalences there. 
+there are two equivalences there.
   - `X extends T` is equivalent to `Null` if `T` is equivalent to `Null`.
   - `FutureOr<Null>` is equivalent `Future<Null>`.