Skip to main content
v0.13.0

Ownership and Move Semantics

Sincev0.12.0RFC-0071behind --move-checknot the default typechecking path

This page describes the implemented ownership model behind the opt-in --move-check flag. Every rule here, including rules with fixture citations, is checked against the real interpreter when the flag is passed. Without it, using a value after it is moved is not rejected: the interpreter behaves as if every value were Copy (a binding reused after a move still resolves, and mutating the new binding does not affect the old one). The flag is off by default while the existing corpus is migrated to the ownership rules, so this page documents an available opt-in mode rather than the default typechecking behavior.

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

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

Drop

Planned forv0.14.0RFC-0071metel-core#261executing destructors when values leave scope. Drop declarations already participate in the implemented ownership checks; only their runtime destructor behavior is planned

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.

Changed inv0.13.0RFC-0071drop takes self: &var Self, not self by value
Formal 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

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)

Drop order

Planned forv0.14.0RFC-0071metel-core#261scope-exit destruction and its ordering rules

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

Planned forv0.14.0RFC-0071metel-core#261the built-in drop(x) operation

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 value as a whole does not. 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 as a whole.

Referenced by: rfc-0071

Legality Rule №2

A field of a Drop type may not be moved out.

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)
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).

Changed inv0.12.0RFC-0071behind --move-checkmoving a field out of a Drop type is now rejected

A Drop type may still be partially borrowed; only moving out is restricted.

Planned forv0.14.0RFC-0137 §5legality-2's ban is superseded in design by row-bounded Drop dispatch — see "Drop dispatch against a narrowed residual" below. Until that mechanism is built, this ban is enforced exactly as stated, unconditionally

Which constructs support partial moves

constructpartial move
struct fieldsyes, at field granularity
tuple elementsyes — positional fields are statically named
record fieldsyes, at field granularityL2
enum payloadsno — matching a variant and moving its payload consumes the enum wholly
array elementsno

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)
Legality Rule №2

Record fields may be moved independently, at field granularity like struct fields; a moved field's siblings remain individually accessible, but using the record value as a whole afterward is rejected as a use of a partially moved value. 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)

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.

Sincev0.13.0RFC-0137metel-core#857a struct's own field projection preserves its nominal brand

h.{ fd } reads fields from a copy of the reference without consuming the original. It produces a residual of h's own brand, not a same-shaped anonymous record:

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.

Sincev0.13.0moving a field out of a value narrows its type

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-moved Handle …". An anonymous record residual is just a Record with 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.

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
Sincev0.13.0Struct narrowing is RFC-0137 slice 2 (metel-core#858); anonymous-record narrowing is RFC-0117 (metel-core#789)

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 (10)
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)
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, non-empty subset of the brand's declared row.

Legality Rule №4
Sincev0.13.0Struct: RFC-0137 slice 2 (metel-core#858). Anonymous record: RFC-0117 (metel-core#789). --move-check agreement: metel-core#950

Using 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.

Tested by (7)
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.

Sincev0.13.0RFC-0137 slice 2metel-core#858
Tested by (2)
Dynamic Semantics №1

A struct's own field projection expression produces exactly the same residual type as the equivalent partial move.

Sincev0.13.0RFC-0137 slice 2metel-core#858
Tested by (2)

Passing a residual to a function

Sincev0.13.0RFC-0137metel-core#857projection-produced residuals match compatible projected parameters

Once move-triggered narrowing lands (metel-core#858), a residual reached that way 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)

Drop dispatch against a narrowed residual

Planned forv0.14.0RFC-0137 §5metel-core#858Needs the narrowed drop receiver (RFC-0109); supersedes the Drop-type partial-move ban above in design, and until implemented that ban is enforced exactly as stated

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.

Sincev0.13.0RFC-0137 slice 2metel-core#858reassigning a moved-out field widens a residual back to its whole type

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).

Sincev0.13.0RFC-0137 slice 2metel-core#858
Tested by (2)
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).

Sincev0.13.0RFC-0137 slice 2metel-core#858For an owned binding

Referenced by: rfc-0137

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:

Sincev0.12.0RFC-0071behind --move-check&var T arguments reborrow

Passing 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)

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 — that is the borrow checker's job, and it is not part of this release. In particular, nothing here prevents two &var T references to the same place; see the References section of the Type System page.