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