From a92bcaf9691f4cfa899268c338dd0bec3d5c479c Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 17:48:34 +0200 Subject: [PATCH] fix(check): qualify cross-module kernel type-cons in user ADT fields MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A consumer module's ADT field could reference a kernel-tier auto-imported type by its bare name in op/value positions (`(new RawBuf ...)`, `RawBuf.get`) but NOT in the type-constructor position of the field declaration: `(con RawBuf (con Int))` stayed the unqualified `RawBuf` and failed to unify with the constructor argument's `raw_buf.RawBuf`, so a RawBuf could not be stored in a user ADT field without spelling the qualified `raw_buf.RawBuf`. `qualify_workspace_module` skipped `Def::Type` entirely, and the `Term::Ctor` arm only qualified field types of cross-module *owning* types — a *local* type carrying a cross-module field was the uncovered case. The fix qualifies each ctor field type in the `Def::Type` arm via the existing `qualify_workspace_types`, which upgrades only genuinely cross-module type-cons (skips `own_local_types` and primitives), so a purely-local field is never spuriously rewritten. This is a check-side workspace transform, not the on-disk canonical form, so no module hash drifts (both hash-pin tests stay green). RED test `rawbuf_in_user_adt_field_resolves_bare_name` in crates/ailang-check/tests/workspace.rs, with the bare-name fixture (now checks/builds/runs -> 42, live=0, the ADT drop cascade frees the buffer slab) and the qualified control twin. This is the Series-substrate shape (a RawBuf wrapped in a user ADT), so the inconsistency would have bitten the pending series milestone. closes #50 --- crates/ailang-check/src/lib.rs | 24 ++++++++++++---- crates/ailang-check/tests/workspace.rs | 35 ++++++++++++++++++++++++ examples/raw_buf_adt_field_bare.ail | 13 +++++++++ examples/raw_buf_adt_field_qualified.ail | 13 +++++++++ 4 files changed, 80 insertions(+), 5 deletions(-) create mode 100644 examples/raw_buf_adt_field_bare.ail create mode 100644 examples/raw_buf_adt_field_qualified.ail diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 0e83cad..59315de 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -4591,11 +4591,25 @@ pub fn qualify_workspace_module( c.ty = qualify_workspace_types(&c.ty, own_local_types, module_types); qualify_workspace_term(&mut c.value, own_local_types, module_types, module_mono_fns); } - Def::Type(_) | Def::Class(_) | Def::Instance(_) => { - // TypeDef.ctors carry field types in the owner's local - // namespace by convention — no qualification at the - // owner's own definition site. Class / Instance defs - // hold types qualified through other mechanisms. + Def::Type(td) => { + // #50: a consumer module's ADT field can reference a + // *cross-module* (kernel-tier auto-imported) type-con by + // its bare name (`(con RawBuf …)`). The owner's own type + // names stay bare — `qualify_workspace_types` skips + // `own_local_types` and primitives — so only genuinely + // cross-module field types are upgraded to `.`, + // matching the qualification the op/value positions and + // the imported-fn signatures already receive. + for ctor in &mut td.ctors { + for field in &mut ctor.fields { + *field = + qualify_workspace_types(field, own_local_types, module_types); + } + } + } + Def::Class(_) | Def::Instance(_) => { + // Class / Instance defs hold types qualified through + // other mechanisms. } } } diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index 96ccbea..9b08eb5 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/crates/ailang-check/tests/workspace.rs @@ -757,3 +757,38 @@ fn rawbuf_borrow_receiver_read_is_linearity_clean() { diags ); } + +/// RED for #50: a kernel-tier `RawBuf` stored in a *user ADT field* +/// typed with the bare name `(con RawBuf (con Int))` must resolve to +/// `raw_buf.RawBuf` — exactly as the auto-import already does in +/// op/value positions (`(new RawBuf …)`, `RawBuf.get`). The property +/// this protects: the kernel-tier auto-import covers the +/// type-constructor position inside a user `data` field, not only +/// op/value positions, so an author can store a `RawBuf` in their own +/// ADT field without spelling the qualified `raw_buf.RawBuf`. +/// +/// Cause: `qualify_workspace_module` +/// (`crates/ailang-check/src/lib.rs`) skips `Def::Type`, so a bare +/// cross-module type-con in a consumer module's ADT field is never +/// qualified; the `Term::Ctor` check arm only qualifies field types +/// when the *owning* type is itself cross-module (`owning_module = +/// Some`), not when a *local* type carries a cross-module field. The +/// field stays `RawBuf` and fails to unify with the constructor +/// arg's `raw_buf.RawBuf`. +/// +/// Control twin `raw_buf_adt_field_qualified.ail` (same module, field +/// typed `(con raw_buf.RawBuf (con Int))`) checks clean today, which +/// isolates the cause to bare-name resolution in the type-con +/// position rather than any loader / syntax issue. +#[test] +fn rawbuf_in_user_adt_field_resolves_bare_name() { + let entry = examples_dir().join("raw_buf_adt_field_bare.ail"); + let ws = load_workspace(&entry).expect("load raw_buf_adt_field_bare"); + let diags = check_workspace(&ws); + assert!( + diags.is_empty(), + "a bare `RawBuf` ADT field type must resolve to raw_buf.RawBuf \ + just like op/value positions do; got: {:#?}", + diags + ); +} diff --git a/examples/raw_buf_adt_field_bare.ail b/examples/raw_buf_adt_field_bare.ail new file mode 100644 index 0000000..31a8c3e --- /dev/null +++ b/examples/raw_buf_adt_field_bare.ail @@ -0,0 +1,13 @@ +(module raw_buf_adt_field_bare + (data Box (ctor Box (con RawBuf (con Int)))) + (fn slot1 + (doc "Reads a RawBuf stored in a user ADT field through a borrow. The Box field is typed with the bare kernel name `(con RawBuf (con Int))`; the kernel-tier auto-import must resolve it to raw_buf.RawBuf exactly as it does in op/value positions.") + (type (fn-type (params (borrow (con Box))) (ret (con Int)))) + (params bx) + (body (match bx (case (pat-ctor Box buf) (app RawBuf.get buf 1))))) + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body (let buf (new RawBuf (con Int) 3) + (let buf (app RawBuf.set buf 1 42) + (let bx (term-ctor Box Box buf) (app print (app slot1 bx)))))))) diff --git a/examples/raw_buf_adt_field_qualified.ail b/examples/raw_buf_adt_field_qualified.ail new file mode 100644 index 0000000..574dcbc --- /dev/null +++ b/examples/raw_buf_adt_field_qualified.ail @@ -0,0 +1,13 @@ +(module raw_buf_adt_field_qualified + (data Box (ctor Box (con raw_buf.RawBuf (con Int)))) + (fn slot1 + (doc "Control twin of raw_buf_adt_field_bare: identical module but the Box field is typed with the fully-qualified `(con raw_buf.RawBuf (con Int))`. This checks clean today, isolating the bug to bare-name resolution in the type-constructor position.") + (type (fn-type (params (borrow (con Box))) (ret (con Int)))) + (params bx) + (body (match bx (case (pat-ctor Box buf) (app RawBuf.get buf 1))))) + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body (let buf (new RawBuf (con Int) 3) + (let buf (app RawBuf.set buf 1 42) + (let bx (term-ctor Box Box buf) (app print (app slot1 bx))))))))