Review and update pattern subsumption and exhaustion (#1691)

* Minimal updates

This first commit makes minimal adjustments to the subsumption and exhaustiveness sections. This keeps the rules fairly high level, and provides more leeway for an implementation to devise any algorithm for managing recursive patterns.

* More extensive rules

Provide more extensive rule definitions for recursive patterns on subsumption and exhaustiveness.

This version leans more closely to the implementation, but also doesn't dive deep enough to provide more clarity on pattern forms where exhaustiveness or subsumption might not be detected.

I'm tempted to use the first commit, but I want people to see both.

* Revert "More extensive rules"

This reverts commit 4858e65.

* Make exhaustiveness minimal

Use a minimal definition for subsumption and exhaustiveness.

* Apply suggestions from code review

Co-authored-by: Nigel-Ecma <6654683+Nigel-Ecma@users.noreply.github.com>

* Edits discussed in 7/1 meeting

Implement the edits discussed in the July 1st meeting.

---------

Co-authored-by: Nigel-Ecma <6654683+Nigel-Ecma@users.noreply.github.com>

Author: BillWagner

standard/expressions.md

@@ -3889,7 +3889,7 @@ If a switch expression is not subject to a *switch expression conversion*, then
 - The type of the *switch_expression* is the best common type [§12.6.3.16](expressions.md#126316-finding-the-best-common-type-of-a-set-of-expressions)) of the *switch_expression_arm_expression*s of the *switch_expression_arm*s, if such a type exists, and each *switch_expression_arm_expression* can be implicitly converted to that type.
 - It is an error if no such type exists.
 
-It is an error if the pattern of any *switch_expression_arm* is *subsumed* by ([§11.3](patterns.md#113-pattern-subsumption)) the set of patterns of earlier *unguarded* ([§13.8.3](statements.md#1383-the-switch-statement)) *switch_expression_arm*s of the switch expression.
+It is an error if the pattern of any *switch_expression_arm* is *subsumed* by (§11.1) the set of patterns of earlier *unguarded* ([§13.8.3](statements.md#1383-the-switch-statement)) *switch_expression_arm*s of the switch expression.
 
 A switch expression is *exhaustive* if every value of its input is handled by at least one arm of the switch expression. A warning may be issued if a switch expression is not exhaustive.
 

standard/patterns.md

@@ -13,6 +13,12 @@ A pattern is tested against a value in a number of contexts:
 
 The value against which a pattern is tested is called the ***pattern input value***.
 
+A pattern `P` is *subsumed* by set of unguarded patterns `Q` if any input value matched by `P` is matched by one of the members of `Q`.
+
+In a switch statement ([§13.8.3](statements.md#1383-the-switch-statement)), it is an error if a case’s pattern is *subsumed* by the preceding set of *unguarded* ([§13.8.3](statements.md#1383-the-switch-statement)) cases. In a switch expression ([§12.11](expressions.md#1211-switch-expression)), it is an error if a *switch_expression_arm*’s pattern is *subsumed* by the preceding set of *unguarded* *switch_expression_arm*s’ patterns.
+
+A set of patterns is exhaustive if, for every possible input value, some pattern in the set is applicable. When an implementation detects that a set of patterns is not exhaustive, it shall issue a warning.
+
 ## 11.2 Pattern forms
 
 ### 11.2.1 General
@@ -446,64 +452,3 @@ If, after applying the preceding rule, the token `_` is still a *discard_pattern
 > ```
 >
 > *end example*
-
-## 11.3 Pattern subsumption
-
-In a switch statement ([§13.8.3](statements.md#1383-the-switch-statement)), it is an error if a case’s pattern is *subsumed* by the preceding set of *unguarded* ([§13.8.3](statements.md#1383-the-switch-statement)) cases. In a switch expression ([§12.11](expressions.md#1211-switch-expression)), it is an error if a *switch_expression_arm*’s pattern is *subsumed* by the preceding set of *unguarded* *switch_expression_arm*s’ patterns.
-> *Note*: This means that any input value would have been matched by one of the previous cases or arms. *end note*
-The following rules define when a set of patterns subsumes a given pattern:
-
-A pattern `P` *would match* a constant `K` if the specification for that pattern’s runtime behavior is that `P` matches `K`.
-
-A set of patterns `Q` *subsumes* a pattern `P` if any of the following conditions hold:
-
-- `P` is a constant pattern and any of the patterns in the set `Q` would match `P`’s *converted value*
-- `P` is a var pattern and the set of patterns `Q` is *exhaustive* ([§11.4](patterns.md#114-pattern-exhaustiveness)) for the type of the pattern input value ([§11.1](patterns.md#111-general)), and either the pattern input value is not of a nullable type or some pattern in `Q` would match `null`.
-- `P` is a declaration pattern with type `T` and the set of patterns `Q` is *exhaustive* for the type `T` ([§11.4](patterns.md#114-pattern-exhaustiveness)).
-
-> *Example*: In the following switch expression, no arm is subsumed even though arms 1, 2, and 3 share the same pattern:
->
-> <!-- Example: {template:"code-in-main", name:"SwitchExprUnguardedSubsumption"} -->
-> ```csharp
-> object x = 10;
-> bool b = false;
-> int y = x switch
-> {
->     int i when !b => 0,
->     int i when b  => 1,
->     int i         => 2,
->     _             => 3
-> };
-> ```
->
-> Arms 1 and 2 have non-constant guards and so are not *unguarded*; only arm 3 is *unguarded* with pattern `int i`, which does not subsume the final `_` arm because it does not match a non-`int` value such as `null`. *end example*
-
-## 11.4 Pattern exhaustiveness
-
-Informally, a set of patterns is exhaustive for a type if, for every possible value of that type other than null, some pattern in the set is applicable.
-The following rules define when a set of patterns is *exhaustive* for a type:
-
-A set of patterns `Q` is *exhaustive* for a type `T` if any of the following conditions hold:
-
-1. `T` is an integral or enum type, or a nullable version of one of those, and for every possible value of `T`’s non-nullable underlying type, some pattern in `Q` would match that value; or
-2. Some pattern in `Q` is a *var pattern*; or
-3. Some pattern in `Q` is a *declaration pattern* for type `D`, and there is an identity conversion, an implicit reference conversion, or a boxing conversion from `T` to `D`.
-
-> *Example*:
->
-> <!-- Example: {template:"standalone-console-without-using", name:"PatternExhaustiveness1", replaceEllipsis:true, customEllipsisReplacements: [""], ignoredWarnings:["CS8321"]} -->
-> ```csharp
-> static void M(byte b)
-> {
->     switch (b) {
->         case 0: case 1: case 2: ... // handle every specific value of byte
->             break;
->         // error: the pattern 'byte other' is subsumed by the (exhaustive)
->         // previous cases
->         case byte other: 
->             break;
->     }
-> }
-> ```
->
-> *end example*

standard/statements.md

@@ -753,7 +753,7 @@ There can be at most one `default` label in a `switch` statement.
 
 It is an error if the pattern of any switch label is not *applicable* ([§11.2.1](patterns.md#1121-general)) to the type of the input expression.
 
-It is an error if the pattern of any switch label is *subsumed* by ([§11.3](patterns.md#113-pattern-subsumption)) the set of patterns of earlier *unguarded* switch labels of the switch statement.
+It is an error if the pattern of any switch label is *subsumed* by (§11.1) the set of patterns of earlier *unguarded* switch labels of the switch statement.
 
 > *Example*:
 >
@@ -949,7 +949,7 @@ A switch label is reachable if at least one of the following is true:
 - The switch’s *selector_expression* is not a constant value and either
   - the label is a `case` without a guard or with a guard whose value is not the constant false; or
   - it is a `default` label and
-    - the set of patterns appearing among the cases of the switch statement that do not have guards or have guards whose value is the constant true, is not *exhaustive* ([§11.4](patterns.md#114-pattern-exhaustiveness)) for the switch governing type; or
+    - the set of patterns appearing among the cases of the switch statement that do not have guards or have guards whose value is the constant true, is not *exhaustive* (§11.1) for the switch governing type; or
     - the switch governing type is a nullable type and the set of patterns appearing among the cases of the switch statement that do not have guards or have guards whose value is the constant true does not contain a pattern that would match the value `null`.
 - The switch label is referenced by a reachable `goto case` or `goto default` statement.
 
@@ -959,7 +959,7 @@ The end point of a `switch` statement is reachable if the switch statement is re
 
 - The `switch` statement contains a reachable `break` statement that exits the `switch` statement.
 - No `default` label is present and either
-  - The switch’s *selector_expression* is a non-constant value, and the set of patterns appearing among the cases of the switch statement that do not have guards or have guards whose value is the constant true, is not *exhaustive* ([§11.4](patterns.md#114-pattern-exhaustiveness)) for the switch governing type.
+  - The switch’s *selector_expression* is a non-constant value, and the set of patterns appearing among the cases of the switch statement that do not have guards or have guards whose value is the constant true, is not *exhaustive* (§11.1) for the switch governing type.
   - The switch’s *selector_expression* is a non-constant value of a nullable type, and no pattern appearing among the cases of the switch statement that do not have guards or have guards whose value is the constant true would match the value `null`.
   - The switch’s *selector_expression* is a constant value and no `case` label without a guard or whose guard is the constant true would match that value.