RFC: better UX around `throw`?

Proposal

Currently, throw "error" : IO A does not typecheck. I would like it to typecheck.

Reasoning:

• As a seasoned Lean programmer it is still hard for me to remember .userError when trying to throw in IO. I suspect this is deeply unfriendly to beginners.
• There is a canonical coercion from String to IO.Error, via .userError.
• User code in IO almost always wants to throw via this canonical coercion, rather than the more internal-to-IO errors.

I have no ideas for how to do this without some major changes to MonadExcept. Suggestions appreciated.

One (bad) option would be to add a MonadExceptOf instance:

instance (priority := low) : MonadExceptOf String IO where
  throw e := throw (.userError e)
  tryCatch x f := tryCatch x (fun
    | .userError e => f e
    | e => throw e)

#check show IO Unit from throwThe String "hi"
#check show IO Unit from throw (.userError "hi")

but this requires throwThe String rather than throw, which I find no better than the status quo.

Community Feedback

Small bit of discussion here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Map.20of.20Lean's.20monads

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading MonadExcept, IO.Error, and the existing String-to-IO.Error coercion described in the proposal, then review the linked Zulip discussion. The design should make throw "error" : IO A typecheck while preserving behavior for other IO errors and avoiding a requirement to use throwThe String.