Elaboration failure with let mut whose RHS is a do notation

[bollu]

Consider the MWE:

def fails : MetaM Unit := do
  let mut val : Bool ← do
      pure true
  -- unknown identifier val
  val := Bool.not val -- FAILS! expected to succeed.
  return ()

This can be worked around by shadowing:

def succeeds : MetaM Unit := do
  let val : Bool ← do
      pure true
  let mut val := val
  val := Bool.not val
  return ()

Reported on zulip at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Elaboration.20failure.20with.20let.20mut.20whose.20RHS.20is.20a.20do.20notation/near/474621276

[alexkeizer]

As a workaround, the following should also work, and is somewhat shorter:

def succeeds : MetaM Unit := do
  let mut val :=← do
      pure true
  val := Bool.not val
  return ()