Unknown free variable in v4.15.0

Stream: lean4

[Marcus Rossel]

I haven't been able to minimize this further so far, but it fails with unknown free variable: _uniq.4:

import Lean

#version -- Lean 4.15.0

example : Std.HashSet Nat := Id.run do
  if "".isEmpty then dbg_trace ""; return ∅
  if (#[] : Array Nat).all (fun _ => True) then return ∅
  return ∅

[Kim Morrison]

This is not new in v4.15.0. I suspect that, as with lean#4418 and lean#4548, this is an issue with the old code generator (and good news, the new one is under active development again!). You can work around this for now by adding noncomputable.