Open issue: how to mitigate break for length patterns?

[jcouv]

Relates to PR dotnet/roslyn#56721
Relates to test plan dotnet/roslyn#51289

Switch

Current rules:

1. The switch is “not exhaustive” if there is a path to default state.
2. We have a “subsumed case” if it’s arm label is unreachable.
3. Also, as part of the list-pattern work we've previously settled on narrowing the domain of Length properties to non-negative integers.

Proposed rules:

1. Restore the domain of Length properties is integers.
2. Introduce the notion of a "negative branch" (see below)
3. The switch is “not exhaustive” if there is a real path to default state (ie. one that doesn't involve a negative branch).
4. We have a “subsumed case” if it’s arm label is unreachable (via any path).
5. Add new warning: we have a “likely subsumed case” if it’s arm label is reachable only by a negative path (ie. a path that involves at least one negative branch). You can only get to a warning- and error- free switch if you avoid tests that yield negative branches.

Negative branch:

In the DAG, we introduce the notion of an “negative branch” which means “only possible if Length could be negative”.
When we test for a Length: we get an “negative branch” if the branch bins only negative remaining values for the Length temp (this branch would be unreachable if the "Length is non-negative" assumption help). But we get a normal/real/positive path if the branch includes some non-negative remaining values for that temp.
We can represent this in the DAG by adding an extra no-op state on negative branches (it's a passthrough node with a special flag).

Impact

Those rules give us a warning, instead of an error, when an arm rests on test like { Length: -1 }.

                // (6,5): warning CS9203: The pattern is unreachable assuming non-negative length for countable and indexable types. Switch exhaustiveness is not checked for such negative values.
                //     { Length: -1 } => 1,
                Diagnostic(ErrorCode.WRN_SwitchArmSubsumedIfNonNegativeLength, "{ Length: -1 }").WithLocation(6, 5),

They also give use exhaustiveness diagnostics that we desire on the positive domain.

// (5,7): warning CS8509: The switch expression does not handle all possible values of its input type (it is not exhaustive). For example, the pattern '{ Length: 0 }' is not covered.
_ = a switch 
{
    { Length: < 0 } => 0,
};

But this approach is unable to produce exhaustiveness warnings on negative values that were missed.
{ Length: >= 0 } => ..., { Length: -1 } => ... produces no exhaustiveness warning for missing -2.

Exploring alternatives:

If we wanted to do that, we might be able to instead use the non-negative integers domain for Length properties, until we reach a test that triggers the domain to be expand from there on in the graph (may be a usability issue since the graph isn't available) or the whole graph.
I think this would introduce undesirable exhaustiveness warnings in case []: case [_]: case { Length: >1 }: because Length > 1 is treated as a triggering test by definition above (it bins only negative values on one side). This was one of the motivating scenarios to restrict the domain of length properties in the first place.
Users would have to write case []: case [_]: case _: instead.

So if we really want to offer exhaustiveness checking on negative length values, we probably need a different definition of what tests trigger a negative branch.

is patterns

Current rules:

For is patterns we produce an "always matches" warning or a "never matches" error if the whenTrue or the whenFalse branch is unreachable.

Proposed rules:

Add a new warning for is patterns: produce a "likely always matches" or "likely never matches" warning if the whenTrue or the whenFalse branch is reachable only by a negative path (ie. unreachable under non-negative assumption).

FYI @alrz

[jcouv]

Discussed in LDM 10/13/2021: in short, all this complexity doesn't seem warranted. Sticking with the assumption of non-negative Length and accepting the compat break seems preferrable at this point. We'll have this break in an early preview so that we can revisit if real-world cases are reported.

[333fred]

Notes: https://github.com/dotnet/csharplang/blob/main/meetings/2021/LDM-2021-10-13.md#length-pattern-backcompat