Cannot mutate mutable variable

Stream: lean4

[Zach Battleman]

Hi! I was working on a little project and I encountered some strange behavior. Here is a minimal working example

def baz (bar : Nat → IO PUnit) := fun x => bar x

def foo : IO Nat := do
  let mut myVar := 0
  baz (fun x => do
      myVar := myVar + 10
      IO.println s!"{myVar}")
  return 0

The error I get is that myVar needs to be declared mutably in order to mutate it, but it clearly is. Is this a result of myVar being fixed when I enter the body of baz? A similar example of nested dos works fine:

def foo' : IO Nat := do
  let mut myVar := 0
  do
    myVar := myVar + 10
  IO.println s!"{myVar}"

  return 0

I guess I'm just wondering if the top example is intended behavior (excluding the error message which seems confusing) and if so specifically why? Thanks so much!

[Kyle Miller]

Basically, mutable variables are only mutable in when you have nested do/if/for/unless expressions, but when you have a do inside a fun then it's not considered to be nested anymore. It might help remembering that the variables are just "mutable" -- the do notation is figuring out how to rewrite your code into functional programming equivalents to pass explicit state around. When you're passing that function to baz, it doesn't have the freedom to change that function so that this state is passed in and returned.

[Kyle Miller]

In the first example, Lean is seeing that you're trying to mutate myVar in a context where myVar isn't declared as a mutable variable (due to the fun separating this do from the outer do, so from that perspective it's the right error message, but it could probably be improved.

[Kyle Miller]

In the second example, directly nested do notation is handled specially so it's able see myVar as still being mutable.

[Zach Battleman]

Ah I see, that makes sense, thanks!

[James Gallicchio]

I'm actually sort of surprised by the error message here -- I would've expected it to say that myVar is a constant defined outside the scope of the do block. It seems useful to differentiate this error from something like

def foo : IO Nat := do
  let myVar := 0
  myVar := 1
  sorry

where the "only variables declared using let mut can be mutated" error message makes more sense

[James Gallicchio]

I find it even more confusing in a situation like this:

def bar := 0

def foo : IO Nat := do
  bar := 1
  return 0
/-
`bar` cannot be mutated, only variables declared using
`let mut` can be mutated. If you did not intent to mutate
but define `bar`, consider using `let bar` instead
-/

But I'm not sure whether that information (is a constant defined in the current do-block?) is available to the do macro.