exact and new goals

Stream: general

[Reid Barton]

How come exact makes _s appearing inside record constructors into new goals?

structure C := (x : ℕ)
example : C := by exact ⟨_⟩ -- error on _, "don't know how to synthesize placeholder"
example : C := by exact { x := _ } -- error on exact, "tactic failed, there are unsolved goals"