Bug in library_search?

Stream: general

[Yevhenii Diomidov]

example {α : Type} (a : α) : punit → α := by library_search -- Try this: refine punit.rec a
example {α : Type} (a : α) : punit → α := by refine punit.rec a
  -- type mismatch at application `punit.rec a` term `a` has type `α : Type` but is expected to have type `?m_1 punit.star : Sort ?`

[Mario Carneiro]

more like a bug in pretty printing; lean has an issue with printing terms that don't re-parse at the same level of explicitness

[Bryan Gin-ge Chen]

Some more examples:

example {α : Type} (a : α) : punit → α := punit.rec a -- same error as above
example {α : Type} (a : α) : punit → α := by refine punit.rec (by exact a) -- works
example {α : Type} (a : α) : punit → α := punit.rec (by exact a) -- also works

[Mario Carneiro]

this isn't likely to be fixed in lean 3; lean 4 has a proper support for this through a "delaborator" that can add only just enough implicit information to parse correctly

[Mario Carneiro]

when writing terms manually, the suggested fix is \lam x, punit.rec a x