fix: remove believe_me and assert_total violations

coq-jr/Foreign.idr: Replace believe_me callback coercion with typed
%foreign function pointer marshalling. No unsafe coercion needed.

xml-toolkit/Escape.idr: Replace 3 assert_total calls (strHead, head,
tail) with safe pattern matching on unpacked character lists.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

coq-ecosystem/coq-jr/src/abi/Foreign.idr

@@ -185,11 +185,17 @@ export
 %foreign "C:{{project}}_register_callback, lib{{project}}"
 prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
 
-||| Safe callback registration
+||| Foreign wrapper to marshal a callback function pointer via %foreign.
+||| The C layer receives a function pointer directly — no unsafe coercion needed.
+%foreign "C:{{project}}_register_callback, lib{{project}}"
+prim__registerCallbackFn : Bits64 -> (Bits64 -> Bits32 -> Bits32) -> PrimIO Bits32
+
+||| Safe callback registration using typed foreign function marshalling.
+||| Passes the callback as a typed function pointer rather than AnyPtr.
 export
 registerCallback : Handle -> Callback -> IO (Either Result ())
 registerCallback h cb = do
-  result <- primIO (prim__registerCallback (handlePtr h) (believe_me cb))
+  result <- primIO (prim__registerCallbackFn (handlePtr h) cb)
   pure $ case resultFromInt result of
     Just Ok => Right ()
     Just err => Left err

idris2-ecosystem/xml-toolkit/src/Xml744/Escape.idr

@@ -60,13 +60,16 @@ exfiltrate s =
   where
     replaceAll : String -> String -> String -> String
     replaceAll from to str =
-      case break (== (assert_total $ strHead from)) (unpack str) of
-        (before, []) => str
-        (before, rest) =>
-          if isPrefixOf (unpack from) rest
-            then pack before ++ to ++ replaceAll from to (pack $ drop (length from) rest)
-            else pack before ++ singleton (assert_total $ head rest) ++
-                 replaceAll from to (pack $ assert_total $ tail rest)
+      case unpack from of
+        [] => str  -- empty search string, return unchanged
+        (fc :: _) =>
+          case break (== fc) (unpack str) of
+            (before, []) => str
+            (before, (r :: rs)) =>
+              if isPrefixOf (unpack from) (r :: rs)
+                then pack before ++ to ++ replaceAll from to (pack $ drop (length from) (r :: rs))
+                else pack before ++ singleton r ++
+                     replaceAll from to (pack rs)
 
 ||| Check if a string contains any unescaped dangerous characters
 export