$\newcommand\Z{\mathbb{Z}}$

Perhaps this is the kind of example you seek.

Consider the theory $T$ in the language with one unary function symbol $S$, which asserts that $S$ is a bijection of the universe with itself, and has no finite cycles. For example, this theory is true in the integers with the usual successor operation $\langle\Z,S\rangle$, and also in the model obtained by placing two or more copies of $\Z$ aside one another.

Suppose you give me any assertion $p$ in this language, no matter how complicated. I claim that we can know that $T$ decides $p$, without knowing which way, simply by pointing out that $T$ is $\aleph_1$-categorical: every model of $T$ of size $\aleph_1$ consists precisely of $\aleph_1$ many copies of $\Z$, and these are all isomorphic. It follows that the theory is complete, and so $T$ decides $p$, even though we wouldn't necessarily know initially which way it is decided. The categoricity existence proof of decidability does not seem to provide any bound on the length of the proof, although I believe that more refined analysis would provide such bounds.

Meanwhile, let me also point out that it will be difficult to say precisely what you mean by not being able to construct an explicit bound, since the function that takes an assertion $p$ to the length of the shortest proof of $p$ in $T$ is a computable function, whose program we can write down, and so our situation is that we have an explicitly given computable function that provides the bound.

**Update.** One can use this example to also make an example over ZFC or another foundational theory. Suppose ZFC is consistent. Fix any $p$ in the language of successor as above, but let $\varphi_p$ be the assertion "$T$ proves $p$", as formalized in the language of set theory. Now, if $T$ really does prove $p$, then we can prove $\varphi_p$ in ZFC. And if it doesn't, then $T$ proves $\neg p$, and we can prove in ZFC that $T$ proves $\neg p$, and so since ZFC proves that $T$ is consistent and complete, we can prove $\neg\varphi_p$ in ZFC. In this way, we have transformed the example above into an example in the foundational theory ZFC.

computableset of (closed) formulas. (Otherwise you could take PA plus all true $\Pi^0_1$-formulas, or just $Th(\mathbb N)$.) $\endgroup$ – Goldstern Oct 31 '13 at 11:17