055 auto discharge cascade

○ Planned This feature is planned but not yet implemented.

Cascading auto-discharge: discharge creates new obligations that also need discharging

Code

// TEST: Auto-discharge cascade - discharge creates new obligations
//
// SCENARIO: Database transaction pattern
//   connect() → Connection[connected!]
//   begin(conn) → Transaction[in_transaction!]  (consumes connected)
//   commit(tx) → Connection[connected!]         (consumes in_transaction, CREATES connected!)
//   close(conn) → void                          (consumes connected)
//
// The key insight: commit() CREATES a new obligation when it returns.
// Auto-discharge must handle this cascade:
//   1. See Transaction[in_transaction!] → insert commit(tx)
//   2. commit returns Connection[connected!] → NEW obligation!
//   3. See Connection[connected!] → insert close(conn)
//   4. close returns void → done
//
// EXPECTED: Flow compiles with auto-inserted commit AND close
// CURRENT: Only handles single-level discharge, not cascades

~import "$app/db"

const std = @import("std");

// THE TEST: This flow should compile with cascading auto-discharge
// User writes only the happy path:
~app.db:connect(host: "localhost")
| connected _ |>
    app.db:begin(conn: _.conn)
    | begun _ |>
        app.db:do_work(tx: _.tx)
        | done _ |> _
        // At this point:
        // - _.tx has Transaction[in_transaction!] obligation
        // Auto-discharge should:
        // 1. Insert commit(tx: _.tx) → returns Connection[connected!]
        // 2. Insert close(conn: <result>.conn) → returns void
        // 3. Done - all obligations satisfied

pub fn main() void {
    std.debug.print("Cascading auto-discharge test\n", .{});
}

input.kz

Imported Files

// Database module with cascading phantom obligations
//
// connect() → Connection[connected!]
// begin()   → Transaction[in_transaction!] (consumes connected)
// commit()  → Connection[connected!]       (consumes in_transaction, CREATES connected!)
// close()   → void                         (consumes connected)

const std = @import("std");

const Connection = struct { handle: i32 };
const Transaction = struct { conn: *Connection };

// connect: creates connection obligation
~pub event connect { host: []const u8 }
| connected { conn: *Connection[connected!] }

~proc connect {
    const c = std.heap.page_allocator.create(Connection) catch unreachable;
    c.* = Connection{ .handle = 42 };
    return .{ .connected = .{ .conn = c } };
}

// begin: consumes connection, creates transaction obligation
~pub event begin { conn: *Connection[!connected] }
| begun { tx: *Transaction[in_transaction!] }

~proc begin {
    const tx = std.heap.page_allocator.create(Transaction) catch unreachable;
    tx.* = Transaction{ .conn = conn };
    return .{ .begun = .{ .tx = tx } };
}

// commit: consumes transaction, CREATES connection obligation
// Marked [!] as default discharge for transactions
~[!]pub event commit { tx: *Transaction[!in_transaction] }
| committed { conn: *Connection[connected!] }

~proc commit {
    const c = tx.conn;
    std.heap.page_allocator.destroy(tx);
    return .{ .committed = .{ .conn = c } };
}

// close: consumes connection obligation, returns void
// Marked [!] as default discharge for connections
~[!]pub event close { conn: *Connection[!connected] }
| closed

~proc close {
    std.heap.page_allocator.destroy(conn);
    return .closed;
}

// do_work: uses transaction without consuming it
~pub event do_work { tx: *Transaction[in_transaction] }
| done { tx: *Transaction[in_transaction] }

~proc do_work {
    std.debug.print("Working with transaction...\n", .{});
    return .{ .done = .{ .tx = tx } };
}

db.kz

← 053 for loop obligation escape obligation lost at boundary →