diff --git a/src/Init/System/Promise.lean b/src/Init/System/Promise.lean
index dcbbe302a5..e3586dab77 100644
--- a/src/Init/System/Promise.lean
+++ b/src/Init/System/Promise.lean
@@ -6,11 +6,15 @@ Authors: Gabriel Ebner
 prelude
 import Init.System.IO
 
+set_option linter.missingDocs true
+
 namespace IO
 
-/-- Internally, a `Promise` is just a `Task` that is in the "Promised" or "Finished" state. -/
-private opaque PromiseImpl (α : Type) : { P : Type // Nonempty α ↔ Nonempty P } :=
-  ⟨Task α, fun ⟨_⟩ => ⟨⟨‹_›⟩⟩, fun ⟨⟨_⟩⟩ => ⟨‹_›⟩⟩
+private opaque PromisePointed : NonemptyType.{0}
+
+private structure PromiseImpl (α : Type) : Type where
+  prom : PromisePointed.type
+  h    : Nonempty α
 
 /--
 `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`.
@@ -26,10 +30,10 @@ Every promise must eventually be resolved.
 Otherwise the memory used for the promise will be leaked,
 and any tasks depending on the promise's result will wait forever.
 -/
-def Promise (α : Type) : Type := (PromiseImpl α).1
+def Promise (α : Type) : Type := PromiseImpl α
 
-instance [Nonempty α] : Nonempty (Promise α) :=
-  (PromiseImpl α).2.1 inferInstance
+instance [s : Nonempty α] : Nonempty (Promise α) :=
+  Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }
 
 /-- Creates a new `Promise`. -/
 @[extern "lean_io_promise_new"]
@@ -43,15 +47,12 @@ Only the first call to this function has an effect.
 @[extern "lean_io_promise_resolve"]
 opaque Promise.resolve (value : α) (promise : @& Promise α) : BaseIO Unit
 
-private unsafe def Promise.resultImpl (promise : Promise α) : Task α :=
-  unsafeCast promise
-
 /--
 The result task of a `Promise`.
 
 The task blocks until `Promise.resolve` is called.
 -/
-@[implemented_by Promise.resultImpl]
+@[extern "lean_io_promise_result"]
 opaque Promise.result (promise : Promise α) : Task α :=
-  have : Nonempty α := (PromiseImpl α).2.2 ⟨promise⟩
+  have : Nonempty α := promise.h
   Classical.choice inferInstance
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index eb6a8c4a00..3077a8a4fd 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1033,6 +1033,8 @@ extern "C" LEAN_EXPORT b_obj_res lean_io_wait_any_core(b_obj_arg task_list) {
     return g_task_manager->wait_any(task_list);
 }
 
+// Internally, a `Promise` is just a `Task` that is in the "Promised" or "Finished" state
+
 extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg) {
     lean_always_assert(g_task_manager);
     bool keep_alive = false;
@@ -1050,6 +1052,11 @@ extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg
     return io_result_mk_ok(box(0));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_promise_result(obj_arg promise) {
+    // the task is the promise itself
+    return promise;
+}
+
 // =======================================
 // Natural numbers