How to lift a monad instance?

Stream: lean4

[StructSeeker]

The following quite natural code can't compile

def foo [Monad m] [MonadReader Nat m] [MonadExcept String m]: m Bool := do
  pure ((<- read) > 4)

def bar [Monad m] [MonadExcept String m]: m Bool := do
  let env : Nat := 2
  ReaderT.run (foo (m:= ReaderT Nat m)) env

I receive the following alert

failed to synthesize
  MonadExcept String (ReaderT Nat m)

Do i need to implement a instance manually whenever i meet this kind of situation?
I ask AI but unable to obtain a satisfactory answer.

[Aaron Liu]

Why do you think you should be able to read a Nat out of ReaderT Bool m?

[StructSeeker]

Aaron Liu
Sorry, i mistyped when trying to create a minimal example. But I still can't solve the problem.

[Eric Wieser]

I think we're missing a MonadExcept instance for ReaderT

[Eric Wieser]

instance [MonadExcept ε m] : MonadExcept ε (ReaderT ρ m) where
  throw e := fun _ => throw e
  tryCatch body handler := fun x => tryCatch (body x) (handler · x)

[Eric Wieser]

I'm quite surprised this is missing; was it removed accidentally recently?

[Eric Wieser]

Ah, it's docs#ReaderT.instMonadExceptOf

[Eric Wieser]

I think you're not supposed to assume MonadExcept, and to use MonadExceptOf isntead?