As Kaveh says in a comment, the issue is not going to be choice. Usually, when we examine what goes wrong when we try to formalize a "nonconstructive" classical proof in a constructive system, the problem that we discover is that the proof is already nonconstructive before the axiom of choice is invoked.
In this case, the issue is that the entire concept of partitions and equivalence classes, which underlies the usual proof of the Banach-Tarski paradox, behaves very differently in constructive systems.
Consider the simpler case of a Vitali set in the real line. Two reals are defined to be equivalent if their difference is rational. That is a perfectly good definition in constructive systems, but it is easy to miss the fact that it involves an implicit universal quantifier over the rationals (or the ability to tell whether an arbitrary real is rational). In this particular case, standard methods show that it will not be possible to prove constructively that "for all reals $x$ and $y$, either $x$ is equivalent to $y$ or $x$ is not equivalent to $y$". Thus it is no longer possible to prove that two equivalence classes $[x]$ and $[y]$ are disjoint or identical, that is, impossible to prove that the equivalence classes form a partition of the real line. But that fact is crucial for the usual proof that the Vitali set is nonmeasurable. The same sort of problem is easy to spot in the usual proof of the Banach-Tarski paradox.
- More precisely, this will be impossible in any of the usual formalized systems for constructive mathematics, including intuitionistic type theory.