Enums & Exhaustiveness

When the selector is an enum, pick matches on variants. Because an enum has a finite set of variants, covering them all makes the * arm optional — the compiler proves the match is total.

Plain enums

enum:Color = { RED, GREEN, BLUE };
func:failsafe = int32(tbb32:err) { exit 1i32; };
func:main = int32() {
    Color:c = Color.GREEN;
    pick (c) {
        (Color.RED)   { exit 0i32; },
        (Color.GREEN) { exit 1i32; },
        (Color.BLUE)  { exit 2i32; }
    }
    exit 9i32;
};

No (*) arm is needed: all three variants are covered. Drop one and the compiler tells you exactly which is missing:

error: Non-exhaustive pick statement. Missing cases: Color.BLUE

Tagged variants (payloads)

A variant may carry a payload. The arm pattern binds the payload to a local for the arm body:

enum:Event = { None, WithCode(int32) };
func:failsafe = int32(tbb32:_code) { exit 1i32; };
func:main = int32() {
    Event:e = Event.WithCode(7);
    pick (e) {
        (Event.WithCode(c)) { exit c; },   // c == 7
        (Event.None)        { exit 0i32; }
    }
    exit 9i32;
};

The binding c is a local copy of the payload, immutable within the arm.

Why exhaustiveness matters

A total pick has no "what if none matched" gap, so the compiler never has to synthesise a hidden error path. This is the same reason expression picks require exhaustiveness: every evaluation must produce a value.

(K does not model enums directly; K tests 208–210 approximate variant dispatch with integer discriminants — see SEMANTIC_GAPS.md.)