(new T ...) drops the explicit element annotation; unobserved element type crashes codegen #51

New Issue

2026-05-30T18:23:17+02:00

Brummel commented

2026-05-30 18:23:17 +02:00

Summary

(new T <elem> <size>) drops the author's explicit element-type annotation at desugar, so any buffer whose element type is not later observed by a get/set passes ail check and then crashes ail build with an internal codegen error. This breaks two distinct shapes:

A legitimate buffer with an allowed but unobserved element. (new RawBuf (con Int) 3) used only via RawBuf.size (never get/set) — the author wrote (con Int), yet build crashes.
A forbidden element. (new RawBuf (con Unit) 3) — Unit is not in the param-in set {Int, Float, Bool}, but it is not rejected at check (see issue split note below); it reaches codegen and crashes the same way.

Both contradict the language identity (every definition carries its full type; mandatory type annotations) — the explicit (con Int) / (con Unit) the author wrote is discarded.

Reproduction (verified, fresh build at current HEAD)

Legitimate-but-unobserved (the more serious leg):

(module intsize
  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
    (body (let b (new RawBuf (con Int) 3)
      (app print (app RawBuf.size b))))))

ail check -> ok (33 symbols across 3 modules)
ail build --alloc=rc -> Error: module raw_buf: def RawBuf_new__Unit: internal: intrinsic fn RawBuf_new__Unit has no registered intercept; an (intrinsic) body must resolve through the intercept registry

The same module with an observed element ((let b (app RawBuf.set b 0 9) (app print (app RawBuf.get b 0)))) builds and runs (9), because the set/get pins the element type during inference.

Forbidden element ((con Unit)) behaves identically — check passes, build crashes with the same RawBuf_new__Unit error.

Root cause (verified, code-pinpointed)

The (new T ...) desugar drops the leading NewArg::Type: crates/ailang-core/src/desugar.rs:1053 (the Term::New arm rewrites to (app T.new <values>), comment: "The leading NewArg::Type is dropped … recovered by ordinary inference from how the result is used"). Decision recorded in the raw-buf milestone spec, § Term::New desugar.
RawBuf.new : forall a. (Int) -> own (RawBuf a) has a only in the result, never in the parameters, so the call-site args can never pin a. It is pinned only if downstream get/set forces unification of the result's a.
When a is unpinned, monomorphisation defaults it to Unit: crates/ailang-codegen/src/subst.rs:56-60 ("Any forall var not pinned by the args … defaults to Unit"). The comment there assumes "the specialised body must not actually read an a-typed value" — false for RawBuf.new, whose body is the element-specialised intrinsic RawBuf_new__<elem>; only Int/Float/Bool are registered intercepts, so RawBuf_new__Unit has none and codegen aborts.

Why this is a design decision, not a one-line patch

Honouring the explicit annotation means carrying the element type from Term::New through to monomorphisation. There is no type-ascription term in the AST today (no Ann/The/ascribe variant), and RawBuf.new's signature cannot pin a from its value args. Candidate directions (a spec revision to § Term::New desugar):

Desugar (new T <elem> <vals>) to a form that pins the element type (a type-ascription term, or a typed application carrying the type-arg) so inference and mono see the author's <elem>.
Give the kernel constructor an element-carrying parameter (e.g. a phantom/size-style type witness) so a is pinned by the args.
Validate NewArg::Type against param-in at pre-desugar AND make mono error (not default to Unit) on an unpinned RC/intrinsic element — turns the crash into a clean diagnostic but still rejects the legitimate RawBuf<Int>-by-size program.

Split note — `param-in` construction-site enforcement

Leg 2 (forbidden element not rejected at check) was investigated as a separate fix. The param-in restricted-set check runs only over written-down type signatures (check_type_well_formed, crates/ailang-check/src/lib.rs:2084); a locally-constructed forbidden element with no RawBuf<T> in any signature is never checked. The natural fix-site is crates/ailang-check/src/pre_desugar_validation.rs (the documented Term::New/desugar lockstep: a reject must precede the desugar that eats NewArg::Type). This is subsumed by, and should be designed together with, the root annotation-preservation decision above.

Context

Surfaced by the comprehensive raw-buf field test (docs/specs/0059-fieldtest-raw-buf-comprehensive.md). The shipped RawBuf fixtures all observe their element via get/set, so none triggered this; it appears the moment a buffer is allocated for its size/capacity alone, or a forbidden element is constructed locally.

Acceptance

(new RawBuf (con Int) 3) used only via RawBuf.size checks, builds, and runs
(new RawBuf (con Unit) 3) is rejected at ail check with param-not-in-restricted-set naming Unit, never reaching codegen
RED tests pinning both legs before the fix

