Is there an algorithm that provably exists although we don't know what it is?
The simplest case I know of an algorithm that exists, though it is not
known which algorithm, concerns finite state automata.

The quotient $L_1/L_2$ of a language $L_1$ by a language $L_2$ is
defined as $L_1/L_2=\{x \mid \exists y\in L_2 \text{ such that } xy\in L_1\}$.

It is easily proved that regular set are closed under quotient by an
arbitrary set.  In other words, if $L_1$ is regular and $L_2$ is arbitrary (not necessarily regular), then $L_1/L_2$ is regular, too.

The proof is quite simple. Let $M=(Q,\Sigma,\delta,q_0,F)$ be a FSA
accepting the regular set $R$, where $Q$ and $F$ are respectively the
set of states and the set of accepting states, and let $L$ be an
arbitrary language. Let $F'=\{q\in Q\mid \exists y\in L \;\;\delta(q,y)\in
F\}$ be the set of states from which a final state can be reached by
accepting a string from $L$.

The automaton $M'=(Q,\Sigma,\delta,q_0,F')$, which differs from $M$
only in its set $F'$ of final states recognizes precisely $R/L$.  (Or see  Hopcroft-Ullman 1979, page 62 for a proof of this fact.)

However, when the set $L$ is not decidable, there may be no algorithm
to decide which states have the property that defines $F'$. So, while
we know that the set $F'$ is a subset of $Q$, we have no algorithm to
determine which subset. Consequently, while we know that $R$ is
accepted by one of $2^{|Q|}$ possible FSA, we do not know which it is.
Though I must confess we know to a large extent what it looks like.

This is an example of what is sometimes called an almost constructive
proof, that is a proof that one of a finite number of answers is the
right one.

I suppose an extension of that could be a proof that one of an
enumerable set of answers is the right one. But I do not know any. Nor
do I know a purely non-constructive proof that some problem is
decidable, for example using only contradiction.