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))))))))