diff --git a/lib/check.ml b/lib/check.ml
index 18f4ce86..33633b18 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -9285,8 +9285,12 @@ and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
      else, and checks nothing: the caller is promising the bytes are that
      type, as with [slice-from]. Both backends already lower a Ptr-to-Ptr
      [Cast] to no instruction. Adding const is allowed; dropping it is not,
-     or a cast would undo the const [addr] put there. There is no cast between
-     a pointer and an integer, and no pointer arithmetic. *)
+     or a cast would undo the const [addr] put there. The rule is about the
+     outer pointer only: the cast is unchecked, so ((Ptr (Ptr u8)) q) over a
+     (Ptr const (Ptr const u8)) is refused for the outer const but a
+     (Ptr (Ptr const u8)) casts to (Ptr (Ptr u8)) — what lies deeper is the
+     writer's promise, like everything else the cast asserts. There is no cast
+     between a pointer and an integer, and no pointer arithmetic. *)
   | Ast.Call ({ Ast.e = Ast.Var "Ptr"; _ }, _)
     when (match type_of_expr head with Some _ -> true | None -> false) ->
     let target = resolve ctx.env (Option.get (type_of_expr head)) in
@@ -12688,6 +12692,19 @@ and ordinary_call ctx ~want loc name args =
            says what the view is: over a Vec it borrows the storage the Vec \
            owns, over an array or a string it looks at the value itself. \
            Write %s" call
+      else if name = "slice-from-ptr" then
+        (* The name this form had before; code written against it lands here.
+           Said as the form to write, with the reader's arguments, and not as
+           a rename — a first-time reader has no old name to be told about. *)
+        let call =
+          match args with
+          | [ p; n ] ->
+            "(slice-from " ^ spell_arg "p" p ^ " " ^ spell_arg "n" n ^ ")"
+          | _ -> "(slice-from p n)"
+        in
+        Loc.failk "check/unknown-function" loc
+          "there is no slice-from-ptr. A slice from a pointer and a count of \
+           the elements behind it is slice-from. Write %s" call
       else if no_such_rand name <> None then
         (* A retired randomness name, which is a name and not a near miss:
            "did you mean rand?" for [rand-f32] would be true and would not say
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 861451e7..c92e97c5 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2541,6 +2541,11 @@ let () =
   rejects_check "a pointer cast of an integer"
     "(defn f [x i64] (Ptr i32) ((Ptr i32) x))"
     ~needle:"no conversion between an integer and a pointer";
+  rejects_check "slice-from-ptr names slice-from"
+    "(defn f [p (Ptr i32) n i32] i32 (length (slice-from-ptr p n)))"
+    ~needle:"Write (slice-from p n)";
+  accepts "a pointer cast checks the outer const only"
+    "(defn f [q (Ptr (Ptr const u8))] (Ptr (Ptr u8)) ((Ptr (Ptr u8)) q))";
   rejects_check "a pointer cast of a dyn"
     "(defn f [x dyn] (Ptr i32) ((Ptr i32) x))"
     ~needle:"A dyn value never holds a pointer";
diff --git a/web/index.html b/web/index.html
index 44150fe4..570f9fcd 100644
--- a/web/index.html
+++ b/web/index.html
@@ -525,7 +525,7 @@ notation reads as exactly one data item.</p>
 <tr><td><code>(Map K V)</code></td><td>open addressing, owning, copies the same way. The only map spelling: braces in type position are not a type</td><td>data + len + log2cap + its allocator</td></tr>
 <tr><td><code>(Pool T)</code></td><td>generational slab storage, owning, copies the same way</td><td>items + slots + its allocator</td></tr>
 <tr><td><code>(Handle T)</code></td><td>a reference into a pool that reports a dead referent</td><td>index and generation packed into an <code>i64</code></td></tr>
-<tr><td><code>(Ptr T)</code></td><td>raw pointer. <code>((Ptr U) p)</code> reads it as a pointer to <code>U</code>; <code>(slice-from p n)</code> makes a <code>[T]</code> of the <code>n</code> elements behind it. Neither checks the memory</td><td>a pointer</td></tr>
+<tr><td><code>(Ptr T)</code></td><td>raw pointer. <code>((Ptr U) p)</code> reads it as a pointer to <code>U</code>, and may add <code>const</code> but not drop it (the outer pointer only: what it points at is taken on trust); <code>(slice-from p n)</code> makes a <code>[T]</code> of the <code>n</code> elements behind it. Neither checks the memory</td><td>a pointer</td></tr>
 <tr><td><code>(Ptr const T)</code></td><td>a pointer nothing is written through: the address of read-only storage, and what a C <code>const T *</code> takes. A <code>(Ptr T)</code> converts to one, never the reverse</td><td>a pointer</td></tr>
 <tr><td><code>(Option T)</code></td><td><code>Some</code> / <code>None</code></td><td>tag byte + T</td></tr>
 <tr><td><code>(Fn [T ...] R)</code></td><td>a function value, which may have captured</td><td>a code address and an environment pointer</td></tr>