fix(check): qualify cross-module kernel type-cons in user ADT fields

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<Int>` and failed to unify with the
constructor argument's `raw_buf.RawBuf<Int>`, 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
This commit is contained in:
2026-05-30 17:48:34 +02:00
parent 43e3b21080
commit a92bcaf969
4 changed files with 80 additions and 5 deletions
+19 -5
View File
@@ -4591,11 +4591,25 @@ pub fn qualify_workspace_module(
c.ty = qualify_workspace_types(&c.ty, own_local_types, module_types); 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); qualify_workspace_term(&mut c.value, own_local_types, module_types, module_mono_fns);
} }
Def::Type(_) | Def::Class(_) | Def::Instance(_) => { Def::Type(td) => {
// TypeDef.ctors carry field types in the owner's local // #50: a consumer module's ADT field can reference a
// namespace by convention — no qualification at the // *cross-module* (kernel-tier auto-imported) type-con by
// owner's own definition site. Class / Instance defs // its bare name (`(con RawBuf …)`). The owner's own type
// hold types qualified through other mechanisms. // names stay bare — `qualify_workspace_types` skips
// `own_local_types` and primitives — so only genuinely
// cross-module field types are upgraded to `<home>.<T>`,
// 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.
} }
} }
} }
+35
View File
@@ -757,3 +757,38 @@ fn rawbuf_borrow_receiver_read_is_linearity_clean() {
diags 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<Int>` — 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<Int>` and fails to unify with the constructor
/// arg's `raw_buf.RawBuf<Int>`.
///
/// 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
);
}
+13
View File
@@ -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))))))))
+13
View File
@@ -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))))))))