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

A function whose parameter is `borrow (RawBuf a)` and which calls
RawBuf.get or RawBuf.size on that parameter even once was rejected at
`ail check` with [consume-while-borrowed] — the exact borrow-receiver
use the ledger advertises for get/size. The diagnostic also misnamed the
cause: the receiver is read, not consumed.

Root cause: the linearity walk's callee_arg_modes looked up the callee
under its spelled name. A type-scoped polymorphic op is spelled
`RawBuf.get` at the call site, but check_module_with_visible registers
the kernel raw_buf ops under their bare def names (get/size). The lookup
missed, the receiver arg defaulted to Consume, and consuming a binder
whose borrow_count==1 (the Borrow param) fired the false positive. The
kernel signatures themselves are correct (receiver slot is `borrow`); the
only defect was the name-resolution gap in the linearity globals lookup.

Fix: on a direct-lookup miss, fall back to the bare method name via the
existing parse_method_qualifier + qualifier_is_class_shape resolvers,
gated on a class/type-shaped qualifier so lowercase cross-module-fn
qualifiers (std_list.length) are excluded. This is how the rest of the
checker already treats type-scoped polymorphic ops; the fix is general,
not RawBuf-specific.

This unblocks the natural borrow-helper decomposition (a shared
read-only buffer behind a helper fn) — the shape the downstream series
milestone's Series.at / Series.total_count need.

Surfaced by the raw-buf fieldtest (finding B1, docs/specs/0058).
RED-first: rawbuf_borrow_receiver_read_is_linearity_clean.
This commit is contained in:
2026-05-30 17:13:56 +02:00
parent 75109f171d
commit 744ad41e47
3 changed files with 71 additions and 1 deletions
+21 -1
View File
@@ -708,7 +708,27 @@ impl<'a> Checker<'a> {
// with mode info). Look up the global symbol table. // with mode info). Look up the global symbol table.
let ty = match self.globals.get(name) { let ty = match self.globals.get(name) {
Some(t) => t, Some(t) => t,
None => return vec![], None => {
// Type-scoped kernel ops (e.g. `RawBuf.get`) are
// registered under their BARE def name (`get`) by
// `check_module_with_visible`. When the direct lookup
// misses and the name is a class/type-shaped qualifier,
// retry under the bare method name so the borrow-receiver
// modes resolve — same treatment the rest of the checker
// gives type-scoped polymorphic ops. A lowercase
// cross-module-fn qualifier (`std_list.length`) is NOT
// class-shaped and resolves by its own path, so it is
// gated out here.
let (method_name, qualifier_opt) = crate::parse_method_qualifier(name);
if qualifier_opt.is_some() && crate::qualifier_is_class_shape(&qualifier_opt) {
match self.globals.get(method_name) {
Some(t) => t,
None => return vec![],
}
} else {
return vec![];
}
}
}; };
let inner = strip_forall(ty); let inner = strip_forall(ty);
match inner { match inner {
+39
View File
@@ -718,3 +718,42 @@ fn borrow_own_demo_is_linearity_clean() {
diags diags
); );
} }
/// RED for fieldtest finding B1 (docs/specs/0058): reading a
/// `borrow (RawBuf a)` *parameter* through a borrow-receiver op
/// (`RawBuf.get` / `RawBuf.size`) must check clean. Both ops are
/// declared `(borrow (RawBuf a))` in the receiver slot by the kernel
/// `raw_buf` module, so reading the receiver through a borrow is the
/// advertised use — the receiver is read, not consumed.
///
/// The linearity walk (`crates/ailang-check/src/linearity.rs`)
/// registers visible-module fns into its `globals` map under their
/// bare def name (`get` / `size`), but the call site spells the
/// type-scoped name `RawBuf.get` / `RawBuf.size`. `callee_arg_modes`
/// looks up `"RawBuf.get"`, misses, returns an empty mode vec, and the
/// receiver arg defaults to `Position::Consume` — consuming a binder
/// whose `borrow_count == 1` and firing a spurious
/// `consume-while-borrowed`.
#[test]
fn rawbuf_borrow_receiver_read_is_linearity_clean() {
let entry = examples_dir().join("raw_buf_borrow_read.ail");
let ws = load_workspace(&entry).expect("load raw_buf_borrow_read");
let diags = check_workspace(&ws);
let lin: Vec<&ailang_check::Diagnostic> = diags
.iter()
.filter(|d| {
d.code == "use-after-consume" || d.code == "consume-while-borrowed"
})
.collect();
assert!(
lin.is_empty(),
"reading a borrow-mode RawBuf param via RawBuf.get / RawBuf.size \
must not fire a linearity error; got: {:#?}",
lin
);
assert!(
diags.is_empty(),
"raw_buf_borrow_read must check clean; got: {:#?}",
diags
);
}
+11
View File
@@ -0,0 +1,11 @@
(module raw_buf_borrow_read
(fn read_one
(doc "Reads its borrow-mode RawBuf receiver via RawBuf.get once. get is a borrow-receiver op (kernel raw_buf: get : (borrow (RawBuf a)) Int -> a), so reading the receiver through a borrow must check clean — the receiver is read, not consumed.")
(type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int))))
(params buf)
(body (app RawBuf.get buf 0)))
(fn count
(doc "Reads its borrow-mode RawBuf receiver via RawBuf.size once. size is a borrow-receiver op (kernel raw_buf: size : (borrow (RawBuf a)) -> Int), so it must check clean for the same reason.")
(type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int))))
(params buf)
(body (app RawBuf.size buf))))