diff --git a/crates/ail/tests/raw_buf_new_poly_elem_pin.rs b/crates/ail/tests/raw_buf_new_poly_elem_pin.rs new file mode 100644 index 0000000..6b4cc71 --- /dev/null +++ b/crates/ail/tests/raw_buf_new_poly_elem_pin.rs @@ -0,0 +1,83 @@ +//! RED-pin for the series-step-1 enabling fix (#61, base-tier): a +//! polymorphic function may allocate a `RawBuf a` over its OWN forall +//! type variable via `new` with NO explicit type-arg — the element +//! type is solved purely from the expected ctor-field context +//! `(con RawBuf a)` — and under monomorphisation the buffer must +//! specialise to the CALLER's concrete element type, NOT default to +//! Unit. +//! +//! Property protected: a check-time-solved element var on +//! `(new RawBuf n)` survives monomorphisation. When the only carrier +//! of the buffer's element type is the enclosing ADT ctor-field type +//! `(con RawBuf a)` (the builder `mk` takes only the size, never a +//! value of type `a`), mono must propagate the check-phase solution +//! for `a` to the caller's concrete instantiation. Today it drops +//! that solution, defaults `a` to Unit, and codegen mints +//! `RawBuf_new__Unit`, which has no registered intercept +//! (crates/ailang-codegen/src/intercepts.rs registers only +//! Int/Float/Bool). The fix lives in mono substitution propagation to +//! Term::New lowering (crates/ailang-check/src/lower_to_mir.rs:501, +//! `elem: None`). Precedent: the #51 explicit-`(con Int)`-type-arg +//! fix carried a WRITTEN annotation through mono; the +//! variable-via-expected-type case here is the untouched gap. +//! +//! This is a CLI-boundary E2E test because the defect spans the +//! check -> mono -> codegen pipeline and the symptom is the exit +//! behaviour of `ail build` itself. The element is read back via +//! `first` (RawBuf.get) so the specialisation is OBSERVABLE: a wrong +//! specialisation could not print the stored Float. + +use std::path::{Path, PathBuf}; +use std::process::Command; + +fn repo_root() -> PathBuf { + let manifest_dir = env!("CARGO_MANIFEST_DIR"); + Path::new(manifest_dir) + .parent() + .unwrap() + .parent() + .unwrap() + .to_path_buf() +} + +/// A polymorphic `Box a` whose builder `mk` allocates `(new RawBuf n)` +/// over its own forall var `a` (no type-arg, element solved from the +/// `(con RawBuf a)` ctor-field context). Instantiated by the caller at +/// `Float`, it must build under `--alloc=rc` and print the stored +/// `1.0` — proving the inner buffer specialised to the caller's +/// element type rather than defaulting to Unit. +#[test] +fn rawbuf_new_poly_elem_specialises_to_caller_type() { + let fixture = repo_root().join("examples/raw_buf_new_poly_elem.ail"); + let tmp = std::env::temp_dir().join(format!( + "ailang_rawbuf_new_poly_elem_{}", + std::process::id() + )); + std::fs::create_dir_all(&tmp).unwrap(); + let out = tmp.join("bin"); + + let build = Command::new(env!("CARGO_BIN_EXE_ail")) + .args(["build", fixture.to_str().unwrap(), "--alloc=rc", "-o"]) + .arg(&out) + .output() + .expect("ail build failed to spawn"); + assert!( + build.status.success(), + "ail build --alloc=rc failed for polymorphic RawBuf over a \ + forall var solved from the ctor-field context: stderr={}", + String::from_utf8_lossy(&build.stderr) + ); + + let run = Command::new(&out).output().expect("execute binary"); + assert!( + run.status.success(), + "binary exited non-zero: {:?}", + run.status + ); + let stdout = String::from_utf8_lossy(&run.stdout); + assert!( + stdout.trim() == "1.0", + "expected the program to print the stored Float `1.0` (buffer \ + specialised to the caller's element type Float), got: {stdout:?}" + ); +} diff --git a/examples/raw_buf_new_poly_elem.ail b/examples/raw_buf_new_poly_elem.ail new file mode 100644 index 0000000..b051613 --- /dev/null +++ b/examples/raw_buf_new_poly_elem.ail @@ -0,0 +1,19 @@ +(module raw_buf_new_poly_elem + (data Box (vars a) (param-in (a Int Float)) (ctor B (con RawBuf a))) + (fn mk + (doc "RED-pin fixture for the series-step-1 enabling fix (#61 base-tier). `mk` allocates a `(new RawBuf n)` with NO explicit element type-arg: the buffer's element var is solved at check-time PURELY from the expected ctor-field type `(con RawBuf a)`, never from a value argument (mk takes only the size). Under monomorphisation the buffer must specialise to the CALLER's concrete element type. Today `ail check` passes (the element var `a` unifies cleanly via the ctor-field context) but `ail build --alloc=rc` aborts: mono drops the check-time solution for `a`, defaults it to Unit, and mints `RawBuf_new__Unit`, which has no registered intercept (crates/ailang-codegen/src/intercepts.rs registers only Int/Float/Bool). Diagnosis pointer (NOT the test's concern): the check phase solves `a`; mono must propagate that solution to Term::New lowering (crates/ailang-check/src/lower_to_mir.rs:501, `elem: None`) instead of defaulting to Unit. Precedent is the #51 explicit-`(con Int)`-type-arg fix; the variable-via-expected-type case is the untouched gap. Expected post-fix: the buffer specialises to the caller's element type (Float here), build succeeds, the program prints the stored Float `1.0`.") + (type (forall (vars a) (fn-type (params (own (con Int))) (ret (own (con Box a)))))) + (params n) + (body (let buf (new RawBuf n) (term-ctor Box B buf)))) + (fn store + (type (forall (vars a) (fn-type (params (own (con Box a)) (own a)) (ret (own (con Box a)))))) + (params b v) + (body (match b (case (pat-ctor B buf) (term-ctor Box B (app RawBuf.set buf 0 v)))))) + (fn first + (type (forall (vars a) (fn-type (params (borrow (con Box a))) (ret (own a))))) + (params b) + (body (match b (case (pat-ctor B buf) (app RawBuf.get buf 0))))) + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body (let b (app store (app mk 1) 1.0) (app print (app first b))))))