If $T$ is a theorem of ZF which says something only about reals, then one may want to prove $T$ using a theory like 2nd order PA or related theories like ZFC$^-$ or GBC$^-$ (minus accounts for the absence of the Power Set axiom). In many cases this goes through, sometimes rather straightforwardly, but there are important counterexamples like Borel Determinacy.

Therefore I wonder whether the diamond $\Diamond_{\omega_1}$ is provable in [2nd order PA, or ZFC$^-$, or GBC$^-$] + [all reals are constructible].

Or at least whether [2nd order PA, or ZFC$^-$, or GBC$^-$] + [all reals are constructible] + $\Diamond_{\omega_1}$ is equiconsistent with 2nd order PA.

It is not quite clear how one can adequately formulate $\Diamond_{\omega_1}$ in say ZFC$^-$. However in GBC$^-$ a standard definition of $\Diamond_{\omega_1}$ can be reformulated with several class quantifiers. Thus the problem is to figure out whether $\Diamond_{\omega_1}$ is relatively consistent with GBC$^-$. (Not more than the consistency of GBC$^-$ should be assumed.)