[patterns] Handle nullable types and other patterns in exhaustiveness.

- Specify that nullable and FutureOr types are expanded as if they were
  sealed supertypes.

- Define how null-check, null-assert, cast, and declaration matcher
  patterns are lifted.

Author: munificent

working/0546-patterns/exhaustiveness.md

@@ -4,7 +4,7 @@ Author: Bob Nystrom
 
 Status: In progress
 
-Version 1.0
+Version 1.1 (see [CHANGELOG](#CHANGELOG) at end)
 
 ## Summary
 
@@ -386,8 +386,8 @@ into spaces:
 *   **Variable pattern:** An extract space whose type is the variable's type
     (which might be inferred).
 
-*   **Literal and constant patterns:** These are handled a little specially
-    depending on the constant value's type:
+*   **Literal or constant matcher:** These are handled specially depending on
+    the constant's type:
 
     *   We treat `bool` like a sealed supertype with subtypes `true` and
         `false`. The Boolean constants `true` and `false` are lifted to extract
@@ -405,19 +405,59 @@ into spaces:
         Dart language. This is just a way to model enums for exhaustiveness
         checking.)
 
-    *   We lift other constants to an extract pattern of that constant's type.
-        This means there is effectively no exhaustiveness checking for constants
-        of other types.
+    *   We lift other constants to an extract pattern whose type is a
+        synthesized subtype of the constant's type based on the constant's
+        identity. Each unique value of the constant's type is a singleton
+        instance of its own type, and the constant's type behaves like an
+        *unsealed* supertype. Two constants have the same synthesized subtype if
+        they are identical values.
+
+        This means you don't get exhaustiveness checking for constants, but do
+        get reachability checking:
+
+        ```dart
+        String s = ...
+        switch (s) {
+          case 'a string': ...
+          case 'a string': ...
+        }
+        ```
+
+        Here, there is an unreachable error on the second case since it matches
+        the same string constant. Also the switch has a non-exhaustive error
+        since it doesn't match the entire `String` type.
+
+*   **Null-check matcher:** An extract space whose type is the underlying
+    non-nullable type of the pattern. It contains a single field, `this` that
+    returns the same value it is called on. That field's space is the lifted
+    subpattern of the null-check pattern. For example:
 
-*   **Extractor patterns:** An extract space whose type is the extractor
+    ```dart
+    Card? card;
+    switch (card) {
+      case Jack(oneEyed: true)?: ...
+    }
+    ```
+
+    The case pattern is lifted to:
+
+    ```
+    Card(this: Jack(oneEyed: true))
+    ```
+
+*   **Extractor pattern:** An extract space whose type is the extractor
     pattern's type and whose fields are the lifted fields of the extractor
     pattern. Positional fields in the extractor pattern get implicit names like
     `field0`, `field1`, etc.
 
-**TODO: Specify how null-check patterns are lifted.**
+*   **Declaration matcher:** The lifted space of the inner subpattern.
+
+*   **Null-assert or cast binder:** An extract space of type `top`. These binder
+    patterns don't often appear in the matcher patterns used in switches where
+    exhaustiveness checking applies, but can occur nested inside a [declaration
+    matcher][] pattern.
 
-**TODO: Specify lifting binder patterns too (cast, null assert, declaration)
-since they can appear in matcher patterns through declaration matchers.**
+    [declaration matcher]: https://github.com/dart-lang/language/blob/master/working/0546-patterns/patterns-feature-specification.md#declaration-matcher
 
 **TODO: Once generics are supported, describe how type patterns are lifted to
 spaces here.**
@@ -653,7 +693,7 @@ result of that subtraction is obvious:
 Jack|Queen|King - Jack = Queen|King
 ```
 
-**Expanding** a type replaces a sealed supertype with its list of subtypes. We
+**Expanding a type** replaces a sealed supertype with its list of subtypes. We
 only do this when the left type is sealed and the right type is a subtype.
 Expanding is recursive:
 
@@ -691,6 +731,24 @@ And now it's easier to see that `Jack` subtracts the first arm leaving:
 Queen(suit: heart)|King(suit: heart)
 ```
 
+If the left type is nullable and the right type is `Null` or non-nullable, then
+expanding expands the nullable type to `Null` and the underlying type, as if the
+nullable type was a sealed supertype of the underlying type and `Null`:
+
+```
+Face? - Face  expands to:  Face|Null - Face = Null
+Jack? - Null  expands to:  Jack|Null - Null = Jack
+```
+
+Likewise, if the left type is `FutureOr<T>` for some type `T` and the right type
+is a subtype of `Future` or `T`, then expanding expands the `FutureOr<T>` to
+`Future<T>|T`.
+
+```
+FutureOr<int> - int     expands to:  Future<int>|int - int = Future<int>
+FutureOr<int> - Future  expands to:  Future<int>|int - Future = int
+```
+
 ### Subtraction
 
 OK, that's enough preliminaries. Here's the algorithm. To subtract two
@@ -953,3 +1011,16 @@ separately.
 Type promotion can safely assume any switch is exhaustive and promote
 accordingly. If that turns out to not be a case, a compile error will be
 reported anyway, so promotion doesn't matter.
+
+
+## Changelog
+
+### 1.1
+
+-   Specify that constants are treated as subtypes based on identity. This way,
+    we can get reachability errors on duplicate constant cases.
+
+-   Specify how null-check, null-assert, cast, and declaration matcher patterns
+    are lifted.
+
+-   Handle nullable and `FutureOr` types in expand type.

working/0546-patterns/exhaustiveness_prototype/lib/intersect.dart

@@ -66,6 +66,18 @@ StaticType? intersectTypes(StaticType left, StaticType right) {
   if (left.isSubtypeOf(right)) return left;
   if (right.isSubtypeOf(left)) return right;
 
+  if (left.isNullable) {
+    if (right.isNullable) {
+      var intersection = intersectTypes(left.underlying, right.underlying);
+      if (intersection == null) return null;
+      return intersection.nullable;
+    } else {
+      return intersectTypes(left.underlying, right);
+    }
+  } else if (right.isNullable) {
+    return intersectTypes(left, right.underlying);
+  }
+
   // If we allow sealed types to share subtypes, then this will need to be more
   // sophisticated. Here:
   //

working/0546-patterns/exhaustiveness_prototype/lib/static_type.dart

@@ -9,8 +9,21 @@ class StaticType {
   /// Built-in top type that all types are a subtype of.
   static final top = StaticType('top', inherits: []);
 
+  static final nullType = StaticType('Null');
+
   final String name;
 
+  late final StaticType nullable = StaticType._nullable(this);
+
+  /// If this type is a nullable type, then this is the underlying type.
+  ///
+  /// Otherwise `null`.
+  final StaticType? _underlying;
+
+  /// The underlying type of this nullable type. It's an error to call this on
+  /// a non-nullable type.
+  StaticType get underlying => _underlying!;
+
   /// Whether this type is sealed. A sealed type is implicitly abstract and has
   /// a closed set of known subtypes. This means that every instance of the
   /// type must be an instance of one of those subtypes. Conversely, if an
@@ -31,44 +44,40 @@ class StaticType {
   /// one of those two types*.
   final bool isSealed;
 
+  bool get isNullable => _underlying != null;
+
   /// The static types of the fields this type exposes for record destructuring.
   ///
   /// Includes inherited fields.
   Map<String, StaticType> get fields {
-    return {for (var supertype in supertypes) ...supertype.fields, ..._fields};
+    return {for (var supertype in _supertypes) ...supertype.fields, ..._fields};
   }
 
   final Map<String, StaticType> _fields;
 
-  final List<StaticType> supertypes = [];
+  final List<StaticType> _supertypes = [];
 
   /// The immediate subtypes of this type.
   Iterable<StaticType> get subtypes => _subtypes;
   final List<StaticType> _subtypes = [];
 
-  Iterable<StaticType> get allSupertypes sync* {
-    for (var supertype in supertypes) {
-      yield supertype;
-      yield* supertype.allSupertypes;
-    }
-  }
-
   StaticType(this.name,
       {this.isSealed = false,
       List<StaticType>? inherits,
       Map<String, StaticType> fields = const {}})
-      : _fields = fields {
+      : _underlying = null,
+        _fields = fields {
     if (inherits != null) {
       for (var type in inherits) {
-        supertypes.add(type);
+        _supertypes.add(type);
         type._subtypes.add(this);
       }
     } else {
-      supertypes.add(top);
+      _supertypes.add(top);
     }
 
     var sealed = 0;
-    for (var supertype in supertypes) {
+    for (var supertype in _supertypes) {
       if (supertype.isSealed) sealed++;
     }
 
@@ -86,9 +95,37 @@ class StaticType {
     if (sealed > 1) throw ArgumentError('Can only have one sealed supertype.');
   }
 
-  bool isSubtypeOf(StaticType supertype) {
-    if (this == supertype) return true;
-    return allSupertypes.contains(supertype);
+  StaticType._nullable(StaticType underlying)
+      : name = '${underlying.name}?',
+        _underlying = underlying,
+        isSealed = true,
+        // No fields because it may match null which doesn't have them.
+        _fields = {} {}
+
+  bool isSubtypeOf(StaticType other) {
+    if (this == other) return true;
+
+    // Null is a subtype of all nullable types.
+    if (this == nullType && other._underlying != null) return true;
+
+    // A nullable type is a subtype if the underlying type and Null both are.
+    var underlying = _underlying;
+    if (underlying != null) {
+      return underlying.isSubtypeOf(other) && nullType.isSubtypeOf(other);
+    }
+
+    // A non-nullable type is a subtype of the underlying type of a nullable
+    // type.
+    var otherUnderlying = other._underlying;
+    if (otherUnderlying != null) {
+      return isSubtypeOf(otherUnderlying);
+    }
+
+    for (var supertype in _supertypes) {
+      if (supertype.isSubtypeOf(other)) return true;
+    }
+
+    return false;
   }
 
   @override

working/0546-patterns/exhaustiveness_prototype/lib/subtract.dart

@@ -156,6 +156,17 @@ bool _isLeftSubspace(StaticType leftType, List<String> fieldNames,
 /// Recursively replaces [left] with a union of its sealed subtypes as long as
 /// doing so enables it to more precisely match against [right].
 List<StaticType> expandType(StaticType left, StaticType right) {
+  // If [left] is nullable and right is null or non-nullable, then expand the
+  // nullable type.
+  if (left.isNullable && (right == StaticType.nullType || !right.isNullable)) {
+    return [...expandType(left.underlying, right), StaticType.nullType];
+  }
+
+  // If [right] is nullable, then expand using its underlying type.
+  if (right.isNullable) {
+    return expandType(left, right.underlying);
+  }
+
   // If [left] is a sealed supertype and [right] is in its subtype hierarchy,
   // then expand out the subtypes (recursively) to more precisely match [right].
   if (left.isSealed && left != right && right.isSubtypeOf(left)) {

working/0546-patterns/exhaustiveness_prototype/test/expand_type_test.dart

@@ -198,6 +198,33 @@ void main() {
     expectExpand(e, d, 'E');
     expectExpand(e, e, 'E');
   });
+
+  test('nullable', () {
+    //   (A)
+    //   / \
+    //  B   C
+    //     / \
+    //    D   E
+    var a = StaticType('A', isSealed: true);
+    var b = StaticType('B', inherits: [a]);
+    var c = StaticType('C', inherits: [a]);
+    var d = StaticType('D', inherits: [c]);
+    var e = StaticType('E', inherits: [c]);
+
+    expectExpand(a.nullable, a, 'A|Null');
+    expectExpand(a, a.nullable, 'A');
+    expectExpand(a.nullable, a.nullable, 'A|Null');
+
+    // Sealed subtype.
+    expectExpand(a.nullable, b, 'B|C|Null');
+    expectExpand(a, b.nullable, 'B|C');
+    expectExpand(a.nullable, b.nullable, 'B|C|Null');
+
+    // Unsealed subtype.
+    expectExpand(c.nullable, d, 'C|Null');
+    expectExpand(c, d.nullable, 'C');
+    expectExpand(c.nullable, d.nullable, 'C|Null');
+  });
 }
 
 void expectExpand(StaticType left, StaticType right, String expected) {

working/0546-patterns/exhaustiveness_prototype/test/intersect_empty_test.dart

@@ -26,10 +26,8 @@ void main() {
   test('records', () {
     expectIntersectEmpty(rec(x: a, y: a), rec(x: a, y: a), isFalse);
     expectIntersectEmpty(rec(x: a, y: a), rec(x: a), isFalse);
-    expectIntersectEmpty(
-        rec(w: a, x: a), rec(y: a, z: a), isFalse);
-    expectIntersectEmpty(rec(w: a, x: a, y: a), rec(x: a, y: a, z: a),
-        isFalse);
+    expectIntersectEmpty(rec(w: a, x: a), rec(y: a, z: a), isFalse);
+    expectIntersectEmpty(rec(w: a, x: a, y: a), rec(x: a, y: a, z: a), isFalse);
   });
 
   test('types', () {

working/0546-patterns/exhaustiveness_prototype/test/intersect_types_test.dart

@@ -73,6 +73,22 @@ void main() {
     expectIntersect(d, e, null);
     expectIntersect(e, e, e);
   });
+
+  test('nullable', () {
+    // A
+    // |
+    // B
+    var a = StaticType('A');
+    var b = StaticType('B', inherits: [a]);
+
+    expectIntersect(a, a.nullable, a);
+    expectIntersect(a, StaticType.nullType, null);
+    expectIntersect(a.nullable, StaticType.nullType, StaticType.nullType);
+
+    expectIntersect(a, b.nullable, b);
+    expectIntersect(a.nullable, b, b);
+    expectIntersect(a.nullable, b.nullable, b.nullable);
+  });
 }
 
 void expectIntersect(StaticType left, StaticType right, StaticType? expected) {