A defconst's value is what the linker writes, on both backends

The refusal moves to the checker: Emit.const refused a computed defconst by
name while the x86 backend ran it through the startup function behind an
.init~once. flag, like a defvar, so the two backends disagreed about the same
program. One refusal in Check.const_defconst_init ends that, and it is the only
place that can name the way through.

The accepted set is unchanged: Tast.const_init's, which is Emit.const's and the
x86 data_sym path's, plus the integer arithmetic collect's folding pass has
already turned into an Int before the initialiser is looked at.

Emit.const's two refusals become a failwith no program reaches; emit_global's
gconst || const_init loses its left half; x86 needed no edit, since it never
classified by the form. test_flan's infers probe asks Check.expression now that
a defconst can no longer wrap an arbitrary expression.

FIX.org

@@ -832,6 +832,9 @@ globals at all.
   program instead, because [Emit.const] has nowhere to run a computed value.
   That divergence predates the re-run rule — the refusal landed in 495629f and
   the flags in 931cf86 — and is noted here rather than fixed.
+  Resolved 2026-09-20: there is no computed [defconst] any more, so the
+  paragraph above describes a program the checker no longer accepts. See "A
+  defconst is a compiler const" below.
 - If the language grows a [def]-style form that re-evaluates, that form
   recomputes on every run. None exists today and none was invented for this;
   the rule is written so that adding one is a new case and not a revision.
@@ -1217,3 +1220,57 @@ function dyn_ops.c *calls*, the call is compiled against the header and the
 symbol has to resolve against flan_dyn.o, so a rename, a removal or a changed
 argument list is a compile or link error in =dune test=. A function nothing
 here calls gets neither. Both comments now say that instead.
+
+* A defconst is a compiler const, decided 2026-09-20
+The author's words: "defconst should not be computed, it's the equivalent to a
+compiler const." So a defconst's initialiser has to be a compile-time constant,
+and the refusal is the checker's — [Check.const_defconst_init], called from
+[check_global] right after the union refusal it sits beside.
+
+It had to move because the two backends were not refusing the same program.
+[Emit.const] refused a computed defconst by name, late and on its way to LLVM
+IR; the x86 backend classified globals by [Tast.const_init] alone, so the same
+defconst fell into the computed set, was stored by the startup function and was
+guarded by an [.init~once.] flag exactly like a defvar. The same split let x86
+accept =(defconst g U (U.B {.x 1}))=, a data type case in a constant, which
+LLVM refused with the byte-level-encoder message. One refusal in the checker
+ends both, and it is the only place that can name the way through.
+
+** The boundary, derived rather than chosen
+What a defconst may be is exactly what [Emit.const] can write and what the x86
+backend's [data_sym] path lowers, which is [Tast.const_init]'s set: an integer,
+float, bool or string literal; unit; a zeroed or uninit value; [None]; a [Some]
+of one of these; and a struct literal or array of them. Nothing that compiled
+on LLVM before stopped compiling.
+
+Integer arithmetic is in the set and is not an exception to it. [collect]'s
+folding pass — [const_int], +, -, *, / and %, over literals and over other
+folded constants, to a fixpoint — has already replaced =(/ screen-height
+cell-size)= with its answer before [check_global] looks at the initialiser, so
+what the refusal sees is an [Int]. That pass is integers only, which is why
+=(defconst half f64 (/ 1.0 2.0))= is computed and refused. Widening it would be
+a second folder and was not done; a test pins that there is not one.
+
+** What came out
+- [Emit.const]'s two refusals are gone. The general one and the data type case
+  one are the checker's now, word for word, so the messages a program sees did
+  not change. What is left in their place is a [failwith] in the file's own
+  idiom: no program reaches it, and it fires only if the checker's accepted set
+  and [Tast.const_init] ever stop agreeing.
+- [emit_global]'s =gconst || const_init ginit= lost its left half. The form no
+  longer decides anything there; the initialiser does, and a zeroinitializer is
+  now always a defvar waiting for the startup function.
+- x86 needed no edit: it never had a defconst case to delete. It classifies by
+  [Tast.const_init], and the checker now guarantees a defconst passes it, so no
+  defconst reaches [Emit.startup_plan] and no [.init~once.] flag is made for
+  one. The flag machinery for defvar is untouched.
+
+** The test harness that depended on the old rule
+test_flan.ml's [infers] read a type off =(defconst probe <expr>)=, which is how
+it pinned literal defaulting and every primitive's result — and most of those
+probes are calls. It asks [Check.expression] now, the way a session checks an
+expression sent from the editor, which is the question the wrapper was only a
+way of asking. A defvar could not stand in: only the defconst form takes no
+type. The one corpus row that relied on an untyped computed defconst,
+=(defconst k (g))= ordered before [g], is a typed defvar and still pins the
+order-independence it was there for.

