chore: update expected output for sanitychecks test

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

src/Lean/Elab/Extra.lean

@@ -573,11 +573,16 @@ def elabDefaultOrNonempty : TermElab :=  fun stx expectedType? => do
   | some expectedType =>
     try
       mkDefault expectedType
-    catch ex => try
+    catch _ => try
       mkOfNonempty expectedType
     catch _ =>
       if stx[1].isNone then
-        throw ex
+        throwError "\
+          failed to synthesize '{.ofConstName ``Inhabited}' or '{.ofConstName ``Nonempty}' instance for\
+          {indentExpr expectedType}\n\
+          \n\
+          If this type is defined using the 'structure' or 'inductive' command, \
+          you can try adding a 'deriving Nonempty' clause to it."
       else
         -- It is in the context of an `unsafe` constant. We can use sorry instead.
         -- Another option is to make a recursive application since it is unsafe.

tests/lean/run/initializeNonemptyErrorMsg.lean

@@ -0,0 +1,30 @@
+/-!
+# Test for improved error message when `initialize` fails due to missing `Nonempty` instance
+
+See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/initialize.20structure.20with.20IO.2ERef/near/564920245
+-/
+
+structure Foo where
+  ref : IO.Ref Nat
+
+def mkFoo : IO Foo := do
+  let ref ← IO.mkRef 0
+  return { ref }
+
+/-- error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
+  Foo
+
+If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it. -/
+#guard_msgs in
+initialize _foo : Foo ← mkFoo
+
+-- The fix: adding `deriving Nonempty` makes it work
+structure Bar where
+  ref : IO.Ref Nat
+  deriving Nonempty
+
+def mkBar : IO Bar := do
+  let ref ← IO.mkRef 0
+  return { ref }
+
+initialize _bar : Bar ← mkBar

tests/lean/sanitychecks.lean.expected.out

@@ -7,10 +7,10 @@ no parameters suitable for structural recursion
 well-founded recursion cannot be used, `unsound` does not take any (non-fixed) arguments
 sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
 sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
-sanitychecks.lean:10:0-10:23: error: failed to synthesize
-  Inhabited False
+sanitychecks.lean:10:0-10:23: error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
+  False
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
 sanitychecks.lean:18:12-18:20: error: invalid use of `partial`, `Foo.unsound3` is not a function
   False
 sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition `Foo.unsound4`, could not prove that the type