test(series): RED pin for polymorphic RawBuf element-var forwarding

Base-tier enabling RED for the `series` milestone step 1 (#61). A
polymorphic fn that allocates `(new RawBuf n)` with no explicit
type-arg — element var solved purely from the enclosing ctor-field
type `(con RawBuf a)`, never from a value argument — checks clean but
fails `ail build --alloc=rc`: mono drops the check-phase solution for
`a`, defaults it to Unit, and codegen mints the unregistered
`RawBuf_new__Unit`. The fixture reads the element back via `RawBuf.get`
so a wrong specialisation is observable (the program must print the
stored `1.0`).

This is the precondition the user picked (option B) so Series can ship
as a pure AILang library extension over RawBuf while keeping the
model-0007 `(new Series (con Float) 3)` caller surface. The #51 fix
carried a WRITTEN `(con Int)` type-arg through mono; the
variable-via-expected-type case is the untouched gap.

RED: `ail check` exits 0; `ail build --alloc=rc` aborts with
`RawBuf_new__Unit has no registered intercept`. GREEN target: builds,
runs, prints `1.0`. The mono fix must not break the INTERCEPTS↔
(intrinsic) bijection or the Term::New↔pre_desugar_validation lockstep.

refs #61
This commit is contained in:
2026-06-02 12:36:01 +02:00
parent c747cdf932
commit e035eff8df
2 changed files with 102 additions and 0 deletions
+19
View File
@@ -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))))))