bug: mut + match + dependent types

Stream: lean4

[Floris van Doorn]

There is a bug when match changes the type of a mutable variable: the mutable variable gets an old value within the match statement.

import Lean
open Lean Meta

structure Foo (n : Nat) where
  (l : List Nat)
  (h : n = n)

def foo (n : Nat) : MetaM Unit := do
  let mut result : Foo n := ⟨[7], rfl⟩
  trace[Meta.Tactic.simp] "Initial value of result: {result.l}"
  result := ⟨List.range n, rfl⟩
  trace[Meta.Tactic.simp] "We have a new value of result {result.l}"
  match n with
  | _ => trace[Meta.Tactic.simp] "The value of result reverted back to the original value {result.l}"

set_option trace.Meta.Tactic.simp true
run_meta do
  foo 5
-- [Meta.Tactic.simp] Initial value of result: [7]
-- [Meta.Tactic.simp] We have a new value of result [0, 1, 2, 3, 4]
-- [Meta.Tactic.simp] The value of result reverted back to the original value [7]
-- **Expected**: -- [Meta.Tactic.simp] The value of result reverted back to the original value [0, 1, 2, 3, 4]

[Floris van Doorn]

Note: replacing trace by logInfo changes the behavior:

import Lean
open Lean Meta

structure Foo (n : Nat) where
  (l : List Nat)
  (h : n = n)

def foo' (n : Nat) : MetaM Unit := do
  let mut result : Foo n := ⟨[7], rfl⟩
  logInfo m!"Initial value of result: {result.l}"
  result := ⟨List.range n, rfl⟩
  logInfo m!"We have a new value of result {result.l}"
  match n with
  | _ => logInfo m!"Now we keep the new value {result.l}"

run_meta do
  foo' 5
-- Initial value of result: [7]
-- We have a new value of result [0, 1, 2, 3, 4]
-- Now we keep the new value [0, 1, 2, 3, 4]

[Floris van Doorn]

In another (non-MWE) instance, adding a trace caused match to find the "right" value for the mutable variable, but with logInfo we got the wrong value.

[Floris van Doorn]

lean#11337

[Jovan Gerbscheid]

I ran into another let mut bug that was really hard to debug, because adding logInfo in some places would remove the bug(!!!). Here's a MWE:

import Std

local instance {α β cmp} [Append β] : Append (Std.TreeMap α β cmp) :=
  ⟨.mergeWith (fun _ ↦ (· ++ ·))⟩

def foo (hyp? : Option Unit) (a : α) : IO (Std.TreeMap Nat (Array α)) := do
  let mut tree := {}
  if true then
    pure ()
  tree := tree ++ (.insert {} 0 #[a])
  if let some _ := hyp? then
    tree := tree
  return tree

-- We expect `foo none 3` to return `Std.TreeMap.ofList [(0, #[3])]`
#eval foo none 3 -- Std.TreeMap.ofList []

Lean automatically infers the type of tree to be Std.TreeMap Nat (Array α), but if I give the type annotation myself, replacing let mut tree := {} with let mut tree : Std.TreeMap Nat (Array α) := {}, the bug goes away!

[Kim Morrison]

Could you open an issue for this one?

[Floris van Doorn]

lean#12229

@Jovan Gerbscheid: I noticed similar behavior, where adding/removing logging would change how match and the mutable variable interact.