Validation and Diagnostics

Safety Rules

Use-after-move is a compile-time error.
Writing through read-only borrow is a compile-time error.
Borrow escapes are compile-time errors unless explicitly converted into owned values by copying.
Mutable alias violations are compile-time errors wherever possible; any need for runtime checking will be explicitly called out in the documentation.
No first-class references; references can never escape or otherwise outlive the function invocation, and may only be created through function or block parameters.

Error Model

For interpreted MVP, runtime checks are acceptable, but they will be called out in comments and documentation.

Diagnostics should identify binding and operation that failed.
Move errors should suggest = (copy) when user intended to keep source valid.
Borrow errors should suggest & (or loop |&x|) when mutation was attempted through read-only access.
Owned-argument errors should suggest plain x (copyable borrow/copy semantics) or <-x (move) for named bindings.
Linear-copy errors should suggest <-x (move) or borrow forms (x/&x).
Map-key errors should state that keys must be copyable and linear keys are invalid.

MVP Checker Matrix (Recommended)

This section defines what is enforced statically versus at runtime in v1.

Static in v1

Parse and validate ownership mode annotations and required return types in function signatures.
Parse and validate local ownership markers (let x, let &x, let @x).
Validate call-site marker compatibility:
- plain arg allowed for T (read-only view) and @T (owned copy).
- &arg allowed only for &T parameters.
- <-arg allowed only for @T parameters, and only when arg is a named place.
- plain rvalue expressions allowed for T and @T (borrow for T, owned temporary for @T).
Treat plain xs[i] and xs[a..b] as read-only access forms; allow copying indexed elements into owned contexts, but reject implicit owned copies of slice views.
Reject obvious invalid borrow targets (& on non-place expressions).
Reject &*expr; mutable pointee borrows must use &name where name: *T.
Reject overlapping mutable/shared uses of the same place while local borrows are live.
Allow disjoint struct-field borrows in the same scope.
Treat index/slice borrow overlap conservatively (same root collection overlaps).
Reject <- on non-place expressions.
Reject illegal assignment forms, including <- from rvalues/non-place sources.
Reject null and pointer-binding condition forms (if (p) |x| { ... }, if (p) |&x| { ... }).
Reject = when operand value is linear.
Reject linear values in copyable containers (Array, slices, Map).
Reject linear values as map keys.
Validate Some(...) and None() constructor arity and enforce match exhaustiveness for Option[T].
Validate *expr only when expr: *T.
Validate for binders (|x|, |&x|) and reject invalid binders like |<-x|.
Allow consuming traversal only as for (<-collection) |x| with named-place move semantics.
if without else is valid only when the then branch is unit.
Enforce that functions declare intended ownership behavior in signatures.

Conformance Examples (v1)

// Assume signatures:
// fn view(x: T) -> T
// fn log(x: T) -> Unit
// fn edit(x: &T) -> Unit
// fn consume(x: @T) -> Unit

let @a = [1, 2]
let @b = a

view(a)        // valid: plain arg to T
view(&a)       // invalid: &arg requires &T parameter
view(<-a)      // invalid: <-arg requires @T parameter

edit(&a)       // valid: mutable borrow to &T
edit(a)        // invalid: missing & for &T parameter
edit(&[1, 2])  // invalid: & requires place expression, not temporary

consume(a)     // valid: copy into @T
consume(<-a)   // valid: explicit move into @T; a invalid after this call
consume(&a)    // invalid: &arg cannot bind to @T
consume([3, 4])// valid: rvalue to @T moves directly
consume(<-[3,4]) // invalid: <- requires a named source to invalidate

// Assume: linear Handle
let @s = make_handle()
let s2 = s      // invalid: linear values cannot be copied
consume(<-s)    // valid: move; s invalid after call

set_map_key(s, 1) // invalid: map keys must be copyable; linear values are not valid keys

let @c <- b      // valid move assignment; b invalid after move
let d = c        // valid read-only view local
let e <- d       // valid move into a read-only view local; d invalid after move
let @f <- [5, 6] // invalid: <- cannot be used with rvalue source
consume(<-e)      // invalid: e is read-only even though it now owns the moved value

if a { log(d) }           // valid: no else and then-branch is unit
if a { view(d) }          // invalid: no else requires unit then-branch
if a { view(d); }         // valid: expression statement discards return value

view(d);                  // valid: return value discarded
let _ <- view(d)          // valid: ordinary binding using move assignment
let _ = view(d)           // valid: ordinary binding using copy assignment

for (d) |item| { log(item); }      // valid plain element binding
for (d) |&item| { log(item); }     // valid mutable-borrow element binding
for (<-d) |item| { log(item); }    // valid consuming traversal; d invalidated
for (d) |<-item| { log(item); }    // invalid: cannot move elements out via loop binding

let @node = Some(@box(Node { value: 1, next: None() }))
match (node) {
  Some(n) => log(int_to_string(n.value)),
  None() => log("empty"),
}

let @p = @box(1)
edit(&p)               // valid: &p borrows pointee as &i64 when p: *i64
edit(&*p)              // invalid: &*expr is rejected

Expected diagnostics for invalid lines should mention: