initialize structure with IO.Ref

Stream: lean4

[Adam Topaz]

What's the correct way to make the following work?

structure Foo where
  ref : IO.Ref Nat

def mkFoo : IO Foo := do
  let ref : IO.Ref Nat ← IO.mkRef 0
  return { ref }

initialize foo : Foo ← mkFoo
/-
failed to synthesize
  Inhabited Foo
-/

For comparison, the following is just fine:

initialize foo : IO.Ref Nat ← IO.mkRef 0

and the following naive things fail:

structure Foo where
  ref : IO.Ref Nat
deriving Inhabited -- fails

#synth Inhabited (IO.Ref Nat) -- fails

[Robin Arnez]

You need deriving Nonempty here

[Adam Topaz]

Ah ok.

[Eric Wieser]

This could probably do with a better error message; I've been tripped up by the same one

[Eric Wieser]

Somehow it seems to be bypassing this code

[Kim Morrison]

https://github.com/leanprover/lean4/pull/11919 improves the error message