A read-only slice refuses a dyn view without promising one later, and taking a read-only element's address is recorded as an open decision

TODO.org

@@ -948,6 +948,9 @@ deliberate absence.
 CLOSED: [2026-09-25]
 =[const T]=; a =[T]= converts at the top of a type or under another const slice, never inside a writable one. =(addr (at v i))= of a read-only element is allowed, since a =(Ptr T)= is the C boundary and has no const form; a store is what is refused.
 
+** TODO The address of a read-only element is taken without complaint
+=(addr (at v i))= over a =[const T]= answers a writable =(Ptr T)=, so =slice-from-ptr= launders one back into a =[T]=; a string's byte refuses the same =addr=. Allowed because raylib's =load-image-from-memory= and =get-codepoint-previous= have no other way to hand a =[const u8]= to C. Decision needed: a const pointer type, or a refusal plus another route to C.
+
 ** TODO (slice d 1) over a dyn string is refused where (at d i) works
 The typed and dyn spaces disagree about a spelling, which the standing rule
 forbids. A dyn slice should exist.

lib/check.ml

@@ -2563,11 +2563,11 @@ let box loc (e : Tast.expr) : Tast.expr =
      dyn side can tell a read-only one apart, so a [[const T]] does not
      cross. *)
   | Types.Slice (Types.Const, elem) ->
-    no_dyn_yet loc ~into:true e.Tast.ty
-      (Printf.sprintf
-         ": a dyn view can be written through, and a [const %s] can only be \
-          read. A dyn view is taken of the writable storage it came from"
-         (Types.to_string elem))
+    Loc.failk "check/dyn-const-view" loc
+      "%s does not cross into dyn: a dyn view can be written through, and a \
+       [const %s] can only be read. A dyn view is taken of the writable \
+       storage it came from"
+      (Types.to_string e.Tast.ty) (Types.to_string elem)
   | Types.Slice (Types.Mut, elem) ->
     (match view_elem elem with
      | None -> view_not_yet loc e.Tast.ty elem