A nice source of examples of this kind are decidable theories whose decision procedures have very high computational complexities.
For example, consider Presburger arithmetic, the first-order theory of arithmetic without multiplication. You can show that the theory is decidable (the proof is simple and very pretty, IMO), which means that any statement in the theory is either provably true or provably false. However, the lower bound on the complexity is $O(2^{2^n})$, and the best actually known algorithms are triply-exponential.
Another example, which you might find more mathematically compelling, is that the first-order theory of real closed fields is also decidable. (Tarski showed this back in the 50s, I think.) A corollary of this is that the theory of Euclidean geometry is decidable. However, it's manifestly not the case that geometry is trivial! Tarski's algorithm had nonelementary complexity, and I think the lower bound is doubly-exponential, though I don't know the complexity of the best modern algorithms.
EDIT: these examples are constructive, in the sense that they are decision procedures. This might not really be what you want.
An example of a fully non-constructive existence proof can be found in the usual proof of the completeness of the Kripke semantics of intuitionistic logic. Since this is a classical proof, the disjunction property of intuitionistic logic (i.e., that $A \vee B$'s provability entails either the provability of $A$ or the provability of $B$) is stated classically -- the completeness proof doesn't yield a procedure to give you a particular disjunct.
