diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 8f2715c72ff4ce71959582900109e4e1d18a9770..aa8eb563b2fba3e6a8171c05d8cc1b3670e9af14 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -56,6 +56,9 @@ Section join_handle.
   Qed.
   Global Instance join_handle_ne : NonExpansive join_handle.
   Proof. apply type_contractive_ne, _. Qed.
+
+  (* TODO: Looks like in Rust, we have T: Send -> JoinHandle<T>: Send and
+     T:Sync -> JoinHandle<T>: Sync. *)
 End join_handle.
 
 Section spawn.