Match ergonomics redesign

My own personal notes. Documents from the successive design meetings:

• 2023-12-13: https://hackmd.io/YLKslGwpQOeAyGBayO9mdw
• 2024-05-15: https://hackmd.io/9SstshpoTP60a8-LrxsWSA
• 2024-06-07: https://hackmd.io/4hJmztFnS_KWG47Zemx-lw
• Latest source for accepted rules: https://github.com/rust-lang/rfcs/pull/3627

Design axioms

The ones that feel most crucial:

1. Patterns do what I mean: writing the right pattern doesn't require sigil-golf to appease the type-checker;
2. Patterns can be fully precise: I can spell out exactly which places I want to access with a pattern;
   • Consequence: in an unsafe block I have confidence I'm not triggering anything unexpected.
3. References get out of the way: I can write a pattern without &/&mut/ref/ref mut and it will do the obvious thing;
4. Patterns are polymorphic: the behavior of a pattern doesn't change if I make a generic type more specific;

The ones that feel important to figure out the proposal:

5. References get out of the way: If I don't need mutability, I can treat &mut T like it's &T;
6. Mutability is predictable: A &mut pattern gives mutable access to the place inside it;
7. Mutability is predictable: A & pattern prevents mutable access to any place inside it;
8. If x: &T, I can copy out the value by writing & before the binding;
9. Inherited and real references are indistinguishable;
10. I can make any binding mutable by adding mut before it;

Vaguer ones:

12. Patterns accomodate semantically-irrelevant code changes;
13. Patterns compose: if let <pat1>(<pat2>) = <expr> behaves the same as if let <pat1>(x) = <expr> && let <pat2> = x;
14. Patterns mirror expressions;
15. Patterns borrow as little as needed;

We mostly have mirroring and composition for patterns without &/&mut/ref/ref mut (which I would call "purely structural patterns"). It gets tricky with references.

We could also extend these to cover my other pattern work with axioms like:

16. Smart pointers get out of the way: the ergonomic distance between using a reference and a smart pointer is as small as necessary;
17. Patterns accomodate semantically-irrelevant code changes: switching from Rc to Arc should require minimal code changes;
18. Impossible cases can be omitted: I shouldn't have to write code for cases that are statically impossible;
19. Pattern semantics are predictable: I can tell what data a pattern touches by looking at it. This is crucial when matching on partially-initialized data.

Typing rules

NOTE: this has been superceded by further discussions; it is kept for posterity only.

I want to formulate match ergonomics in terms of types, ideally as a typing rule. The rule would look like: <pat> @ <expr> : <type> so we can track which place is tested or used for bindings.

Given a pattern p and a type T, we start with p @ q: T (where q is a dummy scrutinee expression to) and apply the rules. This will either error or assign each binding to an expression and a type.

I implemented these rules and variations in a little tool: https://github.com/Nadrieril/typing-rust-patterns.

The expression is the only implicit state that is tracked. This is a feature: implicit state is confusing. This means we don't get match ergonomics 2024 rule 3.

Interestingly, the expression implicitly tracks the DBM: it can be either a place (corresponding to move DBM), &<place> (corresponding to ref DBM) or &mut <place> (corresponding to ref mut DBM). Note that we only inspect the expression for bindings, never in the middle of a pattern.

Note: a rule looks like:

<precondition1>, <precondition2>, ...
------------------------------------- "Rule name"
<postcondition>, <side conditions>

It is applied bottom-to-top. Read the rule like "to get bottom thing, if side conditions apply, we need top things to be (recursively) true". At most one rule should apply to any given case; if no rule applies, then the pattern is not valid for that type. The example derivations below should help understand how this works.

//! Syntax of patterns:
//! - `(mut)? (ref)? (mut)? x`: a binding;
//! - `[p]`: a tuple with one elements;
//! - `[p0, p1]`: a tuple with two elements;
//! - `&p`, `&mut p`: dereferencing patterns.
//!
//! We use tuples for illustration; this applies identially to any adt patterns.

//// Constructor rules

/// Matching a constructor against its type

p0 @ q.0: T0,  p1 @ q.1: T1,  ..
-------------------------------- "Constructor"
[p0, p1, ..] @ q: [T0, T1, ..]


/// Matching a constructor against a reference

p0 @ &(*q).0: &T0,  p1 @ &(*q).1: &T1,  ..
------------------------------------------ "ConstructorRef"
[p0, p1, ..] @ q: &[T0, T1, ..]

