DSLX Match Exhaustiveness Checking with Range Analysis

[mikex-oss]

What's hard to do? (limit 100 words)

I'm not sure how feasible this is in DSLX land, but one gotcha I noticed is that the match arm exhaustiveness checking can be sensitive to what input you use.

For example, take:

fn foo(x: u2) -> u2 {
    match x {
        u2:0 => u2:0,
        u2:1 => u2:1,
        u2:2 => u2:1,
        u2:3 => u2:2,
    }
}

This satisfies exhaustiveness checking. But suppose x is actually encoded as a biased value (i.e. 0 is not a valid value in the natural input space), and the result is more naturally expressed in terms of the unbiased value. You can't write:

fn foo(x: u2) -> u2 {
    let unbiased_x = x as u3 + u3:1;
    match unbiased_x {
        u3:1 => u2:0,
        u3:2 => u2:1,
        u3:3 => u2:1,
        u3:4 => u2:2,
    }
}

since you would get:

uN[3] Match patterns are not exhaustive; e.g. u3:0 not covered; please add remaining patterns to complete the match or a default case via _ => ...

Current best alternative workaround (limit 100 words)

In some cases like above, it's easy to just use a different match pattern (the u2), but otherwise, you can add a default arm that can't ever really be reached.

Your view of the "best case XLS enhancement" (limit 100 words)

It'd be cool if we could infer this is actually exhaustive.

[cdleary]

This is not generally feasible because the exhaustiveness is a function of the structure of the type that is being matched on, not any optimization/analysis information. The idea that operations on values get imbued in the type gets you towards the realm of dependently typed languages, and DSLX is not one (and probably shouldn't strive to be because it would be very incomplete if we added particular one-off things). I'd recommend we close this as WNF, but up to you.

[ericastor]

As an alternative workaround - would it be reasonable to bias your match patterns in-line? That is, since DSLX is intended to be constexpr-friendly, I wonder if:

fn foo(x: u2) -> u2 {
    match x {
        bias(u3:1) => u2:0,
        bias(u3:2) => u2:1,
        bias(u3:3) => u2:1,
        bias(u3:4) => u2:2,
    }
}

would work? (And if not, whether it should?)

[mikex-oss]

@ericastor I couldn't get very far as to whether that would work, since it doesn't appear that we support function calls in match arms:

0024:         bias(u3:1) => u2:0,
~~~~~~~~~~~~~~~~~~^ ParseError: Expected '=>', got '('

I'd recommend we close this as WNF, but up to you.

Fair enough, I'll let y'all driving the DSLX language to make the call.

[cdleary]

Patterns are a different sub-grammar than expressions -- there's a bunch of syntactic constructs that have different meaning in pattern position than they do in expressions, which I think would make "defaulting to constexpr eval of an expression" a messy proposition. For more references on inspiration for what we're going towards, see https://doc.rust-lang.org/reference/patterns.html