Panics in Std.HashMap.find!

Stream: std4

[Kyle Miller]

I can make a mwe for this eventually, but I just noticed that docs#Std.HashMap.find! can sometimes panic even when it succeeds. There's a panic! expression being passed to getD, and while perhaps normally that expression gets inlined into getD, for whatever reason in my case it seems to be lifted out first.

[Mario Carneiro]

can you make a MWE?

[Kyle Miller]

import Std.Data.HashMap

def follow (m : Std.HashMap Nat Nat) (start : Nat) : IO Nat := do
  let mut i := start
  let mut count := 0
  while i != 0 do
    IO.println s!"i = {i}"
    i := m.find! i
    count := count + 1
  return count

#eval follow (Std.HashMap.ofList [(1,3),(3,2),(2,0)]) 1
/-
i = 1
i = 3
i = 2
3
-/
-- Meanwhile
/-
PANIC at Std.HashMap.find! Std.Data.HashMap.Basic:314:23: key is not in the map
PANIC at Std.HashMap.find! Std.Data.HashMap.Basic:314:23: key is not in the map
PANIC at Std.HashMap.find! Std.Data.HashMap.Basic:314:23: key is not in the map
-/

[Mario Carneiro]

fixed in lean4#3043