p0 @ &mut (*q).0: &mut T0,  p1 @ &mut (*q).1: &mut T1,  ..
---------------------------------------------------------- "ConstructorRef"
[p0, p1, ..] @ q: &mut [T0, T1, ..]


/// Matching a constructor against nested references

[p0, ..] @ *q: &T
----------------- "ConstructorMultiRef"
[p0, ..] @ q: &&T

[p0, ..] @ &**q: &T
--------------------- "ConstructorMultiRef"
[p0, ..] @ q: &&mut T

[p0, ..] @ *q: &T
--------------------- "ConstructorMultiRef"
[p0, ..] @ q: &mut &T

[p0, ..] @ &mut **q: &mut T
--------------------------- "ConstructorMultiRef"
[p0, ..] @ q: &mut &mut T


//// Dereferencing rules

p @ *q: T
---------- "Deref(EatOuter)"
&p @ q: &T

p @ *q: T
------------------ "Deref(EatOuter)"
&mut p @ q: &mut T

// If we allow using a `&` pattern on `&mut` (aka match ergo 2024 rule 5).
// The reborrow prevents `&(ref mut x)`, see the "Mutability is predictable" axiom.
&p @ &*q: &T
-------------- "DerefMutWithShared(EatOuter)"
&p @ q: &mut T


//// Binding rules

// Success case
let x: T = q
------------ "Binding"
x @ q: T


// The extra constraint on `q` is because we inspect the DBM.
// If we removed the constraint we'd get the more natural behavior of "just working".
let mut x: T = q
---------------------------------- "Binding"
mut x @ q: T, q is not a reference

// Stable behavior: `mut x` resets the DBM. 
// Error instead for match ergo 2024 rule 1.
mut x @ q: T
-------------- "MutBindingResetBindingMode"
mut x @ &q: &T

// Stable behavior: `mut x` resets the DBM. 
// Error instead for match ergo 2024 rule 1.
mut x @ q: T
---------------------- "MutBindingResetBindingMode"
mut x @ &mut q: &mut T


// The extra constraint on `q` is to avoid referencing a temporary.
x @ &q: &T
---------------------------------- "BindingBorrow"
ref x @ q: T, q is not a reference

x @ &mut q: &mut T
-------------------------------------- "BindingBorrow"
ref mut x @ q: T, q is not a reference


// Stable behavior: `ref x` resets the DBM. 
ref x @ q: T
-------------- "RefBindingResetBindingMode"
ref x @ &q: &T

ref x @ q: T
---------------------- "RefBindingResetBindingMode"
ref x @ &mut q: &mut T

ref mut x @ q: T
------------------ "RefBindingResetBindingMode"
ref mut x @ &q: &T

ref mut x @ q: T
-------------------------- "RefBindingResetBindingMode"
ref mut x @ &mut q: &mut T

Compared to the rules in https://github.com/rust-lang/rust/issues/127559:

• Rule 1: ;
• Rule 2: partially: we do get [&x]: &[&T] => x: &T but not [&mut x]: &[&mut T];
• Rule 3: partially: we accept &[[&x]]: &[&mut [T]] but not &[[x]]: &[&mut [T]];
• Rule 4: I think we do "rule 4 early", see the below derivations;
• Rule 5: .

Example derivations

• Some((&x, ref y)): &Option<(T, U)> => x: T, y: &U

Some((&x, ref y)) @ p: &Option<(T, U)>
// <= (constructor rule)
(&x, ref y) @ &(*p as Some).0: &(T, U)
// <= (constructor rule)
&x: &(*&(*p as Some).0).0: &T
ref y: &(*&(*p as Some).0).1: &U
// <= (dereferencing rule on the first one)
x: *&(*&(*p as Some).0).0: T
ref y: &(*&(*p as Some).0).1: &U
// <= (binding rules on both, assuming the version of today's rust)
let x: T = *&(*&(*p as Some).0).0
let y: &U = &(*&(*p as Some).0).1

// Final bindings (simplified):
let x: T = (*p as Some).0.0;
let y: &U = &(*p as Some).0.1;

• [&x]: &[&T] => x: &T

[&x] @ p: &[&T]
// Applying rule `ConstructorRef`
&x @ &(*p).0: &&T
// Applying rule `Deref(EatOuter)`
x @ *&(*p).0: &T
// Applying rule `Binding`
let x: &T = *&(*p).0

// Final bindings (simplified):
let x: &T = (*p).0;

• [&x]: &[&mut T] => x: &mut T, move error

