Unknown identifier in monad

Stream: lean4

[Thomas Murrills]

Is the following #mwe a bug?

example (x : Option Nat) : MetaM Bool := do
  let r := if let some y := x then
    match ← pure y with -- unknown identifier 'y'
    | _ => true
  else
    true
  pure r

Or is this something equivalent to "not being able to lift ← over a binder", maybe? (If y were extracted with a match expression, that's the error we'd get for any ← expression—but I wonder if the macros here are "smarter" and just know what to exclude from the local context when instead.)

[Mario Carneiro]

yes this is a "lift ← over a binder" issue

[Mario Carneiro]

If you want to stay in the monad so you can use <- you should use let r <- if let some y := x ... instead

[Mario Carneiro]

the bug is that it did not report the correct error, probably because it didn't recognize if let as a binder

[Mario Carneiro]

this is probably even more problematic if you use <- pure x instead, since it will almost certainly lift the effect outside the if let and this will be very strange

[Mario Carneiro]

does the same thing happen if you use if?

[Mario Carneiro]

... it does

[Mario Carneiro]

This seems like a footgun, e.g. you might guess that this program reads either foo or bar but it actually reads both

def readFooOrBar (x : Bool) : IO String := do
  let result := if x then
    ← IO.FS.readFile "foo"
  else
    ← IO.FS.readFile "bar"
  return result

#print readFooOrBar

def readFooOrBar : Bool → IO String :=
fun x => do
  let __do_lift ← IO.FS.readFile { toString := "foo" }
  let __do_lift_1 ← IO.FS.readFile { toString := "bar" }
  let result : String := if x = true then __do_lift else __do_lift_1
  pure result

[Mario Carneiro]

if you use match instead of if you get the "lift <- over binder" error

[Gabriel Ebner]

Yes, this is indeed a common footgun we've fired in the past: lean4#1987

[Patrick Massot]

Note that this issue is carefully explained in Functional programming in Lean.

[Patrick Massot]

But it's still a footgun.