The collector is not dropped by the linker, and a literal is where dyn is sharper

Two claims corrected against the thing they claimed about.

A named object is linked whole -- symbol-driven selection is an archive rule,
and dropping unreached code inside an included object needs -ffunction-sections
and --gc-sections, which the link line does not pass. nm on any corpus program
finds flan_dyn_add and flan_gc_collect in it. So the file said something the
build does not do. What makes --no-gc possible is the other half of the same
argument and was already written beside it: nothing refers to flan_dyn.c, so
not compiling it is a change at three sites and nowhere else.

And the boundary. "Typed Flan has no implicit widening" is true of a value and
not of a literal: (g 1) against (defn g [x f64] ...) compiles, because the
checker gives the literal the type the parameter asks for, while (defn h [y
i64] f64 (g y)) is refused. A dyn value written as 1 has been through
flan_dyn_from_i64 and cannot remember, so the same source read as dyn traps
where read as typed it does not. Stated where the compiler lane will find it,
with the two ways to close it, both of them the compiler's.

docs/SPIKE-DYNAMIC.md

@@ -353,13 +353,39 @@ That is the asymmetry worth defending, because the operators *do* promote (§5).
 questions. An operator has no stated expectation to violate — `(+ 1 2.5)` was written by somebody who
 wanted a number and there is one obvious number. An annotation *is* a stated expectation, written down by
 a person, and quietly turning their `i64` into an `f64` would make the boundary the one place in the
-language where a type changed without anybody writing it. Typed Flan has no implicit widening; the
-boundary into typed Flan should not invent some.
+language where a *value* changed type without anybody writing it. Typed Flan does not widen a value:
 
-The consequence for the compiler lane: a call from dyn code into `(defn f [x f64] ...)` with an integer
-argument traps at run time rather than converting. If that turns out to be too sharp in practice, the
-place to soften it is the *compiler*, by emitting a conversion where the checker can see both sides — not
-here, where the only thing visible is a tag.
+```lisp
+(defn g [x f64] f64 x)
+(defn h [y i64] f64 (g y))   ; scratch.flan:2:24: expected f64, found i64
+```
+
+### The one divergence the compiler lane has to know about
+
+Typed Flan does not widen a *value*, but a **literal adopts its expected type**. `(g 1)` compiles and
+prints `1`, because the checker gives the literal `1` the `f64` the parameter asks for; `(vec-new i64)`
+followed by `(push v 1)` works the same way.
+
+A dyn value has no such history. Once `1` has been through `flan_dyn_from_i64` it is tagged `int`, and
+nothing downstream can recover that it was written as a literal in a position that wanted a float. So:
+
+```lisp
+(g 1)          ; typed: compiles, prints 1
+(g some-dyn)   ; dyn, where some-dyn came from the literal 1: traps, "a float was wanted"
+```
+
+That is a real divergence between the same source read as typed and read as dyn, and it is stated here
+rather than discovered later. Two ways out, both the compiler's and neither this file's:
+
+1. **Tag the literal at the constructor.** Where the checker can see that an unannotated literal flows to
+   a float context, emit `flan_dyn_from_f64` instead of `flan_dyn_from_i64`. This is the same inference
+   the checker already performs for typed literals and it keeps the boundary sharp.
+2. **Emit a conversion at the call**, where both sides are visible, rather than softening
+   `flan_dyn_need_f64` — which sees only a tag and could not tell a literal-derived int from a computed
+   one.
+
+Softening the boundary itself is the option not to take: it would accept `(g (len xs))` as readily as
+`(g 1)`, and those are not the same mistake.
 
 ---
 
@@ -406,16 +432,21 @@ is a property of the build and not a wish:
   back-reference — `flan_rt_init` calling `flan_gc_init`, say, which was the obvious thing to write —
   would make the collector unconditional and the refusal a lie, so the heap initialises itself lazily on
   first allocation instead.
-- Consequently a program that calls no dyn operation pulls nothing out of that object, and the linker
-  leaves it behind.
+**The linker does not drop it today, and this document will not claim it does.** `flan_dyn.o` is a named
+object on the link line, not an archive member, and `ld` includes a named object in full — symbol-driven
+selection is a `.a` rule. Dead-code elimination *inside* an included object needs
+`-ffunction-sections -fdata-sections -Wl,--gc-sections`, which the link line does not pass. Measured
+rather than assumed: build any corpus program and `nm` it, and `flan_dyn_add` and `flan_gc_collect` are
+both there as defined symbols.
 
-The link line does **not** currently pass `-ffunction-sections`/`-Wl,--gc-sections`, and this document
-will not claim a drop the build cannot perform. What the above buys is the cheaper mechanism: the object
-is selected at the *file* level, so `--no-gc` is a one-line change at each of the three sites — the same
-per-target selection `select_csrcs` already performs for a package's C — rather than an argument with the
-linker about which sections are live. `flan_dev.c` is compiled into every build today for a reason its
-comment gives at length (a package's C refers to it and package sources are collected whatever `main`
-does); `flan_dyn.c` has no such entanglement and can genuinely be left out.
+What the one-way dependency buys is the better mechanism anyway. The object is selected at the **file**
+level: `--no-gc` is a one-line change at each of the three sites that name `Runtime_src.dyn_source` — the
+same per-target selection `select_csrcs` already performs for a package's C — and once it is not
+compiled, nothing has to be dropped. That only works because nothing else in the runtime refers to it;
+`flan_dev.c` is compiled into every build today precisely because it *is* referred to (a package's C
+names it, and package sources are collected whatever `main` does), and its own comment says so at length.
+`flan_dyn.c` has no such entanglement, and keeping it that way is the constraint this section exists to
+record.
 
 The residual-dynamism refusal itself — deciding that a program is *not* fully annotated and saying which
 form is not — is the compiler's, and is not attempted here.