lib/check.ml

@@ -7481,6 +7481,51 @@ let no_union_const env loc n (v : Tast.expr) =
       n un
   | _ -> ()
 
+(* A defconst's value is what the linker writes into the program's image, so it
+   has to be a value the linker can write: a literal, a zero, an aggregate of
+   those — [Tast.const_init]'s set, which is [Emit.const]'s accepted set asked
+   as a question. The integer arithmetic a defconst is allowed to be written as
+   is already gone by here: [collect]'s folding pass turned [(/ screen-height
+   cell-size)] into its answer before any type resolved, so what arrives here
+   is an [Int] and passes.
+
+   The author's rule, 2026-09-20: "defconst should not be computed, it's the
+   equivalent to a compiler const." Refused here rather than in a backend
+   because a backend can only refuse the program it is asked to emit, and the
+   two were not asking the same question — [Emit.const] refused a computed
+   defconst by name while the x86 backend ran it through the startup function
+   behind an [.init~once.] flag, like a defvar. One refusal in the checker is
+   the same program refused the same way on both, and it is the only place
+   that can say what to do instead.
+
+   A data type case says it with its own message, which is the one thing a
+   reader could not work out from "this is computed": the case would have to be
+   serialised into the payload blob, and that is an encoder rather than an
+   order of operations. *)
+let const_defconst_init env loc n (v : Tast.expr) =
+  match v.Tast.e with
+  | Tast.MakeCase (dname, case, _) ->
+    fail loc
+      "a constant cannot be %s.%s — a data type's payload is a blob, and \
+       writing a case into one at link time needs a byte-level encoder that \
+       does not exist (a string field could not be encoded at all). Make it a \
+       defvar, whose initialiser runs at startup and stores the case, or \
+       declare it zeroed, which is %s.%s"
+      dname case dname
+      (match Hashtbl.find_opt env.datas dname with
+       | Some { Tast.cases = c :: _; _ } -> c.Tast.vname
+       | _ -> "its first case")
+  | _ when not (Tast.const_init v) ->
+    fail loc
+      "a constant's value must be a compile-time constant — the constant %s \
+       is computed. A defvar may have a computed initialiser, because it runs \
+       at startup and stores the result; a defconst is what the linker writes \
+       into the image and has nowhere to run. Write (defvar %s ...), or give \
+       the constant a literal — integer constants may also be written as \
+       arithmetic over literals and other constants, which is folded here"
+      n n
+  | _ -> ()
+
 (* A global's initialiser runs at startup: from [main], after the runtime is
    up, before a line of the program's own code. Nothing has established a
    handler or a restart by then, and nothing outside the initialiser can — the
@@ -7650,6 +7695,9 @@ let check_global env (d : Ast.decl) : Tast.global option =
       | _ -> check (ctx ()) ~want:ty v
     in
     no_union_const env d.Ast.dloc n ginit;
+    (* After the union's own refusal, so a computed union member keeps the
+       message that names its way through rather than the general one. *)
+    const_defconst_init env d.Ast.dloc n ginit;
     (* [env.consts] holds exactly the constants the folding pass consumed, so
        membership is the question "is this value in the program's shape?" *)
     Some { Tast.gname = n; gty = ty; ginit; gconst = true;

lib/emit.ml

@@ -3313,8 +3313,9 @@ let emit_fn m ?(hidden = false) ?(pnames = []) (fn : Tast.fn) =
    [Check] lifts a computed initialiser into a function and [emit_startup]
    below stores its result before [main] runs. So what reaches here is what
    needs no code — every [defvar] whose initialiser [Tast.const_init] accepts,
-   and every [defconst], which is a different rule. A constant is what the
+   and every [defconst], because a defconst's initialiser is one of those too:
-   linker writes, and a value that has to be computed is not one. *)
+   the checker refuses a computed one outright (2026-09-20). A constant is what
+   the linker writes, and a value that has to be computed is not one. *)
 let rec const m (e : Tast.expr) =
   match e.Tast.e with
   | Tast.Int (n, _) -> Int64.to_string n
