Are there any non-constructive proofs for which an example was never constructed?
The game of Chomp is an example. A short and extremely simple strategy-stealing argument shows that no matter the size of the playing board, the first player always has a winning strategy; the complete argument is given in the Wikipedia article. But there is no general strategy known for an arbitrarily sized board.
There are many. In the proof that every vector space has a basis; in the proof that every ideal can be extended to a maximal ideal; in the proof that every filter can be extended to an ultrafilter.
All those use Zorn's lemma and in fact just show that such object exists. None of these proofs can construct the actual object in explicit details, because it is consistent that Zorn's lemma is false and these sort of objects may not exist sometimes (that is, some vector spaces won't have a basis, and so on). Generally speaking the axiom of choice (which is equivalent to Zorn's lemma) is responsible for a lot of the non-constructiveness of modern mathematics, as the axiom asserts the existence of certain objects which cannot be proved to exist otherwise.
If you want another semi-non constructive proof you can use the Cantor-Bernstein theorem for that. It's very easy to prove there is a bijection between $\Bbb{N^N}$ and $\mathcal P(\Bbb N)$ without constructing one, if you are using Cantor-Bernstein. While it is possible to actually construct such bijection, it's much easier to just prove it exists by other means.
In another direction one can argue, for example, that the proof that a continuous function from a closed and bounded interval to $\Bbb R$ must attain its minimum and maximum is non-constructive, because we don't actually construct the point, we just prove it exists.
Classical examples of non-constructive proofs for where no explicit construction is possible naturally come from proofs that essentially use Zorn's Lemma. One such example would be the fact that any vector space has a basis. In particular, $\mathbb R$ is a vector space over $\mathbb Q$, and so there is a basis for $\mathbb R$ over $\mathbb Q$. Such a basis is called a Hamel basis. But, no such basis is given explicitly.
On the same line of thought but, imo, more striking, is the use of Zermelo's Theorem to prove there must exist a well-ordering of the reals (and thus, that golden dream of having a grip on that elusive first positive real number seems to be closer...).
Yet no such ordering on $\;\Bbb R\;$, as far as I am aware, is known. Of course, Zermelo's Theorem, Zorn's Lemma and The Axiom of Choice are all logically equivalent in ZFC.