return binding in doSeq

Stream: general

[Yicheng Qian]

Why does the following code evaluate to 1?

#eval @id (Lean.CoreM _) do
  let a ← if True then return 1 else pure 2
  return a + 10

I had essentially this in my codebase which caused a bug, and I spent hours trying to figure out what was wrong. Anyway is this expected behaviour, and why?

[Yicheng Qian]

My understanding is that anything to the right of ← shouldn't mess with the control flow, and by the way

#eval @id (Lean.CoreM _) do
  let a ← (if True then return 1 else pure 2)
  return a + 10

evaluates to 11.

[Kyle Miller]

This is a subtle but intentional part of do notation. The control flow can extend into let ... ← for if, do, match, and other doElems. It's how you can bind the result of the doElem. If you have something that looks like it could extend the control flow, it's best to use pure to avoid an accidental early return.

There's a bit of feedback that the editor provides you that you can use to check the interpretation: if you move your cursor right before return, the corresponding do that it returns from is highlighted.

And, yeah, parentheses currently cause it to switch from parsing the if as a doElem to as a term. The return keyword works in as a term as well, and I think it's equivalent to writing do return.

It's unfortunate how subtle return can be, and also how it's not always clear when control flow is joined together in do notation. I've found being able to return from such an if is useful though.