perf: inline hot path of ST

src/Init/Internal/Order/Basic.lean

@@ -16,7 +16,7 @@ public import Init.System.IO  -- for `MonoBind` instance
 import all Init.Control.Except  -- for `MonoBind` instance
 import all Init.Control.StateRef  -- for `MonoBind` instance
 import all Init.Control.Option  -- for `MonoBind` instance
-import all Init.System.IO  -- for `MonoBind` instance
+import all Init.System.ST  -- for `MonoBind` instance
 
 public section
 
@@ -926,16 +926,17 @@ theorem monotone_stateTRun [PartialOrder γ]
     monotone (fun (x : γ) => StateT.run (f x) s) :=
   monotone_apply s _ hmono
 
--- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO is opaque
-noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
+-- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO and friends are opaque
+
+noncomputable instance [Nonempty ε] : CCPO (EST ε σ α) :=
   inferInstanceAs (CCPO ((s : _) → FlatOrder (.error Classical.ofNonempty (Classical.choice ⟨s⟩))))
 
-noncomputable instance [Nonempty ε] : MonoBind (EIO ε) where
+noncomputable instance [Nonempty ε] : MonoBind (EST ε σ) where
   bind_mono_left {_ _ a₁ a₂ f} h₁₂ := by
     intro s
     specialize h₁₂ s
     change FlatOrder.rel (a₁.bind f s) (a₂.bind f s)
-    simp only [EStateM.bind]
+    simp only [EST.bind]
     generalize a₁ s = a₁ at h₁₂; generalize a₂ s = a₂ at h₁₂
     cases h₁₂
     · exact .bot
@@ -943,11 +944,23 @@ noncomputable instance [Nonempty ε] : MonoBind (EIO ε) where
   bind_mono_right {_ _ a f₁ f₂} h₁₂ := by
     intro w
     change FlatOrder.rel (a.bind f₁ w) (a.bind f₂ w)
-    simp only [EStateM.bind]
+    simp only [EST.bind]
     split
     · apply h₁₂
     · exact .refl
 
+noncomputable instance [Nonempty α] : CCPO (ST σ α) :=
+  inferInstanceAs (CCPO ((s : _) → FlatOrder (.mk Classical.ofNonempty (Classical.choice ⟨s⟩))))
+
+noncomputable instance [Nonempty α] : CCPO (BaseIO α) :=
+  inferInstanceAs (CCPO (ST IO.RealWorld α))
+
+noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
+  inferInstanceAs (CCPO (EST ε IO.RealWorld α))
+
+noncomputable instance [Nonempty ε] : MonoBind (EIO ε) :=
+  inferInstanceAs (MonoBind (EST ε IO.RealWorld))
+
 end mono_bind
 
 section implication_order

src/Init/Prelude.lean

@@ -23,6 +23,16 @@ use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler
 
 universe u v w
 
+/-- Marker for information that has been erased by the code generator. -/
+unsafe axiom lcErased : Type
+
+/-- Marker for type dependency that has been erased by the code generator. -/
+unsafe axiom lcAny : Type
+
+/-- Internal representation of `Void` in the compiler. -/
+unsafe axiom lcVoid : Type
+
+
 /--
 The identity function. `id` takes an implicit argument `α : Sort u`
 (a type in any universe), and an argument `a : α`, and returns `a`.
@@ -135,15 +145,6 @@ It can be written as an empty tuple: `()`.
 -/
 @[match_pattern] abbrev Unit.unit : Unit := PUnit.unit
 
-/-- Marker for information that has been erased by the code generator. -/
-unsafe axiom lcErased : Type
-
-/-- Marker for type dependency that has been erased by the code generator. -/
-unsafe axiom lcAny : Type
-
-/-- Internal representation of `IO.RealWorld` in the compiler. -/
-unsafe axiom lcRealWorld : Type
-
 /--
 Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
 

src/Init/System/IO.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
+Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone, Henrik Böving
 -/
 module
 
@@ -18,7 +18,6 @@ public section
 open System
 
 opaque IO.RealWorld.nonemptyType : NonemptyType.{0}
-
 /--
 A representation of “the real world” that's used in `IO` monads to ensure that `IO` actions are not
 reordered.
@@ -28,6 +27,18 @@ reordered.
 instance IO.RealWorld.instNonempty : Nonempty IO.RealWorld :=
   by exact IO.RealWorld.nonemptyType.property
 
+/--
+An `IO` monad that cannot throw exceptions.
+-/
+@[expose] def BaseIO (α : Type) := ST IO.RealWorld α
+
+instance : Monad BaseIO := inferInstanceAs (Monad (ST IO.RealWorld))
+instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (ST IO.RealWorld))
+
+@[always_inline, inline]
+def BaseIO.map (f : α → β) (x : BaseIO α) : BaseIO β :=
+  f <$> x
+
 /--
 A monad that can have side effects on the external world or throw exceptions of type `ε`.
 
@@ -41,21 +52,7 @@ A monad that can have side effects on the external world or throw exceptions of
    def getWorld : IO (IO.RealWorld) := get
    ```
 -/
-@[expose] def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
-
-instance : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
-instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))
-instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))
-instance : OrElse (EIO ε α) := ⟨MonadExcept.orElse⟩
-instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
-
-/--
-An `IO` monad that cannot throw exceptions.
--/
-@[expose] def BaseIO := EIO Empty
-
-instance : Monad BaseIO := inferInstanceAs (Monad (EIO Empty))
-instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (EIO Empty))
+@[expose] def EIO (ε : Type) (α : Type) : Type := EST ε IO.RealWorld α
 
 /--
 Runs a `BaseIO` action, which cannot throw an exception, in any other `EIO` monad.
@@ -66,7 +63,7 @@ lifting](lean-manual://section/lifting-monads) rather being than called explicit
 @[always_inline, inline]
 def BaseIO.toEIO (act : BaseIO α) : EIO ε α :=
   fun s => match act s with
-  | EStateM.Result.ok a s => EStateM.Result.ok a s
+  | .mk a s => .ok a s
 
 instance : MonadLift BaseIO (EIO ε) := ⟨BaseIO.toEIO⟩
 
@@ -77,8 +74,8 @@ action that returns an `Except` value.
 @[always_inline, inline]
 def EIO.toBaseIO (act : EIO ε α) : BaseIO (Except ε α) :=
   fun s => match act s with
-  | EStateM.Result.ok a s     => EStateM.Result.ok (Except.ok a) s
-  | EStateM.Result.error ex s => EStateM.Result.ok (Except.error ex) s
+  | .ok a s     => .mk (.ok a) s
+  | .error ex s => .mk (.error ex) s
 
 /--
 Handles any exception that might be thrown by an `EIO ε` action, transforming it into an
@@ -87,8 +84,25 @@ exception-free `BaseIO` action.
 @[always_inline, inline]
 def EIO.catchExceptions (act : EIO ε α) (h : ε → BaseIO α) : BaseIO α :=
   fun s => match act s with
-  | EStateM.Result.ok a s     => EStateM.Result.ok a s
-  | EStateM.Result.error ex s => h ex s
+  | .ok a s     => .mk a s
+  | .error ex s => h ex s
+
+instance : Monad (EIO ε) := inferInstanceAs (Monad (EST ε IO.RealWorld))
+instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EST ε IO.RealWorld))
+instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EST ε IO.RealWorld))
+instance : OrElse (EIO ε α) := ⟨MonadExcept.orElse⟩
+instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EST ε IO.RealWorld α))
+
+@[always_inline, inline]
+def EIO.map (f : α → β) (x : EIO ε α) : EIO ε β :=
+  f <$> x
+
+@[always_inline, inline]
+protected def EIO.throw (e : ε) : EIO ε α := throw e
+
+@[always_inline, inline]
+protected def EIO.tryCatch (x : EIO ε α) (handle : ε → EIO ε α) : EIO ε α :=
+  MonadExceptOf.tryCatch x handle
 
 /--
 Converts an `Except ε` action into an `EIO ε` action.
@@ -101,6 +115,15 @@ def EIO.ofExcept (e : Except ε α) : EIO ε α :=
   | Except.ok a    => pure a
   | Except.error e => throw e
 
+@[always_inline, inline]
+def EIO.adapt (f : ε → ε') (m : EIO ε α) : EIO ε' α :=
+  fun s => match m s with
+  | .ok a s => .ok a s
+  | .error e s => .error (f e) s
+
+@[deprecated EIO.adapt (since := "2025-09-29"), always_inline, inline]
+def EIO.adaptExcept (f : ε → ε') (m : EIO ε α) : EIO ε' α := EIO.adapt f m
+
 open IO (Error) in
 /--
 A monad that supports arbitrary side effects and throwing exceptions of type `IO.Error`.
@@ -121,7 +144,7 @@ Converts an `EIO ε` action into an `IO` action by translating any exceptions th
 `IO.Error`s using `f`.
 -/
 @[inline] def EIO.toIO (f : ε → IO.Error) (act : EIO ε α) : IO α :=
-  act.adaptExcept f
+  act.adapt f
 
 /--
 Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `IO`
@@ -134,7 +157,7 @@ action that returns an `Except` value.
 Runs an `IO` action in some other `EIO` monad, using `f` to translate `IO` exceptions.
 -/
 @[inline] def IO.toEIO (f : IO.Error → ε) (act : IO α) : EIO ε α :=
-  act.adaptExcept f
+  act.adapt f
 
 /- After we inline `EState.run'`, the closed term `((), ())` is generated, where the second `()`
    represents the "initial world". We don't want to cache this closed term. So, we disable
@@ -154,8 +177,8 @@ duplicate, or delete calls to this function. The side effect may even be hoisted
 causing the side effect to occur at initialization time, even if it would otherwise never be called.
 -/
 @[noinline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
-  match fn.run (unsafeCast Unit.unit) with
-  | EStateM.Result.ok a _ => a
+  match fn (unsafeCast Unit.unit) with
+  | .mk a _ => a
 
 /--
 Executes arbitrary side effects in a pure context, with exceptions indicated via `Except`. This a
@@ -400,7 +423,7 @@ Pauses execution for the specified number of milliseconds.
 -/
 opaque sleep (ms : UInt32) : BaseIO Unit :=
   -- TODO: add a proper primitive for IO.sleep
-  fun s => dbgSleep ms fun _ => EStateM.Result.ok () s
+  fun s => dbgSleep ms fun _ => .mk () s
 
 /--
 Runs `act` in a separate `Task`, with priority `prio`. Because `IO` actions may throw an exception
@@ -1609,7 +1632,10 @@ the `IO` monad.
 -/
 abbrev Ref (α : Type) := ST.Ref IO.RealWorld α
 
-instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩
+instance : MonadLift (ST IO.RealWorld) BaseIO where
+  monadLift mx := fun s =>
+    match mx s with
+    | .mk s a => .mk s a
 
 /--
 Creates a new mutable reference cell that contains `a`.

src/Init/System/ST.lean

@@ -12,24 +12,112 @@ public import Init.Control.Reader
 
 public section
 
-/--
-A restricted version of `IO` in which mutable state and exceptions are the only side effects.
+opaque Void.nonemptyType (σ : Type) : NonemptyType.{0}
 
-It is possible to run `EST` computations in a non-monadic context using `runEST`.
--/
-@[expose] def EST (ε : Type) (σ : Type) : Type → Type := EStateM ε σ
+@[expose] def Void (σ : Type) : Type := Void.nonemptyType σ |>.type
+
+instance Void.instNonempty : Nonempty (Void σ) :=
+  by exact (Void.nonemptyType σ).property
+
+@[extern "lean_void_mk"]
+opaque Void.mk (x : σ) : Void σ
+
+structure ST.Out (σ : Type) (α : Type) where
+  val : α
+  state : Void σ
 
 /--
 A restricted version of `IO` in which mutable state is the only side effect.
 
 It is possible to run `ST` computations in a non-monadic context using `runST`.
 -/
-abbrev ST (σ : Type) := EST Empty σ
+abbrev ST (σ : Type) (α : Type) := Void σ → ST.Out σ α
 
-instance (ε σ : Type) : Monad (EST ε σ) := inferInstanceAs (Monad (EStateM _ _))
-instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) := inferInstanceAs (MonadExceptOf ε (EStateM _ _))
-instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) := inferInstanceAs (Inhabited (EStateM _ _ _))
-instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
+namespace ST
+
+@[always_inline, inline]
+protected def pure (x : α) : ST σ α := fun s => .mk x s
+
+@[always_inline, inline]
+protected def bind (x : ST σ α) (f : α → ST σ β) : ST σ β :=
+  fun s =>
+    match x s with
+    | .mk x s => f x s
+
+end ST
+
+instance (σ : Type) : Monad (ST σ) where
+  pure := ST.pure
+  bind := ST.bind
+
+@[always_inline]
+instance : MonadFinally (ST σ) where
+  tryFinally' x f := fun s =>
+    match x s with
+    | .mk x s =>
+      match f (some x) s with
+      | .mk y s => .mk (x, y) s
+
+instance {σ : Type} {α : Type} [Inhabited α] : Inhabited (ST σ α) where
+  default := fun s => .mk default s
+
+inductive EST.Out (ε : Type) (σ : Type) (α : Type) where
+  | ok : α → Void σ → EST.Out ε σ α
+  | error : ε → Void σ → EST.Out ε σ α
+
+/--
+A restricted version of `IO` in which mutable state and exceptions are the only side effects.
+
+It is possible to run `EST` computations in a non-monadic context using `runEST`.
+-/
+@[expose] def EST (ε : Type) (σ : Type) (α : Type) : Type := Void σ → EST.Out ε σ α
+
+namespace EST
+
+@[always_inline, inline]
+protected def pure (a : α) : EST ε σ α := fun s => .ok a s
+
+@[always_inline, inline]
+protected def bind (x : EST ε σ α) (f : α → EST ε σ β) : EST ε σ β :=
+  fun s => match x s with
+  | .ok a s    => f a s
+  | .error e s => .error e s
+
+@[always_inline, inline]
+protected def throw (e : ε) : EST ε σ α := fun s => .error e s
+
+@[always_inline, inline]
+protected def tryCatch (x : EST ε σ α) (handle : ε → EST ε σ α) : EST ε σ α :=
+  fun s => match x s with
+  | .ok a s => .ok a s
+  | .error e s => handle e s
+
+end EST
+
+instance (ε σ : Type) : Monad (EST ε σ) where
+  pure := EST.pure
+  bind := EST.bind
+
+@[always_inline]
+instance : MonadFinally (EST ε σ) where
+  tryFinally' x f := fun s =>
+    let r := x s
+    match r with
+    | .ok x s =>
+      match f (some x) s with
+      | .ok y s => .ok (x, y) s
+      | .error e s => .error e s
+    | .error e s =>
+      match f none s with
+      | .ok _ s => .error e s
+      | .error e s => .error e s
+
+instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) where
+  throw := EST.throw
+  tryCatch := EST.tryCatch
+
+instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) where
+  default := fun s => .error default s
 
 /--
 An auxiliary class used to infer the “state” of `EST` and `ST` monads.
@@ -37,6 +125,7 @@ An auxiliary class used to infer the “state” of `EST` and `ST` monads.
 class STWorld (σ : outParam Type) (m : Type → Type)
 
 instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n := ⟨⟩
+instance {σ} : STWorld σ (ST σ) := ⟨⟩
 instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
 
 /--
@@ -44,24 +133,22 @@ Runs an `EST` computation, in which mutable state and exceptions are the only si
 -/
 @[noinline, nospecialize]
 def runEST {ε α : Type} (x : (σ : Type) → EST ε σ α) : Except ε α :=
-  match x Unit () with
-  | EStateM.Result.ok a _     => Except.ok a
-  | EStateM.Result.error ex _ => Except.error ex
+  match x Unit (Void.mk ()) with
+  | .ok a _     => Except.ok a
+  | .error ex _ => Except.error ex
 
 /--
 Runs an `ST` computation, in which mutable state via `ST.Ref` is the only side effect.
 -/
 @[noinline, nospecialize]
 def runST {α : Type} (x : (σ : Type) → ST σ α) : α :=
-  match x Unit () with
-  | EStateM.Result.ok a _     => a
-  | EStateM.Result.error ex _ => nomatch ex
+  match x Unit (Void.mk ()) with
+  | .mk a _ => a
 
 @[always_inline]
 instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s =>
   match x s with
-  | EStateM.Result.ok a s     => EStateM.Result.ok a s
-  | EStateM.Result.error ex _ => nomatch ex⟩
+  | .mk a s => .ok a s⟩
 
 namespace ST
 

src/Lean/Compiler/IR/Basic.lean

@@ -54,6 +54,9 @@ instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
 
    - `tobject` an `object` or a `tagged` pointer
 
+   - `void` is used to identify uses of the state token from `BaseIO` which do no longer need
+     to be passed around etc. at this point in the pipeline.
+
    - `struct` and `union` are used to return small values (e.g., `Option`, `Prod`, `Except`)
       on the stack.
 
@@ -81,6 +84,7 @@ inductive IRType where
   | union (leanTypeName : Name) (types : Array IRType) : IRType
   -- TODO: Move this upwards after a stage0 update.
   | tagged
+  | void
   deriving Inhabited, BEq, Repr
 
 namespace IRType
