E0280

A contract clause (requires or ensures) calls a function that is not pure: one with a capability-bearing parameter or receiver, or a cap fn value. A generic call is judged once instantiated: it is impure when any argument, parameter, or receiver type is capability-bearing after its generics are solved, as in apply(log, out) with fn apply<T>(f: fn(T), x: T) and out: Stdout. An operator that dispatches to a trait impl is judged the same way: == or != on capability-bearing operands (an Eq impl), an interpolation hole of a capability-bearing value (a Display impl), and a ? inside a closure that converts a capability-bearing error (a From impl). Each is judged again once the body's types are solved, so a value that turns out capability-bearing later, on a loop's next pass, is caught. Spans the call, the comparison, the hole, or the ?.

Machine-applicable fix: none.

Example

This program fails with E0280.

fn ready(io: Stdout) -> Bool {
    true
}

fn run(io: Stdout) -> Int
    requires ready(io)
{
    1
}

Fixed

The same program, fixed.

fn ready(n: Int) -> Bool {
    n > 0
}

fn run(n: Int) -> Int
    requires ready(n)
{
    1
}

Listed in the checker notes. oskac explain E0280 prints this entry offline.

All error codes