RFC: `open` keyword in `do`-monad

Proposal

I would like to see the following code work:

namespace Foo
def ara: String := "ara"
end Foo

def yolo: IO Unit := do
  open Foo
  IO.print s!"{ara}"

#eval yolo

in other words, it should be syntactically-valid in Lean to write open <namespace> in a do-monad, and have that namespace be opened for the rest of the lines in that do block.

I think it makes sense for the syntax to be open <namespace> and not open <namespace> in, but I don't feel strongly about the presence/absence of in.

Currently, the compiler error message for this case is rather confusing, so making it be legal syntax would eliminate a confusing compiler error message and make it somewhat more convenient to use a do-monad

Community Feedback

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.60open.60.20in.20.60do.60.20blocks

The proposal concerns Lean do-monad syntax and the compiler error produced for open Foo inside a do block, but it names no files, tests, or entry points. Start by tracing parsing and elaboration for do blocks, then review the linked Zulip discussion before deciding between the proposed syntax forms. Done means the example is syntactically valid and the namespace remains open for the rest of the block.