[&x] @ p: &[&mut T]
// Applying rule `ConstructorRef`
&x @ &(*p).0: &&mut T
// Applying rule `Deref(EatOuter)`
x @ *&(*p).0: &mut T
// Applying rule `Binding`
let x: &mut T = *&(*p).0

// Final bindings (simplified):
let x: &mut T = (*p).0; // Borrow-check error: CantCopyRefMut

• [&&mut x]: &[&mut T] => x: T

[&&mut x] @ p: &[&mut T]
// Applying rule `ConstructorRef`
&&mut x @ &(*p).0: &&mut T
// Applying rule `Deref(EatOuter)`
&mut x @ *&(*p).0: &mut T
// Applying rule `Deref(EatOuter)`
x @ **&(*p).0: T
// Applying rule `Binding`
let x: T = **&(*p).0

// Final bindings (simplified):
let x: T = *(*p).0;

• [&mut x]: &mut [&T] => x: &T

[&mut x] @ p: &mut [&T]
// Applying rule `ConstructorRef`
&mut x @ &mut (*p).0: &mut &T
// Applying rule `Deref(EatOuter)`
x @ *&mut (*p).0: &T
// Applying rule `Binding`
let x: &T = *&mut (*p).0

// Final bindings (simplified):
let x: &T = (*p).0;

• [&mut x]: &[&mut T] => type error

[&mut x] @ p: &[&mut T]
// Applying rule `ConstructorRef`
&mut x @ &(*p).0: &&mut T
// Type error for `&mut x @ &(*p).0: &&mut T`: MutabilityMismatch

• &[[x]]: &[&mut [T]] => x: &mut T, borrow error

&[[x]] @ p: &[&mut [T]]
// Applying rule `Deref(EatOuter)`
[[x]] @ *p: [&mut [T]]
// Applying rule `Constructor`
[x] @ (*p).0: &mut [T]
// Applying rule `ConstructorRef`
x @ &mut (*(*p).0).0: &mut T
// Applying rule `Binding`
let x: &mut T = &mut (*(*p).0).0

// Final bindings (simplified):
let x: &mut T = &mut (*(*p).0).0; // Borrow-check error: MutBorrowBehindSharedBorrow

• &[[&x]]: &[&mut [T]] => x: T, borrow error if we don't use simplification rules

&[[&x]] @ p: &[&mut [T]]
// Applying rule `Deref(EatOuter)`
[[&x]] @ *p: [&mut [T]]
// Applying rule `Constructor`
[&x] @ (*p).0: &mut [T]
// Applying rule `ConstructorRef`
&x @ &mut (*(*p).0).0: &mut T
// Applying rule `DerefMutWithShared(EatOuter)`
&x @ &*&mut (*(*p).0).0: &T
// Applying rule `Deref(EatOuter)`
x @ *&*&mut (*(*p).0).0: T
// Applying rule `Binding`
let x: T = *&*&mut (*(*p).0).0

// Final bindings (simplified):
let x: T = (*(*p).0).0;

• &[[&mut x]]: &[&mut [T]] => x: T, borrow error if we don't use simplification rules

&[[&mut x]] @ p: &[&mut [T]]
// Applying rule `Deref(EatOuter)`
[[&mut x]] @ *p: [&mut [T]]
// Applying rule `Constructor`
[&mut x] @ (*p).0: &mut [T]
// Applying rule `ConstructorRef`
&mut x @ &mut (*(*p).0).0: &mut T
// Applying rule `Deref(EatOuter)`
x @ *&mut (*(*p).0).0: T
// Applying rule `Binding`
let x: T = *&mut (*(*p).0).0

// Final bindings (simplified):
let x: T = (*(*p).0).0;

• [&ref mut x]: &mut [T] => x: &mut T, borrow error

[&ref mut x] @ p: &mut [T]
// Applying rule `ConstructorRef`
&ref mut x @ &mut (*p).0: &mut T
// Applying rule `DerefMutWithShared(EatOuter)`
&ref mut x @ &*&mut (*p).0: &T
// Applying rule `Deref(EatOuter)`
ref mut x @ *&*&mut (*p).0: T
// Applying rule `BindingBorrow`
x @ &mut *&*&mut (*p).0: &mut T
// Applying rule `Binding`
let x: &mut T = &mut *&*&mut (*p).0

// Final bindings (simplified):
let x: &mut T = &mut *&(*p).0; // Borrow-check error: MutBorrowBehindSharedBorrow