@@ -3333,34 +3334,19 @@ let rec const m (e : Tast.expr) =
      | _ -> "{ " ^ String.concat ", " inner ^ " }")
   | Tast.Some_ v ->
     Printf.sprintf "{ i8 1, %s %s }" (ll v.Tast.ty) (const m v)
-  (* A data type's payload is declared as a blob of integers, so a constant of one
+  (* No program reaches this. A [defvar] whose initialiser is computed never
-     would have to be the case's fields *serialised into those integers* —
+     asks — it was lifted into a function and this one is only called for the
-     which is a byte-level encoder this compiler does not have, and which could
+     constant ones — and a computed [defconst] is refused by
-     not express a string field at all, since that is a pointer the linker has
+     [Check.const_defconst_init], which is where the two messages that used to
-     to relocate and a byte array has nowhere to put a relocation.
+     be here now live: the one about a data type case needing a byte-level
-
+     encoder, and the general one about a constant having nowhere to run. So
-     Only a [defconst] reaches this now. The same case in a [defvar] is a
+     this is an internal assertion in the file's own idiom rather than a
-     computed initialiser like any other: it is lifted into a function and the
+     diagnostic, and it fires only if that refusal and [Tast.const_init] stop
-     case is written by the same store that writes one in a body, which needs
+     agreeing about the same set. *)
-     no encoder at all. That is the way through, and it is what the message
-     names. *)
-  | Tast.MakeCase (dname, case, _) ->
-    fail e.Tast.loc
-      "a constant cannot be %s.%s — a data type's payload is a blob, and \
-       writing a case into one at link time needs a byte-level encoder that \
-       does not exist (a string field could not be encoded at all). Make it a \
-       defvar, whose initialiser runs at startup and stores the case, or \
-       declare it zeroed, which is %s.%s"
-      dname case dname
-      (match Hashtbl.find_opt m.datas dname with
-       | Some { Tast.cases = c :: _; _ } -> c.Tast.vname
-       | _ -> "its first case")
   | _ ->
