do notation + loops

Stream: lean4

[Siddharth Bhat]

Consider:

def matchInForInMonad (b: Bool) (xs: List String) : IO String := do
    let mut outstr :  String := ""
    for x in xs do
      match b with
      -- | false => () -- fails
      | false => let k : IO Unit := pure (); k -- works
      -- | false => return () -- fails
      | true => outstr := outstr ++ x ++ "\n"
    return outstr

The version that is | false => () stopped compiling when I bumped up my Lean4 nightly from leanprover/lean4:nightly-2022-01-16 to 4.0.0-nightly-2022-03-04. I'm unsure what exactly changed in the desugaring.

I wonder why pure () succeeds while return () fails?

[Sebastian Ullrich]

I'm unsure what exactly changed in the desugaring.

https://github.com/leanprover/lean4/commit/e9d85f49e657787bf6eb899a1ac3591ccf1f36bd

Siddharth Bhat said:

I wonder why pure () succeeds while return () fails?

return exits the entire do block, so the type it is expecting is String