linear_used_twice: a linear value is used more than once
A value of a linear type is consumed twice. The second use is underlined,
and a label points at the first. When the first consumption is not in
straight-line code, the label also says where it sits: “in the Some(v)
arm”, “in the else branch” (with “every arm consumes it” when all of them
do), or “inside a closure that can run more than once (each iteration
consumes it)” for a closure body such as the function passed to List.map.
No linearity error follows a value whose use sits directly inside an expression that already failed to typecheck (a misspelled function, a field access on a non-record): what that expression did with the value is unknown, and the type error is reported instead.
A program that triggers it
mod Main do
needs IO.Console
always_linear type Token = Token(Int)
fn consume(t : Token) : Int do
match t do Token(n) -> n end
end
fn main(_console : Cap(IO.Console)) do
let t = Token(1)
println(int_to_string(consume(t) + consume(t)))
end
end
The fix
Consume the value once and reuse the result, as below. If you need the
value itself twice, the type must not be linear (or must offer an explicit
clone).
mod Main do
needs IO.Console
always_linear type Token = Token(Int)
fn consume(t : Token) : Int do
match t do Token(n) -> n end
end
fn main(_console : Cap(IO.Console)) do
let t = Token(1)
let n = consume(t)
println(int_to_string(n + n))
end
end
Why the rule exists
A linear value stands for something that exists once: a channel endpoint, a uniquely owned buffer. Using it twice would let two parts of the program each believe they hold it, which is exactly the aliasing linearity exists to rule out.
See also: the language reference.