✓
Passing This code compiles and runs correctly.
Code
// Per-arm obligation rule (the multi-arm sibling of 400_107): each resume arm
// IS a resume, so an arm that ISSUES an obligation (`| granted *R<active!>`)
// would hand the proc a fresh obligation per firing that escapes the firing
// un-discharged — incoherent at 0-to-N firing. Rejected at the SIGNATURE
// level, per arm, without inspecting any body. Arm-DISCHARGE (`<!state>`)
// stays coherent, mirroring 400_106.
const std = @import("std");
const Resource = struct { id: usize };
var global_r = Resource{ .id = 99 };
~pub event borrow { n: usize }
! lend usize
| granted *Resource<active!>
| denied
| done usize
~proc borrow|zig {
const r = lend(n);
_ = r;
return .{ .done = n };
}
~borrow(n: 1)
! lend _ => denied
| done d |> _
Frontend must reject with:
CONTAINS error[KORU027]
CONTAINS cannot issue an obligationError Verification
Actual Compiler Output
error[KORU027]: resume arm 'granted' cannot issue an obligation
--> tests/regression/400_RUNTIME_FEATURES/400_124_effect_arm_cannot_issue_obligation/input.kz:12:1
|
12 | ! lend usize
| ^
hint: a `!` effect branch fires 0-to-N times, so resuming `<active!>` (issue) would let the obligation escape un-discharged — drop the trailing `!`, or discharge in-scope with `<!active>`Flows
flow ~borrow click a branch to expand · @labels scroll to their anchor
borrow (n: 1)
Test Configuration
MUST_FAIL