let/if indentation in do blocks

[digama0]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The parser does not accept:

example : Id Nat := do
  let x ← if true then
    pure 1
  else
    pure 2
  pure x

It requires an extra level of indentation:

example : Id Nat := do
  let x ←
    if true then
      pure 1
    else
      pure 2
  pure x

Can we do something to the withPosition stuff for if to support this case? This is tricky because one-sided if is legal in that position (which is part of a do notation, even though the possible productions are limited). My suggested interpretation would be for the if to expect the else to be aligned with the let, if both are on the same line. (Banning one-sided if there is also reasonable since the let x <- part is guaranteed superfluous in that case seeing as it would bind an element of Unit.)

Note that there is no issue with this indentation pattern with let x := if ... else because in this case the if ... else is parsed as an expression and not a do seq item so the else is mandatory and does not need to be aligned in any particular way.

Versions

Lean (version 4.0.0-nightly-2022-04-16, commit 726b735c6df7, Release)

[leodemoura]

Yeah, this issue is quite annoying. I agree it is natural to try to write

  let x ← if true then
    pure 1
  else
    pure 2

I frequently hit this problem too. This issue is a low priority, but we will try to figure out something.

[Kha]

I would suggest a new parser combinator withPositionAfterLinebreak that applies withPosition only if checkLinebreakBefore succeeded. That would allow if to fall back to the let's position if they are on the same line. I can implement it if that sounds right.

[leodemoura]

@Kha Thanks for the suggestion. I think it should work.