Ownership and Move Semantics
--move-checkWhole-binding use-after-move checking is enabled by the opt-in --move-check flag.
Without it, reusing a binding moved as a whole is not rejected. Row narrowing and
widening are ordinary type-checking rules and apply independently of that flag:
reading a removed field or requiring a wider row is rejected in either mode.
The flag remains off by default; enabling it also enforces ownership restrictions
that are not expressed by row types.
Values move by default
A value whose type is not Copy has exactly one owner at any point. Assigning it, passing it
as an argument, or returning it moves it: ownership transfers, and the source binding
becomes invalid.
struct Buffer { data: [i64] }
fun consume(b: Buffer) -> i64 { b.data.len() }
fun main() {
let a := Buffer { data = [1, 2, 3] };
let b := a; // a is moved into b
// let n = a.data; // error: `a` was moved
consume(b); // b is moved into consume
// consume(b); // error: `b` was moved
}
Primitive types and any type implementing Copy are exempt — they are duplicated instead.
Formal rules
Legality Rule №1
Using a non-Copy value in assignment, argument, or return position moves it; a later use
of the source binding is rejected.
Referenced by: rfc-0071
Tested by (9)
1fun main() {
2 let s := "hello";
3 let moved := s;
4 let again := s;
5}
typecheck errorT0019“use of moved value `s`”
1aspect Source { type Item; fun take(self) -> Item; }
2fun invalid<S: Source<Item = { token: String }>>(source: S) -> {} {
3 let { token: _, ..rest } := source.take();
4 let again := source.take(); // ERROR[T0019]
5 rest
6}
7fun main() {}
typecheck errorT0019“use of moved value `source`”
1fun rejected<row R>(value: &{ token: String, ..R }) -> String {
2 value.token // ERROR[T0019]
3}
4fun main() {}
typecheck errorT0019“cannot move `value.token` out of a reference”
1fun add<row R: !{token}>(r: { ..R }) -> { token: String, ..R } {
2 { ..r, token = "secret" }
3}
4
5fun forward<row R: !{token}>(r: { ..R }) -> i64 {
6 let callback := [r] once || {
7 let added := add(r);
8 let again := r; // ERROR[T0019]
9 7
10 };
11 callback()
12}
13
14fun main() {}
typecheck errorT0019“use of moved value `r`”
1fun dup<T>(x: T) -> (T, T) { (x, x) } // ERROR[T0019]
2fun main() {}
typecheck errorT0019at 1“use of moved value”
1record Row { name: String }
2fun main() {
3 let rows: [Row] := [Row { name = "a".to_string() }];
4 for (r in rows) { let n := r.name; } // ERROR[T0019]
5}
typecheck errorT0019at 4“borrowed from a `[T]` view”
1fun duplicate_rest<row R, row Rest>(value: { ..R }) -> ({ ..Rest }, { ..Rest })
2where R = { token: String, ..Rest } {
3 let { token: _, ..rest } := value;
4 let first := rest;
5 (first, rest) // ERROR[T0019]
6}
7fun main() {}
typecheck errorT0019“use of moved value `rest`”
1// old x old: TA x OW, TA x CO, CL x PM, CL x CO, DY x CO, OW x CO, PM x CO, PM x GA
2type Names := [String];
3type Handler := once |i64| -> i64;
4aspect Speak { fun speak(&self) -> String; }
5struct Dog {}
6extend Dog: Speak { fun speak(&self) -> String { "woof".to_string() } }
7enum Msg { Num { n: i64 }, Text { s: String } }
8fun apply(h: Handler, v: i64) -> i64 { h(v) }
9fun identity<T>(x: T) -> T { x }
10fun main() {
11 let names: Names := ["a".to_string(), "b".to_string()];
12 let first := names[0].clone();
13 assert(first == "a");
14 var total := 0;
15 for (n in names) { total := total + n.len(); }
16 assert(total == 2);
17 let add := 10;
18 let h: Handler := [add] once |v: i64| { v + add };
19 assert(apply(h, 5) == 15);
20 let msgs := [Msg::Num { n = 1 }, Msg::Text { s = "hi".to_string() }];
21 var acc := 0;
22 for (m in msgs) {
23 let f := [m] once || {
24 match (m) { Msg::Num { n } => n, Msg::Text { s } => s.len() }
25 };
26 acc := acc + f();
27 }
28 assert(acc == 3);
29 let dogs: [dyn Speak] := [Dog {}, Dog {}];
30 var barks := 0;
31 for (d in dogs) { if (d.speak() == "woof") { barks := barks + 1; } }
32 assert(barks == 2);
33 let moved := names;
34 assert(moved.len() == 2);
35 match (identity(Msg::Num { n = 4 })) { Msg::Num { n } => assert(n == 4), Msg::Text { s } => assert(false) }
36 let o: Perhaps<[i64]> := Perhaps::Some { value = [1, 2] };
37 match (o) { Perhaps::Some { value } => assert(value.len() == 2), None => assert(false) }
38}
passes
1import lib::{Event, events, weight, Doc, make, first_generic};
2fun main() {
3 var total := 0;
4 for (e in events()) { total := total + weight(e); }
5 assert(total == 10);
6 let d := make();
7 let title := d.title;
8 let pages := d.pages;
9 assert(title == "t");
10 assert(first_generic(pages) == 3);
11}
passes
Copy
Copy marks a type whose values may be duplicated rather than moved. It is opt in, and
declared like any other aspect:
struct Point { x: f64, y: f64 }
extend Point: Copy;
A type may implement Copy only if every one of its fields — or, for an enum, every payload
in every variant — is itself Copy. Fixed-size arrays and tuples are Copy when their
elements are.
References: &T is Copy. &var T is not — an exclusive reference must remain unique,
so it is moved or reborrowed rather than duplicated.
Formal rules
Legality Rule №1
A declared Copy implementation is legal only when every struct field or enum payload is
Copy; conditional implementations are considered under their declared bounds.
Referenced by: rfc-0071
Tested by
1// RFC-0071 §2 `Copy` eligibility through a *generic* field type whose own
2// `Copy` impl is conditional (issue #303).
3//
4// Deciding `extend<T: Copy> Outer<T>: Copy` means answering whether the field
5// type `Inner<T>` is `Copy` — a question with no answer in terms of concrete
6// types, since `T` is not one. It is answerable under the impl's own bounds:
7// `T` is assumed `Copy`, which discharges the bound on `Inner`'s conditional
8// impl. The eligibility check used to give up here and reject the program.
9
10struct Inner<T> {
11 value: T,
12}
13
14extend<T: Copy> Inner<T>: Copy;
15
16struct Outer<T> {
17 inner: Inner<T>,
18}
19
20extend<T: Copy> Outer<T>: Copy;
21
22// The same shape with the bound in a `where` clause rather than inline.
23struct Wrapped<T> {
24 held: Inner<T>,
25}
26
27extend<T> Wrapped<T>: Copy where T: Copy;
28
29// And through an enum payload, which takes the other branch of the check.
30enum Held<T> {
31 One { value: Inner<T> },
32 None,
33}
34
35extend<T: Copy> Held<T>: Copy;
36
37fun id<T: Copy>(x: T) -> T {
38 return x;
39}
40
41fun main() {
42 let o := Outer { inner = Inner { value = 1 } };
43 let copied := id(o);
44 assert(copied.inner.value == 1);
45
46 let w := Wrapped { held = Inner { value = 2 } };
47 let w_copied := id(w);
48 assert(w_copied.held.value == 2);
49
50 let h := Held::One { value = Inner { value = 3 } };
51 let h_copied := id(h);
52 match (h_copied) {
53 Held::One { value } => assert(value.value == 3),
54 Held::None => assert(false),
55 }
56}
passes
Drop
LIMIT-EVALUATION-005RFC-0071Drop bodies never run, so only an empty drop body is accepted.Drop gives a type destructor logic that runs when a value goes out of scope:
struct Handle { fd: i64 }
extend Handle: Drop {
fun drop(&var self) { close_fd(self.fd); }
}
Drop is opt in. A type without a Drop implementation is reclaimed by recursively dropping
its fields.
drop takes self: &var Self, not self by valueFormal rules
Legality Rule №1
An extend Type: Drop declaration gives its type Drop status even when its drop body is
empty; that status participates in ownership restrictions.
Referenced by: rfc-0071
Tested by
1struct Handle {
2 name: String,
3 fd: i64,
4}
5
6extend Handle: Drop {
7 fun drop(&var self) { }
8}
9
10fun main() {
11 let handle := Handle { name = "x", fd = 1 };
12 let name := handle.name;
13}
typecheck errorT0019“belongs to a `Drop` type”
Copy and Drop are mutually exclusive
A type may not implement both. A Copy value may be duplicated freely, so there is no single
point at which a destructor should run.
Formal rules
Legality Rule №1
No concrete type instantiation may implement both Copy and Drop; overlapping conditional
implementations are rejected only when an instantiation would receive both aspects.
Referenced by: rfc-0071
Tested by (3)
1// RFC-0071 §4 forbids one *type* having both `Copy` and `Drop`. It does not
2// forbid a program from containing an impl of each, and the check added for
3// issue #302 is deliberately precise about the difference — an approximation
4// that rejected any `Copy` impl and `Drop` impl sharing a target constructor
5// would reject both halves of this file.
6//
7// Two ways the two impls can coexist:
8
9struct Disjoint<T> {
10 val: T,
11}
12
13// 1. Provably disjoint bounds. No `T` is both `Copy` and `!Copy`, so no
14// instantiation of `Disjoint<T>` ever has both aspects.
15extend<T: Copy> Disjoint<T>: Copy;
16
17extend<T: !Copy> Disjoint<T>: Drop {
18 fun drop(&var self) {}
19}
20
21struct Reach<T> {
22 val: T,
23}
24
25// 2. A concrete target outside the blanket's reach. `String` is not `Copy`,
26// so the blanket does not apply to `Reach<String>` and it is free to
27// implement `Drop`. With `i64` here instead this is a §4 violation —
28// see `typechecking/structs/stage5_neg_35_copy_blanket_reaches_drop_instantiation.mtl`.
29extend<T: Copy> Reach<T>: Copy;
30
31extend Reach<String>: Drop {
32 fun drop(&var self) {}
33}
34
35fun main() {
36 let copyable := Disjoint { val = 1 };
37 assert(copyable.val == 1);
38
39 let droppable := Disjoint { val = "owned" };
40 assert((&droppable.val).len() == 5);
41
42 let reached := Reach { val = 7 };
43 assert(reached.val == 7);
44
45 let unreached := Reach { val = "outside" };
46 assert((&unreached.val).len() == 7);
47}
passes
1// RFC-0071 §4 across two *conditional* impls (issue #302).
2//
3// Neither impl target is closed, so the declaration-site check in
4// `typechecker::inference` cannot evaluate either one — it is `coherence`'s
5// cross-aspect overlap check that rejects this. The bounds are not disjoint:
6// `i64` is both `Copy` and `Display`, so `Overlap<i64>` would have both
7// aspects, which §4 forbids.
8
9struct Overlap<T> {
10 val: T,
11}
12
13extend<T: Copy> Overlap<T>: Copy;
14
15extend<T: Display> Overlap<T>: Drop {
16 fun drop(&var self) {}
17}
18
19fun main() {}
typecheck errorT0001“cannot implement both `Copy` and `Drop`”
1// RFC-0071 §4 where a `Copy` blanket and a concrete `Drop` impl meet at one
2// instantiation (issue #302).
3//
4// `i64` is `Copy`, so the blanket reaches `Reach<i64>` — the exact type the
5// `Drop` impl targets. Contrast the accepted case in
6// `evaluator/structs/95_copy_and_drop_non_overlapping_impls.mtl`, which is
7// this program with `String` in place of `i64`: the rejection turns on
8// whether the concrete argument satisfies the blanket's bound, not on the
9// two impls merely sharing a target constructor.
10
11struct Reach<T> {
12 val: T,
13}
14
15extend<T: Copy> Reach<T>: Copy;
16
17extend Reach<i64>: Drop {
18 fun drop(&var self) {}
19}
20
21fun main() {}
typecheck errorT0001“cannot implement both `Copy` and `Drop`”
Drop order
LIMIT-EVALUATION-005RFC-0071Drop bodies never run, so only an empty drop body is accepted.Within a scope, values are dropped in reverse declaration orderD1. A value that has been moved out is not dropped where it was declared — the new owner drops it.
For a type with a Drop implementation, drop(self) runs first, then its fields are dropped
recursivelyD2.
Formal rules
Dynamic Semantics №1
When a scope ends, its still-owned values are dropped in reverse declaration order. A value moved to another owner is dropped by that owner instead.
Exempt from fixture coverage — blocked on metel-core#261: Destructor invocation and drop order are not implemented yet -- non-empty Drop bodies are intentionally rejected until implementation issue #261 (drop order and explicit drop, RFC-0071 3/4) lands. Verified directly: the interpreter has no drop-at-scope-end mechanism to observe order against.
Dynamic Semantics №2
Dropping a value with a Drop implementation invokes drop(self) before recursively dropping
its fields.
Exempt from fixture coverage — blocked on metel-core#261: Same root gap as drop-order.dynamics-1: destructor invocation is not implemented, so drop(self)-before-fields ordering cannot be observed.
Explicit drop
LIMIT-EVALUATION-005RFC-0071Drop bodies never run, so only an empty drop body is accepted.drop(x) consumes x, runs its destructor if it has one, and marks the binding movedD1. Using
x afterwards is an error, exactly as after any other moveL1.
Formal rules
Legality Rule №1
After drop(x) consumes a non-Copy binding, that binding may not be used again.
Exempt from fixture coverage — blocked on metel-core#261: Explicit drop(x) is not implemented -- drop is not a built-in name today (verified directly: it produces a T0003 undefined-name error), so this use-after-drop rejection cannot be observed. Tracked by #261, which also depends on move tracking (#579).
Dynamic Semantics №1
drop(x) consumes x and invokes its destructor when its type implements Drop.
Exempt from fixture coverage — blocked on metel-core#261: Same root gap as explicit-drop.legality-1: drop is not a built-in yet, so this dynamic-semantics claim cannot be exercised.
Partial moves
Moving a field out of a struct leaves the containing value partially moved. The remaining
fields stay accessible; the original whole type is no longer available, but the residual
may be used as a whole at its current type. Since v0.13.0 (RFC-0137) the residual
also gets a named type — Handle becomes Handle.{ fd }, not just internal bookkeeping;
see §Narrowing below.
struct Pair { a: Buffer, b: i64 }
fun main() {
let p := Pair { a = Buffer { data = [1] }, b = 42 };
let x := p.a; // p.a moved out; p is partially moved
let y := p.b; // still fine — p.b was not moved
// consume_pair(p); // error: `p` cannot be used as a whole
}
Tracking is at field granularity. Pattern destructuring may move several fields at once, under the same rules.
A type implementing Drop may not be partially moved — its destructor requires the whole
value.
Reassigning a moved-out field restores that field's own accessibility, and — once every field ever moved out of a value has been reassigned — restores the value's whole-value status tooL3: the compiler tracks which fields are currently missing, not merely whether the value was ever partially moved. Reassigning only some of several moved-out fields leaves the value partially moved until the rest are reassigned too.
Formal rules
Legality Rule №1
After a field of a non-Drop struct is moved, the remaining fields may be accessed but the
containing value may not be used at its original whole type. A whole-value use at
its narrowed residual type, including an empty residual, is legal.
Referenced by: rfc-0071
Tested by
1struct Pair {
2 left: String,
3 right: i64,
4}
5
6fun take(pair: Pair) -> i64 {
7 pair.right
8}
9
10fun main() {
11 let pair := Pair { left = "a", right = 1 };
12 let left: String := pair.left;
13 let value: i64 := take(pair);
14}
typecheck errorT0001“partially-moved `Pair`”
Legality Rule №2
A field of a Drop type may not be moved out.
Tested by (2)
1struct Handle {
2 name: String,
3 fd: i64,
4}
5
6extend Handle: Drop {
7 fun drop(&var self) { }
8}
9
10fun main() {
11 let handle := Handle { name = "x", fd = 1 };
12 let name := handle.name;
13}
typecheck errorT0019“belongs to a `Drop` type”
1aspect Marker {}
2struct Guard<T> { name: String, tag: T }
3extend<T> Guard<T>: Drop where T: Marker {
4 fun drop(&var self) {}
5}
6
7fun denied<T: Marker>(value: Guard<T>) -> String {
8 value.name // ERROR[T0019]
9}
10
11fun main() {}
typecheck errorT0019“belongs to a `Drop` type”
Legality Rule №3
Assigning a value to a field that was moved out restores that field's own accessibility. Once every field ever moved out of a value has been reassigned this way, the value's whole-value status is restored too, and it may be used as a whole again; reassigning only some of several moved-out fields is not enough.
Tested by (2)
1struct Pair {
2 left: String,
3 right: String,
4}
5
6fun main() {
7 var p := Pair { left = "a", right = "b" };
8 let taken := p.left;
9 p.left := "c";
10 let whole := p;
11 assert(taken == "a");
12 assert(whole.left == "c");
13}
passes
1struct Two {
2 left: String,
3 right: String,
4}
5
6fun take(t: Two) -> i64 {
7 t.left.len()
8}
9
10fun main() {
11 var t := Two { left = "a", right = "b" };
12 let taken_left := t.left;
13 let taken_right := t.right;
14 t.left := "c";
15 // t.right is still moved out -- reassigning only one of two moved fields does
16 // not restore whole-value status; `t` stays partially moved.
17 let n := take(t);
18}
typecheck errorT0001“partially-moved `Two`”
Legality Rule №4
Destructuring a struct or tuple with a pattern that binds a subset of its fields (a struct
pattern with .., a tuple pattern, a bound field of a matched variant's payload) moves
exactly those fields, leaving the scrutinee partially moved under the same rules as an
explicit field move — including the Drop-type ban (legality-2L2).
Tested by
1struct Handle {
2 name: String,
3 fd: i64,
4}
5
6extend Handle: Drop {
7 fun drop(&var self) { }
8}
9
10fun main() {
11 let handle := Handle { name = "x", fd = 1 };
12 let n := match (handle.name) {
13 name => name.len(),
14 };
15}
typecheck errorT0019“belongs to a `Drop` type”
--move-checkmoving a field out of a Drop type is now rejectedA Drop type may still be partially borrowed; only moving out is restricted.
GAP-OWNERSHIP-003RFC-0137legality-2's ban is enforced unconditionally; see Drop dispatch against a narrowed residual.Which constructs support partial moves
| construct | partial move |
|---|---|
| struct fields | yes, at field granularity |
| tuple elements | yes — positional fields are statically named |
| record fields | yes, at field granularityL2 |
| enum payloads | no — matching a variant and moving its payload consumes the enum wholly |
| array elements | no |
An array element cannot be moved out because the index may be computed at run time, so which element left is not a static fact.
Formal rules
Legality Rule №1
Tuple elements may be moved independently; moving an enum payload consumes its enum wholly;
array elements may not be moved out; and a non-Copy closure capture moves its enclosing binding.
Referenced by: rfc-0071
Tested by (4)
1fun main() {
2 let pair := ("x", 1);
3 let left := pair.0;
4 let again := pair.0;
5}
typecheck errorT0019“`pair.0` was moved”
1enum MaybeText {
2 Empty,
3 Full { text: String },
4}
5
6fun main() {
7 let value := MaybeText::Full { text = "x" };
8 let n := match (value) {
9 MaybeText::Full { text } => text.len(),
10 MaybeText::Empty => 0,
11 };
12 let again := value;
13}
typecheck errorT0019“use of moved value `value`”
1fun main() {
2 let xs := ["x"];
3 let first := xs[0];
4}
typecheck errorT0019“array element moves are not allowed”
1fun main() {
2 let s := "hello";
3 let f := [s] once || -> String { return s; };
4 let again := s;
5}
typecheck errorT0019“use of moved value `s`”
Legality Rule №2
Record fields may be moved independently, at field granularity like struct fields; a moved field's siblings remain individually accessible. Using the record value at its original wider type is rejected; whole-value use at its residual type is legal. Moving a field narrows the record's static type to the fields that remain (narrowing.legality-1L1, RFC-0117) — the same mechanism struct narrowing uses, minus the brand.
Tested by (2)
1// RFC-0117 (metel-core#789): moving a non-`Copy` field out of an anonymous
2// record narrows the record's static type to the fields that remain -- the same
3// mechanism struct narrowing uses (RFC-0137), minus the brand. The narrowed
4// record is an ordinary value: its siblings stay readable and it fits a
5// parameter whose row matches exactly.
6
7fun right_of(r: { right: i64 }) -> i64 { r.right }
8
9fun main() {
10 let r := { left = "a".to_string(), right = 7 };
11 let taken := r.left; // r : { right: i64 } from here on
12 assert(r.right == 7); // sibling still readable
13 assert(right_of(r) == 7); // exact-row parameter accepts the narrowed record
14
15 // A `Copy` field read by value is a copy, not a move -- no narrowing.
16 let pt := { x = 1, y = 2 };
17 let x_copy := pt.x;
18 assert(pt.x + pt.y == 3); // pt is still the whole record
19 assert(x_copy == 1);
20
21 println(taken);
22}
passes
Narrowing
Every struct is represented, for type-checking purposes, as a fixed nominal identity
(its brand, minted once at declaration) paired with its current row — the set of
fields still present.
h.{ fd } is a move of the named fields that keeps the brand: a Copy field is copied,
a non-Copy field is moved out of h, and h narrows by the fields moved, exactly as
for let n := h.name;. It produces a residual of h's own brand, not a same-shaped
anonymous record (and not a bare field value, which is what the plain move yields):
struct Handle { fd: i64, name: String }
extend Handle {
fun describe(h: Self.{ fd }) -> i64 { h.fd }
}
fun main() -> i64 {
let handle := Handle { fd = 3, name = "x" };
return Handle::describe(handle.{ fd }); // OK -- branded Handle.{ fd }
// Handle::describe({ fd = 3 }) // rejected -- no brand, T0001
}
A projection naming every field the struct declares normalizes back to the plain
struct type instead of staying a distinct residual — h.{ fd, name } here is just
Handle, still rejected by a row bound the same way a bare Handle value already is.
For a struct (RFC-0137 slice 2, metel-core#858), h.name produces the same branded
residual type, h.{ fd }, as a projection does. For an anonymous record (RFC-0117,
metel-core#789), moving r.left out leaves r : { right: i64 }. Using the narrowed value
where the whole type or a wider row is required is a type error at type-check time, not only
a --move-check finding.
The residual is an ordinary value: it can be bound, passed, returned, dropped, and
narrowed again. For a value over N fields, the space of residual shapes is the subset
lattice, bounded by 2^N — there is no row variable and no unification involved in
computing it. The rule applies uniformly to a nominal struct's row (residual of the
same brand, Handle.{ fd }) and to an anonymous record's row (the record type with
the moved label removed, { fd: i64 } — no brand clause). A record-typed field is
moved as a unit — a residual's row never carries a narrower type for a field it
still holds; narrowing a field of a field in place is
RFC-0150's. A field read by
value whose type is Copy is a copy, not a move, and does not narrow; a field whose type
is a bare generic parameter or is not yet resolved is held (not dropped from the row)
until its type is known.
Difference between the two. A struct residual is a distinct type (
Type::Residual, a brand plus a strict subset row), so a whole-value use after a partial move reports against the binding by name — "a partially-movedHandle…". An anonymous record residual is just aRecordwith fewer fields, structurally identical to any other narrower record, so the same mistake reports as an ordinary record-shape mismatch ("cannot unify{ right }with{ left, right }"). Both are type errors at type-check time.
An anonymous record narrows in the same way, and reading the moved-out label is rejected:
fun main() {
let r := { left = "l", right = "r" };
let l := r.left; // r : { right: String }
println(r.right); // fine: `right` is still present
println(r.left); // error: no field `left` on { right: String }
}
Narrowing is path-sensitive: the residual type at a program point reflects the fields
moved on every path reaching it, exactly as move tracking already computes — a field
moved on one arm of an if is conservatively moved after the join. A move made inside a
loop body narrows the value after the loop. A use within the body that only becomes
invalid on a later iteration is still surfaced by --move-check rather than as a
narrowing type error. Narrowing adds no control-flow analysis of its own; it is the
type-level reading of the move state.
A residual's row is never visible to structural matching, regardless of its width.
This is unchanged from today's rule that only a record (not a struct) satisfies a
row boundGenerics L4 — eligibility for
structural matching is scoped to the brand alone, fixed at declaration, never to row
content. A struct value narrowed down to every one of its own fields is still,
unambiguously, that struct — not a same-shaped anonymous record, and not a
record-declared type of the same shape.
Formal rules
Legality Rule №1
GAP-OWNERSHIP-002Moving root.a narrows root's type, but moving root.a.b does not: a record-typed field moves as a unit, so the type checker still treats root as whole.Moving a field out of a value narrows its type to a row with that field removed: a
same-brand residual for a struct, the record type minus that label for an anonymous
record. A Copy field read by value is a copy, not a move, and does not narrow; a field
of unresolved or generic type is held until its type is known. Narrowing is
path-sensitive, joined conservatively at merge points and loop fixpoints, matching move
tracking.
Referenced by: rfc-0117, rfc-0137
Tested by (11)
1// RFC-0137 slice 2 (metel-core#858): moving a non-`Copy` field out of a struct
2// narrows the value's *type* to a residual of the same brand -- `Handle` becomes
3// `Handle.{ fd }` -- and that residual is exactly the one an explicit projection
4// `h.{ fd }` produces, so the two are interchangeable at a `Self.{ fd }`
5// parameter (spec.ownership.narrowing.dynamics-1). With `--move-check` on, a
6// whole-value use of the narrowed value is *not* flagged as a partial-move
7// violation (metel-core#950) -- narrowing removed exactly the moved field.
8
9struct Handle { fd: i64, name: String }
10
11extend Handle {
12 fun describe(h: &Self.{ fd }) -> i64 { h.fd }
13}
14
15fun main() {
16 // Route A: a partial move narrows `h` in place; a borrowed whole-value use
17 // of the narrowed value is accepted, projection and move producing the same
18 // residual type.
19 let h := Handle { fd = 7, name = "a" };
20 let taken := h.name; // h : Handle.{ fd } from here on
21 assert(h.fd == 7); // the sibling field stays readable
22 assert(Handle::describe(&h) == 7); // narrowed value fits `&Self.{ fd }`
23 assert(Handle::describe(&h.{ fd }) == 7); // re-projecting the residual: same type
24
25 // Route B: an explicit projection off a fresh value produces the same type.
26 let h2 := Handle { fd = 7, name = "b" };
27 assert(Handle::describe(&h2.{ fd }) == 7);
28
29 println(taken);
30}
passes
1// RFC-0117 (metel-core#789): moving a non-`Copy` field out of an anonymous
2// record narrows the record's static type to the fields that remain -- the same
3// mechanism struct narrowing uses (RFC-0137), minus the brand. The narrowed
4// record is an ordinary value: its siblings stay readable and it fits a
5// parameter whose row matches exactly.
6
7fun right_of(r: { right: i64 }) -> i64 { r.right }
8
9fun main() {
10 let r := { left = "a".to_string(), right = 7 };
11 let taken := r.left; // r : { right: i64 } from here on
12 assert(r.right == 7); // sibling still readable
13 assert(right_of(r) == 7); // exact-row parameter accepts the narrowed record
14
15 // A `Copy` field read by value is a copy, not a move -- no narrowing.
16 let pt := { x = 1, y = 2 };
17 let x_copy := pt.x;
18 assert(pt.x + pt.y == 3); // pt is still the whole record
19 assert(x_copy == 1);
20
21 println(taken);
22}
passes
1// RFC-0137 / RFC-0117 (metel-core#950): with `--move-check` on, a whole-value use
2// of a binding whose type has narrowed to a residual / narrower record is legal
3// -- narrowing removed exactly the moved fields, so the use touches none of them.
4// Before #950, `move_check` flagged every whole-value use of a partially-moved
5// binding regardless of its current type.
6
7struct Handle { fd: i64, name: String }
8fun take_fd(h: Handle.{ fd }) -> i64 { h.fd }
9fun right_of(r: { right: i64 }) -> i64 { r.right }
10
11fun main() {
12 // Struct: narrowed to Handle.{ fd }, then moved in by value once.
13 let h := Handle { fd = 3, name = "x" };
14 let hn := h.name;
15 assert(take_fd(h) == 3);
16
17 // Anonymous record: narrowed to { right: i64 }, then moved in by value once.
18 let r := { left = "a".to_string(), right = 9 };
19 let rl := r.left;
20 assert(right_of(r) == 9);
21
22 // A narrowed binding read (not moved) as a whole is fine too.
23 let g := Handle { fd = 4, name = "y" };
24 let gn := g.name;
25 let alias := g.{ fd };
26 assert(alias.fd == 4);
27
28 println("${hn} ${rl} ${gn}");
29}
passes
1// metel-core#958: row-narrowing move state is path-sensitive across `if` arms.
2// Both arms move the same non-`Copy` field out of `rec`; the `else` arm does
3// not see the `then` arm's move, so each is an independent partial move. After
4// the `if` the arms join: `rec` is narrowed to `{ keep: i64 }` on every path,
5// its surviving field stays readable, and a whole-value use at the narrowed
6// row is accepted (also under --move-check).
7fun keep_of(r: { keep: i64 }) -> i64 { r.keep }
8
9fun main() {
10 let cond := true;
11 let rec := { gone = "x".to_string(), keep = 3 };
12 if (cond) {
13 let a := rec.gone;
14 assert(a == "x");
15 } else {
16 let b := rec.gone;
17 assert(b == "x");
18 }
19 assert(rec.keep == 3); // surviving field readable at the joined row
20 assert(keep_of(rec) == 3); // whole value fits the narrowed row
21 println("ok");
22}
passes
1// metel-core#958: the same per-arm fork/join for `match`. Two arms each move
2// the same non-`Copy` field of an outer binding; a later arm does not see an
3// earlier arm's move. The arms join after the `match`, narrowing `rec` to
4// `{ keep: i64 }`.
5fun keep_of(r: { keep: i64 }) -> i64 { r.keep }
6
7fun main() {
8 let sel := 2;
9 let rec := { gone = "y".to_string(), keep = 7 };
10 let tag := match (sel) {
11 1 => { let a := rec.gone; 10 },
12 2 => { let b := rec.gone; 20 },
13 _ => { let c := rec.gone; 30 },
14 };
15 assert(tag == 20);
16 assert(rec.keep == 7);
17 assert(keep_of(rec) == 7);
18 println("ok");
19}
passes
1fun take(r: { left: String, right: i64 }) -> i64 {
2 r.right
3}
4
5fun main() {
6 let r := { left = "a".to_string(), right = 1 };
7 let left: String := r.left;
8 let value: i64 := take(r);
9}
typecheck errorT0001“cannot unify”
1struct Two {
2 left: String,
3 right: String,
4}
5
6fun take(t: Two) -> i64 {
7 t.left.len()
8}
9
10fun main() {
11 var t := Two { left = "a", right = "b" };
12 let taken_left := t.left;
13 let taken_right := t.right;
14 t.left := "c";
15 // t.right is still moved out -- reassigning only one of two moved fields does
16 // not restore whole-value status; `t` stays partially moved.
17 let n := take(t);
18}
typecheck errorT0001“partially-moved `Two`”
1// RFC-0117 (metel-core#789): once a field is moved out of an anonymous record,
2// the record's type is the narrower row -- `{ right: i64 }`, not `{ left, right }`.
3// Passing it where the whole record is required is a plain type error at
4// inference time, no longer only a `--move-check` finding. A narrowed record has
5// no distinct type marker, so the diagnostic is the ordinary record-shape
6// mismatch.
7
8fun wants_full(r: { left: String, right: i64 }) -> i64 { r.right }
9
10fun main() {
11 let r := { left = "a".to_string(), right = 1 };
12 let taken := r.left;
13 let _ := wants_full(r);
14 println(taken);
15}
typecheck errorT0001“cannot unify”
1// metel-core#958: the join is the *union* of the arms' moves. Only the `then`
2// arm moves `rec.gone`; after the `if`, `rec` is narrowed to `{ keep: i64 }` on
3// every path (the move is joined in even though the `else` path didn't run it),
4// so a whole-value use at the wider row is rejected.
5fun whole(r: { gone: String, keep: i64 }) -> i64 { r.keep }
6
7fun main() {
8 let cond := true;
9 let rec := { gone = "z".to_string(), keep = 1 };
10 if (cond) {
11 let a := rec.gone;
12 }
13 whole(rec) // rec : { keep: i64 } here -- wider row required
14}
typecheck errorT0001“cannot unify”
1// v0.13.0 cross-feature (integration session, metel-core#956): closure capture
2// (RFC-0157 D5) meets move-triggered struct row narrowing (RFC-0137 slice 2).
3// A non-`Copy` field is moved out first, narrowing `h` to `Handle.{ fd }`; the
4// closure then captures the *narrowed* value by value. The capture list names
5// `h`, the residual moves into the environment once, and `--move-check` is
6// clean -- narrowing already removed the field that left.
7struct Handle { fd: i64, name: String }
8
9fun main() {
10 let h := Handle { fd = 7, name = "n" };
11 let taken := h.name; // h : Handle.{ fd }
12 let get := [h] once || { h.fd }; // captures the residual by value
13 assert(get() == 7);
14 println(taken);
15}
passes
1// Cross-feature (v0.13.0): a `match (h)` (RFC-0156 parenthesized scrutinee) binds
2// a non-`Copy` field out of a struct value through a struct pattern
3// (metel-core#753). That partial move narrows `h` (RFC-0137 slice 2): the moved
4// field is gone, every other field stays readable, and reassigning the moved
5// field widens `h` back to the whole struct.
6
7struct Handle { id: i64, name: String }
8
9fun main() {
10 var h := Handle { id = 7, name = "fd".to_string() };
11
12 // bind and consume `name` via a struct pattern; `h` is now `Handle.{ id }`
13 let taken := match (h) { Handle { name, .. } => name };
14 assert(taken == "fd");
15
16 // a still-present field is readable on the narrowed value
17 assert(h.id == 7);
18
19 // reassigning the moved field widens `h` back to the whole `Handle`
20 h.name := "fd2".to_string();
21 assert(h.name == "fd2");
22 assert(h.id == 7);
23
24 println("ok");
25}
passes
Legality Rule №2
A residual's row is never visible to structural matching; only its brand, fixed at declaration, determines eligibility, regardless of how narrow or wide the current row is.
Referenced by: rfc-0117, rfc-0137
Tested by (2)
1// Regression (metel-core#857, RFC-0137 slice 1): this is the actual motivating bug
2// -- Self.{ fd } used to accept a bare anonymous record literal of the same shape
3// exactly as readily as a value actually derived from a real Handle, since the
4// projection resolved to an unbranded record type. Now rejected: a struct's own
5// projection is branded, and a same-shaped anonymous record never carries that
6// brand.
7
8struct Handle { fd: i64, name: String }
9
10extend Handle {
11 fun describe(h: Self.{ fd }) -> i64 { h.fd }
12}
13
14fun main() {
15 let _ := Handle::describe({ fd = 3 });
16}
typecheck errorT0001
1// Regression (metel-core#857, RFC-0137 slice 1): a genuine (non-full-width) branded
2// residual of a plain `struct` never satisfies a row bound either -- eligibility
3// for structural matching is scoped to the brand alone (RFC-0137 sec3), and a
4// `struct`'s brand is never visible to matching regardless of how narrow its
5// current row is. A `record`'s residual is eligible (RFC-0120 sec3/sec-declarations-
6// records-legality-2) -- that is tested separately, not a contradiction of this one.
7
8struct Handle { fd: i64, name: String, extra: i64 }
9
10fun wants_a_record<record T: { fd: i64, .. }>(t: T) -> i64 { t.fd }
11
12fun main() {
13 let h := Handle { fd = 3, name = "x", extra = 9 };
14 let _ := wants_a_record(h.{ fd });
15}
typecheck errorT0012“struct never satisfies a row bound”
Legality Rule №3
A projection or a residual naming every field the struct declares is not a distinct residual type — it normalizes back to the plain struct type, and is rejected by a row bound exactly as a bare struct value already is. A residual's row is therefore always a strict subset of the brand's declared row, possibly empty. A nominal type declaring no fields has a full-width empty row and remains the plain nominal type.
Write D(B) for a nominal brand's declared field-to-type map and res(B, R)
for its normalized type at current row R, where R is a restriction of D(B).
Normalization is defined by:
res(B, R) = B if R = D(B)
res(B, R) = B.{R} if R is a strict subset of D(B)
Here B.{R} denotes the branded residual whose labels are those of R;
it is not additional source syntax. Thus res(B, {}) = B.{} when D(B)
is nonempty, but res(B, {}) = B when D(B) = {}. For anonymous rows,
res(anonymous, R) = R. Different brands remain distinct at every width,
including zero; neither empty form is Unit.
Tested by (6)
1struct Pair { left: String, right: String }
2record NamedPair { left: String, right: String }
3struct Zero {}
4fun empty_pair(p: Pair.{}) -> Pair.{} { p }
5fun empty_named(p: NamedPair.{}) -> NamedPair.{} { p }
6fun empty_record(r: {}) -> {} { r }
7fun full_pair(p: Pair) -> String { p.left }
8fun main() {
9 var p := Pair { left = "l", right = "r" };
10 let l := p.left;
11 let r := p.right;
12 p.left := "restored";
13 p.right := "again";
14 assert(full_pair(p) == "restored");
15 var a := { left = "l", right = "r" };
16 let al := a.left;
17 let ar := a.right;
18 let ae: {} := empty_record(a);
19 a.left := "back";
20 a.right := "also";
21 assert(a.left == "back");
22 let n := NamedPair { left = "l", right = "r" };
23 let nl := n.left;
24 let nr := n.right;
25 let ne: NamedPair.{} := empty_named(n);
26 let q := Pair { left = "q", right = "s" };
27 let ql := q.left;
28 let qr := q.right;
29 let qe: Pair.{} := empty_pair(q);
30 let qe_again: Pair.{} := empty_pair(qe);
31 let copied := { text = "gone", count = 7 };
32 let text := copied.text;
33 assert(copied.count == 7);
34 let zero: Zero := Zero {};
35 let normalized: Zero.{} := zero;
36 println("ok");
37}
passes
1struct Pair { left: String, right: String }
2record NamedPair { left: String, right: String }
3struct Zero {}
4fun empty_pair(p: Pair.{}) -> Pair.{} { p }
5fun empty_named(p: NamedPair.{}) -> NamedPair.{} { p }
6fun empty_record(r: {}) -> {} { r }
7fun full_pair(p: Pair) -> String { p.left }
8fun main() {
9 var p := Pair { left = "l", right = "r" };
10 let l := p.left;
11 let r := p.right;
12 p.left := "restored";
13 p.right := "again";
14 assert(full_pair(p) == "restored");
15 var a := { left = "l", right = "r" };
16 let al := a.left;
17 let ar := a.right;
18 let ae: {} := empty_record(a);
19 a.left := "back";
20 a.right := "also";
21 assert(a.left == "back");
22 let n := NamedPair { left = "l", right = "r" };
23 let nl := n.left;
24 let nr := n.right;
25 let ne: NamedPair.{} := empty_named(n);
26 let q := Pair { left = "q", right = "s" };
27 let ql := q.left;
28 let qr := q.right;
29 let qe: Pair.{} := empty_pair(q);
30 let qe_again: Pair.{} := empty_pair(qe);
31 let copied := { text = "gone", count = 7 };
32 let text := copied.text;
33 assert(copied.count == 7);
34 let zero: Zero := Zero {};
35 let normalized: Zero.{} := zero;
36 println("ok");
37}
passes
1struct A { value: String }
2struct B { value: String }
3fun take(x: B.{}) {}
4fun main() {
5 let a := A { value = "owned" };
6 let value := a.value;
7 take(a); // ERROR[T0001]
8}
typecheck errorT0001at 7
1struct A { value: String }
2struct B { value: String }
3fun take(x: B.{}) {}
4fun main() {
5 let a := A { value = "owned" };
6 let value := a.value;
7 take(a); // ERROR[T0001]
8}
typecheck errorT0001at 7
1struct Pair { left: String, right: String }
2type Empty := Pair.{};
3type Callback := once || -> Pair;
4
5fun empty() -> Pair.{} {
6 let pair := Pair { left = "old", right = "gone" };
7 let left := pair.left;
8 let right := pair.right;
9 pair
10}
11
12fun rebuild(empty: Pair.{}) -> Pair {
13 var restored := empty;
14 restored.left := "new";
15 restored.right := "back";
16 restored
17}
18
19fun captured(empty: Empty) -> Pair {
20 let callback: Callback := [empty] once || {
21 var restored := empty;
22 restored.left := "new";
23 restored.right := "back";
24 restored
25 };
26 callback()
27}
28
29fun written(empty: Pair.{}) -> Pair {
30 let callback := [empty] once || -> Pair {
31 var restored := empty;
32 restored.left := "new";
33 restored.right := "back";
34 restored
35 };
36 callback()
37}
38
39fun main() {
40 assert(rebuild(empty()).right == "back");
41 assert(captured(empty()).left == "new");
42 assert(written(empty()).right == "back");
43}
passes
1// Regression (metel-core#857, RFC-0137 slice 1's own normalization rule, and
2// RFC-0137 sec3's worked example): a projection naming every field a struct
3// declares normalizes back to the plain struct type rather than staying a
4// distinct branded residual. Confirms the normalization doesn't accidentally
5// earn row-bound eligibility -- h.{ fd, name }, full width, is rejected by a row
6// bound the exact same way a bare `Handle` value already is.
7
8struct Handle { fd: i64, name: String }
9
10fun wants_a_record<record T: { fd: i64, name: String, .. }>(t: T) -> i64 { t.fd }
11
12fun main() {
13 let h := Handle { fd = 3, name = "x" };
14 let _ := wants_a_record(h.{ fd, name });
15}
typecheck errorT0012“struct never satisfies a row bound”
Legality Rule №4
--move-check agreement: metel-core#950Using a narrowed value where a wider row, or the whole type, is required is a type error
at type-check time, not deferred to --move-check; every still-present field stays
readable and its methods callable. A whole-value use at the narrowed type — moving it,
binding it, passing it to a matching-row parameter — is legal, and --move-check does not
flag it.
Moving the last remaining non-Copy field leaves an empty residual. An anonymous
record has type {}; a nominal struct or record retains its brand with an empty
row, written Name.{}. Neither becomes Unit, and a branded empty residual does
not become an anonymous record. Fields read by copying remain in the row.
Using a field that was moved out of a nominal struct or record, by reading it or by
projecting it again, is a T0019 use of a moved value, including when the row is empty.
Naming a label the type never declared, or any label absent from an anonymous record
residual (which no longer remembers what it had), remains a T0003 unknown-field error.
Both are reported independently of --move-check.
An empty residual may be bound, passed, and returned wherever its exact residual
type is accepted. It does not satisfy the original non-empty type or a wider row;
structural eligibility and visibility are unchanged. Consuming its remaining
fields is distinct from moving the residual binding as a whole. A subsequent
whole-binding move obeys the ordinary ownership rules, whose use-after-move
enforcement remains controlled by --move-check.
Let Γ(p) = res(B, R) describe an available place's current row, with B
either a nominal brand or anonymous. Let R[f ↦ T] extend a row not
containing f. For an otherwise legal by-value field use, the row transition is:
Γ(p) = res(B, R[f ↦ T]) T is known T: !Copy
------------------------------------------------ consume-field
Γ ⊢ consume(p.f): T ⇒ Γ[p ↦ res(B, R)]
Γ(p) = res(B, R[f ↦ T]) T: Copy
----------------------------------------------- copy-field
Γ ⊢ read(p.f): T ⇒ Γ
Γ(p) = res(B, R) f ∉ dom(R) B nominal B declares f
----------------------------------------------- moved-field
Γ ⊢ read(p.f) ⇒ T0019
Γ(p) = res(B, R) f ∉ dom(R) otherwise
----------------------------------------------- absent-field
Γ ⊢ read(p.f) ⇒ T0003
The consume-field conclusion includes R = {}. These judgments do not
grant permission to move from a borrowed place or a Drop type. An unresolved
field type is held under legality-1L1.
The moved-field and absent-field judgments and the row transition apply with or without
move checking.
Ordinary binding, argument, and return typing may use res(B, {}) at that
same type. No empty-residual rule supplies missing fields, erases B, or
coerces the result to Unit. A whole-binding consumption updates ownership
state separately: when move checking is enabled, consuming a non-Copy
residual marks its binding moved, and another whole use reports T0019;
consuming its last field does not itself mark that binding wholly moved.
Tested by (40)
1struct Pair {
2 left: String,
3 right: i64,
4}
5
6fun take(pair: Pair) -> i64 {
7 pair.right
8}
9
10fun main() {
11 let pair := Pair { left = "a", right = 1 };
12 let left: String := pair.left;
13 let value: i64 := take(pair);
14}
typecheck errorT0001“partially-moved `Pair`”
1// RFC-0137 / RFC-0117 (metel-core#950): with `--move-check` on, a whole-value use
2// of a binding whose type has narrowed to a residual / narrower record is legal
3// -- narrowing removed exactly the moved fields, so the use touches none of them.
4// Before #950, `move_check` flagged every whole-value use of a partially-moved
5// binding regardless of its current type.
6
7struct Handle { fd: i64, name: String }
8fun take_fd(h: Handle.{ fd }) -> i64 { h.fd }
9fun right_of(r: { right: i64 }) -> i64 { r.right }
10
11fun main() {
12 // Struct: narrowed to Handle.{ fd }, then moved in by value once.
13 let h := Handle { fd = 3, name = "x" };
14 let hn := h.name;
15 assert(take_fd(h) == 3);
16
17 // Anonymous record: narrowed to { right: i64 }, then moved in by value once.
18 let r := { left = "a".to_string(), right = 9 };
19 let rl := r.left;
20 assert(right_of(r) == 9);
21
22 // A narrowed binding read (not moved) as a whole is fine too.
23 let g := Handle { fd = 4, name = "y" };
24 let gn := g.name;
25 let alias := g.{ fd };
26 assert(alias.fd == 4);
27
28 println("${hn} ${rl} ${gn}");
29}
passes
1// metel-core#958: row-narrowing move state is path-sensitive across `if` arms.
2// Both arms move the same non-`Copy` field out of `rec`; the `else` arm does
3// not see the `then` arm's move, so each is an independent partial move. After
4// the `if` the arms join: `rec` is narrowed to `{ keep: i64 }` on every path,
5// its surviving field stays readable, and a whole-value use at the narrowed
6// row is accepted (also under --move-check).
7fun keep_of(r: { keep: i64 }) -> i64 { r.keep }
8
9fun main() {
10 let cond := true;
11 let rec := { gone = "x".to_string(), keep = 3 };
12 if (cond) {
13 let a := rec.gone;
14 assert(a == "x");
15 } else {
16 let b := rec.gone;
17 assert(b == "x");
18 }
19 assert(rec.keep == 3); // surviving field readable at the joined row
20 assert(keep_of(rec) == 3); // whole value fits the narrowed row
21 println("ok");
22}
passes
1// metel-core#958: the same per-arm fork/join for `match`. Two arms each move
2// the same non-`Copy` field of an outer binding; a later arm does not see an
3// earlier arm's move. The arms join after the `match`, narrowing `rec` to
4// `{ keep: i64 }`.
5fun keep_of(r: { keep: i64 }) -> i64 { r.keep }
6
7fun main() {
8 let sel := 2;
9 let rec := { gone = "y".to_string(), keep = 7 };
10 let tag := match (sel) {
11 1 => { let a := rec.gone; 10 },
12 2 => { let b := rec.gone; 20 },
13 _ => { let c := rec.gone; 30 },
14 };
15 assert(tag == 20);
16 assert(rec.keep == 7);
17 assert(keep_of(rec) == 7);
18 println("ok");
19}
passes
1struct S { a: String }
2fun anonymous(r: {}) {}
3fun main() {
4 let s := S { a = "a" };
5 let x := s.a;
6 anonymous(s); // ERROR[T0001]
7}
typecheck errorT0001at 6
1struct S { a: String }
2fun anonymous(r: {}) {}
3fun main() {
4 let s := S { a = "a" };
5 let x := s.a;
6 anonymous(s); // ERROR[T0001]
7}
typecheck errorT0001at 6
1struct Pair { left: String, right: String }
2fun invalid(empty: Pair.{}) -> String {
3 let callback := [empty] once || -> String { empty.left }; // ERROR[T0019]
4 callback()
5}
6fun main() {}
typecheck errorT0019
1struct Pair { left: String, right: String }
2record NamedPair { left: String, right: String }
3struct Zero {}
4fun empty_pair(p: Pair.{}) -> Pair.{} { p }
5fun empty_named(p: NamedPair.{}) -> NamedPair.{} { p }
6fun empty_record(r: {}) -> {} { r }
7fun full_pair(p: Pair) -> String { p.left }
8fun main() {
9 var p := Pair { left = "l", right = "r" };
10 let l := p.left;
11 let r := p.right;
12 p.left := "restored";
13 p.right := "again";
14 assert(full_pair(p) == "restored");
15 var a := { left = "l", right = "r" };
16 let al := a.left;
17 let ar := a.right;
18 let ae: {} := empty_record(a);
19 a.left := "back";
20 a.right := "also";
21 assert(a.left == "back");
22 let n := NamedPair { left = "l", right = "r" };
23 let nl := n.left;
24 let nr := n.right;
25 let ne: NamedPair.{} := empty_named(n);
26 let q := Pair { left = "q", right = "s" };
27 let ql := q.left;
28 let qr := q.right;
29 let qe: Pair.{} := empty_pair(q);
30 let qe_again: Pair.{} := empty_pair(qe);
31 let copied := { text = "gone", count = 7 };
32 let text := copied.text;
33 assert(copied.count == 7);
34 let zero: Zero := Zero {};
35 let normalized: Zero.{} := zero;
36 println("ok");
37}
passes
1struct Pair { left: String, right: String }
2record NamedPair { left: String, right: String }
3struct Zero {}
4fun empty_pair(p: Pair.{}) -> Pair.{} { p }
5fun empty_named(p: NamedPair.{}) -> NamedPair.{} { p }
6fun empty_record(r: {}) -> {} { r }
7fun full_pair(p: Pair) -> String { p.left }
8fun main() {
9 var p := Pair { left = "l", right = "r" };
10 let l := p.left;
11 let r := p.right;
12 p.left := "restored";
13 p.right := "again";
14 assert(full_pair(p) == "restored");
15 var a := { left = "l", right = "r" };
16 let al := a.left;
17 let ar := a.right;
18 let ae: {} := empty_record(a);
19 a.left := "back";
20 a.right := "also";
21 assert(a.left == "back");
22 let n := NamedPair { left = "l", right = "r" };
23 let nl := n.left;
24 let nr := n.right;
25 let ne: NamedPair.{} := empty_named(n);
26 let q := Pair { left = "q", right = "s" };
27 let ql := q.left;
28 let qr := q.right;
29 let qe: Pair.{} := empty_pair(q);
30 let qe_again: Pair.{} := empty_pair(qe);
31 let copied := { text = "gone", count = 7 };
32 let text := copied.text;
33 assert(copied.count == 7);
34 let zero: Zero := Zero {};
35 let normalized: Zero.{} := zero;
36 println("ok");
37}
passes
1record S { a: String, b: String }
2fun main() {
3 let s := S { a = "a", b = "b" };
4 let x := s.a;
5 let y := s.b;
6 println(s.a); // ERROR[T0019]
7}
typecheck errorT0019at 6
1record S { a: String, b: String }
2fun main() {
3 let s := S { a = "a", b = "b" };
4 let x := s.a;
5 let y := s.b;
6 println(s.a); // ERROR[T0019]
7}
typecheck errorT0019at 6
1struct Pair { left: String, right: String }
2type Empty := Pair.{};
3type Callback := once || -> Pair;
4
5fun empty() -> Pair.{} {
6 let pair := Pair { left = "old", right = "gone" };
7 let left := pair.left;
8 let right := pair.right;
9 pair
10}
11
12fun rebuild(empty: Pair.{}) -> Pair {
13 var restored := empty;
14 restored.left := "new";
15 restored.right := "back";
16 restored
17}
18
19fun captured(empty: Empty) -> Pair {
20 let callback: Callback := [empty] once || {
21 var restored := empty;
22 restored.left := "new";
23 restored.right := "back";
24 restored
25 };
26 callback()
27}
28
29fun written(empty: Pair.{}) -> Pair {
30 let callback := [empty] once || -> Pair {
31 var restored := empty;
32 restored.left := "new";
33 restored.right := "back";
34 restored
35 };
36 callback()
37}
38
39fun main() {
40 assert(rebuild(empty()).right == "back");
41 assert(captured(empty()).left == "new");
42 assert(written(empty()).right == "back");
43}
passes
1struct Pair { left: String, right: String }
2fun rebuild(empty: Pair.{}) -> Pair {
3 var restored := empty;
4 restored.left := "new";
5 restored // ERROR[T0001]
6}
7fun main() {}
typecheck errorT0001
1fun main() {
2 let r := { left = "l", right = "r" };
3 let x := r.left;
4 let y := r.right;
5 println(r.left); // ERROR[T0003]
6}
typecheck errorT0003at 5
1fun main() {
2 let r := { left = "l", right = "r" };
3 let x := r.left;
4 let y := r.right;
5 println(r.left); // ERROR[T0003]
6}
typecheck errorT0003at 5
1struct S { a: String, b: String }
2fun main() {
3 let s := S { a = "a", b = "b" };
4 let x := s.a;
5 let y := s.b;
6 println(s.a); // ERROR[T0019]
7}
typecheck errorT0019at 6
1struct S { a: String, b: String }
2fun main() {
3 let s := S { a = "a", b = "b" };
4 let x := s.a;
5 let y := s.b;
6 println(s.a); // ERROR[T0019]
7}
typecheck errorT0019at 6
1fun take(x: ()) {}
2fun main() {
3 let r := { value = "owned" };
4 let value := r.value;
5 take(r); // ERROR[T0001]
6}
typecheck errorT0001at 5
1fun take(x: ()) {}
2fun main() {
3 let r := { value = "owned" };
4 let value := r.value;
5 take(r); // ERROR[T0001]
6}
typecheck errorT0001at 5
1struct Pair { left: String, right: String }
2fun take(p: Pair.{}) {}
3fun main() {
4 let p := Pair { left = "l", right = "r" };
5 let l := p.left;
6 let r := p.right;
7 take(p);
8 take(p); // ERROR[T0019]
9}
typecheck errorT0019at 8
1struct S { a: String }
2fun full(s: S) {}
3fun main() {
4 let s := S { a = "a" };
5 let x := s.a;
6 full(s); // ERROR[T0001]
7}
typecheck errorT0001at 6
1struct S { a: String }
2fun full(s: S) {}
3fun main() {
4 let s := S { a = "a" };
5 let x := s.a;
6 full(s); // ERROR[T0001]
7}
typecheck errorT0001at 6
1// RFC-0137 slice 2 (metel-core#858): once a field is moved out, the value's type
2// is the residual -- `Handle.{ fd }` -- not the whole `Handle`. Passing it where
3// the whole struct is required is a plain type error at inference time, no longer
4// only a `--move-check` finding.
5
6struct Handle { fd: i64, name: String }
7
8fun wants_full(h: Handle) -> i64 { h.fd }
9
10fun main() {
11 let h := Handle { fd = 3, name = "x" };
12 let taken := h.name;
13 let _ := wants_full(h); // rejected: `h` is `Handle.{ fd }`
14 println(taken);
15}
typecheck errorT0001“partially-moved `Handle`”
1// RFC-0117 (metel-core#789): once a field is moved out of an anonymous record,
2// the record's type is the narrower row -- `{ right: i64 }`, not `{ left, right }`.
3// Passing it where the whole record is required is a plain type error at
4// inference time, no longer only a `--move-check` finding. A narrowed record has
5// no distinct type marker, so the diagnostic is the ordinary record-shape
6// mismatch.
7
8fun wants_full(r: { left: String, right: i64 }) -> i64 { r.right }
9
10fun main() {
11 let r := { left = "a".to_string(), right = 1 };
12 let taken := r.left;
13 let _ := wants_full(r);
14 println(taken);
15}
typecheck errorT0001“cannot unify”
1// metel-core#958: the join is the *union* of the arms' moves. Only the `then`
2// arm moves `rec.gone`; after the `if`, `rec` is narrowed to `{ keep: i64 }` on
3// every path (the move is joined in even though the `else` path didn't run it),
4// so a whole-value use at the wider row is rejected.
5fun whole(r: { gone: String, keep: i64 }) -> i64 { r.keep }
6
7fun main() {
8 let cond := true;
9 let rec := { gone = "z".to_string(), keep = 1 };
10 if (cond) {
11 let a := rec.gone;
12 }
13 whole(rec) // rec : { keep: i64 } here -- wider row required
14}
typecheck errorT0001“cannot unify”
1fun duplicate_rest<row R, row Rest>(value: { ..R }) -> ({ ..Rest }, { ..Rest })
2where R = { token: String, ..Rest }, all Rest: Copy {
3 let { token: _, ..rest } := value;
4 let first := rest;
5 let second := rest;
6 (first, second)
7}
8aspect Relay { fun pass<T>(self, value: T) -> T; }
9struct Courier {}
10extend Courier: Relay {
11 fun pass<T>(self, value: T) -> T { value }
12}
13fun extract<T>(value: { payload: T }) -> T {
14 let { payload, ..rest } := value;
15 let empty: {} := rest;
16 payload
17}
18struct Owned { text: String }
19fun forward<T>(value: T) -> T { value }
20fun main() {
21 assert(extract({ payload = "generic owned" }) == "generic owned");
22 assert(extract({ payload = 17 }) == 17);
23 let empty_pair := duplicate_rest({ token = "discarded" });
24 let left: {} := empty_pair.0;
25 let right: {} := empty_pair.1;
26 let pair := duplicate_rest({ token = "discarded", count = 8, enabled = true });
27 assert(pair.0.count == 8);
28 assert(pair.1.enabled);
29 let { token: _, ..empty } := { token = "owned" };
30 let forwarded: {} := Courier {}.pass(empty);
31 let data := { token = "discarded", payload = "kept" };
32 let var { token: _, ..tail } := data;
33 tail.payload := "restored";
34 assert(Courier {}.pass(tail).payload == "restored");
35 let owned := Owned { text = "removed" };
36 let text := owned.text;
37 let forwarded_nominal: Owned.{} := Courier {}.pass(forward(owned));
38 assert(text == "removed");
39}
passes
1record User { id: i64, name: String, count: i64 }
2type UserAlias := User;
3type Callback := once || -> i64;
4
5fun clone_head<row R>(value: { id: i64, ..R }) -> { id: i64, ..R }
6where all R: Clone {
7 value.clone()
8}
9
10fun main() {
11 let row_clone := clone_head({ id = 9 });
12 assert(row_clone.id == 9);
13 let row_clone_with_tail := clone_head({ id = 3, count = 5 });
14 assert(row_clone_with_tail.id + row_clone_with_tail.count == 8);
15
16 let user: UserAlias := User { id = 3, name = "moved", count = 5 };
17 let name := user.name;
18 let residual := user.clone();
19 assert(name == "moved");
20 assert(residual.id + residual.count == 8);
21 let callback: Callback := [residual] once || {
22 residual.id + residual.count
23 };
24 assert(callback() == 8);
25}
passes
1record Ledger { id: i64, memo: String, count: i64 }
2type LedgerAlias := Ledger;
3
4fun main() {
5 let original: LedgerAlias := Ledger { id = 4, memo = "keep", count = 6 };
6 let copied := original.clone();
7 let memo := copied.memo;
8 let callback := [copied] once || { copied.id + copied.count };
9 assert(memo == "keep");
10 assert(callback() == 10);
11}
passes
1record Token { value: String }
2fun take(t: Token.{}) -> i64 { 1 }
3fun main() {
4 let t := Token { value = "x".to_string() };
5 let { value: _, ..rest } := t;
6 take(rest); // ERROR[T0001]
7}
typecheck errorT0001at 6“a record rest pattern (`..rest`) drops the nominal brand”
1record Tok { value: String, id: i64, n: i64 }
2fun take(t: Tok.{ id, n }) -> i64 { t.id + t.n }
3fun main() {
4 let t := Tok { value = "x".to_string(), id = 1, n = 2 };
5 let { value: _, ..rest } := t;
6 assert(take(rest) == 3); // ERROR[T0001]
7}
typecheck errorT0001at 6“an anonymous record is not `Tok.{ id, n }`”
1// A record rest pattern drops the nominal brand (spec.expressions "Record rest patterns"),
2// so aspect dispatch on the remainder follows its anonymous static type, not the hidden
3// brand of the record it came from (metel-core#1446). A whole value (here `u`, after a
4// `Copy` field read that does not narrow it) still dispatches to its nominal impl.
5aspect Describe { fun describe(&self) -> String; }
6record Point { x: i64, y: i64 }
7extend Point: Describe { fun describe(&self) -> String { "point".to_string() } }
8extend<row R> { ..R }: Describe where all R: Copy { fun describe(&self) -> String { "copy-row".to_string() } }
9
10record Tok { value: String, id: i64, n: i64 }
11aspect Keyed { fun key(&self) -> String; }
12extend Tok: Keyed { fun key(&self) -> String { "tok".to_string() } }
13extend<row R: { id: i64, .. }> { ..R }: Keyed where all R: Copy { fun key(&self) -> String { "row".to_string() } }
14
15fun erase(p: Point) -> {} {
16 let { x: _, y: _, ..rest } := p;
17 rest
18}
19
20fun show(d: &dyn Describe) -> String { d.describe() }
21
22fun main() {
23 let e: {} := erase(Point { x = 1, y = 2 });
24 assert(e.describe() == "copy-row");
25 assert(show(&e) == "copy-row");
26
27 let t := Tok { value = "x".to_string(), id = 1, n = 2 };
28 let { value: _, ..rest } := t;
29 assert(rest.key() == "row");
30
31 let u := Point { x = 1, y = 2 };
32 let moved := u.x;
33 assert(u.describe() == "point");
34 assert(moved == 1);
35}
passes
1record Tok { value: String, id: i64, n: i64 }
2fun take(t: Tok.{ id, n }) -> i64 { t.id + t.n }
3fun main() {
4 let t := Tok { value = "x".to_string(), id = 1, n = 2 };
5 let v := t.value;
6 assert(take(t) == 3);
7 assert(v == "x");
8}
passes
1struct Pair { left: String, right: String }
2fun main() {
3 var pair := Pair { left = "gone", right = "kept" };
4 let left := pair.left;
5 let repair := [pair] once |extra| { (pair.right, extra) };
6 let result := repair(7);
7 assert(result.0 == "kept");
8 assert(result.1 == 7);
9
10 var empty_pair := Pair { left = "old-left", right = "old-right" };
11 let old_left := empty_pair.left;
12 let old_right := empty_pair.right;
13 let refill := [empty_pair] once var |extra| {
14 empty_pair.left := "new-left";
15 empty_pair.right := "new-right";
16 (empty_pair, extra)
17 };
18 let restored := refill(9);
19 assert(restored.0.left == "new-left");
20 assert(restored.0.right == "new-right");
21 assert(restored.1 == 9);
22}
passes
1record Pair { left: String, right: String }
2type PairAlias := Pair;
3type Restore := once var || -> PairAlias;
4
5aspect State { fun state(&self) -> i64; }
6extend<row R: { right: String, .. }> { ..R }: State {
7 fun state(&self) -> i64 { 1 }
8}
9extend<row R: !{ right }> { ..R }: State {
10 fun state(&self) -> i64 { 0 }
11}
12
13fun main() {
14 var pair: PairAlias := Pair { left = "left", right = "right" };
15 assert(pair.state() == 1);
16 let left := pair.left;
17 let partial := pair.clone();
18 assert(partial.right == "right");
19 assert(pair.state() == 1);
20 let right := pair.right;
21 assert(pair.state() == 0);
22 let empty: Pair.{} := pair.clone();
23 assert(empty.state() == 0);
24 let restore: Restore := [pair] once var || -> PairAlias {
25 pair.left := "restored";
26 pair.right := "again";
27 assert(pair.state() == 1);
28 pair
29 };
30 match (restore()) {
31 { left, ..rest } => {
32 assert(left == "restored");
33 assert(rest.right == "again");
34 assert(rest.state() == 1);
35 },
36 }
37}
passes
1record Item { name: String, token: String }
2aspect Describe { fun describe(&self) -> String; }
3extend<row R: { name: String, .. }> { ..R }: Describe {
4 fun describe(&self) -> String { self.name.clone() }
5}
6type View := dyn Describe;
7type Callback := once || -> String;
8fun display(value: &View) -> String { value.describe() }
9
10fun main() {
11 let item := Item { name = "kept", token = "discarded" };
12 let token := item.token;
13 let object: View := item;
14 assert(display(&object) == "kept");
15 let callback: Callback := [object] once || { object.describe() };
16 assert(callback() == "kept");
17 let anonymous: View := { name = "anonymous" };
18 assert(display(&anonymous) == "anonymous");
19}
passes
1struct Pair { left: String, right: String }
2fun take(value: Pair.{}) {}
3fun main() {
4 var pair := Pair { left = "old", right = "gone" };
5 let left := pair.left;
6 let right := pair.right;
7 take(pair);
8 let callback := [pair] once var || -> Pair { // ERROR[T0019]
9 pair.left := "new";
10 pair.right := "back";
11 pair
12 };
13}
typecheck errorT0019at 8
1struct Pair { left: String, right: String }
2type Callback := once var || -> Pair;
3
4fun main() {
5 var pair := Pair { left = "old", right = "gone" };
6 let left := pair.left;
7 let right := pair.right;
8 let callback: Callback := [pair] once var || -> Pair {
9 pair.left := "new";
10 pair.right := "back";
11 pair
12 };
13 assert(callback().left == "new");
14
15 var partial := Pair { left = "gone", right = "kept" };
16 let removed := partial.left;
17 let restore := [partial] once var || -> Pair {
18 partial.left := "restored";
19 assert(partial.right == "kept");
20 partial
21 };
22 assert(restore().left == "restored");
23
24 var anonymous := { left = "old", right = "gone" };
25 let row_left := anonymous.left;
26 let restore_row := [anonymous] once var || -> { right: String } {
27 anonymous.right := "back";
28 anonymous
29 };
30 assert(restore_row().right == "back");
31
32 let empty_anonymous := { owned = "gone" };
33 let owned := empty_anonymous.owned;
34 let empty_callback := [empty_anonymous] once || -> {} { empty_anonymous };
35 let empty: {} := empty_callback();
36}
passes
1struct Pair { left: String, right: String }
2fun main() {
3 let pair := Pair { left = "gone", right = "kept" };
4 let left := pair.left;
5 let callback := [pair] once || -> String { pair.left }; // ERROR[T0019]
6}
typecheck errorT0019at 5
1struct Pair { left: String, right: String }
2fun take(value: Pair.{}) {}
3fun main() {
4 var pair := Pair { left = "old", right = "gone" };
5 let left := pair.left;
6 let right := pair.right;
7 let callback := [pair] once var || -> Pair {
8 pair.left := "new";
9 pair.right := "back";
10 pair
11 };
12 take(pair); // ERROR[T0019]
13}
typecheck errorT0019at 12
1struct Box<T> { value: T, text: String }
2fun main() {
3 let box: Box<i64> := Box { value = 3, text = "x" };
4 let text := box.text;
5 var rebound := box;
6 assert(rebound.value == 3);
7 let other: Box<String> := Box { value = "owned", text = "x" };
8 let other_text := other.text;
9 var other_rebound := other;
10 assert(other_rebound.value == "owned");
11}
passes
Legality Rule №5
A residual may itself be projected (h.{ fd } on an already-narrowed h) for a field
still in its row; naming a field already moved out of it is rejected.
Tested by (2)
1// RFC-0137 slice 2 (metel-core#858): moving a non-`Copy` field out of a struct
2// narrows the value's *type* to a residual of the same brand -- `Handle` becomes
3// `Handle.{ fd }` -- and that residual is exactly the one an explicit projection
4// `h.{ fd }` produces, so the two are interchangeable at a `Self.{ fd }`
5// parameter (spec.ownership.narrowing.dynamics-1). With `--move-check` on, a
6// whole-value use of the narrowed value is *not* flagged as a partial-move
7// violation (metel-core#950) -- narrowing removed exactly the moved field.
8
9struct Handle { fd: i64, name: String }
10
11extend Handle {
12 fun describe(h: &Self.{ fd }) -> i64 { h.fd }
13}
14
15fun main() {
16 // Route A: a partial move narrows `h` in place; a borrowed whole-value use
17 // of the narrowed value is accepted, projection and move producing the same
18 // residual type.
19 let h := Handle { fd = 7, name = "a" };
20 let taken := h.name; // h : Handle.{ fd } from here on
21 assert(h.fd == 7); // the sibling field stays readable
22 assert(Handle::describe(&h) == 7); // narrowed value fits `&Self.{ fd }`
23 assert(Handle::describe(&h.{ fd }) == 7); // re-projecting the residual: same type
24
25 // Route B: an explicit projection off a fresh value produces the same type.
26 let h2 := Handle { fd = 7, name = "b" };
27 assert(Handle::describe(&h2.{ fd }) == 7);
28
29 println(taken);
30}
passes
1// v0.13.0 cross-feature (integration session, metel-core#956): a transparent
2// type alias (RFC-0160) qualifying a call, an `extend` method whose receiver is
3// a branded residual `&Self.{ fd }` (RFC-0137 slice 1), and a receiver narrowed
4// by a partial move (RFC-0137 slice 2). The alias erases to `Handle`, so
5// `H::describe` is `Handle::describe`; the narrowed `h` and an explicit
6// re-projection `h.{ fd }` both fit the residual parameter.
7struct Handle { fd: i64, name: String }
8type H := Handle;
9
10extend Handle {
11 fun describe(h: &Self.{ fd }) -> i64 { h.fd }
12}
13
14fun main() {
15 let h: H := Handle { fd = 7, name = "n" };
16 let taken := h.name; // h : Handle.{ fd }
17 assert(H::describe(&h) == 7); // alias-qualified call, narrowed receiver
18 assert(H::describe(&h.{ fd }) == 7); // re-projecting the residual: same type
19 println(taken);
20}
passes
Dynamic Semantics №1
A struct's own field projection expression moves the named non-Copy fields out of its
operand and produces exactly the same residual type as the equivalent partial move; the
operand narrows by the moved fields. A projection through a reference cannot move a
non-Copy field out of it, and a borrowed projection (&h.{ f }, &var h.{ f }) of a
non-Copy field is rejected, because it would move; a borrowing form is reserved for
RFC-0109 and RFC-0122. Projecting a field that was already moved out is a use of a moved
value (T0019), with or without --move-check.
Tested by (15)
1// RFC-0137 slice 2 (metel-core#858): moving a non-`Copy` field out of a struct
2// narrows the value's *type* to a residual of the same brand -- `Handle` becomes
3// `Handle.{ fd }` -- and that residual is exactly the one an explicit projection
4// `h.{ fd }` produces, so the two are interchangeable at a `Self.{ fd }`
5// parameter (spec.ownership.narrowing.dynamics-1). With `--move-check` on, a
6// whole-value use of the narrowed value is *not* flagged as a partial-move
7// violation (metel-core#950) -- narrowing removed exactly the moved field.
8
9struct Handle { fd: i64, name: String }
10
11extend Handle {
12 fun describe(h: &Self.{ fd }) -> i64 { h.fd }
13}
14
15fun main() {
16 // Route A: a partial move narrows `h` in place; a borrowed whole-value use
17 // of the narrowed value is accepted, projection and move producing the same
18 // residual type.
19 let h := Handle { fd = 7, name = "a" };
20 let taken := h.name; // h : Handle.{ fd } from here on
21 assert(h.fd == 7); // the sibling field stays readable
22 assert(Handle::describe(&h) == 7); // narrowed value fits `&Self.{ fd }`
23 assert(Handle::describe(&h.{ fd }) == 7); // re-projecting the residual: same type
24
25 // Route B: an explicit projection off a fresh value produces the same type.
26 let h2 := Handle { fd = 7, name = "b" };
27 assert(Handle::describe(&h2.{ fd }) == 7);
28
29 println(taken);
30}
passes
1// v0.13.0 cross-feature (integration session, metel-core#956): a transparent
2// type alias (RFC-0160) qualifying a call, an `extend` method whose receiver is
3// a branded residual `&Self.{ fd }` (RFC-0137 slice 1), and a receiver narrowed
4// by a partial move (RFC-0137 slice 2). The alias erases to `Handle`, so
5// `H::describe` is `Handle::describe`; the narrowed `h` and an explicit
6// re-projection `h.{ fd }` both fit the residual parameter.
7struct Handle { fd: i64, name: String }
8type H := Handle;
9
10extend Handle {
11 fun describe(h: &Self.{ fd }) -> i64 { h.fd }
12}
13
14fun main() {
15 let h: H := Handle { fd = 7, name = "n" };
16 let taken := h.name; // h : Handle.{ fd }
17 assert(H::describe(&h) == 7); // alias-qualified call, narrowed receiver
18 assert(H::describe(&h.{ fd }) == 7); // re-projecting the residual: same type
19 println(taken);
20}
passes
1// metel-core#1455: a projection moves its non-`Copy` fields, so there is nothing to lend; `&h.{ name }`
2// is rejected until a borrowing form exists (RFC-0109 / RFC-0122).
3struct Handle { fd: i64, name: String }
4
5extend Handle {
6 fun nm(h: &Self.{ name }) -> i64 { 1 }
7}
8
9fun main() {
10 var h := Handle { fd = 7, name = "a".to_string() };
11 let _n := Handle::nm(&h.{ name });
12}
typecheck errorT0001
1// Projecting every field moves the non-`Copy` ones too; only `Copy` fields stay readable.
2struct Handle { fd: i64, name: String }
3
4fun main() {
5 let h := Handle { fd = 3, name = "log".to_string() };
6 let all := h.{ fd, name };
7 println(h.name); // ERROR[T0019]
8}
typecheck errorT0019at 7“use of moved value”
1// metel-core#1454: `h.{ name }` moves the non-`Copy` field out of `h` like a plain move does, so
2// reading `h.name` afterwards is the same T0019 as after `let a := h.name;` (it used to be an
3// internal error, I0001, from the construction pass).
4struct Handle { fd: i64, name: String }
5
6fun main() {
7 let h := Handle { fd = 3, name = "log".to_string() };
8 let p := h.{ name };
9 println(h.name); // ERROR[T0019]
10}
typecheck errorT0019at 9“use of moved value”
1// A projection of a `Copy` field copies it, so the source stays whole; projecting the non-`Copy`
2// field moves it, and the remaining `Copy` field is still readable (metel-core#1454, #1455).
3struct Handle { fd: i64, name: String }
4
5fun main() {
6 let h := Handle { fd = 3, name = "log".to_string() };
7 let a := h.{ fd };
8 assert(a.fd == 3);
9 assert(h.fd == 3);
10 assert(h.name == "log"); // `fd` was Copy: h is still whole
11 let b := h.{ name };
12 assert(b.name == "log");
13 assert(h.fd == 3); // h : Handle.{ fd }
14}
passes
1// metel-core#1455: the non-`Copy` field was moved by the first projection, so it cannot be projected again.
2struct Handle { fd: i64, name: String }
3
4fun main() {
5 var h := Handle { fd = 7, name = "a".to_string() };
6 let _p := h.{ name };
7 let _q := h.{ name };
8}
typecheck errorT0019
1// metel-core#1455: `h.{ name }` is a move of the named fields that keeps the brand: a `Copy`
2// field is copied, a non-`Copy` field is moved out and the source narrows by it.
3struct Handle { fd: i64, name: String }
4
5fun take(p: Handle.{ name }) -> i64 { 1 }
6
7fun main() {
8 var h := Handle { fd = 7, name = "a".to_string() };
9 let p := h.{ name }; // p : Handle.{ name }; h : Handle.{ fd }
10 assert(take(p) == 1);
11 assert(h.fd == 7); // the Copy field is still readable from the narrowed source
12}
passes
1// metel-core#1455: projecting a non-`Copy` field out of a reference would move out of it.
2struct Handle { fd: i64, name: String }
3
4fun f(h: &Handle) { let _p := h.{ name }; }
5
6fun main() {}
typecheck errorT0019
1// Second rerun (2026-10-15), OW x TA: a projection of only Copy fields may still be borrowed
2// (it borrows its copy) and leaves the source whole, through a transparent alias. (metel-core#1455)
3struct Handle { fd: i64, name: String }
4type H := Handle;
5
6extend Handle {
7 fun peek(h: &Self.{ fd }) -> i64 { h.fd }
8}
9
10fun main() {
11 let h: H := Handle { fd = 4, name = "n".to_string() };
12 assert(H::peek(&h.{ fd }) == 4);
13 assert(h.name == "n");
14}
passes
1// Second rerun (2026-10-15), OR x TA x NR: a transparent alias of a nominal struct passes
2// through an open projection parameter `Handle.{ ..R }` that absorbs the whole value, even
3// with a non-Copy remainder. (metel-core#1460, RFC-0160)
4struct Handle { fd: i64, name: String }
5type H := Handle;
6
7fun any_handle<row R>(h: Handle.{ ..R }) -> i64 { 1 }
8
9fun main() {
10 let h: H := Handle { fd = 3, name = "x".to_string() };
11 assert(any_handle(h) == 1);
12}
passes
1// Second rerun (2026-10-15), CL x OW x NR: a projection moves a non-Copy field and keeps the
2// brand; a `move` closure then captures the branded value, and the narrowed source still
3// serves its Copy field. (metel-core#1455)
4struct Handle { fd: i64, name: String }
5
6fun len_of(p: Handle.{ name }) -> i64 { p.name.len() }
7
8fun main() {
9 var h := Handle { fd = 7, name = "abc".to_string() };
10 let p := h.{ name };
11 let f := [p] once || { len_of(p) };
12 assert(f() == 3);
13 assert(h.fd == 7);
14}
passes
1// Second rerun (2026-10-15), PM x OW: the branded value a projection produced travels through
2// `Perhaps` and is matched out; the narrowed source keeps serving its Copy field.
3// (metel-core#1454, #1455)
4struct Handle { fd: i64, name: String }
5
6fun name_len(p: Handle.{ name }) -> i64 { p.name.len() }
7
8fun main() {
9 var h := Handle { fd = 9, name = "xy".to_string() };
10 let wrapped: Perhaps<Handle.{ name }> := Perhaps::Some { value = h.{ name } };
11 match (wrapped) {
12 Perhaps::Some { value } => assert(name_len(value) == 2),
13 Perhaps::None => assert(false),
14 }
15 assert(h.fd == 9);
16}
passes
1// Second rerun (2026-10-15), OW x NR: write a retained field through `&var` to a residual,
2// then the owner restores the moved field and the whole value is usable again.
3// (metel-core#1465)
4struct Handle { fd: i64, name: String }
5
6fun bump(p: &var Handle.{ fd }) { p.fd := p.fd + 1; }
7
8fun main() {
9 var h := Handle { fd = 1, name = "a".to_string() };
10 let name := h.name;
11 bump(&var h);
12 bump(&var h);
13 assert(h.fd == 3);
14 h.name := name;
15 assert(h.name == "a");
16}
passes
1// metel-core#1455 / RFC-0137: there is no implicit truncation at the call boundary, so a whole
2// `&Handle` does not coerce to `&Handle.{ name }`.
3struct Handle { fd: i64, name: String }
4
5extend Handle {
6 fun nm(h: &Self.{ name }) -> i64 { 1 }
7}
8
9fun main() {
10 let h := Handle { fd = 7, name = "a".to_string() };
11 let _n := Handle::nm(&h);
12}
typecheck errorT0001
Passing a residual to a function
Since v0.13.0 (RFC-0137 slice 2, metel-core#858), a residual reached via move-triggered narrowing is passed exactly the same way; nothing here is specific to how the residual arose.
A parameter naming a struct's own projected type (Handle.{ fd }, or Self.{ fd }
inside Handle's own extend block) is ordinary type-matching, available to every
struct regardless of whether it opts into any structural-matching mechanism:
struct Handle { fd: i64, name: String }
extend Handle {
fun describe(h: Self.{ fd }) -> i64 { h.fd }
}
fun main() {
let handle := Handle { fd = 3, name = "x" };
Handle::describe(handle.{ fd });
}
A caller must match the parameter's row exactly — there is no implicit truncation at the
call boundary. Passing Handle.{ fd, name } where Handle.{ fd } is expected requires
the caller to narrow itself first; the call never silently discards name.
Formal rules
Legality Rule №1
A function parameter may name a struct's own projected type; a caller's argument must match that row exactly, with no implicit narrowing at the call site.
Referenced by: rfc-0137
Tested by (2)
1// Regression (metel-core#857, RFC-0137 slice 1): a struct's own field projection is
2// now branded -- Self.{ fd } accepts a value actually projected from a real Handle
3// (h.{ fd }), the case this fixture confirms still works. The companion negative
4// case (a bare anonymous record of the same shape must now be REJECTED, which is
5// the actual bug this closes) lives in typechecking/structs, since it's a T0001
6// rejection, not something evaluable.
7
8struct Handle { fd: i64, name: String }
9
10extend Handle {
11 fun describe(h: Self.{ fd }) -> i64 { h.fd }
12}
13
14fun main() {
15 let handle := Handle { fd = 3, name = "x" };
16 assert(Handle::describe(handle.{ fd }) == 3);
17}
passes
1// Regression (metel-core#857, RFC-0137 slice 1): this is the actual motivating bug
2// -- Self.{ fd } used to accept a bare anonymous record literal of the same shape
3// exactly as readily as a value actually derived from a real Handle, since the
4// projection resolved to an unbranded record type. Now rejected: a struct's own
5// projection is branded, and a same-shaped anonymous record never carries that
6// brand.
7
8struct Handle { fd: i64, name: String }
9
10extend Handle {
11 fun describe(h: Self.{ fd }) -> i64 { h.fd }
12}
13
14fun main() {
15 let _ := Handle::describe({ fd = 3 });
16}
typecheck errorT0001
Drop dispatch against a narrowed residual
GAP-OWNERSHIP-003RFC-0137Moving a field out of a Drop type is always rejected; row-bounded Drop dispatch would allow it where the destructor does not need that field.A struct implementing Drop whose destructor needs a field that has since been narrowed
away must not silently skip the destructor's work. Dispatch is row-bounded: a Drop
impl's required field set is the residual row its drop method's receiver is declared
with — the fields named in a projected receiver (fun drop(&var self: Self.{ fd })) or
in its where clause (fun drop<row R>(&var self: Self.R) where R: { fd, .. }). A drop
method whose receiver is the bare &var self requires the struct's whole row, and no
partial move of such a type is permitted. The destructor fires against any residual of
the correct brand whose current row is a superset of that declared set, regardless of
what else has already been moved out. The destructor body is checked against its declared
receiver row: it may name only fields in that row, and may call only self-methods whose
own declared receiver row that row satisfies.
Coercing a value of a Drop-implementing type to dyn Aspect is one more checkpoint for
the same required set — the row information the check depends on is discarded once the
value is erased behind a fat pointer, so the check must run before that erasure, not
after.
Formal rules
Legality Rule №1
A Drop impl's required field set is the residual row its drop method's receiver is
declared with; a drop method with a bare &var self receiver requires the struct's
whole declared row.
Referenced by: rfc-0137
Exempt from fixture coverage — blocked on metel-core#949: Row-bounded Drop dispatch is not implemented (RFC-0137 §5, metel-core#949); RFC-0071's unconditional partial-move-with-Drop ban is still enforced today (behind --move-check, off by default).
Dynamic Semantics №1
A Drop impl's destructor fires against any residual of the correct brand whose current
row is a superset of the impl's required field set.
Exempt from fixture coverage — blocked on metel-core#949: Depends on the legality rule above; not implemented.
Legality Rule №2
Coercing a value of a Drop-implementing type to dyn Aspect is rejected when the
value's current row does not satisfy that type's Drop impl's required field set.
Exempt from fixture coverage — blocked on metel-core#949: Depends on row-bounded Drop dispatch (above, RFC-0137 slice 2, metel-core#858). dyn Aspect itself is fully implemented now (RFC-0008, metel-core#865/#863/#864, closed 2026-08-28) -- syntax, object safety, and coercion of a value to one -- so the erasure side of this checkpoint is real; what is still missing is the narrowed residual to run it against, which is metel-core#949's job. Do not attempt this checkpoint until #949 lands.
Legality Rule №3
A Drop impl's drop method may declare its &var self receiver as a residual type of
Self — a field projection (&var self: Self.{ a, b }) or a row parameter constrained
by an open lower bound (fun drop<row R>(&var self: Self.R) where R: { a, b, .. }). The
fields named by that declaration are the impl's required field set (legality-1). A bare
&var self names every field.
Exempt from fixture coverage — blocked on metel-core#949: Row-bounded Drop dispatch is not implemented (RFC-0137 §5, metel-core#949); the narrowed drop-receiver forms additionally depend on their own not-yet-integrated syntax (RFC-0109 named views for the fixed projection form, RFC-0147; RFC-0146 for the row-parameter form, RFC-0148). Until then a drop receiver is always the whole value and the required set is always the whole row.
Legality Rule №4
Within a Drop impl whose drop receiver is declared narrowed (legality-3), the
destructor body may read or write only fields in that declared row, and may call a
self-method only when that method's own declared receiver row is satisfied by the
drop receiver's declared row. Each is a local check at the access or call site; no
whole-body or call-graph analysis derives the required field set.
Exempt from fixture coverage — blocked on metel-core#949: Row-bounded Drop dispatch is not implemented (RFC-0137 §5, metel-core#949); with no narrowed drop-receiver form yet, there is no declared row for a body to be checked against. The reject_inert_destructor gate (metel-core#292) additionally rejects any non-empty drop body until destructor invocation (metel-core#261) lands.
Widening
Reassigning a moved-out field already restores the containing value's whole-value
status todayL3, for every struct regardless of
Drop — this is existing, unconditional --move-check behavior, not itself part of
RFC-0137.
Handle.{ fd } becomes Handle again once name is reassigned. This formalizes the
whole-value-restoring behavior reassignment already has; it does not require another RFC.
Widening does not check the reassembled value against constructor invariants. Ordinary field
reassignment can already bypass such an invariant independently of narrowing or widening;
RFC-0114 (Constructor Aspect and Canonical Construction, still 0-draft) proposes a
separate solution.
Formal rules
Legality Rule №1
A field assignment on a narrowed residual (h.name := …) is legal even though name is
absent from the residual's current row: the assigned field is resolved against the
brand's full declared row, and the write reintroduces it. Widening applies only to an
owned binding; a non-Copy field cannot be moved out of — and so cannot be
reassigned back into — a value reached through a reference
(references-and-moves.legality-1L1).
Tested by (4)
1// RFC-0137 slice 2 (metel-core#858): assigning a value to a field missing from a
2// residual's row widens the residual's type back to the whole brand
3// (spec.ownership.widening.dynamics-1). Only for an owned binding; widening does
4// not re-check any constructor invariant. With `--move-check` on, the widened
5// binding is whole again -- a by-value use is a clean move, not a partial-move
6// violation.
7
8struct Handle { fd: i64, name: String }
9
10fun wants_full(h: Handle) -> i64 { h.fd }
11
12fun main() {
13 var h := Handle { fd = 5, name = "x" };
14 let taken := h.name; // h : Handle.{ fd }
15 h.name := "y"; // widens back: h : Handle
16 assert(h.name == "y"); // sibling readable at the widened type
17 assert(wants_full(h) == 5); // whole `Handle` moved in, once
18 println(taken);
19}
passes
1struct Pair { left: String, right: String }
2fun invalid(empty: Pair.{}) {
3 var restored := empty;
4 restored.left := 3; // ERROR[T0001]
5}
6fun main() {}
typecheck errorT0001
1// RFC-0137 slice 2 (metel-core#858): narrowing and widening apply only to an
2// owned binding. A non-`Copy` field cannot be moved out of a value reached
3// through a reference (RFC-0071 §7.1), so there is never a residual to narrow to
4// or widen from behind one — this rule is unchanged by RFC-0137.
5//
6// Needs move_check = true: the move-out-of-a-reference ban is a move-checker
7// rule, not one of the always-on typecheck rules.
8
9struct Handle { fd: i64, name: String }
10
11fun consume_name(h: &var Handle) -> String {
12 let n := h.name; // rejected: moving `name` out through `&var Handle`
13 n
14}
15
16fun main() {
17 var h := Handle { fd = 1, name = "x" };
18 println(consume_name(&var h));
19}
typecheck errorT0019“reference”
1// Cross-feature (v0.13.0): a `match (h)` (RFC-0156 parenthesized scrutinee) binds
2// a non-`Copy` field out of a struct value through a struct pattern
3// (metel-core#753). That partial move narrows `h` (RFC-0137 slice 2): the moved
4// field is gone, every other field stays readable, and reassigning the moved
5// field widens `h` back to the whole struct.
6
7struct Handle { id: i64, name: String }
8
9fun main() {
10 var h := Handle { id = 7, name = "fd".to_string() };
11
12 // bind and consume `name` via a struct pattern; `h` is now `Handle.{ id }`
13 let taken := match (h) { Handle { name, .. } => name };
14 assert(taken == "fd");
15
16 // a still-present field is readable on the narrowed value
17 assert(h.id == 7);
18
19 // reassigning the moved field widens `h` back to the whole `Handle`
20 h.name := "fd2".to_string();
21 assert(h.name == "fd2");
22 assert(h.id == 7);
23
24 println("ok");
25}
passes
Dynamic Semantics №1
Assigning a value to a field missing from a residual's current row widens the residual's type to include that field, at the same brand; once every moved-out field has been reassigned the type is the plain struct again and the value may be used as a whole (partial-moves.legality-3L3).
This includes widening from an empty residual. For a mutable anonymous-record binding the restored labels recover its original record type; for a mutable nominal binding they recover the original nominal type once all fields are restored.
Using res as defined in narrowing.legality-3L3,
let O(p) be the binding's original field-to-type map (the declared row for
a nominal value, the original inferred or annotated row for an anonymous record).
For a mutable owned binding, restoration obeys:
Γ ⊢ e: T ⇒ Γ₁ Γ₁(p) = res(B, R) O(p)(f) = T f ∉ dom(R)
---------------------------------------------------------------- restore-field
Γ ⊢ p.f := e ⇒ Γ₁[p ↦ res(B, R[f ↦ T])]
The right-hand side is evaluated before the field is restored, using the
ordinary field-assignment evaluation rules. The transition applies when R = {};
restoring only one of several missing fields does not restore the others.
An unknown original label, a wrong value type, or an immutable binding is
still rejected by the ordinary assignment rules. Restoration does not revive
a binding that was moved as a whole.
Referenced by: rfc-0137
Tested by (12)
1// RFC-0137 slice 2 (metel-core#858): assigning a value to a field missing from a
2// residual's row widens the residual's type back to the whole brand
3// (spec.ownership.widening.dynamics-1). Only for an owned binding; widening does
4// not re-check any constructor invariant. With `--move-check` on, the widened
5// binding is whole again -- a by-value use is a clean move, not a partial-move
6// violation.
7
8struct Handle { fd: i64, name: String }
9
10fun wants_full(h: Handle) -> i64 { h.fd }
11
12fun main() {
13 var h := Handle { fd = 5, name = "x" };
14 let taken := h.name; // h : Handle.{ fd }
15 h.name := "y"; // widens back: h : Handle
16 assert(h.name == "y"); // sibling readable at the widened type
17 assert(wants_full(h) == 5); // whole `Handle` moved in, once
18 println(taken);
19}
passes
1struct Pair { left: String, right: String }
2record NamedPair { left: String, right: String }
3struct Zero {}
4fun empty_pair(p: Pair.{}) -> Pair.{} { p }
5fun empty_named(p: NamedPair.{}) -> NamedPair.{} { p }
6fun empty_record(r: {}) -> {} { r }
7fun full_pair(p: Pair) -> String { p.left }
8fun main() {
9 var p := Pair { left = "l", right = "r" };
10 let l := p.left;
11 let r := p.right;
12 p.left := "restored";
13 p.right := "again";
14 assert(full_pair(p) == "restored");
15 var a := { left = "l", right = "r" };
16 let al := a.left;
17 let ar := a.right;
18 let ae: {} := empty_record(a);
19 a.left := "back";
20 a.right := "also";
21 assert(a.left == "back");
22 let n := NamedPair { left = "l", right = "r" };
23 let nl := n.left;
24 let nr := n.right;
25 let ne: NamedPair.{} := empty_named(n);
26 let q := Pair { left = "q", right = "s" };
27 let ql := q.left;
28 let qr := q.right;
29 let qe: Pair.{} := empty_pair(q);
30 let qe_again: Pair.{} := empty_pair(qe);
31 let copied := { text = "gone", count = 7 };
32 let text := copied.text;
33 assert(copied.count == 7);
34 let zero: Zero := Zero {};
35 let normalized: Zero.{} := zero;
36 println("ok");
37}
passes
1struct Pair { left: String, right: String }
2record NamedPair { left: String, right: String }
3struct Zero {}
4fun empty_pair(p: Pair.{}) -> Pair.{} { p }
5fun empty_named(p: NamedPair.{}) -> NamedPair.{} { p }
6fun empty_record(r: {}) -> {} { r }
7fun full_pair(p: Pair) -> String { p.left }
8fun main() {
9 var p := Pair { left = "l", right = "r" };
10 let l := p.left;
11 let r := p.right;
12 p.left := "restored";
13 p.right := "again";
14 assert(full_pair(p) == "restored");
15 var a := { left = "l", right = "r" };
16 let al := a.left;
17 let ar := a.right;
18 let ae: {} := empty_record(a);
19 a.left := "back";
20 a.right := "also";
21 assert(a.left == "back");
22 let n := NamedPair { left = "l", right = "r" };
23 let nl := n.left;
24 let nr := n.right;
25 let ne: NamedPair.{} := empty_named(n);
26 let q := Pair { left = "q", right = "s" };
27 let ql := q.left;
28 let qr := q.right;
29 let qe: Pair.{} := empty_pair(q);
30 let qe_again: Pair.{} := empty_pair(qe);
31 let copied := { text = "gone", count = 7 };
32 let text := copied.text;
33 assert(copied.count == 7);
34 let zero: Zero := Zero {};
35 let normalized: Zero.{} := zero;
36 println("ok");
37}
passes
1struct Pair { left: String, right: String }
2fun main() {
3 var p := Pair { left = "l", right = "r" };
4 let l := p.left;
5 let r := p.right;
6 p.left := "back";
7 let missing := p.right; // ERROR[T0019]
8}
typecheck errorT0019at 7
1struct Pair { left: String, right: String }
2fun main() {
3 var p := Pair { left = "l", right = "r" };
4 let l := p.left;
5 let r := p.right;
6 p.left := "back";
7 let missing := p.right; // ERROR[T0019]
8}
typecheck errorT0019at 7
1struct Pair { left: String, right: String }
2type Empty := Pair.{};
3type Callback := once || -> Pair;
4
5fun empty() -> Pair.{} {
6 let pair := Pair { left = "old", right = "gone" };
7 let left := pair.left;
8 let right := pair.right;
9 pair
10}
11
12fun rebuild(empty: Pair.{}) -> Pair {
13 var restored := empty;
14 restored.left := "new";
15 restored.right := "back";
16 restored
17}
18
19fun captured(empty: Empty) -> Pair {
20 let callback: Callback := [empty] once || {
21 var restored := empty;
22 restored.left := "new";
23 restored.right := "back";
24 restored
25 };
26 callback()
27}
28
29fun written(empty: Pair.{}) -> Pair {
30 let callback := [empty] once || -> Pair {
31 var restored := empty;
32 restored.left := "new";
33 restored.right := "back";
34 restored
35 };
36 callback()
37}
38
39fun main() {
40 assert(rebuild(empty()).right == "back");
41 assert(captured(empty()).left == "new");
42 assert(written(empty()).right == "back");
43}
passes
1struct Pair { left: String, right: String }
2fun rebuild(empty: Pair.{}) -> Pair {
3 var restored := empty;
4 restored.left := "new";
5 restored // ERROR[T0001]
6}
7fun main() {}
typecheck errorT0001
1fun main() {
2 var r := { left = "l", right = "r" };
3 let left := r.left;
4 r.left := r.right;
5 assert(r.left == "r");
6 let missing := r.right; // ERROR[T0003]
7}
typecheck errorT0003at 6
1fun main() {
2 var r := { left = "l", right = "r" };
3 let left := r.left;
4 r.left := r.right;
5 assert(r.left == "r");
6 let missing := r.right; // ERROR[T0003]
7}
typecheck errorT0003at 6
1record Pair { left: String, right: String }
2type PairAlias := Pair;
3type Restore := once var || -> PairAlias;
4
5aspect State { fun state(&self) -> i64; }
6extend<row R: { right: String, .. }> { ..R }: State {
7 fun state(&self) -> i64 { 1 }
8}
9extend<row R: !{ right }> { ..R }: State {
10 fun state(&self) -> i64 { 0 }
11}
12
13fun main() {
14 var pair: PairAlias := Pair { left = "left", right = "right" };
15 assert(pair.state() == 1);
16 let left := pair.left;
17 let partial := pair.clone();
18 assert(partial.right == "right");
19 assert(pair.state() == 1);
20 let right := pair.right;
21 assert(pair.state() == 0);
22 let empty: Pair.{} := pair.clone();
23 assert(empty.state() == 0);
24 let restore: Restore := [pair] once var || -> PairAlias {
25 pair.left := "restored";
26 pair.right := "again";
27 assert(pair.state() == 1);
28 pair
29 };
30 match (restore()) {
31 { left, ..rest } => {
32 assert(left == "restored");
33 assert(rest.right == "again");
34 assert(rest.state() == 1);
35 },
36 }
37}
passes
1struct Pair { left: String, right: String }
2type Callback := once var || -> Pair;
3
4fun main() {
5 var pair := Pair { left = "old", right = "gone" };
6 let left := pair.left;
7 let right := pair.right;
8 let callback: Callback := [pair] once var || -> Pair {
9 pair.left := "new";
10 pair.right := "back";
11 pair
12 };
13 assert(callback().left == "new");
14
15 var partial := Pair { left = "gone", right = "kept" };
16 let removed := partial.left;
17 let restore := [partial] once var || -> Pair {
18 partial.left := "restored";
19 assert(partial.right == "kept");
20 partial
21 };
22 assert(restore().left == "restored");
23
24 var anonymous := { left = "old", right = "gone" };
25 let row_left := anonymous.left;
26 let restore_row := [anonymous] once var || -> { right: String } {
27 anonymous.right := "back";
28 anonymous
29 };
30 assert(restore_row().right == "back");
31
32 let empty_anonymous := { owned = "gone" };
33 let owned := empty_anonymous.owned;
34 let empty_callback := [empty_anonymous] once || -> {} { empty_anonymous };
35 let empty: {} := empty_callback();
36}
passes
1struct Pair { left: String, right: String }
2fun main() {
3 var pair := Pair { left = "old", right = "gone" };
4 let left := pair.left;
5 let right := pair.right;
6 let callback := [pair] once var || -> Pair { // ERROR[T0001]
7 pair.left := "new";
8 pair
9 };
10}
typecheck errorT0001at 6
References and moves
&T is Copy, so a shared reference is duplicated on use and the original stays valid.
&var T is not Copy — an exclusive reference must stay unique to be exclusive. It is
therefore moved on use, with one exception:
--move-check&var T arguments reborrowPassing a &var T to an &var T parameter reborrows it rather than moving it, so the
original binding remains usable after the call. Every other use moves.
struct Counter { n: i64 }
fun bump(r: &var Counter) { }
fun main() {
var c := Counter { n = 0 };
let r := &var c;
bump(r);
bump(r); // fine — each call reborrows
let q := r; // moves: plain binding is not a reborrow
// bump(r); // error: `r` was moved into `q`
}
Returning a reference, storing one in a struct, and capturing one in a closure all move it,
for the same reason let does: a reborrow lasts for a call, and none of those is bounded by
one.
Formal rules
Legality Rule №1
A non-Copy value may not be moved out through either kind of reference; a shared reference
itself is Copy, while an exclusive reference is moved except for an argument-position
reborrow to an &var parameter.
Referenced by: rfc-0071
Tested by (6)
1struct Counter {
2 value: i64,
3}
4
5fun bump(r: &var Counter) { }
6
7fun main() {
8 var c := Counter { value = 0 };
9 let r := &var c;
10 let q := r;
11 bump(r);
12}
typecheck errorT0019“non-reborrow use”
1// #648: a shared reference only ever grants access, never ownership (RFC-0071
2// SS7.1) -- moving `String` (non-Copy) out of `*p` is illegal on the *first*
3// call, not just a repeated one. Before #648 this compiled and only the
4// second `eat(*p)` was rejected, as an ordinary use-after-move -- the wrong
5// diagnosis, since the first move was never legal to begin with.
6fun eat(s: String) -> i64 { 1 }
7
8fun main() {
9 let s := "hello";
10 let p := &s;
11 let first := eat(*p);
12}
typecheck errorT0019“cannot move `(*p)` out of a reference”
1// #648, RFC-0071 SS7.1's own named example: `let x: B = *r;`.
2struct B { v: String }
3
4fun main() {
5 let b := B { v = "x" };
6 let r := &b;
7 let x: B := *r;
8}
typecheck errorT0019“cannot move `(*r)` out of a reference”
1// #648, RFC-0071 SS7.1's other named example: `f(*r)`.
2struct B { v: String }
3
4fun takes(b: B) -> String {
5 b.v
6}
7
8fun main() {
9 let b := B { v = "x" };
10 let r := &b;
11 let n := takes(*r);
12}
typecheck errorT0019“cannot move `(*r)` out of a reference”
1// RFC-0071 §9a item 1: `&T` is `Copy` (a shared reference may be used
2// repeatedly); `&var T` is not (see 10_mut_ref_non_reborrow_move.mtl for the
3// negative half -- moving a `&var T` binding and then using it again is
4// rejected).
5fun show(r: &i64) -> i64 { *r }
6
7fun main() {
8 let x := 5;
9 let r := &x;
10 assert(show(r) == 5);
11 assert(show(r) == 5);
12}
passes
1// RFC-0137 slice 2 (metel-core#858): narrowing and widening apply only to an
2// owned binding. A non-`Copy` field cannot be moved out of a value reached
3// through a reference (RFC-0071 §7.1), so there is never a residual to narrow to
4// or widen from behind one — this rule is unchanged by RFC-0137.
5//
6// Needs move_check = true: the move-out-of-a-reference ban is a move-checker
7// rule, not one of the always-on typecheck rules.
8
9struct Handle { fd: i64, name: String }
10
11fun consume_name(h: &var Handle) -> String {
12 let n := h.name; // rejected: moving `name` out through `&var Handle`
13 n
14}
15
16fun main() {
17 var h := Handle { fd = 1, name = "x" };
18 println(consume_name(&var h));
19}
typecheck errorT0019“reference”
The reborrow's duration is not tracked — tracking it is the borrow checker's job. The rule above only prevents a reference from being consumed; it grants no exclusivity guarantee. See §What ownership does not cover.
Closures
Closures capture by value, so capturing a non-Copy value moves it. To keep using the
original, capture a shared reference — &T is Copy, so the reference is duplicated and the
referent is untouched.
What ownership does not cover
Ownership answers how many owners a value has, and Copy answers whether a value may be
duplicated. Neither answers what is borrowed at a given point, which is a borrow checker's job; see the
References section of the Type System page.
GAP-OWNERSHIP-001RFC-0122RFC-0067Nothing prevents a shared and an exclusive reference to the same place from coexisting.Known gaps
GAP-OWNERSHIP-001 — No borrow checking: reference exclusivity and duration are not enforced. Nothing prevents a shared and an exclusive reference to the same place from coexisting. Open record ↗plannedGAP-OWNERSHIP-002 — A deeper move does not narrow the enclosing value's row. Moving root.a narrows root's type, but moving root.a.b does not: a record-typed field moves as a unit, so the type checker still treats root as whole. Open record ↗plannedGAP-OWNERSHIP-003 — A field cannot be moved out of a Drop type, even where its destructor would not need it. Moving a field out of a Drop type is always rejected; row-bounded Drop dispatch would allow it where the destructor does not need that field. Open record ↗