How far is it true that statements dependent on Axiom of Choice are not constructive.

We know it is impossible to define a Hamel basis for $\Bbb R$ over $\Bbb Q$ (or construct a non-principal ultrafilter, and so on) because it is a theorem:

If $\sf ZFC$ is consistent, then the theory $\sf ZF+\text{There is no Hamel basis for }\Bbb R\text{ over }\Bbb Q$ is consistent.

Since it is consistent with $\sf ZF$ that there is no such basis, it means that we cannot prove from $\sf ZF$ that such basis exists. We have to assume more, in terms of choice.

Remember the completeness theorem tells us that $\sf ZF\vdash\varphi$ if and only if $\varphi$ is true in every model of $\sf ZF$. Similarly for $\sf ZFC$. So given a statement $\varphi$ which is provable from $\sf ZFC$, if we can find a model of $\sf ZF$ where $\varphi$ fails, we can be certain that $\sf ZF$ cannot prove it, and some axiom of choice is needed for the proof.

For example, we know that if $\sf ZFC$ is consistent then we can create a model in which there is no Hamel basis of $\Bbb R$ over $\Bbb Q$. Of course, in that model the axiom of choice fails, but the process itself is consistent. Of course it might be the case that there are no models of $\sf ZFC$ at all, but we still know how to make it work then. We can translate these arguments into syntactic arguments which state the quote text above.

Depending on one's interpretation of the "meta-theorem" you stated, the following might be seen as a counterexample.

There is a sentence $\varphi$ such that it is a theorem of $\mathsf{ZF}$ that $\varphi$ defines a Hamel basis $B$ of $\mathbb{R} \cap L$ over $\mathbb{Q}$. Here $L$ denotes Goedel's constructible universe. It is a theorem of $\mathsf{ZF}$ that $L \models \mathsf{ZFC} + V=L$, that the relativization $\varphi^L$ of $\varphi$ to $L$ defines the same set $B$ within $L$, and that $L \models B \text{ is a Hamel basis of $\mathbb{R}$ over $\mathbb{Q}$.}$

So here we have a "construction" (definition) $\varphi$ such that $\mathsf{ZF}$ proves that it defines a unique object, and that this object is a $\mathbb{Q}$-linearly independent set of reals, but does not prove that the $\mathbb{Q}$-linear span of the set of reals so defined is all of $\mathbb{R}$. On the other hand, the theory $\mathsf{ZFC} + V = L$ "verifies" (proves) that the set $B$ defined by $\varphi$ does in fact span $\mathbb{R}$, and therefore is a Hamel basis for $\mathbb{R}$ over $\mathbb{Q}$.

The only problem with this counterexample is that the "verification" requires the theory $\mathsf{ZFC} + V = L$, which is properly stronger than $\mathsf{ZFC}$. I'm not sure if this addresses your question (which is a bit fuzzy) but I thought it was worth mentioning.

EDIT: One main point of this "counterexample" is that, although many people think of models of AC as containing more sets (e.g. more $\mathbb{Q}$-linearly independent subsets of $\mathbb{R}$, including some that span) it makes just as much sense to think of them as containing fewer sets (e.g. fewer reals, so that spanning becomes easier.) Given models $M$ and $N$ of $\mathsf{ZF}$ with $M \subset N$, one can have $M \models \mathsf{AC}$ and $N \models \neg \mathsf{AC}$ or vice versa. So it is not always right to think of $\mathsf{AC}$ as providing "extra" sets.