-    fail e.Tast.loc
+    failwith
-      "a constant's value must be a compile-time constant — this one is \
+      ("no constant image for " ^ Types.to_string e.Tast.ty ^ " at "
-       computed. A defvar may have a computed initialiser, because it runs at \
+       ^ Loc.to_string e.Tast.loc)
-       startup and stores the result; a defconst is what the linker writes \
-       into the image and has nowhere to run"
 
 (* A dev build emits a [defconst] as a mutable [global]. Two things follow, and
    both are wanted: LLVM can no longer fold a read of it, and a redefinition
@@ -3380,11 +3366,11 @@ let emit_global m ?(hidden = false) (g : Tast.global) =
        (if hidden then "hidden " else "")
        (if g.Tast.gconst && not m.dev then "constant" else "global")
        (ll g.Tast.gty)
-       (* A [defconst] goes through [const] whatever its initialiser is, so a
+       (* The initialiser decides, and the form no longer has to be asked: a
-          computed one is refused there by name rather than quietly zeroed
+          [defconst]'s initialiser is always one [const] can write, because the
-          here: a constant has nowhere to run. *)
+          checker refuses a computed one. So a zeroinitializer here is always a
-       (if g.Tast.gconst || Tast.const_init g.Tast.ginit then
+          [defvar] waiting for the startup function. *)
-          const m g.Tast.ginit
+       (if Tast.const_init g.Tast.ginit then const m g.Tast.ginit
         else "zeroinitializer"))
 
 (* ── Startup ───────────────────────────────────────────────────────── *)
@@ -3424,12 +3410,14 @@ let startup_sym = fname ".init-globals"
    reaches neither.
 
    The split is [Tast.const_init]'s, and it is over the *initialiser* and not
-   over the form — nothing below asks [gconst]. A [defconst] with a computed
+   over the form — nothing below asks [gconst], and nothing has to: since
-   initialiser would therefore be guarded here like any [defvar], and on the
+   2026-09-20 a [defconst]'s initialiser is always a compile-time constant,
-   x86 backend it is. On this one it never arrives: [const] refuses a computed
+   because [Check.const_defconst_init] refuses a computed one on the way in.
-   [defconst] by name, because a constant has nowhere to run. So the two
+   The two therefore coincide for a constant and no [defconst] reaches the
-   backends disagree about that one program, and the disagreement is older
+   plan below. Until then they did not, and the backends disagreed about that
-   than this rule.
+   one program: [const] refused a computed [defconst] by name while the x86
+   backend guarded it here like any [defvar]. One refusal in the checker is
+   what ended it.
 
    So each computed initialiser guards itself with a flag of its own. Per
    global and not per startup function, because the rule belongs to the form:

test/programs/dev-rerun.flan

@@ -8,9 +8,11 @@
 ;;;; calls ran again from the top and stored the initial value back over
 ;;;; whatever the last run had left. A [defconst] whose initialiser is a
 ;;;; compile-time constant is written into the image and no startup code
-;;;; reaches it at all, so the question does not arise for it. The split is
+;;;; reaches it at all, so the question does not arise for it. Since
-;;;; over the initialiser and not over the form — a computed [defconst] would
+;;;; 2026-09-20 there is no other kind: a defconst's initialiser has to be a
-;;;; be guarded like a [defvar], and the LLVM backend refuses one outright.
+;;;; compile-time constant, refused in the checker so that both backends
+;;;; refuse the same program. Before that the LLVM backend refused a computed
+;;;; one while x86 guarded it at startup like a defvar.
 ;;;;
 ;;;; So each line printed below is a claim about one of those cases, and the
 ;;;; run number is the first of them: [runs] is computed, so before the fix it

test/test_acceptance.ml

@@ -4090,9 +4090,12 @@ level "1"
       "the payload past the case in hand is indeterminate";
     (* A *constant* cannot hold a case, because writing one at link time means
        serialising the fields into the payload blob and a string field is a
-       relocation a byte array has nowhere to put. Refused in the emitter,
+       relocation a byte array has nowhere to put. Refused in the checker since
-       where the rest of the rule about what the image can hold lives, so the
+       2026-09-20, with the same words it was refused with in the emitter: a
-       assertion has to get that far rather than stopping at the checker. *)
+       constant's initialiser has to be one the linker can write on *both*
+       backends, and a refusal reached only by emitting was a refusal only one
+       of them made. The pipeline below still runs the emitter, so the test
+       does not care which of the two stopped it. *)
     (let name = "a constant initialised with a data type case" in
      let src =
        "(defdata U [A (B [x i32])])\n(defconst g U (U.B {.x 1}))\n\
@@ -4130,7 +4133,10 @@ level "1"
        Printf.printf "FAIL  %s\n        refused: %S\n" name m);
     (* And a computed initialiser on a defconst is refused by name, because a
        constant is what the linker writes and there is nowhere for it to run.
-       The emitter again: the checker has no opinion about what folds. *)
+       The checker, so that the x86 backend refuses it too — it used to run one
+       through its startup function like a defvar. What folds is still not the
+       checker's opinion: the accepted set is [Tast.const_init]'s, plus the
+       integer arithmetic [collect] had already folded before this ran. *)
     (let name = "a defconst with a computed initialiser" in
      let src =
        "(defn two [] i64 2)\n(defconst c i64 (two))\n(defn main [] i32 0)"

test/test_flan.ml

@@ -735,20 +735,34 @@ let () =
 
 let checked src = program src |> Check.program
 
-(* The type a defconst's value infers to, as the checker prints it. Enough to
+(* The environment a bare expression is checked against: the prelude and
-   pin down literal defaulting and every primitive's result. *)
+   nothing else, built once because building it is the expensive half and no
+   probe below declares anything. *)
+let probe_env = lazy (snd (Check.program_with_env []))
+
+(* The type an expression infers to, as the checker prints it. Enough to pin
+   down literal defaulting and every primitive's result.
+
+   Checked as an expression, the way a session checks one sent from the editor.
+   It used to be the type of [(defconst probe <src>)], which stopped working on
+   2026-09-20: a defconst's initialiser has to be a compile-time constant now
+   and most of the probes below are calls — (cast ...), (len ...), a
+   comparison. A defvar would not do either, since only the defconst form
+   takes no type. This asks [check] the question the wrapper was only ever a
+   way of asking. *)
 let infers name src expected =
-  match checked (Printf.sprintf "(defconst probe %s)" src) with
+  match
-  | p ->
+    let form = List.hd (read src) in
-    (match List.find_opt (fun (g : Tast.global) -> g.gname = "probe") p.globals with
+    let e = Parse.with_imported [] (fun () -> Parse.expr form) in
-     | Some g ->
+    let t, _, _ = Check.expression (Lazy.force probe_env) e in
-       let got = Types.to_string g.gty in
+    Types.to_string t.Tast.ty
+  with
+  | got ->
     if got <> expected then begin
       incr failures;
       Printf.printf "FAIL  %s\n        src: %s\n        got: %s\n    wanted: %s\n"
         name src got expected
     end
-     | None -> incr failures; Printf.printf "FAIL  %s: no probe\n" name)
   | exception Loc.Error { Loc.dloc = loc; dmsg = msg; _ } ->
     incr failures;
     Printf.printf "FAIL  %s\n        src: %s\n      error: %s: %s\n"
@@ -2050,11 +2064,49 @@ let () =
     "(defvar grid [rows i32]) (defconst rows 8)";
   accepts "constants defined out of order"
     "(defconst a (+ b 1)) (defconst b 1)";
-  accepts "an untyped constant from a later function"
+  (* A typed [defvar] here and not an untyped [defconst], which it was until
-    "(defconst k (g)) (defn g [] u8 1)";
+     2026-09-20: a computed initialiser belongs to a defvar now, and only the
+     defconst form takes no type. The order-independence being pinned is the
+     same one either way — [g] is resolved from a declaration further down the
+     file. *)
+  accepts "a global initialised from a later function"
+    "(defvar k u8 (g)) (defn g [] u8 1)";
   rejects_check "a genuinely unknown constant still reports itself"
     "(defconst a (+ nope 1))" ~needle:"unknown name nope";
 
+  (* ── What a defconst's value may be, decided 2026-09-20 ─────────── *)
+
+  (* The author's rule: a defconst is the equivalent of a compiler const, so
+     its value is what the linker writes and never something that runs. The
+     accepted set is [Tast.const_init]'s, which is [Emit.const]'s — and the
+     integer arithmetic below is in it because [collect]'s folding pass has
+     already turned it into its answer by the time the initialiser is looked
+     at, which is the same pass that makes (/ w cell) usable as an array
+     length. Both backends refuse the computed one here now, at the checker,
+     rather than one of them refusing and the other running it at startup. *)
+  rejects_check "a computed defconst"
+    "(defn seed [] i64 7) (defconst c i64 (seed))"
+    ~needle:"a constant's value must be a compile-time constant";
+  rejects_check "a computed defconst names the way through"
+    "(defn seed [] i64 7) (defconst c i64 (seed))"
+    ~needle:"Write (defvar c ...)";
+  accepts "a constant written as a literal"
+    "(defconst x u64 0xcbf29ce484222325)";
+  accepts "a constant written as arithmetic over other constants"
+    "(defconst w i64 640) (defconst cell i64 16) (defconst cols i64 (/ w cell))";
+  accepts "a constant aggregate of literals"
+    "(defstruct P [x i32 y i32]) (defconst origin P (P {.x 1 .y 2}))";
+  accepts "a constant array of literals"
+    "(defconst xs [3 i32] [1 2 3])";
+  accepts "a zeroed constant"
+    "(defstruct P [x i32 y i32]) (defconst origin P (P {}))";
+  (* The fold is over integers only, so the same shape in floats is computed
+     and refused — deliberately, because widening it would be a second folder
+     and this pins that there is not one. *)
+  rejects_check "float arithmetic is not folded into a constant"
+    "(defconst half f64 (/ 1.0 2.0))"
+    ~needle:"a constant's value must be a compile-time constant";
+
   (* ── Conditions, spec-conditions.md §1 and §2 ──────────────────── *)
 
   accepts "handler-bind over a struct condition"