Reject-free borrow (RawBuf a) receiver: a single get/size is misclassified consume-while-borrowed #46

New Issue

2026-05-30T16:31:02+02:00

Brummel commented

2026-05-30 16:31:02 +02:00

Summary

A function whose parameter is borrow (RawBuf a) and which calls
RawBuf.get or RawBuf.size on that parameter even once is rejected
at ail check with consume-while-borrowed. Both ops are
borrow-receiver ops per design/models/0007-kernel-extensions.md
(§RawBuf) and docs/specs/0054-raw-buf.md, so borrowing the receiver
to read it is exactly the advertised use. The diagnostic also names
the wrong cause: the receiver is read, not consumed.

Reproduction (verified)

ail check <<module>>
(module m
  (fn read_one
    (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int))))
    (params buf)
    (body (app RawBuf.get buf 0))))

→ error: [consume-while-borrowed] read_one: \buf` is consumed while a borrow of it is still live`

Same with RawBuf.size. An inline owned let-bound buffer reads
fine (the shipped raw-buf fixtures); the misclassification appears
only when the buffer is behind a borrow-mode parameter. Full
worked fixture: examples/fieldtest/rawbuf_1_score_table.ail.

Impact

The borrow signatures the ledger advertises for get/size are
unreachable from the natural decomposition — a helper function over a
shared read-only buffer. This blocks the series milestone, the
raw-buf milestone's stated downstream consumer: Series.at /
Series.total_count read through a borrow (Series a) and would hit
the same path.

Surfaced by the raw-buf fieldtest (finding B1), spec
docs/specs/0058-fieldtest-raw-buf.md. Commit 8e9f0f0.

Acceptance

A borrow (RawBuf Int) helper doing one RawBuf.get checks ok
RED test pinning the above before the fix

## Summary A function whose parameter is `borrow (RawBuf a)` and which calls `RawBuf.get` or `RawBuf.size` on that parameter even once is rejected at `ail check` with `consume-while-borrowed`. Both ops are `borrow`-receiver ops per `design/models/0007-kernel-extensions.md` (§RawBuf) and `docs/specs/0054-raw-buf.md`, so borrowing the receiver to read it is exactly the advertised use. The diagnostic also names the wrong cause: the receiver is read, not consumed. ## Reproduction (verified) ``` ail check <<module>> (module m (fn read_one (type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int)))) (params buf) (body (app RawBuf.get buf 0)))) ``` → `error: [consume-while-borrowed] read_one: \`buf\` is consumed while a borrow of it is still live` Same with `RawBuf.size`. An inline owned `let`-bound buffer reads fine (the shipped raw-buf fixtures); the misclassification appears only when the buffer is behind a `borrow`-mode *parameter*. Full worked fixture: `examples/fieldtest/rawbuf_1_score_table.ail`. ## Impact The `borrow` signatures the ledger advertises for `get`/`size` are unreachable from the natural decomposition — a helper function over a shared read-only buffer. This blocks the `series` milestone, the raw-buf milestone's stated downstream consumer: `Series.at` / `Series.total_count` read through a `borrow (Series a)` and would hit the same path. Surfaced by the raw-buf fieldtest (finding B1), spec `docs/specs/0058-fieldtest-raw-buf.md`. Commit `8e9f0f0`. ## Acceptance - [ ] A `borrow (RawBuf Int)` helper doing one `RawBuf.get` checks `ok` - [ ] RED test pinning the above before the fix

Brummel added the bug label 2026-05-30 16:31:02 +02:00

Brummel referenced this issue

2026-05-30 16:31:27 +02:00

Owned RawBuf threaded through a loop binder passes check but panics codegen unknown variable #47

Brummel referenced this issue from a commit

2026-05-30 17:24:43 +02:00

fix(check): resolve type-scoped borrow-receiver ops in linearity (closes #46)

Brummel closed this issue

2026-05-30 17:24:43 +02:00

Brummel referenced this issue from a commit

2026-05-30 17:24:43 +02:00

docs(raw-buf): refresh fixture outcomes; ratify set non-enforcement (refs #7)