Proving decidability of formula without deciding it I am looking for a theory $T$ and a formula $p$ such that there is a metaproof which establishes that either $T \vdash p$ or $T \vdash \neg p$, but which does not enable us to decide which of these two cases holds.
Of course, we can define an algorithm that searches the proof space for derivations of $p$ or $\neg p$ from $T$, and given that either $T \vdash p$ or $T \vdash \neg p$, we can be sure that the algorithm will terminate at some point. Considering this, what I want is that the metaproof of the decidability of $p$ in $T$ does not enable us to construct an explicit upper bound for the time this algorithm needs.
If such $T$ and $p$ can be found, I am especially interested in a case where $T$ is some well-known foundational theory (like ZFC or PA) and $p$ is some interesting – or at least intuitively meaningful – statement (and not some practically uninterpretable formula). 
 A: $\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. 
A: Let $p$ state that there is no proof over PA of length at most $2^{21820}$ of the Collatz conjecture. Then clearly PA either proves $p$ or $¬p$, but we have no idea which. Furthermore, there is some evidence that Collatz-type behaviour do not have simple proofs in general, so if $p$ is true then the shortest proof of $p$ may be to simply verify all proofs of length at most $2^{21820}$, and if $p$ is false then the shortest proof of $¬p$ may be to verify some huge number of ad-hoc cases that happen to suffice for ad-hoc reasons.
Of course, this kind of example is not restricted to the Collatz conjecture. Any conjecture that sits on the border between decidability and undecidability as far as we can tell would be a good candidate for this method of generating relatively short arithmetical sentences that are provable by PA but with truth values we have no good guess for.
