From 9107d273688d7941b28058e4daf2952edf8536cd Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 29 Aug 2025 12:33:57 -0300 Subject: [PATCH] fix: remove extend from async and await (#10173) This PR removes the `extends Monad` from `MonadAwait` and `MonadAsync` to avoid underdetermined instances. The issue was discussed here: [#lean4 > Is Std.Internal.IO.Async.MonadAsync.toMonad a bad instance?](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Is.20Std.2EInternal.2EIO.2EAsync.2EMonadAsync.2EtoMonad.20a.20bad.20instance.3F) --- src/Std/Internal/Async/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean index 43676d15ea..fbd9a571cc 100644 --- a/src/Std/Internal/Async/Basic.lean +++ b/src/Std/Internal/Async/Basic.lean @@ -70,7 +70,7 @@ with non async code that uses them. Typeclass for monads that can "await" a computation of type `t α` in a monad `m` until the result is available. -/ -class MonadAwait (t : Type → Type) (m : Type → Type) extends Monad m where +class MonadAwait (t : Type → Type) (m : Type → Type) where /-- Awaits the result of `t α` and returns it inside the `m` monad. -/ @@ -79,7 +79,7 @@ class MonadAwait (t : Type → Type) (m : Type → Type) extends Monad m where /-- Represents monads that can launch computations asynchronously of type `t` in a monad `m`. -/ -class MonadAsync (t : Type → Type) (m : Type → Type) extends Monad m where +class MonadAsync (t : Type → Type) (m : Type → Type) where /-- Starts an asynchronous computation in another monad. -/ @@ -107,7 +107,7 @@ instance [MonadAwait t m] : MonadAwait t (StateRefT' s n m) where await := liftM (m := m) ∘ MonadAwait.await @[default_instance] -instance [MonadAwait t m] : MonadAwait t (StateT s m) where +instance [Monad m] [MonadAwait t m] : MonadAwait t (StateT s m) where await := liftM (m := m) ∘ MonadAwait.await @[default_instance] @@ -119,7 +119,7 @@ instance [MonadAsync t m] : MonadAsync t (StateRefT' s n m) where async p prio := MonadAsync.async (prio := prio) ∘ p @[default_instance] -instance [Functor t] [inst : MonadAsync t m] : MonadAsync t (StateT s m) where +instance [Monad m] [Functor t] [inst : MonadAsync t m] : MonadAsync t (StateT s m) where async p prio := fun s => do let t ← inst.async (prio := prio) (p s) pure (t <&> Prod.fst, s)