ADR-175: A Build-Time Value May Be an Array

Status: Superseded by ADR-311 — its D1-D3 are D3-D5 there Date: September 20, 2026 Target Version: Nikaia 0.0.108 Related: ADR-287 D6 (the comptime evaluator’s stages), ADR-287 (what a build-time body may do), ADR-079 §3 (an evaluator that can loop and push), ADR-152 (Array[T, N], and a literal’s layout decided by its use), ADR-135 (the list literal), ADR-285 D1 (an index out of bounds), #174, Part I 6.8, Part III C.2

1. Context

The build-time evaluator could loop and could call, and had nowhere to put what a loop produced. ADR-079 §3 named the gap and did not shorten it — “an evaluator that can loop and push … this is the real work behind the feature” — and #174 carried it as no push and no aggregate value, with two records waiting behind it.

What a comptime handed down was what a Rust const can hold, and that was one integer or one bool. So ADR-079 §3’s table could be computed and had nowhere to arrive.

2. Decisions

D1 — The aggregate is an array, and it is what a `push` crosses as.

Corrected at 0.0.111, and the heading is the correction. This decision was written and there is no push, with the measurement below as the reason. The measurement is right and the conclusion drawn from it was too narrow: what NK1104 refuses is a function’s declared result, and a comptime is not one. By the time a declaration is compared the build has computed the value, so its length is a fact — which is ADR-079’s own title, growable going in, fixed coming out, and that record is now built for a list. What stands unchanged is everything after the first sentence: the crossed form is [T; N], and a Vec still cannot be what a const holds.

Value::List in the evaluator, landing as a Rust const array: comptime TABLE: Array[i64, 5] = squares() becomes const TABLE: [i64; 5] = [0, 1, 4, 9, 16];.

Measured rather than chosen. .push on a list hands back a Vec[?], and a Vec allocates, so a const cannot hold one; NK1104 refuses a Vec[?] against an Array[i64, 5] long before this evaluator is reached. [T; N] is exactly what a const holds (ADR-152). So a build-time table is written at its length and filled by index, and #174’s push is answered by the shape the type system already had rather than by a new one.

What the evaluator gained for it: the list literal, xs[i], xs[i] = …, xs[i] += … and xs.len() — the four things writing a table by hand needs and nothing else.

D2 — An index the array does not have is refused by name (`NK1165`).

xs[7] of three elements, in a body being run while the program is built. ADR-285 D1 aborts with this sentence at run time; here there is no run to abort in, and answering this compiler cannot evaluate it would send the reader looking for a missing feature instead of at the line (Part III C.2).

And a refusal by name is said once. NK1152 and NK1165 each say what NK1127 would, with the part that matters in it — so NK1127 is kept for the case it is actually about, a shape this evaluator does not read. Two errors for one mistake is what the old shape printed.

D3 — An array knows its own length in the ledger.

Array::len and Array::is_empty in std.contracts. Array[T, N] carries its length in its type and lowers to [T; N], which has both — and nothing said so, so xs.len() on one resolved to no entry. It lowered and it ran; what it cost was the enclosing function’s touch set, because an unresolved call is unknown (ADR-292). The visible price was that for i in 0..<xs.len() — the natural spelling — made a function uncallable from a comptime with nothing says what it touches, while 0..<5 was fine.

3. Consequences

The compiler stopped crashing on a correct program. expect is called with the word "const" for a comptime whose value disagrees with its type, and that word had no diagnostic code: an unreachable!, reached by comptime PRIMES: Array[i64, 4] = [2, 3, 5, 7]. That is Part I 6.8’s a raw internal error reaching you is a Nikaia bug, met by the compiler on itself. The word has NK1166 now, and the literal it crashed on is answered by its annotation the way a let’s is (ADR-152 D4) — one line that was in the let path and not here.

ADR-079 §3’s table has somewhere to arrive, which is what the three records waiting on §2.8 were waiting for.

4. What this does not decide

A Vec at build time. D1 answers why there is none, and nothing wants one: what would carry it down does not exist. Asked and answered at 0.0.111: a Vec in the body is ADR-079 D1’s growable half, and what carries it down is the array this record built. A Vec as the crossed form stays impossible, which is what the sentence was right about — NK1167 says so by name now.
Text. A String at build time is its own question and no record asks it.
An array of arrays. The evaluator holds one, and the landing says nothing rather than guessing a type with a length per level.
The walk over a type’s fields (ADR-088 D1, Part II 10.3), which is #174’s after it and waits on #178 — running a grammar while the program is built is not interpretation.

5. What is built

All of D1, D2 and D3.

build_time::Value::List, the list literal, Expr::Index, an indexed assignment (with and without an operator) and xs.len().
rust_constant_type reads Array[T, N] as [T; N]; a table with no declared type takes its element type from its elements.
NK1165, NK1166, and NK1127 withheld where a refusal was already made by name.
Array::len and Array::is_empty in std.contracts, which the ledger’s own length guard in tests/contracts.rs had to be told about — that test is what makes adding a fifth ::len a decision rather than a line.
crates/nikaia/tests/build_time.rs: the computed table, the hand-written one, the two refusals, the one-error-per-mistake rule at both codes, and the ledger entry.

This site is open source. Improve this page.