Empty types in exhaustiveness, a shiny future

Motivation

We would like:

• To omit match arms that are unreachable, e.g. Some(_) when matching on x: Option<!>;
• To be explicit about side-effects, e.g. match *x {} with x: *const ! has the side-effect of asserting validity of the data at place *x, which is not clearly indicated by the match; this proposes match *x { ! } instead;
• To be correct, e.g. not warn "unreachable" on an arm that is in fact reachable 😅, see here.

Terminology

An empty type or uninhabited type is a type that has no valid value, like !, Result<!, !>, or Result<(i32, !), !>. (For this purpose, we pretend that private fields in foreign structs are inhabited).

An empty pattern for a type is a pattern that can be written but does not match a valid value of the type. E.g. Some(_) for the type Option<!>. (For this purpose, we pretend that private fields in foreign structs are inhabited).

Given a match expression, an arm is:

• Useful if removing it changes the semantics of the match expression, namely:
  • Changing which arm is run;
  • Changing side-effects, in particular which places' values are asserted valid.
• Reachable if it is possible to set up the scrutinee such that the corresponding arm is taken.

Most of the time, usefulness and reachability coincide. It is however possible to get an arm which is useful && !reachable, with the combination of empty patterns and partially-initialized values. This is the trickiness that I want to address in this proposal.

Example (under conservative assumptions, see Unresolved Questions):

fn never_ptr(x: *const !) {
    unsafe {
        match *x {
            // Reachable because an uninitialized value would take this arm.
            // Useful because reachable.
            _ => {} // useful, reachable

        }
        match *x {
            // Unreachable because `_a` loads the value and there is no valid
            // value to load. Useful because it asserts validity.
            _a => {} // useful, !reachable
            _ => {} // !useful, !reachable
        }
    }
}
fn union_option_never() {
    union Uninit<T: Copy> {
        value: T,
        uninit: (),
    }
    let x: Uninit<Option<!>> = Uninit { uninit: () };
    match x.value {
        None => {} // useful, reachable
        // Reachable with a partially-initialized `Some(_)`. See
        // Unresolved Questions for why we consider this possible.
        _ => {} // useful, reachable
    }
    match x.value {
        None => {} // useful, reachable
        _a => {} // useful, !reachable
    }
}

Never patterns

We add ! as a pattern that is allowed for any uninhabited type (e.g. ! or (u32, !)). The never pattern means the ! pattern. A never pattern means any pattern that contains !.

An arm whose pattern is a never pattern must omit its body, e.g.:

let x: Uninit<Option<!>> = Uninit { uninit: () };
match x.value {
    None => {}
    Some(!)
}

Semantically, a never pattern acts as a load of a nonexistent value from the place. A Some(!) arm is semantically indistinguishable from Some(a) => match a {}. In particular, a never pattern is always unreachable in the sense above (but can be useful).

Validity tracking

We compute usefulness and reachability by tracking validity of the data at each place on top of the existing exhaustiveness algorithm.

A place is known_valid if it is known to contain data valid for its type. We consider a place known_valid except if it is inside a union field or a deref (raw ptr or &T). We check this syntactically for the scrutinee, then recursively as we dig into patterns.

If a place is known_valid, then empty patterns are unreachable and unuseful. If a place is !known_valid, then an empty pattern can be reachable and/or useful, depending. If it has a ! or a binding on an empty type, it is unreachable. Other cases build on the usual exhaustiveness algorithm.

Shiny future diagnostics

The diagnostics I propose are:

• If an arm is useful && reachable, we don't lint anything;
• If an arm is !useful && !reachable, we suggest the user remove it;
• If an arm is useful && !reachable and it isn't already a never pattern, we suggest the user replace it with a corresponding never pattern;
• If an extra _ => {} at the bottom of the match would be reachable, the match is not exhaustive. The user must add arms to make it exhaustive. If a never pattern would make sense we suggest that, otherwise we suggest a normal pattern.

Under this proposal:

• Arms that truly can't be reached can be omitted, which allows let Ok(x) = y if y: Result<T, !>;
  • Sadly this isn't allowed if y: Result<T, &!>, see discussion of safety below.
• A match is required to be explicit about which validity-asserting loads it performs. E.g. match *x {} is not allowed; we require match *x { ! } or match *x { _ => {} }.

Current status

Phrased in terms of validity, the current stable implementation of exhaustiveness assumes all places invalid, except specifically the scrutinee if its type is ! or an empty enum.

The current implementation of the exhaustive_patterns feature essentially assumes all places valid (with a small inconsistency around &!).

Both of these warn unreachable on arms that are useful, which is pretty bad; see e.g. https://github.com/rust-lang/rust/issues/117119.

Both of these also allow some empty matches that have side-effects. Specifically match ... {} is allowed on stable if the scrutinee has type enum Void {} or !, even if the place comes from a raw ptr/union field/reference. We'll need to carve out this exception for backwards-compatibility, at least at first. Ideally we can deprecate this in favor of a never pattern. Note: this exception does not concern composite types like (u32, !) or Result<!, !>; only specifically non-nested ! and empty enums.

Less-shiny intermediate steps

• Step 1: Don't warn unreachable on arms that are useful. This doesn't change which code we allow, only lints.
• Step 2: Add minimal_exhaustive_patterns that does the diagnostics I proposed, except we don't suggest never patterns.
  • This allows let Ok(x) = y for y: Result<T, !>.
  • We carve out the backwards-compatibility exception mentioned above.
• Step 3: RFC never patterns based on this here document, and implement.
• Step 3.1: Deprecate side-effecting empty matches, suggest match ... { ! }.
• Step 3.2: Deprecate exhaustive_patterns in favor of never_patterns.
• Step 4: Stabilize never patterns, rejoice!
• Step 5 (over an edition, maybe): Disallow side-effecting empty matches, require match ... { ! }.

Unresolved questions

Opsem decisions

What is or isn't valid depends on opsem decisions. I tried to err on the side of future-compatibility. These questions include:

• whether a valid &T must point to a valid T (https://github.com/rust-lang/unsafe-code-guidelines/issues/413);
• whether a possibly-invalid Option<T> can have variant Some with not-fully-valid data for T (https://github.com/rust-lang/unsafe-code-guidelines/issues/443);
• whether casting/type coercion performs a load.

Safety

Most users would like to write let Ok(x) = y; when y: Result<T, &!>. This is when y is safe for its type. This is in tension with the desire to be explicit about side-effects, since this implicitly asserts that y is not Err(&uninit). It's not unthinkable that there'd be a middle way; for example it seems correct to assume safety if there are no unsafe blocks anywhere in the crate.

The current proposal is forward-compatible with assuming safety later. Note also that we can write let Ok(x) | Err(&!) = ...; which isn't too bad.