Bug in `Std.HashSet`?

Stream: lean4

[Frédéric Dupuis]

In the following code snippet, I get the very strange error unknown free variable: _kernel_fresh.278:

import Std.Data.HashSet.Basic

def validUpdate (upd : Array Nat) (rules : Std.HashSet (Nat × Nat)) : Bool := Id.run do
  for i in [:upd.size-1] do
    for hj : j in [i+1:upd.size] do
      if rules.contains ⟨upd[j], upd[i]!⟩ then return false
  return true

Did I just hit a bug in Std.HashSet?

If I replace Std.HashSet by Array, the error disappears.

[Markus Himmel]

This looks like an instance of lean4#4548, could you add your example there?

[Frédéric Dupuis]

Done!