(slice d ...) over a dyn text answers a text, in the three spellings the typed slice has

TODO.org

@@ -939,9 +939,10 @@ pairs. Rules out a type slot in =let=.
 CLOSED: [2026-09-25]
 =[const T]= and =(Ptr const T)=; a =[T]= or =(Ptr T)= converts at the top of a type or under another const one, never inside a writable one. The const is shallow: an element of a =[const [u8]]= and a Vec's buffer are writable. The address of read-only storage, a string's byte included, is a =(Ptr const T)=, and a C =const T *= parameter takes one.
 
-** TODO (slice d 1) over a dyn string is refused where (at d i) works
+** TODO (slice d 1) over a dyn vec traps where the typed Vec's works
-The typed and dyn spaces disagree about a spelling, which the standing rule
+A text slices to a copy, which is the typed view's meaning because a text is
-forbids. A dyn slice should exist.
+immutable. A vec's slice has to share the vec's elements, so it needs a view
+object over a dyn vec; a copy would compute something else.
 
 ** TODO (slice "abc" 0 99) is not refused at compile time
 A string type carries no length, so there is nothing to compare the bound against

lib/check.ml

@@ -9866,6 +9866,20 @@ and named_call ?(qualified = false) ctx ~want loc name args =
        (* A Vec leaves here: everything below is written around a length the
           compiler can see, and a Vec's is a word the runtime reads. *)
        | Types.Vec elem -> vec_slice ctx ~want loc target elem bounds
+       (* A dyn leaves too, as [at] over one does: the bounds are dyn, like
+          [at]'s index, and a missing [hi] is nil, which the runtime reads as
+          the length. *)
+       | Types.Dyn ->
+         let bound b = check ctx ~want:Types.Dyn b in
+         let nil () = rt loc Types.Dyn "flan_dyn_nil" [] in
+         let lo, hi = match bounds with
+           | [] -> box loc (mk loc dyn_i64 (Tast.Int (0L, Types.I64))), nil ()
+           | [ lo ] -> bound lo, nil ()
+           | [ lo; hi ] -> bound lo, bound hi
+           | _ -> assert false
+         in
+         expect ctx loc ~want
+           (rt loc Types.Dyn "flan_dyn_slice" [ target; lo; hi; here loc ])
        | _ ->
        (* A string slices to a string, not to a [u8]: the result views the
           same bytes and is read-only for the same reason the source is, and

lib/emit.ml

@@ -4941,6 +4941,7 @@ declare i64 @flan_dyn_ge(i64, i64, ptr, i64)
 declare i64 @flan_dyn_eq(i64, i64)
 declare i64 @flan_dyn_len(i64)
 declare i64 @flan_dyn_at(i64, i64, ptr, i64)
+declare i64 @flan_dyn_slice(i64, i64, i64, ptr, i64)
 declare void @flan_dyn_set_at(i64, i64, i64, ptr, i64)
 declare void @flan_dyn_push(i64, i64, ptr, i64)
 declare void @flan_dyn_print(i64)

runtime/flan_dyn.c

@@ -2930,6 +2930,33 @@ flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i, const uint8_t *loc,
   return o->u.v.items[k];
 }
 
+/* (slice s lo) and (slice s lo hi) over a text; nil for [hi] is the length.
+ * The typed slice of a string is a view, and this is a copy: a text is
+ * immutable, so no program can tell the two apart. A vec's slice would have
+ * to share its elements with the vec to mean what the typed one means, which
+ * a copy does not, so a vec traps by type rather than answering differently. */
+flan_dyn flan_dyn_slice(flan_dyn v, flan_dyn lo, flan_dyn hi,
+                        const uint8_t *loc, int64_t loclen) {
+  int64_t a, b, len;
+  flan_obj *o;
+  if (!is_text(v))
+    trap2(loc, loclen, TYPE_TRAP, "slice", "only a text is sliced", v, lo);
+  o = dyn_obj(v);
+  len = o->len;
+  a = need_index(loc, loclen, "slice", v, lo);
+  b = flan_dyn_tag(hi) == FLAN_DYN_TAG_NIL
+        ? len : need_index(loc, loclen, "slice", v, hi);
+  if (a < 0 || b < a || b > len) {
+    char sv[SAY_MAX];
+    say(sv, SAY_MAX, v);
+    flan_say(loc, loclen,
+             "dyn slice: [%lld %lld) is out of bounds for text of length %lld "
+             "— %s", (long long)a, (long long)b, (long long)len, sv);
+    flan_trap((const uint8_t *)"DynRange", 8);
+  }
+  return flan_dyn_from_bytes(obj_text_bytes(o) + a, b - a);
+}
+
 void flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x, const uint8_t *loc,
                      int64_t loclen) {
   int64_t k;

runtime/flan_dyn.h

@@ -217,6 +217,11 @@ flan_dyn flan_dyn_len(flan_dyn v);
 flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i, const uint8_t *loc,
                      int64_t loclen);
 
+/* A copy of the text's bytes [lo, hi); nil for [hi] is the length. A vec, or
+ * any other value, traps: see the definition. */
+flan_dyn flan_dyn_slice(flan_dyn v, flan_dyn lo, flan_dyn hi,
+                        const uint8_t *loc, int64_t loclen);
+
 /* Vec only — a text is immutable and says so rather than being copied. */
 void flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x, const uint8_t *loc,
                      int64_t loclen);

test/programs/dyn-slice.flan

@@ -0,0 +1,17 @@
+;; (slice d ...) over a dyn text, in the three spellings the typed slice has.
+;; The result is a text of its own; the source is untouched.
+;;
+;; With an argument, the last slice runs past the end and traps.
+
+(defn main [args [string]] i32
+  (let [d (the dyn "hello")]
+    (println (slice d))
+    (println (slice d 1))
+    (println (slice d 1 3))
+    (println (slice d 5))
+    (println (length (slice d 2)))
+    (println (= (slice d 0 2) "he"))
+    (println d)
+    (when (> (length args) 1)
+      (println (slice d 2 9))))
+  0)

test/test_acceptance.ml

@@ -5018,6 +5018,22 @@ level "1"
       "programs/dyn-vec.flan" dyn_vec_out;
     outputs ~x86:true "dyn: a heterogeneous vector, --x86"
       "programs/dyn-vec.flan" dyn_vec_out;
+    (* (slice d ...) over a dyn text, and the bound past the end trapping
+       with the site. *)
+    let dyn_slice_out = "hello\nello\nel\n\n3\ntrue\nhello\n" in
+    outputs "dyn: slice of a text" "programs/dyn-slice.flan" dyn_slice_out;
+    outputs ~x86:true "dyn: slice of a text, --x86"
+      "programs/dyn-slice.flan" dyn_slice_out;
+    (let exe = compile "programs/dyn-slice.flan" in
+     let code, text = run exe (Some "x") in
+     let want = "programs/dyn-slice.flan:16:16: dyn slice: [2 9) is out of \
+                 bounds for text of length 5" in
+     if code <> 134 || not (contains text want) then begin
+       incr failures;
+       Printf.printf
+         "FAIL  dyn: slice past the end\n        got: %S (exit %d)\n     \
+          wanted: %S (exit 134)\n" text code want
+     end);
     (* Maps and keywords, the M2 additions, over all three rows like the dyn
        cases above them. The expectations were captured from the running
        program, not composed: the map line pins the renderer's edn shape with