Redundant conjunctive patterns (&, as) may trigger spurious exhaustiveness warning

[brianrourkeboll]

Redundant conjunctive patterns (&, as) may trigger a spurious exhaustiveness warning in some scenarios.

Repro steps

Minimal repro

A normal exhaustive pattern match does not trigger an exhaustiveness warning, as expected:

type T = A | B | C

let f x =
    match x with
    | A | B -> ()
    | C -> ()

However, given this example, adding a redundant match on case C with a conjunctive pattern like & or as will trigger a spurious exhaustiveness warning:

type T = A | B | C

let f x =
    match x with
    | A | B -> ()
    | C & C -> ()

//      match x with
//  ----------^

//stdin(4,11): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'A' may indicate a case not covered by the pattern(s).

More realistic/useful repro

Another, perhaps more realistic and useful example is this, where you might want to bind the first two elements of a list as well as the tail of the original list (i.e., including the second element but not the first):

let f xs =
    match xs with
    | [] | [_] -> ()
    | e1 :: e2 :: _ & _ :: tail -> ()

//      match xs with
//  ----------^^

//stdin(2,11): warning FS0025: Incomplete pattern matches on this expression. For example, the value '[]' may indicate a case not covered by the pattern(s).

It is impossible to make the compiler happy in that scenario — we cannot turn e1 :: e2 :: _ & _ :: tail into (e1 :: e2 :: _ & _ :: tail | []), because we cannot bind e1, e2, or tail in the [] case which the compiler is (unnecessarily) asking us to add.

Note that no warning is emitted if one side of the conjunctive pattern is a simple named pattern, e.g.,

let f x =
    match x with // No warning.
    | A | B -> ()
    | C & c -> ()

let f x =
    match x with // No warning.
    | A | B -> ()
    | C as c -> ()

Codegen

This even affects codegen — an unreachable MatchFailureException branch is emitted:

type T = A | B | C

let f x =
    match x with // No warning.
    | A | B -> true
    | C -> false
    
let f' x =
    match x with // Warning, different codegen.
    | A | B -> true
    | C & C -> false

SharpLab

public static bool f(T x)
{
    switch (x._tag)
    {
        default:
            return true;
        case 2:
            return false;
    }
}

public static bool f'(T x)
{
    switch (x._tag)
    {
        default:
            return true;
        case 2:
            if (x._tag == 2)
            {
                return false;
            }
            throw new MatchFailureException("#mirrorsharp-virtual-fs\\f4765ba6-b1f5-44e9-b186-0abc7ae58e28\\_.fs", 10, 10);
    }
}

Expected behavior

No exhaustiveness warning should be emitted, and the codegen should be identical.

Actual behavior

An exhaustiveness warning and an unreachable MatchFailureException branch are emitted.

Known workarounds

N/A.

Related information

This behavior appears to be old — it reproduces for me in .NET 3.1, and it is still present in the latest .NET 9 SDK.

[T-Gro]

Hi Brian.

I think the compiler does go deep into intersection patterns and their logical relation. This is indeed a good feature improvement idea.