@@ -99,6 +103,7 @@ def isObj : IRType → Bool
   | object  => true
   | tagged  => true
   | tobject => true
+  | void    => true
   | _       => false
 
 def isPossibleRef : IRType → Bool
@@ -113,9 +118,13 @@ def isErased : IRType → Bool
   | erased => true
   | _ => false
 
+def isVoid : IRType → Bool
+  | void => true
+  | _ => false
+
 def boxed : IRType → IRType
   | object | float | float32 => object
-  | tagged | uint8 | uint16 => tagged
+  | void | tagged | uint8 | uint16 => tagged
   | _ => tobject
 
 end IRType

src/Lean/Compiler/IR/Boxing.lean

@@ -42,7 +42,7 @@ private def N.mkFresh : N VarId :=
 
 def requiresBoxedVersion (env : Environment) (decl : Decl) : Bool :=
   let ps := decl.params
-  (ps.size > 0 && (decl.resultType.isScalar || ps.any (fun p => p.ty.isScalar || p.borrow) || isExtern env decl.name))
+  (ps.size > 0 && (decl.resultType.isScalar || ps.any (fun p => p.ty.isScalar || p.borrow || p.ty.isVoid) || isExtern env decl.name))
   || ps.size > closureMaxArgs
 
 def mkBoxedVersionAux (decl : Decl) : N Decl := do

src/Lean/Compiler/IR/EmitC.lean

@@ -69,6 +69,7 @@ def toCType : IRType → String
   | IRType.tagged     => "lean_object*"
   | IRType.tobject    => "lean_object*"
   | IRType.erased     => "lean_object*"
+  | IRType.void       => "lean_object*"
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 
@@ -110,6 +111,8 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
   unless ps.isEmpty do
     emit "("
     -- We omit erased parameters for extern constants
+    -- TODO: I think we are guaranteed to be allowed to remove erased parameters always as well
+    let ps := ps.filter (fun p => !p.ty.isVoid)
     let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isErased) else ps
     if ps.size > closureMaxArgs && isBoxedName decl.name then
       emit "lean_object**"
@@ -173,7 +176,7 @@ def emitMainFn : M Unit := do
     /- We disable panic messages because they do not mesh well with extracted closed terms.
        See issue #534. We can remove this workaround after we implement issue #467. -/
     emitLn "lean_set_panic_messages(false);"
-    emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */, lean_io_mk_world());")
+    emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */);")
     emitLn "lean_set_panic_messages(true);"
     emitLns ["lean_io_mark_end_initialization();",
              "if (lean_io_result_is_ok(res)) {",
@@ -188,9 +191,9 @@ def emitMainFn : M Unit := do
                " n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
                " in = n;",
               "}"]
-      emitLn ("res = " ++ leanMainFn ++ "(in, lean_io_mk_world());")
+      emitLn ("res = " ++ leanMainFn ++ "(in);")
     else