lib/build.ml

@@ -864,14 +864,19 @@ let executable ?(opts = default) ?(csrcs = []) ?(lflags = []) ?(pnames = [])
   let objs =
     cc ~warn:runtime_warnings Runtime_src.source "flan_rt.c"
     :: [ cc ~warn:runtime_warnings Runtime_src.dev_source "flan_dev.c";
-         (* The dynamic-value runtime. Compiled into every build for the
-            reason flan_dev.c is, and dropped by the same means: it is its own
-            translation unit and nothing in the other two names a symbol in
-            it, so a program with no dyn operation in it pulls nothing out of
-            this object and the linker leaves it behind. Selecting it away at
-            the file level — which is what `--no-gc` will do once the compiler
-            lane can prove a program is fully annotated — is then a one-line
-            change here rather than an argument with the linker. *)
+         (* The dynamic-value runtime. Compiled into every build today, as
+            flan_dev.c is, but for a weaker reason: nothing refers to it. It is
+            its own translation unit and no line of flan_rt.c or flan_dev.c
+            names a symbol in it, so leaving it out is a change *here* and
+            nowhere else — which is what `--no-gc` will be, once the compiler
+            lane can prove a program is fully annotated.
+
+            The linker is not the mechanism and would not be: a named object is
+            linked whole, and dropping unreached code inside one needs
+            -ffunction-sections and --gc-sections, which this line does not
+            pass. So the selection is at the file level, the same shape
+            [select_csrcs] applies to a package's C. See docs/SPIKE-DYNAMIC.md,
+            "Dropping the collector". *)
          cc ~warn:runtime_warnings Runtime_src.dyn_source "flan_dyn.c" ]
     (* wasi-libc's entry point, which is not [main]. See [wasm_main_source].
        Not the browser's: emscripten's start code calls [main] under that name,

runtime/flan_dyn.c

@@ -15,12 +15,13 @@
  *
  * flan_rt.c, and nothing else in the tree. The dependency does not run the
  * other way: no line of flan_rt.c or flan_dev.c names anything defined here.
- * That is the whole of what makes a `--no-gc` build possible — a program that
- * calls no dyn operation references no symbol in this translation unit, so the
- * object contributes nothing but its own size, and the compiler lane is free
- * to refuse to link it at all. A single back-reference from the release
- * runtime would make the collector unconditional and the refusal a lie. See
- * the doc's "Dropping the collector".
+ * That is the whole of what makes a `--no-gc` build possible — not because the
+ * linker drops this object (it does not; a named object is linked whole, and
+ * `nm` on any corpus program finds flan_dyn_add in it), but because nothing
+ * else needs it, so *not compiling it* is a change at the three sites that
+ * name it and nowhere else. A single back-reference from the release runtime
+ * would make the collector unconditional and the refusal a lie. See the doc's
+ * "Dropping the collector".
  *
  * ── Threads ───────────────────────────────────────────────────────────
  *
@@ -780,12 +781,23 @@ int64_t flan_dyn_need_i64(flan_dyn v) {
  * an omission: typed Flan has no implicit widening anywhere — [(print-i64 x)]
  * used to force an explicit [(i64 x)] at every site — and a boundary that
  * quietly turned an int into a float would be the one place in the language
- * where a type changed without anybody writing it down. The dyn *operators*
- * promote, because arithmetic between a 2 and a 2.5 has an obvious answer and
- * refusing it makes dynamic code worse; the boundary into a typed f64
- * parameter does not, because there the annotation is somebody's stated
- * expectation and a mismatch is worth hearing about. That asymmetry is
- * deliberate and is argued at length in the doc. */
+ * where a *value* changed type without anybody writing it down. The dyn
+ * *operators* promote, because arithmetic between a 2 and a 2.5 has an obvious
+ * answer and refusing it makes dynamic code worse; the boundary into a typed
+ * f64 parameter does not, because there the annotation is somebody's stated
+ * expectation and a mismatch is worth hearing about.
+ *
+ * Where this is sharper than the typed language is a *literal*. `(g 1)`
+ * against `(defn g [x f64] ...)` compiles, because the checker gives the
+ * literal the type the parameter asks for; a dyn value written as `1` has
+ * already been through flan_dyn_from_i64 and cannot remember that it was a
+ * literal. So the same source read as dyn traps where read as typed it does
+ * not. That is a real divergence, it is the compiler's to close — by tagging
+ * such a literal as a float where it can see the context — and it is written
+ * down in the doc's boundary section so that closing it is a decision somebody
+ * makes rather than a surprise somebody meets. Softening the check here is the
+ * option not to take: this function sees a tag and nothing else, so it could
+ * not tell (g 1) from (g (len xs)). */
 double flan_dyn_need_f64(flan_dyn v) {
   if (flan_dyn_tag(v) != FLAN_DYN_TAG_FLOAT)
     trap1(TYPE_TRAP, "f64", "a float was wanted", v);