Fall — Explicit Fallthrough

pick has no implicit fallthrough. When you genuinely want one arm to continue into another, you ask for it explicitly with fall <label>;.

Labelling arms

Any arm may carry a label, written label: before the pattern:

func:failsafe = int32(tbb32:err) { exit 1i32; };
func:main = int32() {
    int32:x = 1;
    pick (x) {
        first:  (1) { fall second; },
        second: (2) { exit 2i32; },
        (*)         { exit 9i32; }
    }
    exit 0i32;
};

Selecting 1 enters the first arm, which immediately fall second; transfers control into the second arm body — so the program exits 2.

Rules

• fall targets a label, never a pattern or a bare value.
• The target label must exist on an arm of the same pick. An unknown label is ARIA-PICK-004:

error: ARIA-PICK-004: 'fall' target 'third' is not a label in this pick

• fall runs the target arm's body; it does not re-test the target's pattern. This is a deliberate, explicit jump.
• A fall to a label that resolves to an arm earlier than the current one is permitted but is your responsibility to keep loop-free — the checker does not prove termination.

Fall vs. nesting

fall resolves to a label in the nearest enclosing pick. Inside a nested pick, fall refers to the inner pick's labels; it cannot jump out to an outer pick's arm.

(K test 034 covers labelled fall; the v0.37.x fall regressions are bug808–bug819.)