-      emitLn ("res = " ++ leanMainFn ++ "(lean_io_mk_world());")
+      emitLn ("res = " ++ leanMainFn ++ "();")
     emitLn "}"
     -- `IO _`
     let retTy := env.find? `main |>.get! |>.type |>.getForallBody
@@ -413,7 +416,8 @@ def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M
   -- We must remove erased arguments to extern calls.
   discard <| ys.size.foldM
     (fun i _ (first : Bool) =>
-      if ps[i]!.ty.isErased then
+      let ty := ps[i]!.ty
+      if ty.isErased || ty.isVoid then
         pure first
       else do
         unless first do emit ", "
@@ -433,9 +437,11 @@ def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do
   emitLhs z
   let decl ← getDecl f
   match decl with
-  | .fdecl .. | .extern _ _ _ { entries := [.opaque _], .. } =>
+  | .fdecl (xs := ps) .. | .extern (xs := ps) (ext := { entries := [.opaque _], .. }) .. =>
     emitCName f
-    if ys.size > 0 then emit "("; emitArgs ys; emit ")"
+    if ys.size > 0 then
+      let (ys, _) := ys.zip ps |>.filter (fun (_, p) => !p.ty.isVoid) |>.unzip
+      emit "("; emitArgs ys; emit ")"
     emitLn ";"
   | Decl.extern _ ps _ extData => emitExternCall f ps extData ys
 
@@ -575,22 +581,23 @@ def emitTailCall (v : Expr) : M Unit :=
     let ctx ← read
     let ps := ctx.mainParams
     if h : ps.size = ys.size then
+      let (ps, ys) := ps.zip ys |>.filter (fun (p, _) => !p.ty.isVoid) |>.unzip
       if overwriteParam ps ys then
         emitLn "{"
         ps.size.forM fun i _ => do
           let p := ps[i]
-          let y := ys[i]
+          let y := ys[i]!
           unless paramEqArg p y do
             emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
         ps.size.forM fun i _ => do
           let p := ps[i]
-          let y := ys[i]
+          let y := ys[i]!
           unless paramEqArg p y do emit p.x; emit " = _tmp_"; emit i; emitLn ";"
         emitLn "}"
       else
-        ys.size.forM fun i _ => do
+        ps.size.forM fun i _ => do
           let p := ps[i]
-          let y := ys[i]
+          let y := ys[i]!
           unless paramEqArg p y do emit p.x; emit " = "; emitArg y; emitLn ";"
       emitLn "goto _start;"
     else
@@ -676,6 +683,7 @@ def emitDeclAux (d : Decl) : M Unit := do
         if xs.size > closureMaxArgs && isBoxedName d.name then
           emit "lean_object** _args"
         else
+          let xs := xs.filter (fun p => !p.ty.isVoid)
           xs.size.forM fun i _ => do
             if i > 0 then emit ", "
             let x := xs[i]
@@ -717,7 +725,7 @@ def emitDeclInit (d : Decl) : M Unit := do
   if isIOUnitInitFn env n then
     if isIOUnitBuiltinInitFn env n then
       emit "if (builtin) {"
-    emit "res = "; emitCName n; emitLn "(lean_io_mk_world());"
+    emit "res = "; emitCName n; emitLn "();"
     emitLn "if (lean_io_result_is_error(res)) return res;"
     emitLn "lean_dec_ref(res);"
     if isIOUnitBuiltinInitFn env n then
@@ -727,7 +735,7 @@ def emitDeclInit (d : Decl) : M Unit := do
     | some initFn =>
       if getBuiltinInitFnNameFor? env d.name |>.isSome then
         emit "if (builtin) {"
-      emit "res = "; emitCName initFn; emitLn "(lean_io_mk_world());"
+      emit "res = "; emitCName initFn; emitLn "();"
       emitLn "if (lean_io_result_is_error(res)) return res;"
       emitCName n
       if d.resultType.isScalar then
@@ -744,16 +752,16 @@ def emitDeclInit (d : Decl) : M Unit := do
 def emitInitFn : M Unit := do
   let env ← getEnv
   let modName ← getModName
-  env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin, lean_object*);")
+  env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin);")
   emitLns [
     "static bool _G_initialized = false;",
-    "LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin, lean_object* w) {",
+    "LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin) {",
     "lean_object * res;",
     "if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));",
     "_G_initialized = true;"
   ]
   env.imports.forM fun imp => emitLns [
-    "res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin, lean_io_mk_world());",
+    "res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin);",
     "if (lean_io_result_is_error(res)) return res;",
     "lean_dec_ref(res);"]
   let decls := getDecls env

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -329,6 +329,7 @@ def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
   | IRType.tagged     => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.tobject    => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.erased     => do LLVM.pointerType (← LLVM.i8Type llvmctx)
+  | .void             => do LLVM.pointerType (← LLVM.i8Type llvmctx)
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 

src/Lean/Compiler/IR/Format.lean

@@ -66,6 +66,7 @@ private partial def formatIRType : IRType → Format
   | IRType.uint64       => "u64"
   | IRType.usize        => "usize"
   | IRType.erased       => "◾"
+  | IRType.void         => "void"
   | IRType.object       => "obj"
   | IRType.tagged       => "tagged"
   | IRType.tobject      => "tobj"

src/Lean/Compiler/IR/ToIR.lean

@@ -20,7 +20,8 @@ public section
 namespace Lean.IR
 
 open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
-                    LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl?)
+  LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl? LCNF.FVarSubst LCNF.MonadFVarSubst
+  LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar)
 
 namespace ToIR
 
@@ -28,14 +29,23 @@ structure BuilderState where
   vars : Std.HashMap FVarId Arg := {}
   joinPoints : Std.HashMap FVarId JoinPointId := {}
   nextId : Nat := 1
+  subst : LCNF.FVarSubst := {}
 
 abbrev M := StateRefT BuilderState CoreM
 
+instance : LCNF.MonadFVarSubst M false where
+  getSubst := return (← get).subst
+
+instance : LCNF.MonadFVarSubstState M where
+  modifySubst f := modify fun s => { s with subst := f s.subst }
+
 def M.run (x : M α) : CoreM α := do
   x.run' {}
 
 def getFVarValue (fvarId : FVarId) : M Arg := do
-  return (← get).vars.get! fvarId
+  match ← LCNF.normFVar fvarId with
+  | .fvar fvarId => return (← get).vars.get! fvarId
+  | .erased => return .erased
 
 def getJoinPointValue (fvarId : FVarId) : M JoinPointId := do
   return (← get).joinPoints.get! fvarId
@@ -98,10 +108,13 @@ def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
   | .usize i => ⟨.expr (.uproj i base), .usize⟩
   | .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
   | .erased => ⟨.erased, .erased⟩
+  | .void => ⟨.erased, .void⟩
 
 def lowerParam (p : LCNF.Param) : M Param := do
   let x ← bindVar p.fvarId
   let ty ← toIRType p.type
+  if ty.isVoid || ty.isErased then
+    Compiler.LCNF.addSubst p.fvarId .erased
   return { x, borrow := p.borrow, ty }
 
 mutual
@@ -117,40 +130,61 @@ partial def lowerCode (c : LCNF.Code) : M FnBody := do
     let joinPointId ← getJoinPointValue fvarId
     return .jmp joinPointId (← args.mapM lowerArg)
   | .cases cases =>
-    -- `casesOn` for inductive predicates should have already been expanded.
-    let .var varId := (← getFVarValue cases.discr) | unreachable!
-    return .case cases.typeName
-                 varId
-                 (← nameToIRType cases.typeName)
-                 (← cases.alts.mapM (lowerAlt varId))
+    if let some info ← hasTrivialStructure? cases.typeName then
+      assert! cases.alts.size == 1
+      let .alt ctorName ps k := cases.alts[0]! | unreachable!
+      assert! ctorName == info.ctorName
+      assert! info.fieldIdx < ps.size
+      for idx in 0...ps.size do
+        let p := ps[idx]!
+        if idx == info.fieldIdx then
+          LCNF.addSubst p.fvarId (.fvar cases.discr)
+        else
+          bindErased p.fvarId
+      lowerCode k
+    else
+      -- `casesOn` for inductive predicates should have already been expanded.
+      let .var varId := (← getFVarValue cases.discr) | unreachable!
+      return .case cases.typeName
+                   varId
+                   (← nameToIRType cases.typeName)
+                   (← cases.alts.mapM (lowerAlt varId))
   | .return fvarId =>
     return .ret (← getFVarValue fvarId)
   | .unreach .. => return .unreachable
   | .fun .. => panic! "all local functions should be λ-lifted"
 
 partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
-  match decl.value with
+  let value ← LCNF.normLetValue decl.value
+  match value with
   | .lit litValue =>
     let var ← bindVar decl.fvarId
     let ⟨litValue, type⟩ := lowerLitValue litValue
     return .vdecl var type (.lit litValue) (← lowerCode k)
   | .proj typeName i fvarId =>
-    match (← getFVarValue fvarId) with
-    | .var varId =>
-      let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
-        | panic! "projection of non-structure type"
-      let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
-      let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
-      match result with
-      | .expr e =>
-        let var ← bindVar decl.fvarId
-        return .vdecl var type e (← lowerCode k)
+    if let some info ← hasTrivialStructure? typeName then
+      if info.fieldIdx == i then
+        LCNF.addSubst decl.fvarId (.fvar fvarId)
+      else
+        bindErased decl.fvarId
+      lowerCode k
+    else
+      match (← getFVarValue fvarId) with
+      | .var varId =>
+        let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
+          | panic! "projection of non-structure type"
+        let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
+        let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
+        match result with
+        | .expr e =>
+          let var ← bindVar decl.fvarId
+          return .vdecl var type e (← lowerCode k)
+        | .erased =>
+          bindErased decl.fvarId
+          lowerCode k
       | .erased =>
         bindErased decl.fvarId
         lowerCode k
-    | .erased =>
-      bindErased decl.fvarId
-      lowerCode k
   | .const name _ args =>
     let irArgs ← args.mapM lowerArg
     if let some decl ← findDecl name then
@@ -160,43 +194,48 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
     let env ← Lean.getEnv
     match env.find? name with
     | some (.ctorInfo ctorVal) =>
-      let type ← nameToIRType ctorVal.induct
-      if type.isScalar then
-        let var ← bindVar decl.fvarId
-        return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
+      if let some info ← hasTrivialStructure? ctorVal.induct then
+        let arg := args[info.numParams + info.fieldIdx]!
+        LCNF.addSubst decl.fvarId arg
+        lowerCode k
+      else
+        let type ← nameToIRType ctorVal.induct
+        if type.isScalar then
+          let var ← bindVar decl.fvarId
+          return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
 
-      let ⟨ctorInfo, fields⟩ ← getCtorLayout name
-      let irArgs := irArgs.extract (start := ctorVal.numParams)
-      if irArgs.size != fields.size then
-        -- An overapplied constructor arises from compiler
-        -- transformations on unreachable code
-        return .unreachable
+        let ⟨ctorInfo, fields⟩ ← getCtorLayout name
+        let irArgs := irArgs.extract (start := ctorVal.numParams)
+        if irArgs.size != fields.size then
+          -- An overapplied constructor arises from compiler
+          -- transformations on unreachable code
+          return .unreachable
 
-      let objArgs : Array Arg ← do
-        let mut result : Array Arg := #[]
-        for h : i in *...fields.size do
-          match fields[i] with
-          | .object .. =>
-            result := result.push irArgs[i]!
-          | .usize .. | .scalar .. | .erased => pure ()
-        pure result
-      let objVar ← bindVar decl.fvarId
-      let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
-        let rec loop (i : Nat) : M FnBody := do
-          match irArgs[i]? with
-          | some (.var varId) =>
-            match fields[i]! with
-            | .usize usizeIdx =>
-              let k ← loop (i + 1)
-              return .uset objVar usizeIdx varId k
-            | .scalar _ offset argType =>
-              let k ← loop (i + 1)
-              return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
-            | .object .. | .erased => loop (i + 1)
-          | some .erased => loop (i + 1)
-          | none => lowerCode k
-        loop 0
-      return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
+        let objArgs : Array Arg ← do
+          let mut result : Array Arg := #[]
+          for h : i in *...fields.size do
+            match fields[i] with
+            | .object .. =>
+              result := result.push irArgs[i]!
+            | .usize .. | .scalar .. | .erased | .void => pure ()
+          pure result
+        let objVar ← bindVar decl.fvarId
+        let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
+          let rec loop (i : Nat) : M FnBody := do
+            match irArgs[i]? with
+            | some (.var varId) =>
+              match fields[i]! with
+              | .usize usizeIdx =>
+                let k ← loop (i + 1)
+                return .uset objVar usizeIdx varId k
+              | .scalar _ offset argType =>
+                let k ← loop (i + 1)
+                return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
+              | .object .. | .erased | .void => loop (i + 1)
+            | some .erased => loop (i + 1)
+            | none => lowerCode k
+          loop 0
+        return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
     | some (.defnInfo ..) | some (.opaqueInfo ..) =>
       mkFap name irArgs
     | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>

src/Lean/Compiler/IR/ToIRType.lean

@@ -17,7 +17,9 @@ public section
 namespace Lean
 namespace IR
 
-open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType)
+open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType
+  LCNF.TrivialStructureInfo LCNF.getOtherDeclBaseType LCNF.getParamTypes LCNF.instantiateForall
+  LCNF.Irrelevant.hasTrivialStructure?)
 
 def irTypeForEnum (numCtors : Nat) : IRType :=
   if numCtors == 1 then
@@ -34,6 +36,23 @@ def irTypeForEnum (numCtors : Nat) : IRType :=
 builtin_initialize irTypeExt : LCNF.CacheExtension Name IRType ←
   LCNF.CacheExtension.register
 
+builtin_initialize trivialStructureInfoExt :
+    LCNF.CacheExtension Name (Option LCNF.TrivialStructureInfo) ←
+  LCNF.CacheExtension.register
+
+/--
+The idea of this function is the same as in `ToMono`, however the notion of "irrelevancy" has
+changed because we now have the `void` type which can only be erased in impure context and thus at
+earliest at the conversion from mono to IR.
+-/
+def hasTrivialStructure? (declName : Name) : CoreM (Option LCNF.TrivialStructureInfo) := do
+  let isVoidType type := do
+    let type ← Meta.whnfD type
+    return type matches .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _)
+  let irrelevantType type :=
+    Meta.isProp type <||> Meta.isTypeFormerType type <||> isVoidType type
+  LCNF.Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
+
 def nameToIRType (name : Name) : CoreM IRType := do
   match (← irTypeExt.find? name) with
   | some type => return type
@@ -54,7 +73,7 @@ where fillCache : CoreM IRType := do
     -- `Int` is specified as an inductive type with two constructors that have relevant arguments,
     -- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
     | ``Int => return .tobject
-    | ``lcRealWorld => return .tagged
+    | ``lcVoid => return .void
     | _ =>
       let env ← Lean.getEnv
       let some (.inductInfo inductiveVal) := env.find? name | return .tobject
@@ -86,13 +105,13 @@ private def isAnyProducingType (type : Lean.Expr) : Bool :=
   | .forallE _ _ b _ => isAnyProducingType b
   | _ => false
 
-def toIRType (type : Lean.Expr) : CoreM IRType := do
+partial def toIRType (type : Lean.Expr) : CoreM IRType := do
   match type with
-  | .const name _ => nameToIRType name
+  | .const name _ => visitApp name #[]
   | .app .. =>
     -- All mono types are in headBeta form.
     let .const name _ := type.getAppFn | unreachable!
-    nameToIRType name
+    visitApp name type.getAppArgs
   | .forallE _ _ b _ =>
     -- Type formers are erased, but can be used polymorphically as
     -- an arrow type producing `lcAny`. The runtime representation of
@@ -104,18 +123,28 @@ def toIRType (type : Lean.Expr) : CoreM IRType := do
       return .object
   | .mdata _ b => toIRType b
   | _ => unreachable!
+where
+  visitApp (declName : Name) (args : Array Lean.Expr) : CoreM IRType := do
+    if let some info ← hasTrivialStructure? declName then
+      let ctorType ← LCNF.getOtherDeclBaseType info.ctorName []
+      let monoType ← LCNF.toMonoType (LCNF.getParamTypes (← LCNF.instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
+      toIRType monoType
+    else
+      nameToIRType declName
 
 inductive CtorFieldInfo where
   | erased
   | object (i : Nat) (type : IRType)
   | usize  (i : Nat)
   | scalar (sz : Nat) (offset : Nat) (type : IRType)
+  | void
   deriving Inhabited
 
 namespace CtorFieldInfo
 
 def format : CtorFieldInfo → Format
   | erased => "◾"
+  | void => "void"
   | object i type => f!"obj@{i}:{type}"
   | usize i    => f!"usize@{i}"
   | scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
@@ -160,6 +189,7 @@ where fillCache := do
         pure <| .object i irFieldType
       | .usize => pure <| .usize 0
       | .erased => .pure <| .erased
+      | .void => .pure <| .void
       | .uint8 =>
         has1BScalar := true
         .pure <| .scalar 1 0 .uint8
@@ -186,7 +216,7 @@ where fillCache := do
       | .usize _ => do
         let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
         return .usize i
-      | .object .. | .scalar .. | .erased => return field
+      | .object .. | .scalar .. | .erased | .void => return field
     let numUSize := nextIdx - numObjs
     let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
         : Array CtorFieldInfo × Nat :=
@@ -198,7 +228,7 @@ where fillCache := do
             return .scalar sz offset type
           else
             return field
-        | .object .. | .usize _ | .erased => return field
+        | .object .. | .usize _ | .erased | .void => return field
     let mut nextOffset := 0
     if has8BScalar then
       ⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset

src/Lean/Compiler/LCNF.lean

@@ -44,3 +44,4 @@ public import Lean.Compiler.LCNF.Closure
 public import Lean.Compiler.LCNF.LambdaLifting
 public import Lean.Compiler.LCNF.ReduceArity
 public import Lean.Compiler.LCNF.Probing
+public import Lean.Compiler.LCNF.Irrelevant

src/Lean/Compiler/LCNF/Irrelevant.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Compiler.LCNF.BaseTypes
+import Lean.Compiler.LCNF.Util
+
+namespace Lean.Compiler.LCNF
+
+/--
+Given a constructor, return a bitmask `m` s.t. `m[i]` is true if field `i` is
+computationally relevant.
+-/
+def getRelevantCtorFields (ctorName : Name) (trivialType : Expr → MetaM Bool) :
+    CoreM (Array Bool) := do
+  let .ctorInfo info ← getConstInfo ctorName | unreachable!
+  Meta.MetaM.run' do
+    Meta.forallTelescopeReducing info.type fun xs _ => do
+      let mut result := #[]
+      for x in xs[info.numParams...*] do
+        let type ← Meta.inferType x
+        result := result.push !(← trivialType type)
+      return result
+
+/--
+We say a structure has a trivial structure if it has not builtin support in the runtime,
+it has only one constructor, and this constructor has only one relevant field.
+-/
+public structure TrivialStructureInfo where
+  ctorName  : Name
+  numParams : Nat
+  fieldIdx  : Nat
+  deriving Inhabited, Repr
+
+/--
+Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
+- It does not have builtin support in the runtime.
+- It has only one constructor.
+- This constructor has only one computationally relevant field.
+-/
+public def Irrelevant.hasTrivialStructure?
+    (cacheExt : CacheExtension Name (Option TrivialStructureInfo))
+    (trivialType : Expr → MetaM Bool) (declName : Name) : CoreM (Option TrivialStructureInfo) := do
+  match (← cacheExt.find? declName) with
+  | some info? => return info?
+  | none =>
+    let info? ← fillCache
+    cacheExt.insert declName info?
+    return info?
+where fillCache : CoreM (Option TrivialStructureInfo) := do
+  if isRuntimeBuiltinType declName then return none
+  let .inductInfo info ← getConstInfo declName | return none
+  if info.isUnsafe || info.isRec then return none
+  let [ctorName] := info.ctors | return none
+  let ctorType ← getOtherDeclBaseType ctorName []
+  if ctorType.isErased then return none
+  let mask ← getRelevantCtorFields ctorName trivialType
+  let mut result := none
+  for h : i in *...mask.size do
+    if mask[i] then
+      if result.isSome then return none
+      result := some { ctorName, fieldIdx := i, numParams := info.numParams }
+  return result
+
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -10,36 +10,13 @@ public import Lean.Meta.InferType
 public import Lean.Compiler.LCNF.Util
 public import Lean.Compiler.LCNF.BaseTypes
 public import Lean.Compiler.LCNF.CompilerM
+public import Lean.Compiler.LCNF.Irrelevant
 
 public section
 
 namespace Lean.Compiler.LCNF
 
-/--
-Given a constructor, return a bitmask `m` s.t. `m[i]` is true if field `i` is
-computationally relevant.
--/
-def getRelevantCtorFields (ctorName : Name) : CoreM (Array Bool) := do
-  let .ctorInfo info ← getConstInfo ctorName | unreachable!
-  Meta.MetaM.run' do
-    Meta.forallTelescopeReducing info.type fun xs _ => do
-      let mut result := #[]
-      for x in xs[info.numParams...*] do
-        let type ← Meta.inferType x
-        result := result.push !(← Meta.isProp type <||> Meta.isTypeFormerType type)
-      return result
-
-/--
-We say a structure has a trivial structure if it has not builtin support in the runtime,
-it has only one constructor, and this constructor has only one relevant field.
--/
-structure TrivialStructureInfo where
-  ctorName  : Name
-  numParams : Nat
-  fieldIdx  : Nat
-  deriving Inhabited, Repr
-
-builtin_initialize trivialStructureInfoExt : CacheExtension Name (Option TrivialStructureInfo) ←
+private builtin_initialize trivialStructureInfoExt : CacheExtension Name (Option TrivialStructureInfo) ←
   CacheExtension.register
 
 /--
@@ -49,26 +26,8 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
 - This constructor has only one computationally relevant field.
 -/
 def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
-  match (← trivialStructureInfoExt.find? declName) with
-  | some info? => return info?
-  | none =>
-    let info? ← fillCache
-    trivialStructureInfoExt.insert declName info?
-    return info?
-where fillCache : CoreM (Option TrivialStructureInfo) := do
-  if isRuntimeBuiltinType declName then return none
-  let .inductInfo info ← getConstInfo declName | return none
-  if info.isUnsafe || info.isRec then return none
-  let [ctorName] := info.ctors | return none
-  let ctorType ← getOtherDeclBaseType ctorName []
-  if ctorType.isErased then return none
-  let mask ← getRelevantCtorFields ctorName
-  let mut result := none
-  for h : i in *...mask.size do
-    if mask[i] then
-      if result.isSome then return none
-      result := some { ctorName, fieldIdx := i, numParams := info.numParams }
-  return result
+  let irrelevantType type := Meta.isProp type <||> Meta.isTypeFormerType type
+  Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
 
 def getParamTypes (type : Expr) : Array Expr :=
   go type #[]

src/Lean/Compiler/LCNF/Types.lean

@@ -163,8 +163,8 @@ where
     | .forallE .. => visitForall type #[]
     | .app ..  => type.withApp visitApp
     | .fvar .. => visitApp type #[]
-    | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
-      return mkConst ``lcRealWorld
+    | .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _) =>
+      return mkConst ``lcVoid
     | _        => return mkConst ``lcAny
 
   whnfEta (type : Expr) : MetaM Expr := do

src/Lean/LoadDynlib.lean

@@ -38,7 +38,7 @@ opaque Dynlib.get? (dynlib : @& Dynlib) (sym : @& String) : Option dynlib.Symbol
 /--
 Runs a module initializer function.
 The symbol should have the signature `(builtin : Bool) → IO Unit`
-(e.g., `initialize_Foo(uint8_t builtin, obj_arg)`).
+(e.g., `initialize_Foo(uint8_t builtin)`).
 
 This function is unsafe because there is no guarantee the symbol has the
 expected signature. An invalid symbol can thus produce undefined behavior.

src/Lean/Server/Requests.lean

@@ -258,7 +258,7 @@ open FileWorker
 open Snapshots
 
 def runInIO (x : RequestM α) (ctx : RequestContext) : IO α := do
-  x.run ctx |>.adaptExcept (IO.userError ·.message)
+  x.run ctx |>.adapt (IO.userError ·.message)
 
 def readDoc [Monad m] [MonadReaderOf RequestContext m] : m EditableDocument := do
   let rc ← readThe RequestContext

src/Std/Do/WP.lean

@@ -8,5 +8,4 @@ module
 prelude
 public import Std.Do.WP.Basic
 public import Std.Do.WP.Monad
-public import Std.Do.WP.IO
 public import Std.Do.WP.SimpLemmas

src/Std/Do/WP/IO.lean

@@ -1,43 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Init.System.IO
-public import Std.Do.WP.Monad
-
-@[expose] public section
-
-/-!
-# Barebones `WP` instance for `IO`
-
-This module defines a `WP` instance for `IO` without any synthetic model of the `IO.RealWorld` whatsoever.
-This is useful for reasoning about `IO` programs when the precise result of a side-effect is irrelevant;
-for example it can be used to reason about random number generation.
-It is however inadequate for reasoning about, e.g., `IO.Ref`s.
--/
-
-namespace Std.Do.IO.Bare
-
-open Std.Do
-
-/--
-This is pretty much the instance for `EStateM` specialized to `σ = IO.RealWorld`.
-However, `IO.RealWorld` is omitted in the `PredShape`.
--/
-noncomputable scoped instance instWP : WP (EIO ε) (.except ε .pure) where
-  wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
-    { apply := fun Q => match x Classical.ofNonempty with
-        | .ok a _rw => Q.1 a
-        | .error e _rw => Q.2.1 e
-      conjunctive := by
-        intro _ _
-        apply SPred.bientails.of_eq
-        dsimp
-        cases (x Classical.ofNonempty) <;> rfl
-    }
-
-instance instLawfulMonad : LawfulMonad (EIO ε) := inferInstanceAs (LawfulMonad (EStateM ε IO.RealWorld))

src/Std/Internal/Async/Basic.lean

@@ -166,7 +166,7 @@ Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an e
 protected def bindEIO (x : ETask ε α) (f : α → EIO ε (ETask ε β)) (prio := Task.Priority.default) (sync := false) : EIO ε (ETask ε β) :=
   EIO.bindTask x (prio := prio) (sync := sync) fun
     | .ok a => f a
-    | .error e => .error e
+    | .error e => throw e
 
 /--
 Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an error, the returned
@@ -176,7 +176,7 @@ Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an e
 protected def mapEIO (f : α → EIO ε β) (x : ETask ε α) (prio := Task.Priority.default) (sync := false) : BaseIO (ETask ε β) :=
   EIO.mapTask (t := x) (prio := prio) (sync := sync) fun
     | .ok a => f a
-    | .error e => .error e
+    | .error e => throw e
 
 /--
 Block until the `ETask` in `x` finishes and returns its value. Propagates any error encountered
@@ -186,7 +186,7 @@ during execution.
 def block (x : ETask ε α) : EIO ε α := do
   match x.get with
   | .ok a => return a
-  | .error e => .error e
+  | .error e => throw e
 
 /--
 Create an `ETask` that resolves to the value of the promise `x`. If the promise gets dropped then it
@@ -235,7 +235,7 @@ Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an err
 protected def mapIO (f : α → IO β) (x : AsyncTask α) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
   EIO.mapTask (t := x) (prio := prio) (sync := sync) fun
     | .ok a => f a
-    | .error e => .error e
+    | .error e => throw e
 
 /--
 Construct an `AsyncTask` that is already resolved with value `x`.
@@ -274,7 +274,7 @@ Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an er
 def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
   IO.bindTask x (prio := prio) (sync := sync) fun
     | .ok a => f a
-    | .error e => .error e
+    | .error e => throw e
 
 /--
 Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
@@ -284,7 +284,7 @@ Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an err
 def mapTaskIO (f : α → IO β) (x : AsyncTask α) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
   IO.mapTask (t := x) (prio := prio) (sync := sync) fun
     | .ok a => f a
-    | .error e => .error e
+    | .error e => throw e
 
 /--
 Block until the `AsyncTask` in `x` finishes.
@@ -292,7 +292,7 @@ Block until the `AsyncTask` in `x` finishes.
 def block (x : AsyncTask α) : IO α :=
   match x.get with
   | .ok a => return a
-  | .error e => .error e
+  | .error e => throw e
 
 /--
 Create an `AsyncTask` that resolves to the value of `x`.
@@ -450,7 +450,7 @@ Lifts a `BaseIO` action into a `BaseAsync` computation.
 -/
 @[inline]
 protected def lift (x : BaseIO α) : BaseAsync α :=
-  .mk <| (.pure ∘ .pure) =<< x
+  .mk <| (pure ∘ pure) =<< x
 
 /--
 Waits for the result of the `BaseAsync` computation, blocking if necessary.
@@ -638,7 +638,7 @@ protected def wait (self : EAsync ε α) : EIO ε α := do
   let result ← self |> BaseAsync.wait
   match result with
   | .ok a => return a
-  | .error e => .error e
+  | .error e => throw e
 
 /--
 Lifts an `EAsync` computation into an `ETask` that can be awaited and joined.

src/include/lean/lean.h

@@ -2828,10 +2828,31 @@ LEAN_EXPORT lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
 LEAN_EXPORT lean_obj_res lean_decode_uv_error(int errnum, b_lean_obj_arg fname);
 
 static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }
+
+static inline lean_obj_res lean_void_mk(lean_obj_arg a) {
+    lean_dec(a);
+    return lean_box(0);
+}
+
+static inline b_lean_obj_res lean_baseio_out_val(b_lean_obj_arg r) {
+    // TODO: This function needs to become identity after we are done.
+    // return lean_ctor_get(r, 0);
+    return r;
+}
+
+static inline lean_obj_res lean_mk_baseio_out(lean_obj_arg i) {
+    // lean_object * r = lean_alloc_ctor(0, 2, 0);
+    // lean_ctor_set(r, 0, i);
+    // lean_ctor_set(r, 1, lean_box(0));
+    // return i;
+    return i;
+}
+
 static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; }
 static inline bool lean_io_result_is_error(b_lean_obj_arg r) { return lean_ptr_tag(r) == 1; }
 static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert(lean_io_result_is_ok(r)); return lean_ctor_get(r, 0); }
 static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); }
+
 static inline lean_obj_res lean_io_result_take_value(lean_obj_arg r) {
     assert(lean_io_result_is_ok(r));
     lean_object* v = lean_ctor_get(r, 0);
@@ -2839,18 +2860,17 @@ static inline lean_obj_res lean_io_result_take_value(lean_obj_arg r) {
     lean_dec(r);
     return v;
 }
+
 LEAN_EXPORT void lean_io_result_show_error(b_lean_obj_arg r);
 LEAN_EXPORT void lean_io_mark_end_initialization(void);
 static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) {
-    lean_object * r = lean_alloc_ctor(0, 2, 0);
+    lean_object * r = lean_alloc_ctor(0, 1, 0);
     lean_ctor_set(r, 0, a);
-    lean_ctor_set(r, 1, lean_box(0));
     return r;
 }
 static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
-    lean_object * r = lean_alloc_ctor(1, 2, 0);
+    lean_object * r = lean_alloc_ctor(1, 1, 0);
     lean_ctor_set(r, 0, e);
-    lean_ctor_set(r, 1, lean_box(0));
     return r;
 }
 
@@ -2882,11 +2902,81 @@ LEAN_EXPORT lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
 
 
 /* ST Ref primitives */
-LEAN_EXPORT lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
-LEAN_EXPORT lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
-LEAN_EXPORT lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
-LEAN_EXPORT lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
-LEAN_EXPORT lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
+
+/*
+  Important: we have added support for initializing global constants
+  at program startup. This feature is particularly useful for
+  initializing `ST.Ref` values. Any `ST.Ref` value created during
+  initialization will be marked as persistent. Thus, to make `ST.Ref`
+  API thread-safe, we must treat persistent `ST.Ref` objects created
+  during initialization as a multi-threaded object. Then, whenever we store
+  a value `val` into a global `ST.Ref`, we have to mark `va`l as a multi-threaded
+  object as we do for multi-threaded `ST.Ref`s. It makes sense since
+  the global `ST.Ref` may be used to communicate data between threads.
+*/
+static inline bool lean_st_ref_maybe_mt(b_lean_obj_arg ref) {
+    return lean_is_mt(ref) || lean_is_persistent(ref);
+}
+
+static inline lean_obj_res lean_st_mk_result(lean_obj_arg a) {
+    return a;
+}
+
+LEAN_EXPORT lean_obj_res lean_st_mk_ref(lean_obj_arg);
+
+LEAN_EXPORT lean_obj_res lean_st_ref_get_mt(b_lean_obj_arg);
+static inline lean_obj_res lean_st_ref_get(b_lean_obj_arg ref) {
+    if (LEAN_UNLIKELY(lean_st_ref_maybe_mt(ref))) {
+        return lean_st_ref_get_mt(ref);
+    } else {
+        lean_object * val = lean_to_ref(ref)->m_value;
+        assert(val != NULL);
+        lean_inc(val);
+        return lean_st_mk_result(val);
+    }
+}
+
+LEAN_EXPORT lean_obj_res lean_st_ref_take_mt(b_lean_obj_arg);
+static inline lean_obj_res lean_st_ref_take(b_lean_obj_arg ref) {
+    if (LEAN_UNLIKELY(lean_st_ref_maybe_mt(ref))) {
+        return lean_st_ref_take_mt(ref);
+    } else {
+        lean_object * val = lean_to_ref(ref)->m_value;
+        assert(val != NULL);
+        lean_to_ref(ref)->m_value = NULL;
+        return lean_st_mk_result(val);
+    }
+}
+
+LEAN_EXPORT lean_obj_res lean_st_ref_set_mt(b_lean_obj_arg, lean_obj_arg);
+static inline lean_obj_res lean_st_ref_set(b_lean_obj_arg ref, lean_obj_arg a) {
+    if (LEAN_UNLIKELY(lean_st_ref_maybe_mt(ref))) {
+        return lean_st_ref_set_mt(ref, a);
+    } else {
+        if (lean_to_ref(ref)->m_value != NULL)
+            lean_dec(lean_to_ref(ref)->m_value);
+        lean_to_ref(ref)->m_value = a;
+        return lean_st_mk_result(lean_box(0));
+    }
+}
+
+LEAN_EXPORT lean_obj_res lean_st_ref_swap_mt(b_lean_obj_arg, lean_obj_arg);
+static inline lean_obj_res lean_st_ref_swap(b_lean_obj_arg ref, lean_obj_arg a) {
+    if (LEAN_UNLIKELY(lean_st_ref_maybe_mt(ref))) {
+        return lean_st_ref_swap_mt(ref, a);
+    } else {
+        lean_object * old_a = lean_to_ref(ref)->m_value;
+        if (old_a == NULL)
+            lean_internal_panic("null reference read");
+        lean_to_ref(ref)->m_value = a;
+        return lean_st_mk_result(old_a);
+    }
+}
+
+static inline uint8_t lean_st_ref_ptr_eq(b_lean_obj_arg ref1, b_lean_obj_arg ref2) {
+    // TODO(Leo): ref_maybe_mt
+    return lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value;
+}
 
 /* pointer address unsafe primitive  */
 static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; }

src/initialize/init.cpp

@@ -16,9 +16,9 @@ Author: Leonardo de Moura
 #include "initialize/init.h"
 
 namespace lean {
-extern "C" object* initialize_Init(uint8_t, object* w);
-extern "C" object* initialize_Std(uint8_t, object* w);
-extern "C" object* initialize_Lean(uint8_t, object* w);
+extern "C" object* initialize_Init(uint8_t);
+extern "C" object* initialize_Std(uint8_t);
+extern "C" object* initialize_Lean(uint8_t);
 
 /* Initializes the Lean runtime. Before executing any code which uses the Lean package,
 you must first call this function, and then `lean::io_mark_end_initialization`. In between
@@ -32,9 +32,9 @@ extern "C" LEAN_EXPORT void lean_initialize() {
     // * calling exported Lean functions from C++
     // * calling into native code of the current module from a previous stage when `prefer_native`
     //   is set
-    consume_io_result(initialize_Init(builtin, io_mk_world()));
-    consume_io_result(initialize_Std(builtin, io_mk_world()));
-    consume_io_result(initialize_Lean(builtin, io_mk_world()));
+    consume_io_result(initialize_Init(builtin));
+    consume_io_result(initialize_Std(builtin));
+    consume_io_result(initialize_Lean(builtin));
     initialize_kernel_module();
     init_default_print_fn();
     initialize_library_core_module();

src/kernel/trace.cpp

@@ -122,9 +122,9 @@ scope_trace_env::~scope_trace_env() {
     get_disabled_trace_classes().resize(m_disable_sz);
 }
 
-extern "C" obj_res lean_io_eprint(obj_arg s, obj_arg w);
+extern "C" obj_res lean_io_eprint(obj_arg s);
 static void io_eprint(obj_arg s) {
-    object * r = lean_io_eprint(s, lean_io_mk_world());
+    object * r = lean_io_eprint(s);
     if (!lean_io_result_is_ok(r))
         lean_io_result_show_error(r);
     lean_dec(r);
@@ -161,7 +161,7 @@ extern "C" lean_object* lean_mk_metavar_ctx(lean_object*);
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
 */
-extern "C" object * lean_pp_expr(object * env, object * mctx, object * lctx, object * opts, object * e, object * w);
+extern "C" object * lean_pp_expr(object * env, object * mctx, object * lctx, object * opts, object * e);
 
 /*
 @[export lean_format_pretty]
@@ -173,7 +173,7 @@ std::string pp_expr(elab_environment const & env, options const & opts, local_ct
     options o = opts;
     // o = o.update(name{"pp", "proofs"}, true); --
     object_ref fmt = get_io_result<object_ref>(lean_pp_expr(env.to_obj_arg(), lean_mk_metavar_ctx(lean_box(0)), lctx.to_obj_arg(), o.to_obj_arg(),
-                                                            e.to_obj_arg(), io_mk_world()));
+                                                            e.to_obj_arg()));
     string_ref str(lean_format_pretty(fmt.to_obj_arg(), lean_unsigned_to_nat(80), lean_unsigned_to_nat(0), lean_unsigned_to_nat(0)));
     return str.to_std_string();
 }

src/lake/Lake/CLI/Main.lean

@@ -98,7 +98,7 @@ def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall
 /-- Compute the Lake environment based on `opts`. Error if an install is missing. -/
 def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
   Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) opts.elanInstall?
-    opts.noCache |>.adaptExcept fun msg => .invalidEnv msg
+    opts.noCache |>.adapt fun msg => .invalidEnv msg
 
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
 public def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig := do

src/library/dynlib.cpp

@@ -67,7 +67,7 @@ static inline void * symbol_ptr(b_obj_arg sym) {
 }
 
 /* Dynlib.load : System.FilePath -> IO Dynlib */
-extern "C" LEAN_EXPORT obj_res lean_dynlib_load(b_obj_arg path, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_dynlib_load(b_obj_arg path) {
 #ifdef LEAN_WINDOWS
     HMODULE h = LoadLibrary(string_cstr(path));
     if (!h) {
@@ -114,22 +114,22 @@ extern "C" LEAN_EXPORT obj_res lean_dynlib_get(b_obj_arg dynlib, b_obj_arg name)
 }
 
 /* Dynlib.Symbol.runAsInit : {Dynlib} -> Symbol -> IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_dynlib_symbol_run_as_init(b_obj_arg /* dynlib */, b_obj_arg sym, obj_arg) {
-    auto init_fn = reinterpret_cast<object *(*)(uint8_t, object *)>(symbol_ptr(sym));
-    return init_fn(1 /* builtin */, io_mk_world());
+extern "C" LEAN_EXPORT obj_res lean_dynlib_symbol_run_as_init(b_obj_arg /* dynlib */, b_obj_arg sym) {
+    auto init_fn = reinterpret_cast<object *(*)(uint8_t)>(symbol_ptr(sym));
+    return init_fn(1 /* builtin */);
 }
 
 /* Lean.loadDynlib : System.FilePath -> IO Unit */
-extern "C" obj_res lean_load_dynlib(obj_arg path, obj_arg);
+extern "C" obj_res lean_load_dynlib(obj_arg path);
 
 void load_dynlib(std::string path) {
-    consume_io_result(lean_load_dynlib(mk_string(path), io_mk_world()));
+    consume_io_result(lean_load_dynlib(mk_string(path)));
 }
 
 /* Lean.loadPlugin : System.FilePath -> IO Unit */
-extern "C" obj_res lean_load_plugin(obj_arg path, obj_arg);
+extern "C" obj_res lean_load_plugin(obj_arg path);
 
 void load_plugin(std::string path) {
-    consume_io_result(lean_load_plugin(mk_string(path), io_mk_world()));
+    consume_io_result(lean_load_plugin(mk_string(path)));
 }
 }

src/library/ir_interpreter.cpp

@@ -218,7 +218,8 @@ std::string format_fn_body_head(fn_body const & b) {
 }
 
 static bool type_is_scalar(type t) {
-    return t != type::Object && t != type::Tagged && t != type::TObject && t != type::Irrelevant;
+    return t != type::Object && t != type::Tagged && t != type::TObject && t != type::Irrelevant
+            && t != type::Void;
 }
 
 extern "C" object* lean_get_regular_init_fn_name_for(object* env, object* fn);
@@ -272,6 +273,7 @@ object * box_t(value v, type t) {
     case type::Tagged:
     case type::TObject:
     case type::Irrelevant:
+    case type::Void:
         return v.m_obj;
     case type::Struct:
     case type::Union:
@@ -290,6 +292,7 @@ value unbox_t(object * o, type t) {
     case type::UInt64:  return unbox_uint64(o);
     case type::USize:   return unbox_size_t(o);
     case type::Irrelevant:
+    case type::Void:
     case type::Object:
     case type::Tagged:
     case type::TObject:
@@ -520,6 +523,7 @@ private:
                     case type::UInt64: return cnstr_get_uint64(o, offset);
                     case type::USize:
                     case type::Irrelevant:
+                    case type::Void:
                     case type::Object:
                     case type::Tagged:
                     case type::TObject:
@@ -591,6 +595,7 @@ private:
                             case type::TObject:
                                 return n.to_obj_arg();
                             case type::Irrelevant:
+                            case type::Void:
                                 break;
                             case type::Union:
                             case type::Struct:
@@ -713,6 +718,7 @@ private:
                         case type::UInt64: cnstr_set_uint64(o, offset, v.m_num); break;
                         case type::USize:
                         case type::Irrelevant:
+                        case type::Void:
                         case type::Object:
                         case type::Tagged:
                         case type::TObject:
@@ -889,6 +895,7 @@ private:
                 case type::Tagged:
                 case type::TObject:
                 case type::Irrelevant:
+                case type::Void:
                     return *static_cast<object **>(e.m_native.m_addr);
                 case type::Struct:
                 case type::Union:
@@ -1100,7 +1107,7 @@ public:
 
     object * run_init(name const & decl, name const & init_decl) {
         try {
-            object * args[] = { io_mk_world() };
+            object * args[] = {};
             object * r = call_boxed(init_decl, 1, args);
             if (io_result_is_ok(r)) {
                 object * o = io_result_get_value(r);
@@ -1150,9 +1157,9 @@ uint32 run_main(elab_environment const & env, options const & opts, list_ref<str
 }
 
 /* runMain (env : Environment) (opts : Iptions) (args : List String) : BaseIO UInt32 */
-extern "C" LEAN_EXPORT obj_res lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args, obj_arg) {
+extern "C" LEAN_EXPORT uint32_t lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args) {
     uint32 ret = run_main(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(list_ref<string_ref>, args));
-    return io_result_mk_ok(box(ret));
+    return ret;
 }
 
 extern "C" LEAN_EXPORT object * lean_eval_const(object * env, object * opts, object * c) {
@@ -1169,9 +1176,9 @@ extern "C" obj_res lean_mk_module_initialization_function_name(obj_arg);
 extern "C" LEAN_EXPORT object * lean_run_mod_init(object * mod, object *) {
     string_ref mangled = string_ref(lean_mk_module_initialization_function_name(mod));
     if (void * init = lookup_symbol_in_cur_exe(mangled.data())) {
-        auto init_fn = reinterpret_cast<object *(*)(uint8_t, object *)>(init);
+        auto init_fn = reinterpret_cast<object *(*)(uint8_t)>(init);
         uint8_t builtin = 0;
-        object * r = init_fn(builtin, io_mk_world());
+        object * r = init_fn(builtin);
         if (io_result_is_ok(r)) {
             dec_ref(r);
             return lean_io_result_mk_ok(box(true));

src/library/ir_types.h

@@ -16,10 +16,11 @@ inductive IRType
 | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
 | union (leanTypeName : Name) (types : Array IRType) : IRType
 | tagged
+| void
 
 Remark: we don't create struct/union types from C++.
 */
-enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union, Tagged };
+enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union, Tagged, Void };
 
 typedef nat        var_id;
 typedef nat        jp_id;

src/library/time_task.cpp

@@ -39,9 +39,9 @@ void display_cumulative_profiling_times(std::ostream & out) {
 }
 
 /* displayCumulativeProfilingTimes : BaseIO Unit */
-extern "C" LEAN_EXPORT obj_res lean_display_cumulative_profiling_times(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_display_cumulative_profiling_times() {
    display_cumulative_profiling_times(std::cerr);
-   return lean_io_result_mk_ok(box(0));
+   return lean_mk_baseio_out(box(0));
 }
 
 void initialize_time_task() {

src/runtime/interrupt.cpp

@@ -16,7 +16,7 @@ namespace lean {
 LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
 LEAN_THREAD_VALUE(size_t, g_heartbeat, 0);
 
-extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat() {
 #ifdef LEAN_DEFAULT_MAX_HEARTBEAT
     return lean_box(LEAN_DEFAULT_MAX_HEARTBEAT);
 #else
@@ -32,7 +32,7 @@ void set_max_heartbeat(size_t max) { g_max_heartbeat = max; }
 
 extern "C" LEAN_EXPORT obj_res lean_internal_set_max_heartbeat(usize max) {
     set_max_heartbeat(max);
-    return lean_io_result_mk_ok(lean_box(0));
+    return lean_mk_baseio_out(lean_box(0));
 }
 
 size_t get_max_heartbeat() { return g_max_heartbeat; }
@@ -58,12 +58,12 @@ LEAN_THREAD_VALUE(lean_object *, g_cancel_tk, nullptr);
 LEAN_EXPORT scope_cancel_tk::scope_cancel_tk(lean_object * o):flet<lean_object *>(g_cancel_tk, o) {}
 
 /* CancelToken.isSet : @& IO.CancelToken → BaseIO Bool */
-extern "C" lean_obj_res lean_io_cancel_token_is_set(b_lean_obj_arg cancel_tk, lean_obj_arg);
+extern "C" lean_obj_res lean_io_cancel_token_is_set(b_lean_obj_arg cancel_tk);
 
 void check_interrupted() {
     if (g_cancel_tk) {
         inc_ref(g_cancel_tk);
-        if (get_io_scalar_result<bool>(lean_io_cancel_token_is_set(g_cancel_tk, lean_io_mk_world())) &&
+        if (lean_io_cancel_token_is_set(g_cancel_tk) &&
             !std::uncaught_exception()) {
             throw interrupted();
         }

src/runtime/io.cpp

@@ -78,8 +78,8 @@ static bool g_initializing = true;
 extern "C" LEAN_EXPORT void lean_io_mark_end_initialization() {
     g_initializing = false;
 }
-extern "C" LEAN_EXPORT obj_res lean_io_initializing(obj_arg) {
-    return io_result_mk_ok(box(g_initializing));
+extern "C" LEAN_EXPORT uint8_t lean_io_initializing() {
+    return g_initializing;
 }
 
 static obj_res mk_file_not_found_error(b_obj_arg fname) {
@@ -116,49 +116,49 @@ MK_THREAD_LOCAL_GET(object_ref, get_stream_current_stdout, g_stream_stdout);
 MK_THREAD_LOCAL_GET(object_ref, get_stream_current_stderr, g_stream_stderr);
 
 /* getStdin : BaseIO FS.Stream */
-extern "C" LEAN_EXPORT obj_res lean_get_stdin(obj_arg /* w */) {
-    return io_result_mk_ok(get_stream_current_stdin().to_obj_arg());
+extern "C" LEAN_EXPORT obj_res lean_get_stdin() {
+    return lean_mk_baseio_out(get_stream_current_stdin().to_obj_arg());
 }
 
 /* getStdout : BaseIO FS.Stream */
-extern "C" LEAN_EXPORT obj_res lean_get_stdout(obj_arg /* w */) {
-    return io_result_mk_ok(get_stream_current_stdout().to_obj_arg());
+extern "C" LEAN_EXPORT obj_res lean_get_stdout() {
+    return lean_mk_baseio_out(get_stream_current_stdout().to_obj_arg());
 }
 
 /* getStderr : BaseIO FS.Stream */
-extern "C" LEAN_EXPORT obj_res lean_get_stderr(obj_arg /* w */) {
-    return io_result_mk_ok(get_stream_current_stderr().to_obj_arg());
+extern "C" LEAN_EXPORT obj_res lean_get_stderr() {
+    return lean_mk_baseio_out(get_stream_current_stderr().to_obj_arg());
 }
 
 /* setStdin  : FS.Stream -> BaseIO FS.Stream */
-extern "C" LEAN_EXPORT obj_res lean_get_set_stdin(obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_get_set_stdin(obj_arg h) {
     object_ref & x = get_stream_current_stdin();
     object * r = x.steal();
     x = object_ref(h);
-    return io_result_mk_ok(r);
+    return lean_mk_baseio_out(r);
 }
 
 /* setStdout  : FS.Stream -> BaseIO FS.Stream */
-extern "C" LEAN_EXPORT obj_res lean_get_set_stdout(obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_get_set_stdout(obj_arg h) {
     object_ref & x = get_stream_current_stdout();
     object * r = x.steal();
     x = object_ref(h);
-    return io_result_mk_ok(r);
+    return lean_mk_baseio_out(r);
 }
 
 /* setStderr  : FS.Stream -> BaseIO FS.Stream */
-extern "C" LEAN_EXPORT obj_res lean_get_set_stderr(obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_get_set_stderr(obj_arg h) {
     object_ref & x = get_stream_current_stderr();
     object * r = x.steal();
     x = object_ref(h);
-    return io_result_mk_ok(r);
+    return lean_mk_baseio_out(r);
 }
 
 static FILE * io_get_handle(lean_object * hfile) {
     return static_cast<FILE *>(lean_get_external_data(hfile));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_obj_arg fname) {
+extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname) {
     object * details = mk_string(strerror(errnum));
     // Keep in sync with lean_decode_uv_error below
     switch (errnum) {
@@ -255,7 +255,7 @@ extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_obj_arg fname)
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_decode_uv_error(int errnum, b_obj_arg fname) {
+extern "C" LEAN_EXPORT obj_res lean_decode_uv_error(int errnum, b_lean_obj_arg fname) {
     object * details = mk_string(uv_strerror(errnum));
     // Keep in sync with lean_decode_io_error above
     switch (errnum) {
@@ -369,7 +369,7 @@ obj_res mk_embedded_nul_error(b_obj_arg str) {
 }
 
 /* IO.setAccessRights (filename : @& String) (mode : UInt32) : IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode) {
     const char* fname = string_cstr(filename);
     if (strlen(fname) != lean_string_size(filename) - 1) {
         return mk_embedded_nul_error(filename);
@@ -382,7 +382,7 @@ extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode, ob
 }
 
 /* Handle.mk (filename : @& String) (mode : FS.Mode) : IO Handle */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8 mode, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8 mode) {
     int flags = 0;
 #ifdef LEAN_WINDOWS
     // do not translate line endings
@@ -431,7 +431,7 @@ static inline HANDLE win_handle(FILE * fp) {
 }
 
 /* Handle.lock : (@& Handle) → (exclusive : Bool) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x) {
     OVERLAPPED o = {0};
     HANDLE wh = win_handle(io_get_handle(h));
     DWORD flags = x ? LOCKFILE_EXCLUSIVE_LOCK : 0;
@@ -443,7 +443,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x,
 }
 
 /* Handle.tryLock : (@& Handle) → (exclusive : Bool) → IO Bool */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x) {
     OVERLAPPED o = {0};
     HANDLE wh = win_handle(io_get_handle(h));
     DWORD flags = (x ? LOCKFILE_EXCLUSIVE_LOCK : 0) | LOCKFILE_FAIL_IMMEDIATELY;
@@ -459,7 +459,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t
 }
 
 /* Handle.unlock : (@& Handle) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h) {
     OVERLAPPED o = {0};
     HANDLE wh = win_handle(io_get_handle(h));
     if (UnlockFileEx(wh, 0, MAXDWORD, MAXDWORD, &o)) {
@@ -477,7 +477,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /
 #else
 
 /* Handle.lock : (@& Handle) → (exclusive : Bool) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h,  uint8_t x, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x) {
     FILE * fp = io_get_handle(h);
     if (!flock(fileno(fp), x ? LOCK_EX : LOCK_SH)) {
         return io_result_mk_ok(box(0));
@@ -487,7 +487,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h,  uint8_t x,
 }
 
 /* Handle.tryLock : (@& Handle) → (exclusive : Bool) → IO Bool */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x) {
     FILE * fp = io_get_handle(h);
     if (!flock(fileno(fp), (x ? LOCK_EX : LOCK_SH) | LOCK_NB)) {
         return io_result_mk_ok(box(1));
@@ -501,7 +501,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t
 }
 
 /* Handle.unlock : (@& Handle) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
     if (!flock(fileno(fp), LOCK_UN)) {
         return io_result_mk_ok(box(0));
@@ -513,7 +513,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /
 #endif
 
 /* Handle.isTty : (@& Handle) → BaseIO Bool */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_tty(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT uint8_t lean_io_prim_handle_is_tty(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
 #ifdef LEAN_WINDOWS
     /*
@@ -533,21 +533,21 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_tty(b_obj_arg h, obj_arg /
     and Lean does not support pre-Windows 10.
     */
     DWORD mode;
-    return io_result_mk_ok(box(GetConsoleMode(win_handle(fp), &mode) != 0));
+    return GetConsoleMode(win_handle(fp), &mode) != 0;
 #else
     // We ignore errors for consistency with Windows.
-    return io_result_mk_ok(box(isatty(fileno(fp))));
+    return isatty(fileno(fp));
 #endif
 }
 
 /* Handle.isEof : (@& Handle) → BaseIO Bool */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_eof(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT uint8_t lean_io_prim_handle_is_eof(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
-    return io_result_mk_ok(box(std::feof(fp) != 0));
+    return std::feof(fp) != 0;
 }
 
 /* Handle.flush : (@& Handle) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
     if (!std::fflush(fp)) {
         return io_result_mk_ok(box(0));
@@ -557,7 +557,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /*
 }
 
 /* Handle.rewind : (@& Handle) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_rewind(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_rewind(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
     if (!std::fseek(fp, 0, SEEK_SET)) {
         return io_result_mk_ok(box(0));
@@ -567,7 +567,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_rewind(b_obj_arg h, obj_arg /
 }
 
 /* Handle.truncate : (@& Handle) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
 #ifdef LEAN_WINDOWS
     if (!_chsize_s(_fileno(fp), _ftelli64(fp))) {
@@ -581,7 +581,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h, obj_arg
 }
 
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
     FILE * fp = io_get_handle(h);
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
@@ -599,7 +599,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbyte
 }
 
 /* Handle.write : (@& Handle) → (@& ByteArray) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf) {
     FILE * fp = io_get_handle(h);
     usize n = lean_sarray_size(buf);
     usize m = std::fwrite(lean_sarray_cptr(buf), 1, n, fp);
@@ -611,7 +611,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg
 }
 
 /* Handle.getLine : (@& Handle) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h) {
     FILE * fp = io_get_handle(h);
 
     std::string result;
@@ -635,7 +635,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg
 }
 
 /* Handle.putStr : (@& Handle) → (@& String) → IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s) {
     FILE * fp = io_get_handle(h);
     usize n = lean_string_size(s) - 1; // - 1 to ignore the terminal NULL byte.
     usize m = std::fwrite(lean_string_cstr(s), 1, n, fp);
@@ -647,7 +647,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_ar
 }
 
 /* Std.Time.Timestamp.now : IO Timestamp */
-extern "C" LEAN_EXPORT obj_res lean_get_current_time(obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_get_current_time() {
     using namespace std::chrono;
 
     std::chrono::system_clock::time_point now = std::chrono::system_clock::now();
@@ -664,7 +664,7 @@ extern "C" LEAN_EXPORT obj_res lean_get_current_time(obj_arg /* w */) {
 }
 
 /* Std.Time.Database.Windows.getNextTransition : @&String -> Int64 -> Bool -> IO (Option (Int64 × TimeZone)) */
-extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezone_str, uint64_t tm_obj, uint8 default_time, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezone_str, uint64_t tm_obj, uint8 default_time) {
 #if defined(LEAN_WINDOWS)
     UErrorCode status = U_ZERO_ERROR;
     const char* dst_name_id = lean_string_cstr(timezone_str);
@@ -778,7 +778,7 @@ extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezo
 }
 
 /* Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt : Int64 → IO String */
-extern "C" LEAN_EXPORT obj_res lean_get_windows_local_timezone_id_at(uint64_t tm_obj, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_get_windows_local_timezone_id_at(uint64_t tm_obj) {
 #if defined(LEAN_WINDOWS)
     UErrorCode status = U_ZERO_ERROR;
     UCalendar* cal = ucal_open(NULL, -1, NULL, UCAL_GREGORIAN, &status);
@@ -817,23 +817,23 @@ extern "C" LEAN_EXPORT obj_res lean_get_windows_local_timezone_id_at(uint64_t tm
 }
 
 /* monoMsNow : BaseIO Nat */
-extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now() {
     static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64");
     auto now = std::chrono::steady_clock::now();
     auto tm = std::chrono::duration_cast<std::chrono::milliseconds>(now.time_since_epoch());
-    return io_result_mk_ok(uint64_to_nat(tm.count()));
+    return lean_mk_baseio_out(uint64_to_nat(tm.count()));
 }
 
 /* monoNanosNow : BaseIO Nat */
-extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now(obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now() {
     static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64");
     auto now = std::chrono::steady_clock::now();
     auto tm = std::chrono::duration_cast<std::chrono::nanoseconds>(now.time_since_epoch());
-    return io_result_mk_ok(uint64_to_nat(tm.count()));
+    return lean_mk_baseio_out(uint64_to_nat(tm.count()));
 }
 
 /* getRandomBytes (nBytes : USize) : IO ByteArray */
-extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) {
     // Adapted from https://github.com/rust-random/getrandom/blob/30308ae845b0bf3839e5a92120559eaf56048c28/src/
 
     if (nbytes == 0) return io_result_mk_ok(lean_alloc_sarray(1, 0, 0));
@@ -894,9 +894,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes, obj_arg
 }
 
 /* timeit {α : Type} (msg : @& String) (fn : IO α) : IO α */
-extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
+extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn) {
     auto start = std::chrono::steady_clock::now();
-    w = apply_1(fn, w);
+    obj_arg w = apply_1(fn, lean_io_mk_world());
     auto end   = std::chrono::steady_clock::now();
     auto diff  = std::chrono::duration<double>(end - start);
     sstream out;
@@ -911,33 +911,33 @@ extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg
 }
 
 /* allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α */
-extern "C" LEAN_EXPORT obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn, obj_arg w) {
+extern "C" LEAN_EXPORT obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn) {
     std::ostringstream out;
     obj_res res;
     {
         allocprof prof(out, string_cstr(msg));
-        res = apply_1(fn, w);
+        res = apply_1(fn, lean_io_mk_world());
     }
     io_eprintln(mk_string(out.str()));
     return res;
 }
 
 /* getNumHeartbeats : BaseIO Nat */
-extern "C" LEAN_EXPORT obj_res lean_io_get_num_heartbeats(obj_arg /* w */) {
-    return io_result_mk_ok(lean_uint64_to_nat(get_num_heartbeats()));
+extern "C" LEAN_EXPORT obj_res lean_io_get_num_heartbeats() {
+    return lean_mk_baseio_out(lean_uint64_to_nat(get_num_heartbeats()));
 }
 
 /* setHeartbeats (count : Nat) : BaseIO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_set_heartbeats(obj_arg count, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_set_heartbeats(obj_arg count) {
     set_heartbeats(lean_uint64_of_nat(count));
     lean_dec(count);
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var) {
     const char* env_var_str = string_cstr(env_var);
     if (strlen(env_var_str) != lean_string_size(env_var) - 1) {
-        return io_result_mk_ok(mk_option_none());
+        return lean_mk_baseio_out(mk_option_none());
     }
 #if defined(LEAN_EMSCRIPTEN)
     // HACK(WN): getenv doesn't seem to work in Emscripten even though it should
@@ -958,21 +958,21 @@ extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
     if (val) {
         object * valLean = mk_string(val);
         free(val);
-        return io_result_mk_ok(mk_option_some(valLean));
+        return lean_mk_baseio_out(mk_option_some(valLean));
     } else {
-        return io_result_mk_ok(mk_option_none());
+        return lean_mk_baseio_out(mk_option_none());
     }
 #else
     char * val = std::getenv(env_var_str);
     if (val) {
-        return io_result_mk_ok(mk_option_some(mk_string(val)));
+        return lean_mk_baseio_out(mk_option_some(mk_string(val)));
     } else {
-        return io_result_mk_ok(mk_option_none());
+        return lean_mk_baseio_out(mk_option_none());
     }
 #endif
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_realpath(obj_arg filename, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_realpath(obj_arg filename) {
     const char* fname = string_cstr(filename);
     if (strlen(fname) != lean_string_size(filename) - 1) {
         obj_res res = mk_embedded_nul_error(filename);
@@ -1034,7 +1034,7 @@ structure DirEntry where
 
 constant readDir : @& FilePath → IO (Array DirEntry)
 */
-extern "C" LEAN_EXPORT obj_res lean_io_read_dir(b_obj_arg dirname, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_read_dir(b_obj_arg dirname) {
     const char* dirname_ptr = string_cstr(dirname);
     if (strlen(dirname_ptr) != lean_string_size(dirname) - 1) {
         return mk_embedded_nul_error(dirname);
@@ -1109,7 +1109,7 @@ static obj_res metadata_core(struct stat const & st) {
     return io_result_mk_ok(mdata);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename) {
     const char* fname = string_cstr(filename);
     if (strlen(fname) != lean_string_size(filename) - 1) {
         return mk_embedded_nul_error(filename);
@@ -1121,9 +1121,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename, obj_arg) {
     return metadata_core(st);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename) {
 #ifdef LEAN_WINDOWS
-    return lean_io_metadata(filename, io_mk_world());
+    return lean_io_metadata(filename);
 #else
     const char* fname = string_cstr(filename);
     if (strlen(fname) != lean_string_size(filename) - 1) {
@@ -1137,7 +1137,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename, obj_
 #endif
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p) {
     const char* str = string_cstr(p);
     if (strlen(str) != lean_string_size(p) - 1) {
         return mk_embedded_nul_error(p);
@@ -1153,7 +1153,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p, obj_arg) {
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p) {
     const char* str = string_cstr(p);
     if (strlen(str) != lean_string_size(p) - 1) {
         return mk_embedded_nul_error(p);
@@ -1165,7 +1165,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean_object * /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to) {
     const char* from_str = string_cstr(from);
     if (strlen(from_str) != lean_string_size(from) - 1) {
         return mk_embedded_nul_error(from);
@@ -1197,7 +1197,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean
 }
 
 /* hardLink (orig link : @& FilePath) : IO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_hard_link(b_obj_arg orig, b_obj_arg link, lean_object * /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_hard_link(b_obj_arg orig, b_obj_arg link) {
     const char* orig_str = string_cstr(orig);
     if (strlen(orig_str) != lean_string_size(orig) - 1) {
         return mk_embedded_nul_error(orig);
@@ -1307,7 +1307,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempdir(lean_object * /* w */) {
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg filename, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg filename) {
     const char* fname = string_cstr(filename);
     if (strlen(fname) != lean_string_size(filename) - 1) {
         return mk_embedded_nul_error(filename);
@@ -1319,7 +1319,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg filename, obj_arg)
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_app_path() {
 #if defined(LEAN_WINDOWS)
     HMODULE hModule = GetModuleHandle(NULL);
     char path[MAX_PATH];
@@ -1374,7 +1374,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_arg) {
 #endif
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_current_dir(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_current_dir() {
     char buffer[PATH_MAX];
     char * cwd = getcwd(buffer, sizeof(buffer));
     if (cwd) {
@@ -1386,192 +1386,142 @@ extern "C" LEAN_EXPORT obj_res lean_io_current_dir(obj_arg) {
 
 // =======================================
 // ST ref primitives
-extern "C" LEAN_EXPORT obj_res lean_st_mk_ref(obj_arg a, obj_arg) {
+
+
+extern "C" LEAN_EXPORT obj_res lean_st_mk_ref(obj_arg a) {
     lean_ref_object * o = (lean_ref_object*)lean_alloc_small_object(sizeof(lean_ref_object));
     lean_set_st_header((lean_object*)o, LeanRef, 0);
     o->m_value = a;
-    return io_result_mk_ok((lean_object*)o);
+    return lean_st_mk_result((lean_object*)o);
 }
 
-static object * g_io_error_nullptr_read = nullptr;
-
 static inline atomic<object*> * mt_ref_val_addr(object * o) {
     return reinterpret_cast<atomic<object*> *>(&(lean_to_ref(o)->m_value));
 }
 
-/*
-  Important: we have added support for initializing global constants
-  at program startup. This feature is particularly useful for
-  initializing `ST.Ref` values. Any `ST.Ref` value created during
-  initialization will be marked as persistent. Thus, to make `ST.Ref`
-  API thread-safe, we must treat persistent `ST.Ref` objects created
-  during initialization as a multi-threaded object. Then, whenever we store
-  a value `val` into a global `ST.Ref`, we have to mark `va`l as a multi-threaded
-  object as we do for multi-threaded `ST.Ref`s. It makes sense since
-  the global `ST.Ref` may be used to communicate data between threads.
-*/
-static inline bool ref_maybe_mt(b_obj_arg ref) { return lean_is_mt(ref) || lean_is_persistent(ref); }
-
-extern "C" LEAN_EXPORT obj_res lean_st_ref_get(b_obj_arg ref, obj_arg) {
-    if (ref_maybe_mt(ref)) {
-        atomic<object *> * val_addr = mt_ref_val_addr(ref);
-        while (true) {
-            /*
-              We cannot simply read `val` from the ref and `inc` it like in the `else` branch since someone else could
-              write to the ref in between and remove the last owning reference to the object. Instead, we must take
-              ownership of the RC token in the ref via `exchange`, duplicate it, then put one RC token back. */
-            object * val = val_addr->exchange(nullptr);
-            if (val != nullptr) {
-                inc(val);
-                object * tmp = val_addr->exchange(val);
-                if (tmp != nullptr) {
-                    /* this may happen if another thread wrote `ref` */
-                    dec(tmp);
-                }
-                return io_result_mk_ok(val);
+extern "C" LEAN_EXPORT obj_res lean_st_ref_get_mt(b_obj_arg ref) {
+    atomic<object *> * val_addr = mt_ref_val_addr(ref);
+    while (true) {
+        /*
+          We cannot simply read `val` from the ref and `inc` it like in the `else` branch since someone else could
+          write to the ref in between and remove the last owning reference to the object. Instead, we must take
+          ownership of the RC token in the ref via `exchange`, duplicate it, then put one RC token back. */
+        object * val = val_addr->exchange(nullptr);
+        if (val != nullptr) {
+            inc(val);
+            object * tmp = val_addr->exchange(val);
+            if (tmp != nullptr) {
+                /* this may happen if another thread wrote `ref` */
+                dec(tmp);
             }
+            return lean_st_mk_result(val);
         }
-    } else {
-        object * val = lean_to_ref(ref)->m_value;
-        lean_assert(val != nullptr);
-        inc(val);
-        return io_result_mk_ok(val);
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_st_ref_take(b_obj_arg ref, obj_arg) {
-    if (ref_maybe_mt(ref)) {
-        atomic<object *> * val_addr = mt_ref_val_addr(ref);
-        while (true) {
-            object * val = val_addr->exchange(nullptr);
-            if (val != nullptr)
-                return io_result_mk_ok(val);
-        }
-    } else {
-        object * val = lean_to_ref(ref)->m_value;
-        lean_assert(val != nullptr);
-        lean_to_ref(ref)->m_value = nullptr;
-        return io_result_mk_ok(val);
+extern "C" LEAN_EXPORT obj_res lean_st_ref_take_mt(b_obj_arg ref) {
+    atomic<object *> * val_addr = mt_ref_val_addr(ref);
+    while (true) {
+        object * val = val_addr->exchange(nullptr);
+        if (val != nullptr)
+            return lean_st_mk_result(val);
     }
 }
 
 static_assert(sizeof(atomic<unsigned short>) == sizeof(unsigned short), "`atomic<unsigned short>` and `unsigned short` must have the same size"); // NOLINT
 
-extern "C" LEAN_EXPORT obj_res lean_st_ref_set(b_obj_arg ref, obj_arg a, obj_arg) {
-    if (ref_maybe_mt(ref)) {
-        /* We must mark `a` as multi-threaded if `ref` is marked as multi-threaded.
-           Reason: our runtime relies on the fact that a single-threaded object
-           cannot be reached from a multi-thread object. */
-        mark_mt(a);
-        atomic<object *> * val_addr = mt_ref_val_addr(ref);
+extern "C" LEAN_EXPORT obj_res lean_st_ref_set_mt(b_obj_arg ref, obj_arg a) {
+    /* We must mark `a` as multi-threaded if `ref` is marked as multi-threaded.
+       Reason: our runtime relies on the fact that a single-threaded object
+       cannot be reached from a multi-thread object. */
+    mark_mt(a);
+    atomic<object *> * val_addr = mt_ref_val_addr(ref);
+    object * old_a = val_addr->exchange(a);
+    if (old_a != nullptr)
+        dec(old_a);
+    return lean_st_mk_result(box(0));
+}
+
+extern "C" LEAN_EXPORT obj_res lean_st_ref_swap_mt(b_obj_arg ref, obj_arg a) {
+    /* See io_ref_write */
+    mark_mt(a);
+    atomic<object *> * val_addr = mt_ref_val_addr(ref);
+    while (true) {
         object * old_a = val_addr->exchange(a);
         if (old_a != nullptr)
-            dec(old_a);
-        return io_result_mk_ok(box(0));
-    } else {
-        if (lean_to_ref(ref)->m_value != nullptr)
-            dec(lean_to_ref(ref)->m_value);
-        lean_to_ref(ref)->m_value = a;
-        return io_result_mk_ok(box(0));
+            return lean_st_mk_result(old_a);
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_st_ref_swap(b_obj_arg ref, obj_arg a, obj_arg) {
-    if (ref_maybe_mt(ref)) {
-        /* See io_ref_write */
-        mark_mt(a);
-        atomic<object *> * val_addr = mt_ref_val_addr(ref);
-        while (true) {
-            object * old_a = val_addr->exchange(a);
-            if (old_a != nullptr)
-                return io_result_mk_ok(old_a);
-        }
-    } else {
-        object * old_a = lean_to_ref(ref)->m_value;
-        if (old_a == nullptr)
-            return io_result_mk_error(g_io_error_nullptr_read);
-        lean_to_ref(ref)->m_value = a;
-        return io_result_mk_ok(old_a);
-    }
-}
-
-extern "C" LEAN_EXPORT obj_res lean_st_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
-    // TODO(Leo): ref_maybe_mt
-    bool r = lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value;
-    return io_result_mk_ok(box(r));
-}
-
-/* {α : Type} (act : BaseIO α) (_ : IO.RealWorld) : α */
-static obj_res lean_io_as_task_fn(obj_arg act, obj_arg) {
+/* {α : Type} (act : BaseIO α) : α */
+static obj_res lean_io_as_task_fn(obj_arg act) {
     object_ref r(apply_1(act, io_mk_world()));
-    return object_ref(io_result_get_value(r.raw()), true).steal();
+    return object_ref(lean_baseio_out_val(r.raw()), true).steal();
 }
 
 /* asTask {α : Type} (act : BaseIO α) (prio : Nat) : BaseIO (Task α) */
-extern "C" LEAN_EXPORT obj_res lean_io_as_task(obj_arg act, obj_arg prio, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_as_task(obj_arg act, obj_arg prio) {
     object * c = lean_alloc_closure((void*)lean_io_as_task_fn, 2, 1);
     lean_closure_set(c, 0, act);
     object * t = lean_task_spawn_core(c, lean_unbox(prio), /* keep_alive */ true);
-    return io_result_mk_ok(t);
+    return lean_mk_baseio_out(t);
 }
 
 /* {α β : Type} (f : α → BaseIO β) (a : α) : β */
 static obj_res lean_io_bind_task_fn(obj_arg f, obj_arg a) {
     object_ref r(apply_2(f, a, io_mk_world()));
-    return object_ref(io_result_get_value(r.raw()), true).steal();
+    return object_ref(lean_baseio_out_val(r.raw()), true).steal();
 }
 
 /*  mapTask (f : α → BaseIO β) (t : Task α) (prio : Nat) (sync : Bool) : BaseIO (Task β) */
-extern "C" LEAN_EXPORT obj_res lean_io_map_task(obj_arg f, obj_arg t, obj_arg prio, uint8 sync,
-        obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_map_task(obj_arg f, obj_arg t, obj_arg prio, uint8 sync) {
     object * c = lean_alloc_closure((void*)lean_io_bind_task_fn, 2, 1);
     lean_closure_set(c, 0, f);
     object * t2 = lean_task_map_core(c, t, lean_unbox(prio), sync, /* keep_alive */ true);
-    return io_result_mk_ok(t2);
+    return lean_mk_baseio_out(t2);
 }
 
 /*  bindTask (t : Task α) (f : α → BaseIO (Task β)) (prio : Nat) (sync : Bool) : BaseIO (Task β) */
-extern "C" LEAN_EXPORT obj_res lean_io_bind_task(obj_arg t, obj_arg f, obj_arg prio, uint8 sync,
-        obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_bind_task(obj_arg t, obj_arg f, obj_arg prio, uint8 sync) {
     object * c = lean_alloc_closure((void*)lean_io_bind_task_fn, 2, 1);
     lean_closure_set(c, 0, f);
     object * t2 = lean_task_bind_core(t, c, lean_unbox(prio), sync, /* keep_alive */ true);
-    return io_result_mk_ok(t2);
+    return lean_mk_baseio_out(t2);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_check_canceled(obj_arg) {
-    return io_result_mk_ok(box(lean_io_check_canceled_core()));
+extern "C" LEAN_EXPORT uint8_t lean_io_check_canceled() {
+    return lean_io_check_canceled_core();
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_cancel(b_obj_arg t, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_cancel(b_obj_arg t) {
     lean_io_cancel_core(t);
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_get_task_state(b_obj_arg t, obj_arg) {
-    return io_result_mk_ok(box(lean_io_get_task_state_core(t)));
+extern "C" LEAN_EXPORT uint8_t lean_io_get_task_state(b_obj_arg t) {
+    return lean_io_get_task_state_core(t);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_wait(obj_arg t, obj_arg) {
-    return io_result_mk_ok(lean_task_get_own(t));
+extern "C" LEAN_EXPORT obj_res lean_io_wait(obj_arg t) {
+    return lean_mk_baseio_out(lean_task_get_own(t));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code) {
     exit(code);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_force_exit(uint8_t code, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_io_force_exit(uint8_t code) {
     std::_Exit((int)code);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_runtime_mark_multi_threaded(obj_arg a, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_runtime_mark_multi_threaded(obj_arg a) {
     lean_mark_mt(a);
-    return io_result_mk_ok(a);
+    return lean_mk_baseio_out(a);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a) {
     lean_mark_persistent(a);
-    return io_result_mk_ok(a);
+    return lean_mk_baseio_out(a);
 }
 
 #if defined(__has_feature)
@@ -1580,13 +1530,13 @@ extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /
 #endif
 #endif
 
-extern "C" LEAN_EXPORT obj_res lean_runtime_forget(obj_arg o, obj_arg /* w */) {
+extern "C" LEAN_EXPORT obj_res lean_runtime_forget(obj_arg o) {
 #if defined(__has_feature)
 #if __has_feature(address_sanitizer)
     __lsan_ignore_object(o);
 #endif
 #endif
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
 extern "C" LEAN_EXPORT obj_res lean_option_get_or_block(obj_arg o_opt) {
@@ -1604,8 +1554,6 @@ extern "C" LEAN_EXPORT obj_res lean_option_get_or_block(obj_arg o_opt) {
 }
 
 void initialize_io() {
-    g_io_error_nullptr_read = lean_mk_io_user_error(mk_ascii_string_unchecked("null reference read"));
-    mark_persistent(g_io_error_nullptr_read);
     g_io_handle_external_class = lean_register_external_class(io_handle_finalizer, io_handle_foreach);
 #if defined(LEAN_WINDOWS)
     _setmode(_fileno(stdout), _O_BINARY);

src/runtime/memory.cpp

@@ -114,7 +114,7 @@ namespace lean {
 static size_t g_max_memory = 0;
 LEAN_THREAD_VALUE(size_t, g_counter, 0);
 
-extern "C" LEAN_EXPORT lean_obj_res lean_internal_get_default_max_memory(lean_obj_arg) {
+extern "C" LEAN_EXPORT lean_obj_res lean_internal_get_default_max_memory() {
 #ifdef LEAN_DEFAULT_MAX_MEMORY
     return lean_box(LEAN_DEFAULT_MAX_MEMORY);
 #else
@@ -128,7 +128,7 @@ void set_max_memory(size_t max) {
 
 extern "C" LEAN_EXPORT lean_obj_res lean_internal_set_max_memory(size_t max) {
     set_max_memory(max);
-    return lean_io_result_mk_ok(lean_box(0));
+    return lean_mk_baseio_out(lean_box(0));
 }
 
 void set_max_memory_megabyte(unsigned max) {

src/runtime/mutex.cpp

@@ -22,23 +22,23 @@ static mutex * basemutex_get(lean_object * mtx) {
     return static_cast<mutex *>(lean_get_external_data(mtx));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basemutex_new(obj_arg) {
-    return io_result_mk_ok(lean_alloc_external(g_basemutex_external_class, new mutex));
+extern "C" LEAN_EXPORT obj_res lean_io_basemutex_new() {
+    return lean_mk_baseio_out(lean_alloc_external(g_basemutex_external_class, new mutex));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basemutex_lock(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_basemutex_lock(b_obj_arg mtx) {
     basemutex_get(mtx)->lock();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basemutex_try_lock(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT uint8_t lean_io_basemutex_try_lock(b_obj_arg mtx) {
     bool success = basemutex_get(mtx)->try_lock();
-    return io_result_mk_ok(box(success));
+    return success;
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basemutex_unlock(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_basemutex_unlock(b_obj_arg mtx) {
     basemutex_get(mtx)->unlock();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
 static lean_external_class * g_condvar_external_class = nullptr;
@@ -51,25 +51,25 @@ static condition_variable * condvar_get(lean_object * mtx) {
     return static_cast<condition_variable *>(lean_get_external_data(mtx));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_condvar_new(obj_arg) {
-    return io_result_mk_ok(lean_alloc_external(g_condvar_external_class, new condition_variable));
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_new() {
+    return lean_mk_baseio_out(lean_alloc_external(g_condvar_external_class, new condition_variable));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_condvar_wait(b_obj_arg condvar, b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_wait(b_obj_arg condvar, b_obj_arg mtx) {
     unique_lock<mutex> lock(*basemutex_get(mtx), std::adopt_lock_t());
     condvar_get(condvar)->wait(lock);
     lock.release();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_one(b_obj_arg condvar, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_one(b_obj_arg condvar) {
     condvar_get(condvar)->notify_one();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_all(b_obj_arg condvar, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_all(b_obj_arg condvar) {
     condvar_get(condvar)->notify_all();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
 static lean_external_class * g_baserecmutex_external_class = nullptr;
@@ -82,23 +82,23 @@ static recursive_mutex * baserecmutex_get(lean_object * mtx) {
     return static_cast<recursive_mutex *>(lean_get_external_data(mtx));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_new(obj_arg) {
-    return io_result_mk_ok(lean_alloc_external(g_baserecmutex_external_class, new recursive_mutex));
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_new() {
+    return lean_mk_baseio_out(lean_alloc_external(g_baserecmutex_external_class, new recursive_mutex));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_lock(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_lock(b_obj_arg mtx) {
     baserecmutex_get(mtx)->lock();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_try_lock(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT uint8_t lean_io_baserecmutex_try_lock(b_obj_arg mtx) {
     bool success = baserecmutex_get(mtx)->try_lock();
-    return io_result_mk_ok(box(success));
+    return success;
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_unlock(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_unlock(b_obj_arg mtx) {
     baserecmutex_get(mtx)->unlock();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
 // We use a `shared_timed_mutex` instead of a `shared_mutex` for now as the latter is only available
@@ -113,38 +113,38 @@ static shared_timed_mutex * basesharedmutex_get(lean_object * mtx) {
     return static_cast<shared_timed_mutex *>(lean_get_external_data(mtx));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_new(obj_arg) {
-    return io_result_mk_ok(lean_alloc_external(g_basesharedmutex_external_class, new shared_timed_mutex));
+extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_new() {
+    return lean_mk_baseio_out(lean_alloc_external(g_basesharedmutex_external_class, new shared_timed_mutex));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_write(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_write(b_obj_arg mtx) {
     basesharedmutex_get(mtx)->lock();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_try_write(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT uint8_t lean_io_basesharedmutex_try_write(b_obj_arg mtx) {
     bool success = basesharedmutex_get(mtx)->try_lock();
-    return io_result_mk_ok(box(success));
+    return success;
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_write(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_write(b_obj_arg mtx) {
     basesharedmutex_get(mtx)->unlock();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_read(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_read(b_obj_arg mtx) {
     basesharedmutex_get(mtx)->lock_shared();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_try_read(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT uint8_t lean_io_basesharedmutex_try_read(b_obj_arg mtx) {
     bool success = basesharedmutex_get(mtx)->try_lock_shared();
-    return io_result_mk_ok(box(success));
+    return success;
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_read(b_obj_arg mtx, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_read(b_obj_arg mtx) {
     basesharedmutex_get(mtx)->unlock_shared();
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
 void initialize_mutex() {

src/runtime/object.cpp

@@ -1065,7 +1065,7 @@ extern "C" LEAN_EXPORT obj_res lean_task_pure(obj_arg a) {
     return (lean_object*)alloc_task(a);
 }
 
-static obj_res task_map_fn(obj_arg f, obj_arg t, obj_arg) {
+static obj_res task_map_fn(obj_arg f, obj_arg t, obj_arg w) {
     b_obj_res v = lean_to_task(t)->m_value;
     lean_assert(v != nullptr);
     lean_inc(v);
@@ -1188,14 +1188,14 @@ void lean_promise_resolve(obj_arg value, b_obj_arg promise) {
     g_task_manager->resolve(lean_to_promise(promise)->m_result, mk_option_some(value));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_promise_new() {
     lean_object * o = lean_promise_new();
-    return io_result_mk_ok(o);
+    return lean_mk_baseio_out(o);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise) {
     lean_promise_resolve(value, promise);
-    return io_result_mk_ok(box(0));
+    return lean_mk_baseio_out(box(0));
 }
 
 extern "C" LEAN_EXPORT obj_res lean_io_promise_result_opt(b_obj_arg promise) {
@@ -2636,9 +2636,9 @@ extern "C" LEAN_EXPORT object * lean_max_small_nat(object *) {
 // =======================================
 // Debugging helper functions
 
-extern "C" obj_res lean_io_eprintln(obj_arg s, obj_arg w);
+extern "C" obj_res lean_io_eprintln(obj_arg s);
 void io_eprintln(obj_arg s) {
-    object * r = lean_io_eprintln(s, lean_io_mk_world());
+    object * r = lean_io_eprintln(s);
     lean_assert(lean_io_result_is_ok(r));
     lean_dec(r);
 }

src/runtime/object.h

@@ -466,17 +466,17 @@ LEAN_EXPORT void io_eprintln(obj_arg s);
 
 // =======================================
 // ST ref primitives
-inline obj_res st_mk_ref(obj_arg v, obj_arg w) { return lean_st_mk_ref(v, w); }
-inline obj_res st_ref_get(b_obj_arg r, obj_arg w) { return lean_st_ref_get(r, w); }
-inline obj_res st_ref_set(b_obj_arg r, obj_arg v, obj_arg w) { return lean_st_ref_set(r, v, w); }
-inline obj_res st_ref_reset(b_obj_arg r, obj_arg w) { return lean_st_ref_reset(r, w); }
-inline obj_res st_ref_swap(b_obj_arg r, obj_arg v, obj_arg w) { return lean_st_ref_swap(r, v, w); }
+inline obj_res st_mk_ref(obj_arg v) { return lean_st_mk_ref(v); }
+inline obj_res st_ref_get(b_obj_arg r) { return lean_st_ref_get(r); }
+inline obj_res st_ref_take(b_obj_arg r) { return lean_st_ref_take(r); }
+inline obj_res st_ref_set(b_obj_arg r, obj_arg v) { return lean_st_ref_set(r, v); }
+inline obj_res st_ref_swap(b_obj_arg r, obj_arg v) { return lean_st_ref_swap(r, v); }
 
 obj_res lean_promise_new();
 void lean_promise_resolve(obj_arg value, b_obj_arg promise);
 
-extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg);
-extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise, obj_arg);
+extern "C" LEAN_EXPORT obj_res lean_io_promise_new();
+extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise);
 extern "C" LEAN_EXPORT obj_res lean_io_promise_result_opt(obj_arg promise);
 extern "C" LEAN_EXPORT obj_res lean_get_or_block(obj_arg opt);
 

src/runtime/process.cpp

@@ -62,7 +62,7 @@ lean_object * wrap_win_handle(HANDLE h) {
     return lean_alloc_external(g_win_handle_external_class, static_cast<void *>(h));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir() {
     char path[MAX_PATH];
     DWORD sz = GetCurrentDirectory(MAX_PATH, path);
     if (sz != 0) {
@@ -72,7 +72,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path) {
     if (SetCurrentDirectory(string_cstr(path))) {
         return io_result_mk_ok(box(0));
     } else {
@@ -80,15 +80,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, o
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
-    return lean_io_result_mk_ok(box_uint32(GetCurrentProcessId()));
+extern "C" LEAN_EXPORT uint32_t lean_io_process_get_pid() {
+    return GetCurrentProcessId();
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
-    return lean_io_result_mk_ok(box_uint64(GetCurrentThreadId()));
+extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
+    return GetCurrentThreadId();
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     DWORD exit_code;
     if (WaitForSingleObject(h, INFINITE) == WAIT_FAILED) {
@@ -100,7 +100,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
     return lean_io_result_mk_ok(box_uint32(exit_code));
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     DWORD exit_code;
     DWORD ret = WaitForSingleObject(h, 0);
@@ -116,7 +116,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_a
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child) {
     HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
     if (!TerminateProcess(h, 1)) {
         return io_result_mk_error((sstream() << GetLastError()).str());
@@ -300,7 +300,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
     return lean_io_result_mk_ok(r.steal());
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild) {
     object_ref child(lchild);
     object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), cnstr_get_ref(child, 3));
     object_ref r = mk_cnstr(0, cnstr_get_ref(child, 0), child2);
@@ -314,7 +314,7 @@ void finalize_process() {}
 
 #else
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir() {
     char path[PATH_MAX];
     if (getcwd(path, PATH_MAX)) {
         return io_result_mk_ok(mk_string(path));
@@ -323,7 +323,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path) {
     if (!chdir(string_cstr(path))) {
         return io_result_mk_ok(box(0));
     } else {
@@ -331,12 +331,12 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, o
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
+extern "C" LEAN_EXPORT uint32_t lean_io_process_get_pid() {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
-    return lean_io_result_mk_ok(box_uint32(getpid()));
+    return getpid();
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
+extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
     uint64_t tid;
 #ifdef __APPLE__
     lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
@@ -347,10 +347,10 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
     // glibc 2.30 would provide a wrapper
     tid = (pid_t)syscall(SYS_gettid);
 #endif
-    return lean_io_result_mk_ok(box_uint64(tid));
+    return tid;
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
     int status;
@@ -366,7 +366,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
     int status;
@@ -388,7 +388,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_a
     }
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
     bool setsid = cnstr_get_uint8(child, 3 * sizeof(object *) + sizeof(pid_t));
@@ -534,7 +534,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
     return lean_io_result_mk_ok(r.steal());
 }
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild) {
     object_ref child(lchild);
     object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), sizeof(pid_t));
     cnstr_set_uint32(child2.raw(), 3 * sizeof(object *), cnstr_get_uint32(child.raw(), 3 * sizeof(object *)));
@@ -549,7 +549,7 @@ void finalize_process() {}
 
 extern "C" lean_object* lean_mk_io_error_other_error(uint32_t, lean_object*);
 
-extern "C" LEAN_EXPORT obj_res lean_io_process_spawn(obj_arg args_, obj_arg) {
+extern "C" LEAN_EXPORT obj_res lean_io_process_spawn(obj_arg args_) {
     object_ref args(args_);
     object_ref stdio_cfg = cnstr_get_ref(args, 0);
     stdio stdin_mode  = static_cast<stdio>(cnstr_get_uint8(stdio_cfg.raw(), 0));

src/runtime/uv/dns.cpp

@@ -33,7 +33,7 @@ bool is_safe_ascii_str(const char *s, size_t len) {
 }
 
 // Std.Internal.IO.Async.DNS.getAddrInfo (host service : @& String) (family : UInt8) : IO (IO.Promise (Except IO.Error (Array IPAddr)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family) {
     char const * name_cstr = lean_string_cstr(name);
     char const * service_cstr = lean_string_cstr(service);
 
@@ -110,7 +110,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_a
 }
 
 // Std.Internal.IO.Async.DNS.getNameInfo (host : @& SocketAddress) : IO (IO.Promise (Except IO.Error (String × String)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr) {
     lean_object* promise = lean_promise_new();
     mark_mt(promise);
 
@@ -161,14 +161,14 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr, obj_arg
 #else
 
 // Std.Internal.IO.Async.DNS.getAddrInfo (host service : @& String) (family : UInt8) : IO (IO.Promise (Except IO.Error (Array IPAddr)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.IO.Async.DNS.getNameInfo (host : @& SocketAddress) : IO (IO.Promise (Except IO.Error (String × String)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );

src/runtime/uv/dns.h

@@ -19,7 +19,7 @@ using namespace std;
 
 // =======================================
 // DNS functions
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr);
 
 }

src/runtime/uv/event_loop.cpp

@@ -102,7 +102,7 @@ void event_loop_run_loop(event_loop_t * event_loop) {
 }
 
 /* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options) {
     bool accum = lean_ctor_get_uint8(options, 0);
     bool block = lean_ctor_get_uint8(options, 1);
 
@@ -122,16 +122,16 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg optio
 
     event_loop_unlock(&global_ev);
 
-    return lean_io_result_mk_ok(lean_box(0));
+    return lean_mk_baseio_out(lean_box(0));
 }
 
-/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
+/* Std.Internal.UV.Loop.alive : BaseIO Bool */
+extern "C" LEAN_EXPORT uint8_t lean_uv_event_loop_alive() {
     event_loop_lock(&global_ev);
     int is_alive = uv_loop_alive(global_ev.loop);
     event_loop_unlock(&global_ev);
 
-    return lean_io_result_mk_ok(lean_box(is_alive));
+    return is_alive;
 }
 
 void initialize_libuv_loop() {
@@ -141,15 +141,15 @@ void initialize_libuv_loop() {
 #else
 
 /* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options) {
     return io_result_mk_error("lean_uv_event_loop_configure is not supported");
 }
 
 /* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive() {
     return io_result_mk_error("lean_uv_event_loop_alive is not supported");
 }
 
 #endif
 
-}
+}

src/runtime/uv/event_loop.h

@@ -44,8 +44,8 @@ void event_loop_run_loop(event_loop_t *event_loop);
 
 // =======================================
 // Global event loop manipulation functions
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ );
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ );
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options);
+extern "C" LEAN_EXPORT uint8_t lean_uv_event_loop_alive();
 
 // Helpers
 

src/runtime/uv/net_addr.cpp

@@ -217,7 +217,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
 }
 
 /* Std.Net.networkInterface : IO (Array InterfaceAddress) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses() {
     uv_interface_address_t* info;
     int count;
 
@@ -291,7 +291,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
 }
 
 /* Std.Net.networkInterface : IO (Array InterfaceAddress) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );

src/runtime/uv/net_addr.h

@@ -38,7 +38,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses(obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses();
 
 
 }

src/runtime/uv/signal.cpp

@@ -51,7 +51,7 @@ void handle_signal_event(uv_signal_t* handle, int signum) {
 
     if (signal->m_repeating) {
         if (!signal_promise_is_finished(signal)) {
-            lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world());
+            lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise);
             lean_dec(res);
         }
     } else {
@@ -59,7 +59,7 @@ void handle_signal_event(uv_signal_t* handle, int signum) {
         uv_signal_stop(signal->m_uv_signal);
         signal->m_state = SIGNAL_STATE_FINISHED;
 
-        lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world());
+        lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise);
         lean_dec(res);
 
         lean_dec(obj);
@@ -67,7 +67,7 @@ void handle_signal_event(uv_signal_t* handle, int signum) {
 }
 
 /* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating) {
     int signum = (int)(int32_t)signum_obj;
 
     lean_uv_signal_object * signal = (lean_uv_signal_object*)malloc(sizeof(lean_uv_signal_object));
@@ -98,16 +98,11 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8
 }
 
 /* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj) {
     lean_uv_signal_object * signal = lean_to_uv_signal(obj);
 
     auto create_promise = []() {
-        lean_object * prom_res = lean_io_promise_new(lean_io_mk_world());
-        lean_object * promise = lean_ctor_get(prom_res, 0);
-        lean_inc(promise);
-        lean_dec(prom_res);
-
-        return promise;
+        return lean_io_promise_new();
     };
 
     auto setup_signal = [create_promise, obj, signal]() {
@@ -186,7 +181,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj, obj_arg /
 }
 
 /* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj) {
     lean_uv_signal_object * signal = lean_to_uv_signal(obj);
 
     if (signal->m_state == SIGNAL_STATE_RUNNING) {
@@ -215,21 +210,21 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj, obj_arg /
 #else
 
 /* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 /* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 /* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
@@ -237,4 +232,4 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_ar
 
 #endif
 
-}
+}

src/runtime/uv/signal.h

@@ -48,8 +48,8 @@ static inline lean_uv_signal_object* lean_to_uv_signal(lean_object * o) { return
 
 // =======================================
 // Signal manipulation functions
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal);
 
 }

src/runtime/uv/system.cpp

@@ -19,7 +19,7 @@ typedef struct {
 } random_req_t;
 
 // Std.Internal.UV.System.getProcessTitle : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title() {
     char title[512];
     int result = uv_get_process_title(title, sizeof(title));
 
@@ -32,7 +32,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.setProcessTitle : String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title) {
     const char* title_str = lean_string_cstr(title);
     if (strlen(title_str) != lean_string_size(title) - 1) {
         return mk_embedded_nul_error(title);
@@ -47,7 +47,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, o
 }
 
 // Std.Internal.UV.System.uptime : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime() {
     double uptime;
 
     int result = uv_uptime(&uptime);
@@ -62,19 +62,19 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.osGetPid : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid() {
     uv_pid_t pid = uv_os_getpid();
     return lean_io_result_mk_ok(lean_box_uint64(pid));
 }
 
 // Std.Internal.UV.System.osGetPpid : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid() {
     uv_pid_t ppid = uv_os_getppid();
     return lean_io_result_mk_ok(lean_box_uint64(ppid));
 }
 
 // Std.Internal.UV.System.cpuInfo : IO (Array CPUInfo)
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info() {
     uv_cpu_info_t* cpu_infos;
     int count;
 
@@ -110,7 +110,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.cwd : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd() {
     char buffer[PATH_MAX];
     size_t size = sizeof(buffer);
 
@@ -125,7 +125,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.chdir : String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path) {
     const char* path_str = lean_string_cstr(path);
     if (strlen(path_str) != lean_string_size(path) - 1) {
         return mk_embedded_nul_error(path);
@@ -142,7 +142,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w *
 }
 
 // Std.Internal.UV.System.osHomedir : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir() {
     char buffer[PATH_MAX];
     size_t size = sizeof(buffer);
 
@@ -157,7 +157,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.osTmpdir : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir() {
     char buffer[PATH_MAX];
     size_t size = sizeof(buffer);
 
@@ -172,7 +172,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.osGetPasswd : IO PasswdInfo
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd() {
     uv_passwd_t passwd;
 
     int result = uv_os_get_passwd(&passwd);
@@ -200,7 +200,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.osGetGroup : IO (Option GroupInfo)
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid) {
 #if UV_VERSION_HEX >= 0x012D00
     uv_group_t group;
     int result = uv_os_get_group(&group, gid);
@@ -244,7 +244,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /
 }
 
 // Std.Internal.UV.System.osEnviron : IO (Array (String × String))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
     uv_env_item_t* env;
     int count;
     int result = uv_os_environ(&env, &count);
@@ -272,7 +272,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.osGetenv : String → IO (Option String)
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
     const char* name_str = lean_string_cstr(name);
     if (strlen(name_str) != lean_string_size(name) - 1) {
         return lean_io_result_mk_ok(lean_box(0));
@@ -314,7 +314,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /*
 
 
 // Std.Internal.UV.System.osSetenv : String → String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
     const char* name_str = lean_string_cstr(name);
     const char* value_str = lean_string_cstr(value);
     if (strlen(name_str) != lean_string_size(name) - 1) {
@@ -334,7 +334,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg
 }
 
 // Std.Internal.UV.System.osUnsetenv : String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
     const char* name_str = lean_string_cstr(name);
     if (strlen(name_str) != lean_string_size(name) - 1) {
         return mk_embedded_nul_error(name);
@@ -350,7 +350,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg
 }
 
 // Std.Internal.UV.System.osGetHostname : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname() {
     char hostname[256];
     size_t size = sizeof(hostname);
 
@@ -365,7 +365,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.osGetPriority : UInt64 → IO Int64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid) {
     int priority;
 
     int result = uv_os_getpriority(pid, &priority);
@@ -378,7 +378,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg
 }
 
 // Std.Internal.UV.System.osSetPriority : UInt64 → Int → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority) {
     int result = uv_os_setpriority(pid, priority);
 
     if (result < 0) {
@@ -389,7 +389,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t
 }
 
 // Std.Internal.UV.System.osUname : IO UnameInfo
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname() {
     uv_utsname_t uname_info;
 
     int result = uv_os_uname(&uname_info);
@@ -413,13 +413,13 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.hrtime : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime() {
     uint64_t time = uv_hrtime();
     return lean_io_result_mk_ok(lean_box_uint64(time));
 }
 
 // Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error (Array UInt8)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size) {
     lean_object* promise = lean_promise_new();
     mark_mt(promise);
 
@@ -476,7 +476,7 @@ static inline uint64_t timeval_to_millis(uv_timeval_t t) {
 }
 
 // Std.Internal.UV.System.getrusage : IO RUsage
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage() {
     uv_rusage_t usage;
     int result = uv_getrusage(&usage);
     if (result < 0) {
@@ -505,7 +505,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.exePath : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath() {
     char buffer[PATH_MAX];
     size_t size = sizeof(buffer);
 
@@ -519,25 +519,25 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) {
 }
 
 // Std.Internal.UV.System.freeMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory() {
     uint64_t mem = uv_get_free_memory();
     return lean_io_result_mk_ok(lean_box_uint64(mem));
 }
 
 // Std.Internal.UV.System.totalMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory() {
     uint64_t mem = uv_get_total_memory();
     return lean_io_result_mk_ok(lean_box_uint64(mem));
 }
 
 // Std.Internal.UV.System.constrainedMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory() {
     uint64_t mem = uv_get_constrained_memory();
     return lean_io_result_mk_ok(lean_box_uint64(mem));
 }
 
 // Std.Internal.UV.System.availableMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory() {
 #if UV_VERSION_HEX >= 0x012D00
     uint64_t mem = uv_get_available_memory();
     return lean_io_result_mk_ok(lean_box_uint64(mem));
@@ -551,191 +551,191 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */
 #else
 
 // Std.Internal.UV.System.getProcessTitle : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.setProcessTitle : @& String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.uptime : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetPid : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetPpid : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.cpuInfo : IO (Array CPUInfo)
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.cwd : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.chdir : String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osHomedir : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osTmpdir : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetPasswd : IO PasswdInfo
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetGroup : IO (Option GroupInfo)
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osEnviron : IO (Array (String × String))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetenv : String → IO (Option String)
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osSetenv : String → String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osUnsetenv : String → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetHostname : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osGetPriority : UInt64 → IO Int
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osSetPriority : UInt64 → Int → IO Unit
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.osUname : IO UnameInfo
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.hrtime : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error (Array UInt8)))
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 // Std.Internal.UV.System.getrusage : IO RUsage
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 // Std.Internal.UV.System.exePath : IO String
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 // Std.Internal.UV.System.freeMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 // Std.Internal.UV.System.totalMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 // Std.Internal.UV.System.constrainedMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 // Std.Internal.UV.System.availableMemory : IO UInt64
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );

src/runtime/uv/system.h

@@ -12,33 +12,33 @@ using namespace std;
 // =======================================
 // System information functions
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory();
 
 }

src/runtime/uv/tcp.cpp

@@ -81,7 +81,7 @@ void initialize_libuv_tcp_socket() {
 // TCP Socket Operations
 
 /* Std.Internal.UV.TCP.Socket.new : IO Socket */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new() {
     lean_uv_tcp_socket_object* tcp_socket = (lean_uv_tcp_socket_object*)malloc(sizeof(lean_uv_tcp_socket_object));
 
     tcp_socket->m_promise_accept = nullptr;
@@ -114,7 +114,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */) {
 }
 
 /* Std.Internal.UV.TCP.Socket.connect (socket : @& Socket) (addr : @& SocketAddress) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     lean_object* promise = lean_promise_new();
@@ -166,7 +166,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_
 }
 
 /* Std.Internal.UV.TCP.Socket.send (socket : @& Socket) (data : Array ByteArray) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     size_t array_len = lean_array_size(data_array);
@@ -242,7 +242,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
 }
 
 /* Std.Internal.UV.TCP.Socket.recv? (socket : @& Socket) (size : UInt64) : IO (IO.Promise (Except IO.Error (Option ByteArray))) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     // Locking early prevents potential parallelism issues setting the byte_array.
@@ -317,7 +317,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t
 }
 
 /* Std.Internal.UV.TCP.Socket.waitReadable (socket : @& Socket) : IO (IO.Promise (Except IO.Error Bool)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -384,7 +384,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket,
 }
 
 /* Std.Internal.UV.TCP.Socket.cancelRecv (socket : @& Socket) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -413,7 +413,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, ob
 }
 
 /* Std.Internal.UV.TCP.Socket.bind (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     sockaddr_storage addr_ptr;
@@ -431,7 +431,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg
 }
 
 /* Std.Internal.UV.TCP.Socket.listen (socket : @& Socket) (backlog : Int32) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -484,7 +484,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t
 }
 
 /* Std.Internal.UV.TCP.Socket.accept (socket : @& Socket) : IO (IO.Promise (Except IO.Error Socket)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     // Locking early prevents potential parallelism issues setting m_promise_accept.
@@ -497,7 +497,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg
     lean_object* promise = lean_promise_new();
     mark_mt(promise);
 
-    lean_object* client = lean_io_result_take_value(lean_uv_tcp_new(lean_box(0)));
+    lean_object* client = lean_io_result_take_value(lean_uv_tcp_new());
 
     lean_uv_tcp_socket_object* client_socket = lean_to_uv_tcp_socket(client);
 
@@ -525,7 +525,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg
 }
 
 /* Std.Internal.UV.TCP.Socket.shutdown (socket : @& Socket) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     // Locking early prevents potential parallelism issues setting the m_promise_shutdown.
@@ -581,7 +581,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_a
 }
 
 /* Std.Internal.UV.TCP.Socket.getPeerName (socket : @& Socket) : IO SocketAddress */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     sockaddr_storage addr_storage;
@@ -601,7 +601,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, ob
 }
 
 /* Std.Internal.UV.TCP.Socket.getSockName (socket : @& Socket) : IO SocketAddress */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     struct sockaddr_storage addr_storage;
@@ -620,7 +620,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, ob
 }
 
 /* Std.Internal.UV.TCP.Socket.noDelay (socket : @& Socket) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -635,7 +635,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_ar
 }
 
 /* Std.Internal.UV.TCP.Socket.keepAlive (socket : @& Socket) (enable : Int8) (delay : UInt32) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -653,49 +653,49 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int3
 // =======================================
 // TCP Socket Operations
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
@@ -705,29 +705,29 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_a
 // =======================================
 // TCP Socket Utility Functions
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 #endif
-}
+}

src/runtime/uv/tcp.h

@@ -41,23 +41,23 @@ static inline lean_uv_tcp_socket_object* lean_to_uv_tcp_socket(lean_object* o) {
 // =======================================
 // TCP Socket Operations
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket);
 
 // =======================================
 // TCP Socket Utility Functions
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay);
 
 }

src/runtime/uv/timer.cpp

@@ -55,14 +55,14 @@ void handle_timer_event(uv_timer_t* handle) {
    if (timer->m_repeating) {
         // For repeating timers, only resolves if the promise exists and is not finished
         if (timer->m_promise != NULL && !timer_promise_is_finished(timer)) {
-            lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise, lean_io_mk_world());
+            lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise);
             lean_dec(res);
         }
     } else {
         // For non-repeating timers, resolves if the promise exists
         if (timer->m_promise != NULL) {
             lean_assert(!timer_promise_is_finished(timer));
-            lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise, lean_io_mk_world());
+            lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise);
             lean_dec(res);
         }
 
@@ -75,7 +75,7 @@ void handle_timer_event(uv_timer_t* handle) {
 }
 
 /* Std.Internal.UV.Timer.mk (timeout : UInt64) (repeating : Bool) : IO Timer */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating) {
     lean_uv_timer_object * timer = (lean_uv_timer_object*)malloc(sizeof(lean_uv_timer_object));
     timer->m_timeout = timeout;
     timer->m_repeating = repeating;
@@ -104,16 +104,11 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t r
 }
 
 /* Std.Internal.UV.Timer.next (timer : @& Timer) : IO (IO.Promise Unit) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj) {
     lean_uv_timer_object * timer = lean_to_uv_timer(obj);
 
     auto create_promise = []() {
-        lean_object * prom_res = lean_io_promise_new(lean_io_mk_world());
-        lean_object * promise = lean_ctor_get(prom_res, 0);
-        lean_inc(promise);
-        lean_dec(prom_res);
-
-        return promise;
+        return lean_io_promise_new();
     };
 
     auto setup_timer = [create_promise, obj, timer]() {
@@ -199,7 +194,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj, obj_arg /*
 }
 
 /* Std.Internal.UV.Timer.reset (timer : @& Timer) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj) {
     lean_uv_timer_object * timer = lean_to_uv_timer(obj);
 
     // Locking to access the state in order to avoid data-race
@@ -230,7 +225,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj, obj_arg /
 }
 
 /* Std.Internal.UV.Timer.stop (timer : @& Timer) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj) {
     lean_uv_timer_object * timer = lean_to_uv_timer(obj);
 
     // Locking to access the state in order to avoid data-race
@@ -258,7 +253,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj, obj_arg /*
 }
 
 /* Std.Internal.UV.Timer.cancel (timer : @& Timer) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj) {
     lean_uv_timer_object * timer = lean_to_uv_timer(obj);
 
     // It's locking here to avoid changing the state during other operations.
@@ -289,31 +284,31 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj, obj_arg
 
 void lean_uv_timer_finalizer(void* ptr);
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer, obj_arg /* w */ ) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );

src/runtime/uv/timer.h

@@ -47,11 +47,11 @@ static inline lean_uv_timer_object* lean_to_uv_timer(lean_object * o) { return (
 
 // =======================================
 // Timer manipulation functions
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg timer, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg timer);
 
 #endif
 

src/runtime/uv/udp.cpp

@@ -60,7 +60,7 @@ void initialize_libuv_udp_socket() {
 // UDP Socket Operations
 
 /* Std.Internal.UV.UDP.Socket.new : IO Socket */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new() {
     lean_uv_udp_socket_object* udp_socket = (lean_uv_udp_socket_object*)malloc(sizeof(lean_uv_udp_socket_object));
 
     udp_socket->m_promise_read = nullptr;
@@ -89,7 +89,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */) {
 }
 
 /* Std.Internal.UV.UDP.Socket.bind (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
     sockaddr_storage addr_ptr;
@@ -107,7 +107,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg
 }
 
 /* Std.Internal.UV.UDP.Socket.connect (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
     sockaddr_storage addr_ptr;
@@ -125,7 +125,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_
 }
 
 /* Std.Internal.UV.UDP.Socket.send (socket : @& Socket) (data : Array ByteArray) (addr : @& Option SocketAddress) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
     size_t array_len = lean_array_size(data_array);
@@ -211,7 +211,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
 }
 
 /* Std.Internal.UV.UDP.Socket.recv (socket : @& Socket) (size : UInt64) : IO (IO.Promise (Except IO.Error (ByteArray × SocketAddress))) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     // Locking earlier to avoid parallelism issues with m_promise_read.
@@ -295,7 +295,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t
 }
 
 /* Std.Internal.UV.UDP.Socket.waitReadable (socket : @& Socket) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
     // Locking earlier to avoid parallelism issues with m_promise_read.
@@ -361,7 +361,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket,
 }
 
 /* Std.Internal.UV.UDP.Socket.cancelRecv (socket : @& Socket) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
     lean_inc(socket);
@@ -397,7 +397,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, ob
 // UDP Socket Utility Functions
 
 /* Std.Internal.UV.UDP.Socket.getPeerName (socket : @& Socket) : IO SocketAddress */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     struct sockaddr_storage addr_storage;
@@ -436,7 +436,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getsockname(b_obj_arg socket) {
 }
 
 /* Std.Internal.UV.UDP.Socket.setBroadcast (socket : @& Socket) (on : Bool) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -451,7 +451,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket,
 }
 
 /* Std.Internal.UV.UDP.Socket.setMulticastLoop (socket : @& Socket) (on : Bool) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -466,7 +466,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg soc
 }
 
 /* Std.Internal.UV.UDP.Socket.setMulticastTTL (socket : @& Socket) (ttl : UInt32) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -481,7 +481,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg sock
 }
 
 /* Std.Internal.UV.UDP.Socket.setMembership (socket : @& Socket) (multicastAddr : @& IpAddr) (interfaceAddr : @& Option IpAddr) (membership : UInt8) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     char multicast_addr_str[INET_ADDRSTRLEN];
@@ -507,7 +507,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket,
 }
 
 /* Std.Internal.UV.UDP.Socket.setMulticastInterface (socket : @& Socket) (interfaceAddr : @& IPAddr) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     char interface_addr_str[INET_ADDRSTRLEN];
@@ -525,7 +525,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_ar
 }
 
 /* Std.Internal.UV.UDP.Socket.setTTL (socket : @& Socket) (ttl : UInt32) : IO Unit  */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl) {
     lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
 
     event_loop_lock(&global_ev);
@@ -541,31 +541,31 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32
 
 #else
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new() {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data, b_obj_arg opt_addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data, b_obj_arg opt_addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
@@ -574,7 +574,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t
 // =======================================
 // UDP Socket Utility Functions
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
@@ -586,41 +586,41 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getsockname(b_obj_arg socket) {
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl) {
     lean_always_assert(
         false && ("Please build a version of Lean4 with libuv to invoke this.")
     );
 }
 
 #endif
-}
+}

src/runtime/uv/udp.h

@@ -38,24 +38,24 @@ static inline lean_uv_udp_socket_object* lean_to_uv_udp_socket(lean_object * o)
 // =======================================
 // UDP Socket Operations
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new();
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket);
 
 // =======================================
 // UDP Socket Utility Functions
 
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getsockname(b_obj_arg socket);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl);
 
 }

src/util/io.h

@@ -50,4 +50,5 @@ template<typename T> T get_io_scalar_result(object * o) {
         return r;
     }
 }
+
 }

src/util/option_declarations.cpp

@@ -14,10 +14,10 @@ typedef object_ref option_decl;
 
 extern "C" object * lean_data_value_to_string (obj_arg d);
 
-extern "C" object * lean_get_option_decls_array(obj_arg w);
+extern "C" object * lean_get_option_decls_array();
 
 option_declarations get_option_declarations() {
-    auto decl_array = get_io_result<array_ref<pair_ref<name, option_decl> > > (lean_get_option_decls_array(io_mk_world()));
+    auto decl_array = get_io_result<array_ref<pair_ref<name, option_decl> > > (lean_get_option_decls_array());
     option_declarations r;
     for (pair_ref<name, option_decl> const & p : decl_array) {
         option_decl decl = p.snd();
@@ -46,10 +46,10 @@ data_value mk_data_value(data_value_kind k, char const * val) {
     }
 }
 
-extern "C" object * lean_register_option(obj_arg name, obj_arg decl, obj_arg w);
+extern "C" object * lean_register_option(obj_arg name, obj_arg decl);
 
 void register_option(name const & n, name const & decl_name, data_value_kind k, char const * default_value, char const * description) {
     object_ref decl = mk_cnstr(0, decl_name, mk_data_value(k, default_value), string_ref(""), string_ref(description));
-    consume_io_result(lean_register_option(n.to_obj_arg(), decl.to_obj_arg(), io_mk_world()));
+    consume_io_result(lean_register_option(n.to_obj_arg(), decl.to_obj_arg()));
 }
 }

src/util/shell.cpp

@@ -157,9 +157,9 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
 
 using namespace lean; // NOLINT
 
-extern "C" obj_res lean_display_header(obj_arg);
+extern "C" obj_res lean_display_header();
 static void display_header() {
-    consume_io_result(lean_display_header(io_mk_world()));
+    consume_io_result(lean_display_header());
 }
 
 static void display_version(std::ostream & out) {
@@ -174,9 +174,9 @@ static void display_features(std::ostream & out) {
     out << "]\n";
 }
 
-extern "C" obj_res lean_display_help(uint8 use_stderr, obj_arg);
+extern "C" obj_res lean_display_help(uint8 use_stderr);
 static void display_help(bool use_stderr) {
-    consume_io_result(lean_display_help(use_stderr, io_mk_world()));
+    consume_io_result(lean_display_help(use_stderr));
 }
 
 static int only_src_deps = 0;
@@ -292,8 +292,7 @@ extern "C" obj_res lean_shell_main(
     uint8    json_output,
     obj_arg  error_kinds,
     uint8    print_stats,
-    uint8    run,
-    obj_arg  w
+    uint8    run
 );
 uint32 run_shell_main(
     int argc, char* argv[],
@@ -342,19 +341,18 @@ uint32 run_shell_main(
         json_output,
         error_kinds.to_obj_arg(),
         print_stats,
-        run,
-        io_mk_world()
+        run
     ));
 }
 
-extern "C" object* lean_init_search_path(object* w);
+extern "C" object* lean_init_search_path();
 void init_search_path() {
-    get_io_scalar_result<unsigned>(lean_init_search_path(io_mk_world()));
+    get_io_scalar_result<unsigned>(lean_init_search_path());
 }
 
-extern "C" object* lean_environment_free_regions(object * env, object * w);
+extern "C" object* lean_environment_free_regions(object * env);
 void environment_free_regions(elab_environment && env) {
-    consume_io_result(lean_environment_free_regions(env.steal(), io_mk_world()));
+    consume_io_result(lean_environment_free_regions(env.steal()));
 }
 }
 
@@ -365,7 +363,7 @@ void check_optarg(char const * option_name) {
     }
 }
 
-extern "C" object * lean_enable_initializer_execution(object * w);
+extern "C" object * lean_enable_initializer_execution();
 
 namespace lean {
 extern void (*g_lean_report_task_get_blocked_time)(std::chrono::nanoseconds);
@@ -437,7 +435,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
         std::cerr << "error: " << ex.what() << std::endl;
         return 1;
     }
-    consume_io_result(lean_enable_initializer_execution(io_mk_world()));
+    consume_io_result(lean_enable_initializer_execution());
 
     options opts = get_default_options();
     optional<std::string> c_output;