# 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;
1. 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.
1. References get out of the way: I can write a pattern without `&`/`&mut`/`ref`/`ref mut` and it will do the obvious thing;
1. 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`;
1. Mutability is predictable: A `&mut` pattern gives mutable access to the place inside it;
1. Mutability is predictable: A `&` pattern prevents mutable access to any place inside it;
1. If `x: &T`, I can copy out the value by writing `&` before the binding;
1. Inherited and real references are indistinguishable;
1. I can make any binding mutable by adding `mut` before it;

Vaguer ones:

12. Patterns accomodate semantically-irrelevant code changes;
1. Patterns compose: `if let <pat1>(<pat2>) = <expr>` behaves the same as `if let <pat1>(x) = <expr> && let <pat2> = x`;
1. Patterns mirror expressions;
1. 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;
1. Patterns accomodate semantically-irrelevant code changes: switching from `Rc` to `Arc` should require minimal code changes;
1. Impossible cases can be omitted: I shouldn't have to write code for cases that are statically impossible;
1. 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: :heavy_check_mark:;
- 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: :heavy_check_mark:.

### 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