owned this note
owned this note
Published
Linked with GitHub
---
title: "Match ergonomics rules as inference rules"
author: TC
date: 2024-09-05
url: https://hackmd.io/zUqs2ISNQ0Wrnxsa9nhD0Q
---
# Match ergonomics rules as inference rules
This is a sketch of the various match ergonomics rules (including some related borrow checker rules) framed as inference rules.
## Notation
We represent the DBM state as a combination of the binding mode (of which there are three states) and the most restrictive binding mode we've encountered (`max_mode`).
Note that the *"binding"* rules only apply to *identifiers*.
As an example of how to read these rules, consider if we're trying to prove:
```rust
[[[x]]]: [[[u8]]]
```
To make this proof, we would apply the *"unwrap"* rule three times (read bottom to top):
```rust
----------------------------------- // By "binding".
DBM(Move, Move) ⊢ x : u8
----------------------------------- // By "unwrap".
DBM(Move, Move) ⊢ [x] : [u8]
----------------------------------- // By "unwrap".
DBM(Move, Move) ⊢ [[x]] : [[u8]]
----------------------------------- // By "unwrap".
DBM(Move, Move) ⊢ [[[x]]]: [[[u8]]]
```
Since the pattern then becomes an identifier, we can trivially prove that with the appropriate *"binding"* rule as the final step (a rule with nothing on top is terminal).
In these rules, the turnstile should be read as follows. Given:
```rust
B ⊢ A
```
...we say that `A` is true in the context of `B`. As a slight abuse of notation, we mean precisely that `B ⊢ A` is equivalent to `⊢ A ∧ B`, rather than to `⊢ A ∨ ¬B` as it is in normal sequent calculus.
## Before RFC 2005
These were the rules before RFC 2005 and are what the rules are today if a pattern does not use match ergonomics at all.
### Rules
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(Move, max) ⊢ $pat : T
----------------------------
DBM(Move, max) ⊢ [$pat]: [T]
/// Mutable deref
DBM(Move, RefMut) ⊢ $pat: T
-------------------------------------
DBM(Move, _) ⊢ &mut $pat: &mut T
/// Shared deref
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
/// Mutable binding
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 2005
These are the rules on stable Rust today.
### Rules
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut`
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, Ref) ⊢ [$pat]: T
----------------------------------------
DBM(Move | RefMut, Ref) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
------------------------------
DBM(Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref
DBM(Move, RefMut) ⊢ $pat: T
-----------------------------------------
DBM(_, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(Move, Ref) ⊢ $pat: T
----------------------------------
DBM(_, Ref) ⊢ &mut $pat: &mut T
/// Shared deref
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(_, _) ⊢ &$pat: &T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(_, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 (edition-dependent rules only)
These are the rules planned for stabilization in Rust 2024.
As compared with the rules above, *Rule 1* affects the *"mutable binding"* rule and *Rule 2* affects the *"deref"* rules.
### Rules
- **Rule 1**: When the DBM (default binding mode) is not `move` (whether or not behind a reference), writing `mut` on a binding is an error.
- **Rule 2**: When a reference pattern matches against a reference, do not update the DBM.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut`
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, Ref) ⊢ [$pat]: T
----------------------------------------
DBM(Move | RefMut, Ref) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
------------------------------
DBM(Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 2
DBM(mode, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(mode, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(mode, Ref) ⊢ $pat: T
----------------------------------
DBM(mode, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2
DBM(mode, Ref) ⊢ $pat: T
---------------------------
DBM(mode, _) ⊢ &$pat: &T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 (Rules 1-3)
These are the two edition-dependent rules along with *Rule 3*, which is not edition-dependent. *Rule 3* is simple and not particularly controversial, so we highlight this separately before introducing *Rules 4-5*.
As compared with the rules above, *Rule 3* affects the *"pass `&mut`"* rules and makes `DBM(RefMut, Ref)` into an invalid state.
### Rules
- **Rule 1**: When the DBM (default binding mode) is not `move` (whether or not behind a reference), writing `mut` on a binding is an error.
- **Rule 2**: When a reference pattern matches against a reference, do not update the DBM.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee, set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat: T
---------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 2
DBM(mode, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(mode, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(mode, Ref) ⊢ $pat: T
----------------------------------
DBM(mode, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2
DBM(mode, Ref) ⊢ $pat: T
--------------------------
DBM(mode, _) ⊢ &$pat: &T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: T
---------------------------------------
DBM(RefMut, RefMut) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 (Rules 1-3 + Rule 5)
Here, we add in *Rule 5*, which is also simple. We leave out for the moment *Rule 4* so we can introduce that separately below, as *Rule 4* is the most involved of all the rules.
As compared with the rules above, *Rule 5* adds one new eponymously named rule.
### Rules
- **Rule 1**: When the DBM (default binding mode) is not `move` (whether or not behind a reference), writing `mut` on a binding is an error.
- **Rule 2**: When a reference pattern matches against a reference, do not update the DBM.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee (or against a mutable reference treated as a shared one under *Rule 5*), set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
- **Rule 5**: If an `&` pattern is being matched against a mutable reference type, act as if the type were a shared reference instead.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
---------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 2
DBM(mode, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(mode, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(mode, Ref) ⊢ $pat: T
----------------------------------
DBM(mode, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2
DBM(mode, Ref) ⊢ $pat: T
--------------------------
DBM(mode, _) ⊢ &$pat: &T
/// Rule 5
DBM(mode, max) ⊢ &$pat: & T
------------------------------
DBM(mode, max) ⊢ &$pat: &mut T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: T
---------------------------------------
DBM(RefMut, RefMut) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 (Rules 1-5)
Here we bring together all of the rules adopted in RFC 3627, including *Rule 4*.
As compared with the rules above, adding *Rule 4* affects the *"deref"* rules and *"Rule 5"*.
### Rules
- **Rule 1**: When the DBM (default binding mode) is not `move` (whether or not behind a reference), writing `mut` on a binding is an error.
- **Rule 2**: When a reference pattern matches against a reference, do not update the DBM.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee (or against a `ref` DBM under *Rule 4*, or against a mutable reference treated as a shared one or a `ref mut` DBM treated as a `ref` one under *Rule 5*), set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
- **Rule 4**: If an `&` pattern is being matched against a non-reference type or an `&mut` pattern is being matched against a shared reference type or a non-reference type, **and if** the DBM is `ref` or `ref mut`, match the pattern against the DBM as though it were a type.
- **Rule 5**: If an `&` pattern is being matched against a mutable reference type (or against a `ref mut` DBM under *Rule 4*), act as if the type were a shared reference instead (or that the `ref mut` DBM is a `ref` DBM instead).
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
---------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4(X)
DBM(Move, RefMut) ⊢ $pat: T
---------------------------------- where T != &mut U
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rules 4
DBM(Move, Ref) ⊢ $pat: T
------------------------- where T != &U, T != &mut U
DBM(Ref, Ref) ⊢ &$pat: T
/// Mutable deref w/Rule 2
DBM(mode, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(mode, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(mode, Ref) ⊢ $pat: T
----------------------------------
DBM(mode, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2
DBM(mode, Ref) ⊢ $pat: T
--------------------------
DBM(mode, _) ⊢ &$pat: &T
/// Rule 5
DBM(mode, max) ⊢ &$pat: & T
------------------------------
DBM(mode, max) ⊢ &$pat: &mut T
/// Rule 5 w/Rule 4
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------ where T != &U, T != &mut U
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: T
---------------------------------------
DBM(RefMut, RefMut) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 (Rules 1-5) modulo Rule 4X2
In this section we apply the *Rule 4X2* variant of *Rule 4* under consideration here:
- https://github.com/rust-lang/rust/issues/127559
Compared to the above, this affects the statement of *Rule 5* and has the effect of applying *Rule 4* before *Rule 5*.
### Rules
- **Rule 1**: When the DBM (default binding mode) is not `move` (whether or not behind a reference), writing `mut` on a binding is an error.
- **Rule 2**: When a reference pattern matches against a reference, do not update the DBM.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee (or against a `ref` DBM under *Rule 4*, or against a mutable reference treated as a shared one or a `ref mut` DBM treated as a `ref` one under *Rule 5*), set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
- **Rule 4X2**: If an `&` pattern is being matched against a mutable reference type or a non-reference type, or if an `&mut` pattern is being matched against a shared reference type or a non-reference type, and if the DBM is `ref` or `ref mut`, match the pattern against the DBM as though it were a type.
- **Rule 5**: If an `&` pattern is being matched against a mutable reference type (or against a `ref mut` DBM under *Rule 4*), act as if the type were a shared reference instead (or that the `ref mut` DBM is a `ref` DBM instead).
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
---------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4(X)
DBM(Move, RefMut) ⊢ $pat: T
---------------------------------- where T != &mut U
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rule 4X2
DBM(Move, Ref) ⊢ $pat: T
------------------------- where T != &U
DBM(Ref, Ref) ⊢ &$pat: T
/// Mutable deref w/Rule 2
DBM(mode, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(mode, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(mode, Ref) ⊢ $pat: T
----------------------------------
DBM(mode, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2
DBM(mode, Ref) ⊢ $pat: T
--------------------------
DBM(mode, _) ⊢ &$pat: &T
/// Rule 5 w/Rule 4X2
DBM(Move, max) ⊢ &$pat: & T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------ where T != &U
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: T
---------------------------------------
DBM(RefMut, RefMut) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, max) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 (Rules 1-5) modulo Rule 4X3
In this section we apply the *Rule 4X3* variant of *Rule 4*.
The behavior we're looking for here is:
```rust
[&x]: &[&mut T]
x: &T // 4X
x: &mut T // 4X2
x: &mut T // 4X3
x: &mut T // 4E
[&ref x]: &mut [&mut T]
x: &T // 4X
x: &&mut T // 4X2
x: &T // 4X3
x: &&mut T // 4E
```
That is, we match the `&` pattern first against the scrutinee without *Rule 5*, then against the DBM without *Rule 5*, then against the scrutinee with *Rule 5*, then against the DBM with *Rule 5*.
### Rules
- **Rule 1**: When the DBM (default binding mode) is not `move` (whether or not behind a reference), writing `mut` on a binding is an error.
- **Rule 2**: When a reference pattern matches against a reference, do not update the DBM.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee (or against a `ref` DBM under *Rule 4*, or against a mutable reference treated as a shared one or a `ref mut` DBM treated as a `ref` one under *Rule 5*), set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
- **Rule 4X3**: In the `ref` DBM if an `&` pattern is being matched against a mutable reference type or a non-reference type, or in the `ref mut` DBM if an `&` pattern is being matched against a non-reference type, or in the `ref mut` DBM if an `&mut` pattern is being matched against a shared reference type or a non-reference type, match the pattern against the DBM as though it were a type.
- **Rule 5**: If an `&` pattern is being matched against a mutable reference type (or against a `ref mut` DBM under *Rule 4*), act as if the type were a shared reference instead (or that the `ref mut` DBM is a `ref` DBM instead).
Here are comparatively worded statement of other *Rule 4* variants:
- **Rule 4**: In the `ref` DBM if an `&` pattern is being matched against a non-reference type, or in the `ref mut` DBM if an `&` pattern is being matched against a non-reference type, or in the `ref mut` DBM if an `&mut` pattern is being matched against a shared reference type or a non-reference type, match the pattern against the DBM as though it were a type.
- **Rule 4X2**: In the `ref` DBM if an `&` pattern is being matched against a mutable reference type or a non-reference type, or in the `ref mut` DBM if an `&` is being matched against a mutable reference type or a non-reference type, or in the `ref mut` DBM if an `&mut` pattern is being matched against a shared reference type or a non-reference type, match the pattern against the DBM as though it were a type.
WIP:
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
---------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4X3
DBM(Move, RefMut) ⊢ $pat: T
---------------------------------- where T != &mut U
DBM(RefMut, RefMut) ⊢ &mut $pat: T
DBM(Move, Ref) ⊢ $pat: T
------------------------------ where T != &U, T != &mut U
DBM(RefMut, RefMut) ⊢ &$pat: T
/// Shared deref w/Rule 4X3
DBM(Move, Ref) ⊢ $pat: T
------------------------- where T != &U
DBM(Ref, Ref) ⊢ &$pat: T
/// Mutable deref w/Rule 2
DBM(mode, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(mode, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(mode, Ref) ⊢ $pat: T
----------------------------------
DBM(mode, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2
DBM(mode, Ref) ⊢ $pat: T
--------------------------
DBM(mode, _) ⊢ &$pat: &T
/// Rule 5 w/Rule 4X3
DBM(Move, max) ⊢ &$pat: & T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
/// RefMut binding
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: T
---------------------------------------
DBM(RefMut, RefMut) ⊢ $ident: T
/// Ref binding
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
DBM(Move, max) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 modulo Rule 1C, Rule 4E
He we adapt RFC 3627 with *Rule 1C* (from RFC 3627-nano), and with *Rule 4E* (early) in place of *Rule 4* and *Rule 2*.
### Rules
- **Rule 1C**: When the DBM is not `move` (whether or not behind a reference), writing `mut`, `ref`, or `ref mut` on a binding is an error.
- **Rule 4E**: If the DBM is `ref` or `ref mut`, match a reference pattern against the DBM as though it were a type before considering the scrutinee.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4E
DBM(Move, max) ⊢ $pat: T
----------------------------------
DBM(Move, max) ⊢ &mut $pat: &mut T
DBM(Move, RefMut) ⊢ $pat: T
----------------------------------
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rule 4E
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
DBM(Move, Ref) ⊢ $pat: T
-------------------------
DBM(Ref, Ref) ⊢ &$pat: T
/// Rule 5 w/Rule 4E
DBM(Move, max) ⊢ &$pat: &T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
/// Ref binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Apply DBM
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 modulo Rule 4E
He we adapt RFC 3627 with *Rule 4E* (early) in place of *Rule 4* and *Rule 2*.
### Rules
- **Rule 4E**: If the DBM is `ref` or `ref mut`, match a reference pattern against the DBM as though it were a type before considering the scrutinee.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4E
DBM(Move, max) ⊢ $pat: T
----------------------------------
DBM(Move, max) ⊢ &mut $pat: &mut T
DBM(Move, RefMut) ⊢ $pat: T
----------------------------------
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rule 4E
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
DBM(Move, Ref) ⊢ $pat: T
-------------------------
DBM(Ref, Ref) ⊢ &$pat: T
/// Rule 5 w/Rule 4E
DBM(Move, max) ⊢ &$pat: &T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding w/Rule 1
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(_, max) ⊢ ref mut $ident: T
/// Ref binding w/Rule 1
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(_, max) ⊢ ref $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Apply DBM
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627 modulo Rule 1C, Rule 3, Rule 4E
Here we adapt RFC 3627 with *Rule 4E* (early) in place of *Rule 4* and *Rule 2*. We preserve **Rule 1C** from Rust 2024. We do not adopt **Rule 3**.
### Rules
- **Rule 1C**: When the DBM is not `move` (whether or not behind a reference), writing `mut`, `ref`, or `ref mut` on a binding is an error.
- **Rule 4E**: If the DBM is `ref` or `ref mut`, match a reference pattern against the DBM as though it were a type before considering the scrutinee.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut`
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, Ref) ⊢ [$pat]: T
----------------------------------------
DBM(Move | RefMut, Ref) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
------------------------------
DBM(Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4E
DBM(Move, max) ⊢ $pat: T
----------------------------------
DBM(Move, max) ⊢ &mut $pat: &mut T
DBM(Move, RefMut) ⊢ $pat: T
----------------------------------
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rule 4E
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
DBM(Move, Ref) ⊢ $pat: T
-------------------------
DBM(Ref, Ref) ⊢ &$pat: T
/// Rule 5 w/Rule 4E
DBM(Move, max) ⊢ &$pat: &T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
/// Ref binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Apply DBM
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## Nadri's 2024-08-15 proposal
These are the rules that Nadri proposed on 2024-08-15, reframed so as to match the notation and approach above. This includes the adoption of *Rule 3* and *Rule 5*.
This RFC 3627 modulo Rule 4E except that rather than adopting Rule 1C, it allows for `ref` and `ref mut` bindings to create double references that may require creating temporaries.
### Rules
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 4E
DBM(Move, max) ⊢ $pat: T
----------------------------------
DBM(Move, max) ⊢ &mut $pat: &mut T
DBM(Move, RefMut) ⊢ $pat: T
----------------------------------
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rule 4E
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
DBM(Move, Ref) ⊢ $pat: T
-------------------------
DBM(Ref, Ref) ⊢ &$pat: T
/// Rule 5 w/Rule 4E
DBM(Move, max) ⊢ &$pat: &T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding (w/double refs)
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: &mut T
--------------------------------------------
DBM(RefMut, RefMut) ⊢ ref mut $ident: T
DBM(Move, RefMut) ⊢ ref $ident: &mut T
----------------------------------------
DBM(RefMut, RefMut) ⊢ ref $ident: T
DBM(Move, RefMut) ⊢ ref mut $ident: T
---------------------------------------
DBM(RefMut, RefMut) ⊢ $ident: T
/// Ref binding (w/double refs)
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: &T
-------------------------------
DBM(Ref, Ref) ⊢ ref $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627-min
Here's a set of rules that is maximal forward compatible subset of both RFC 3627 and Nadri's proposal.
Starting from the RFC 3627 rules, which we adopt verbatim, we extend *Rules 1-2* to save more space by making more cases into errors.
### Rules
- **Rule 1C**: When the DBM is not `move` (whether or not behind a reference), writing `mut`, `ref`, or `ref mut` on a binding is an error.
- **Rule 2C**: Reference patterns can only match against references in the scrutinee when the DBM is `move`.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee (or against a `ref` DBM under *Rule 4*, or against a mutable reference treated as a shared one or a `ref mut` DBM treated as a `ref` one under *Rule 5*), set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
- **Rule 4**: If an `&` pattern is being matched against a non-reference type or an `&mut` pattern is being matched against a shared reference type or a non-reference type, **and if** the DBM is `ref` or `ref mut`, match the pattern against the DBM as though it were a type.
- **Rule 5**: If an `&` pattern is being matched against a mutable reference type (or against a `ref mut` DBM under *Rule 4*), act as if the type were a shared reference instead (or that the `ref mut` DBM is a `ref` DBM instead).
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 2C
DBM(Move, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(Move, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(Move, Ref) ⊢ $pat: T
----------------------------------
DBM(Move, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2C
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
/// Mutable deref w/Rule 4(X)
DBM(Move, RefMut) ⊢ $pat: T
---------------------------------- where T != &mut U
DBM(RefMut, RefMut) ⊢ &mut $pat: T
/// Shared deref w/Rule 4
DBM(Move, Ref) ⊢ $pat: T
-------------------------- where T != &U, &mut U
DBM(Ref, Ref) ⊢ &$pat: &T
/// Rule 5
DBM(mode, max) ⊢ &$pat: & T
------------------------------
DBM(mode, max) ⊢ &$pat: &mut T
/// Rule 5 w/Rule 4
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------ where T != &U, T != &mut U
DBM(RefMut, RefMut) ⊢ &$pat: T
/// RefMut binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
/// Ref binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Apply DBM
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627-micro
Here's an even more minimal set of rules that is forward compatible to both RFC 3627 and to Nadri's proposal.
Starting from RFC 3627-min, we remove *Rule 4(X)*. This creates the property that once we leave the `Move` DBM, we cannot reenter it in any way.
### Rules
- **Rule 1C**: When the DBM is not `move` (whether or not behind a reference), writing `mut`, `ref`, or `ref mut` on a binding is an error.
- **Rule 2C**: Reference patterns can only match against references in the scrutinee when the DBM is `move`.
- **Rule 3**: If we've previously matched against a shared reference in the scrutinee (or against a mutable reference treated as a shared one under *Rule 5*), set the DBM to `ref` whenever we would otherwise set it to `ref mut`.
- **Rule 5**: If an `&` pattern is being matched against a mutable reference type, act as if the type were a shared reference instead.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut` w/Rule 3
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
-------------------------------------
DBM(Move | Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 2C
DBM(Move, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(Move, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(Move, Ref) ⊢ $pat: T
----------------------------------
DBM(Move, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2C
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
/// Rule 5
DBM(mode, max) ⊢ &$pat: & T
------------------------------
DBM(mode, max) ⊢ &$pat: &mut T
/// RefMut binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
/// Ref binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Apply DBM
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## RFC 3627-nano
Here's the most minimal set of rules (compared with RFC 2005) that is forward compatible to both RFC 3627 and to Nadri's proposal. This is what Nadri would propose to do.
Starting from RFC 3627-micro, we also remove *Rule 3* and *Rule 5*.
### Rules
- **Rule 1C**: When the DBM is not `move` (whether or not behind a reference), writing `mut`, `ref`, or `ref mut` on a binding is an error.
- **Rule 2C**: Reference patterns can only match against references in the scrutinee when the DBM is `move`.
```rust
// - `$ident` is an identifier.
// - `$pat` is a pattern.
// - `T`, `U` are types.
//
// Without loss of generality, we assume that `[..]` is the only
// constructor and that it has only arity of one.
enum BindingMode {
Move,
RefMut,
Ref,
}
struct DBM(mode: BindingMode, max_mode: BindingMode);
/// Unwrap
DBM(mode, max) ⊢ $pat : T
----------------------------
DBM(mode, max) ⊢ [$pat]: [T]
/// Pass `&mut`
DBM(RefMut, RefMut) ⊢ [$pat]: T
-----------------------------------------
DBM(Move, Move | RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, RefMut) ⊢ [$pat]: T
------------------------------------
DBM(RefMut, RefMut) ⊢ [$pat]: &mut T
DBM(RefMut, Ref) ⊢ [$pat]: T
----------------------------------------
DBM(Move | RefMut, Ref) ⊢ [$pat]: &mut T
DBM(Ref, Ref) ⊢ [$pat]: T
------------------------------
DBM(Ref, Ref) ⊢ [$pat]: &mut T
/// Pass `&`
DBM(Ref, Ref) ⊢ [$pat]: T
--------------------------
DBM(_, _) ⊢ [$pat]: &T
/// Mutable deref w/Rule 2C
DBM(Move, RefMut) ⊢ $pat: T
--------------------------------------------
DBM(Move, Move | RefMut) ⊢ &mut $pat: &mut T
DBM(Move, Ref) ⊢ $pat: T
----------------------------------
DBM(Move, Ref) ⊢ &mut $pat: &mut T
/// Shared deref w/Rule 2C
DBM(Move, Ref) ⊢ $pat: T
--------------------------
DBM(Move, _) ⊢ &$pat: &T
/// RefMut binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &mut T
---------------------------------------
DBM(Move, max) ⊢ ref mut $ident: T
/// Ref binding w/Rule 1C
DBM(Move, max) ⊢ $ident: &T
-------------------------------
DBM(Move, max) ⊢ ref $ident: T
/// Mutable binding w/Rule 1
DBM(Move, max) ⊢ $ident: T
------------------------------
DBM(Move, max) ⊢ mut $ident: T
/// Apply DBM
DBM(Move, max) ⊢ ref mut $ident: T
------------------------------------
DBM(RefMut, max) ⊢ $ident: T
DBM(Move, Ref) ⊢ ref $ident: T
------------------------------
DBM(Ref, Ref) ⊢ $ident: T
/// Binding
---------------------------
DBM(Move, Move) ⊢ $ident: T
----------------------------------- where T: Copy
DBM(Move, RefMut | Ref) ⊢ $ident: T
```
## Notes
### Interaction between Rule 4 and Rule 5
The interaction between *Rule 4* and *Rule 5* is particularly subtle, because it matters which of the two rules is applied first. As adopted in RFC 3627, we apply *Rule 5* first.
Here's how this matters. Under our rules, `[&x]: &[&mut T]` is true:
```rust
-------------------------------- // By "binding".
DBM(Move, Ref) ⊢ x : T
-------------------------------- // By "deref".
DBM(Ref, Ref) ⊢ &x : & T
-------------------------------- // By "Rule 5".
DBM(Ref, Ref) ⊢ &x : &mut T
--------------------------------- // By "unwrap".
DBM(Ref, Ref) ⊢ [&x]: [&mut T]
--------------------------------- // By "pass `&`".
DBM(Move, Move) ⊢ [&x]: &[&mut T]
```
This is what we want given the mental model of RFC 3627 and RFC 2005 which we call the *primacy of structural matching*. What we mean by that, roughly, is that if something in the pattern can match something *in the same position* (relative to constructor boundaries) in the scrutinee, then that should never fail. Since *Rule 5* allows for `&` patterns to match against `&mut` in the scrutinee, that demands that `[&x]: &[&mut T]` should be true.
However, if we were to apply *Rule 4* first (which we call *Rule 4X2*), then it's no longer true. Using our model, we can state *Rule 4X2* as a modified *Rule 5*:
```rust
/// Rule 5 w/Rule 4X2
DBM(Move, max) ⊢ &$pat: & T
------------------------------
DBM(Move, max) ⊢ &$pat: &mut T
DBM(Ref, Ref) ⊢ &$pat: T
------------------------------ where T != &U
DBM(RefMut, RefMut) ⊢ &$pat: T
DBM(Ref, Ref) ⊢ &$pat: & T
-----------------------------
DBM(Ref, Ref) ⊢ &$pat: &mut T
```
Under that rule, we get:
```rust
⊢ (ERROR: &mut T: ?Copy)
--------------------------------
DBM(Move, Ref) ⊢ x : &mut T
-------------------------------- // By "Rule 4X2".
DBM(Ref, Ref) ⊢ &x : &mut T
--------------------------------- // By "unwrap".
DBM(Ref, Ref) ⊢ [&x]: [&mut T]
--------------------------------- // By "pass `&`".
DBM(Move, Move) ⊢ [&x]: &[&mut T]
```
Note that applying *Rule 5* first does not accept strictly more, however. E.g., `[&&mut x]: &[&mut T]` is an error:
```rust
⊢ (ERROR: mismatched types)
--------------------------------------
DBM(Ref, Ref) ⊢ &mut x : T
-------------------------------------- // By "deref".
DBM(Ref, Ref) ⊢ &&mut x : & T
-------------------------------------- // By "Rule 5".
DBM(Ref, Ref) ⊢ &&mut x : &mut T
-------------------------------------- // By "unwrap".
DBM(Ref, Ref) ⊢ [&&mut x]: [&mut T]
-------------------------------------- // By "pass `&`".
DBM(Move, Move) ⊢ [&&mut x]: &[&mut T]
```
That is, the `&&mut x` does match against `&mut T` structurally, but then we're left with a `&mut x` pattern that can't match against either the type or the DBM.
However, if we were to apply *Rule 4* first (*Rule 4X2*), then we would accept it:
```rust
-------------------------------------- // By "binding".
DBM(Move, Ref) ⊢ x : T
-------------------------------------- // By "deref".
DBM(Move, Ref) ⊢ &mut x : &mut T
-------------------------------------- // By "Rule 4X2".
DBM(Ref, Ref) ⊢ &&mut x : &mut T
-------------------------------------- // By "unwrap".
DBM(Ref, Ref) ⊢ [&&mut x]: [&mut T]
-------------------------------------- // By "pass `&`".
DBM(Move, Move) ⊢ [&&mut x]: &[&mut T]
```
There are cases too that are accepted under both orderings but with a different meaning. E.g., given `[&ref x]: &[&mut T]`, we would infer `x: &T` under *Rule 4(X)*:
```rust
------------------------------------- // By "binding".
DBM(Move, Ref) ⊢ x : &T
------------------------------------- // By "ref binding".
DBM(Ref, Ref) ⊢ ref x : T
------------------------------------- // By "deref".
DBM(Ref, Ref) ⊢ &ref x : & T
------------------------------------- // By "Rule 5".
DBM(Ref, Ref) ⊢ &ref x : &mut T
------------------------------------- // By "unwrap".
DBM(Ref, Ref) ⊢ [&ref x]: [&mut T]
------------------------------------- // By "pass `&`".
DBM(Move, Move) ⊢ [&ref x]: &[&mut T]
```
But under *Rule 4X2* or *Rule 4E*, we would infer `x: &&mut T`:
```rust
DBM(Move, Ref) ⊢ x : &&mut T
------------------------------------- // By "ref binding".
DBM(Move, Ref) ⊢ ref x : &mut T
------------------------------------- // By "Rule 4X2".
DBM(Ref, Ref) ⊢ &ref x : &mut T
------------------------------------- // By "unwrap".
DBM(Ref, Ref) ⊢ [&ref x]: [&mut T]
------------------------------------- // By "pass `&`".
DBM(Move, Move) ⊢ [&ref x]: &[&mut T]
```
### Interaction between Rule 4 and "deref"
Originally, *Rule 4* applied only when the scrutinee was a non-reference type (let's call that *Rule 4-original*). That is, we applied this rule:
```rust
/// Mutable deref w/Rule 4-original
DBM(Move, RefMut) ⊢ $pat: T
---------------------------------- where T != &U, T != &mut U
DBM(RefMut, RefMut) ⊢ &mut $pat: T
```
...instead of this one:
```rust
/// Mutable deref w/Rule 4(X)
DBM(Move, RefMut) ⊢ $pat: T
---------------------------------- where T != &mut U
DBM(RefMut, RefMut) ⊢ &mut $pat: T
```
We called this the extended version of *Rule 4*, or *"Rule 4X"* (and also, since its adoption in RFC 3627, plain *Rule 4* or *Rule 4(X)*). Loosening the `where` clause allows us to accept cases like `[&mut x]: &mut [&T]`:
```rust
----------------------------------------- // By "binding".
DBM(Move, RefMut) ⊢ x : &T
----------------------------------------- // By "mutable deref w/Rule 4(X)".
DBM(RefMut, RefMut) ⊢ &mut x : &T
----------------------------------------- // By "unwrap".
DBM(RefMut, RefMut) ⊢ [&mut x]: [&T]
----------------------------------------- // By "pass `&mut`".
DBM(Move, Move) ⊢ [&mut x]: &mut [&T]
```
We considered this desirable as it serves to close the distance between *Rule 4* and an alternate rule, *Rule 4E* (*Rule 4 Early*), in that it causes our *Rule 4* to accept most of what *Rule 4E* would accept, and it avoids the following potential oddity:
```rust
[& x]: & [&T] // Valid.
[&mut x]: &mut [&T] // Invalid under Rule 4-original.
// Valid under Rule 4(X), Rule 4E.
```
However, *Rule 4(X)* does not accept everything that's accepted under *Rule 4E*. This is due to applying *Rule 5* ahead of *Rule 4*, as we saw in the last section. Consequently:
```rust
[&& x]: &[& T] // Valid.
[&&mut x]: &[&mut T] // Invalid under Rule 4X.
// Valid under Rule 4X2, Rule 4E.
```
Our willingness under *Rule 4(X)* to fall back from a failed structural match to matching against the DBM, combined with our willing to match `&` patterns against `&mut` references but not `&mut` patterns against `&` references, also creates this unfortunate oddity:
```rust
[&mut (ref x)]: &mut [&mut T] // x: &T
[&mut (ref x)]: &mut [& T] // x: &&T
```
(The original *Rule 4* (prior to [#127257](https://github.com/rust-lang/rust/issues/127257)) did not have this oddity, and one option for eliminating it is to go back to that original rule.)
The inference on the first proceeds as:
```rust
--------------------------------------------------- // By "binding".
DBM(Move, RefMut) ⊢ x : &T
--------------------------------------------------- // By "ref binding".
DBM(Move, RefMut) ⊢ ref x : T
--------------------------------------------------- // By "deref".
DBM(RefMut, RefMut) ⊢ &mut (ref x) : &mut T
--------------------------------------------------- // By "unwrap".
DBM(RefMut, RefMut) ⊢ [&mut (ref x)]: [&mut T]
--------------------------------------------------- // By "pass `&mut`.
DBM(Move, Move) ⊢ [&mut (ref x)]: &mut [&mut T]
```
...and one the second as:
```rust
----------------------------------------------- // By "binding".
DBM(Move, RefMut) ⊢ x : &&T
----------------------------------------------- // By "ref binding".
DBM(Move, RefMut) ⊢ ref x : &T
----------------------------------------------- // By "Rule 4(X)".
DBM(RefMut, RefMut) ⊢ &mut (ref x) : &T
----------------------------------------------- // By "unwrap".
DBM(RefMut, RefMut) ⊢ [&mut (ref x)]: [&T]
----------------------------------------------- // By "pass `&mut`".
DBM(Move, Move) ⊢ [&mut (ref x)]: &mut [&T]
```
If we had a kind of *Rule 5* that was willing to match `&mut` patterns against `&` references, we can see that would restore the symmetry needed to avoid this, as then we'd apply that rule in preference to *Rule 4(X)* here. But, of course, there are good reasons to not have that rule.
Alternatively, if we weren't willing to fall back from the failed structural match to matching against the DBM (*Rule 4-original*), then the second case would simply be an error.
### Drawbacks of Rule 4X2
Of course, *Rule 4X2* would create its own oddities (which it shares with *Rule 4E*). These are mostly centered on where we might expect *Rule 5* to apply E.g.:
```rust
[&x]: &[& T] //~ x: &T
[&x]: &[&mut T] //~ ERROR cannot move
```
To get the desired behavior, we instead must write the latter case as:
```rust
[&&ref x]: &[&mut T] //~ x: &T
```
### Decision on Rule 4X2
We have an open issue for deciding whether or not to adopt *Rule 4X2*. That's tracked here:
- https://github.com/rust-lang/rust/issues/127559
## Acknowledgments
Thanks to Eric Holk for a useful conversation about notation, and thanks to Nadri for a useful conversation about his proposal and for checking our statement of it above for correctness.
Google Drive
Gist
Clipboard
Sign in with Wallet
