diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 4bebcc80d4..34fee1550b 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -116,8 +116,10 @@ reference counting is not needed (== 0). We don't use reference counting for obj
 marked as persistent.
 
 For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
-stored in compact regions, we use the page information to retrieve its size. This is not an option
-with mimalloc, so there we always use `m_cs_sz` (TODO: do everywhere?).
+stored in compact regions, we use the page information to retrieve its size so that we can reuse
+`m_cs_sz` to store the deletion list inline. Using the page information is not an option with
+mimalloc, so there we always use `m_cs_sz`; reusing it for the deletion list is fine in this case as
+we do not need the size after an object has been marked for deletion (see `lean_free_small_object`).
 
 During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
 These two fields together have 48-bits, and this is enough for modern computers.
@@ -421,7 +423,9 @@ static inline void lean_free_small_object(lean_object * o) {
 #ifdef LEAN_SMALL_ALLOCATOR
     lean_free_small(o);
 #elif defined(LEAN_MIMALLOC)
-    mi_free_size((void *)o, o->m_cs_sz);
+    // We must NOT use `m_cs_sz` here as it is repurposed for the deletion list; as `mi_free_size`
+    // is no different from `mi_free` at the time of writing, we don't lose anything from that.
+    mi_free((void *)o);
 #else
     size_t* ptr = (size_t*)o - 1;
     free_sized(ptr, *ptr + sizeof(size_t));