## Summary `(new T <elem> <size>)` drops the author's explicit element-type annotation at desugar, so any buffer whose element type is not later *observed* by a `get`/`set` passes `ail check` and then crashes `ail build` with an internal codegen error. This breaks two distinct shapes: 1. A **legitimate** buffer with an allowed but unobserved element. `(new RawBuf (con Int) 3)` used only via `RawBuf.size` (never `get`/`set`) — the author wrote `(con Int)`, yet build crashes. 2. A **forbidden** element. `(new RawBuf (con Unit) 3)` — `Unit` is not in the `param-in` set `{Int, Float, Bool}`, but it is not rejected at check (see issue split note below); it reaches codegen and crashes the same way. Both contradict the language identity (every definition carries its full type; mandatory type annotations) — the explicit `(con Int)` / `(con Unit)` the author wrote is discarded. ## Reproduction (verified, fresh build at current HEAD) Legitimate-but-unobserved (the more serious leg): ``` (module intsize (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body (let b (new RawBuf (con Int) 3) (app print (app RawBuf.size b)))))) ``` - `ail check` -> `ok (33 symbols across 3 modules)` - `ail build --alloc=rc` -> `Error: module raw_buf: def RawBuf_new__Unit: internal: intrinsic fn RawBuf_new__Unit has no registered intercept; an (intrinsic) body must resolve through the intercept registry` The same module with an observed element (`(let b (app RawBuf.set b 0 9) (app print (app RawBuf.get b 0)))`) builds and runs (`9`), because the `set`/`get` pins the element type during inference. Forbidden element (`(con Unit)`) behaves identically — check passes, build crashes with the same `RawBuf_new__Unit` error. ## Root cause (verified, code-pinpointed) - The `(new T ...)` desugar drops the leading `NewArg::Type`: `crates/ailang-core/src/desugar.rs:1053` (the `Term::New` arm rewrites to `(app T.new <values>)`, comment: "The leading NewArg::Type is dropped … recovered by ordinary inference from how the result is used"). Decision recorded in the raw-buf milestone spec, § Term::New desugar. - `RawBuf.new : forall a. (Int) -> own (RawBuf a)` has `a` only in the result, never in the parameters, so the call-site args can never pin `a`. It is pinned only if downstream `get`/`set` forces unification of the result's `a`. - When `a` is unpinned, monomorphisation defaults it to `Unit`: `crates/ailang-codegen/src/subst.rs:56-60` ("Any forall var not pinned by the args … defaults to Unit"). The comment there assumes "the specialised body must not actually read an `a`-typed value" — false for `RawBuf.new`, whose body is the element-specialised intrinsic `RawBuf_new__<elem>`; only `Int`/`Float`/`Bool` are registered intercepts, so `RawBuf_new__Unit` has none and codegen aborts. ## Why this is a design decision, not a one-line patch Honouring the explicit annotation means carrying the element type from `Term::New` through to monomorphisation. There is no type-ascription term in the AST today (no `Ann`/`The`/`ascribe` variant), and `RawBuf.new`'s signature cannot pin `a` from its value args. Candidate directions (a spec revision to § Term::New desugar): - Desugar `(new T <elem> <vals>)` to a form that pins the element type (a type-ascription term, or a typed application carrying the type-arg) so inference and mono see the author's `<elem>`. - Give the kernel constructor an element-carrying parameter (e.g. a phantom/size-style type witness) so `a` is pinned by the args. - Validate `NewArg::Type` against `param-in` at pre-desugar AND make mono error (not default to `Unit`) on an unpinned RC/intrinsic element — turns the crash into a clean diagnostic but still rejects the legitimate `RawBuf<Int>`-by-size program. ## Split note — `param-in` construction-site enforcement Leg 2 (forbidden element not rejected at check) was investigated as a separate fix. The `param-in` restricted-set check runs only over written-down type signatures (`check_type_well_formed`, `crates/ailang-check/src/lib.rs:2084`); a locally-constructed forbidden element with no `RawBuf<T>` in any signature is never checked. The natural fix-site is `crates/ailang-check/src/pre_desugar_validation.rs` (the documented `Term::New`/desugar lockstep: a reject must precede the desugar that eats `NewArg::Type`). This is subsumed by, and should be designed together with, the root annotation-preservation decision above. ## Context Surfaced by the comprehensive raw-buf field test (`docs/specs/0059-fieldtest-raw-buf-comprehensive.md`). The shipped RawBuf fixtures all observe their element via `get`/`set`, so none triggered this; it appears the moment a buffer is allocated for its size/capacity alone, or a forbidden element is constructed locally. ## Acceptance - [ ] `(new RawBuf (con Int) 3)` used only via `RawBuf.size` checks, builds, and runs - [ ] `(new RawBuf (con Unit) 3)` is rejected at `ail check` with `param-not-in-restricted-set` naming `Unit`, never reaching codegen - [ ] RED tests pinning both legs before the fix

Brummel added the bug label 2026-05-30 18:23:17 +02:00

Brummel referenced this issue from a commit

2026-05-30 18:30:08 +02:00

fieldtest: raw-buf comprehensive — 4 examples, 8 findings (refs #7)

Brummel referenced this issue from a commit

2026-05-31 12:46:30 +02:00

test(raw-buf): RED-pin #51 — (new T <elem> …) must honour the element type-arg

Brummel referenced this issue from a commit

2026-05-31 12:46:30 +02:00

fix(check): honour the written element type-arg on polymorphic (new T …)

Brummel closed this issue

2026-05-31 12:46:30 +02:00