Here is one explanation of why countable choice is not problematic in constructive mathematics.
For this discussion it is useful to formulate the axiom of choice as follows:
$(\forall x \in X . \exists y \in Y . R(x,y)) \implies \exists f \in Y^X . \forall x \in X . R(x,f(x))$
This says that a total relation $R \subseteq X \times Y$ contains a function. The usual formulation of the axiom of choice is equivalent to the above one. Indeed, if $(S_i)_{i \in I}$ is a family of non-empty sets we take $X = I$, $Y = \bigcup_i S_i$ and $R(i,x) \iff x \in S_i$ to obtain a choice function $f : I \to \bigcup_i S_i$. Conversely, given a total relation $R \subseteq X \times Y$, consider the the family $(S_x)_{x \in X}$ where $S_x = \lbrace y \in Y \mid R(x,y)\rbrace$ and apply the usual axiom of choice.
One way of viewing sets in constructive mathematics is to imagine that they are collections together with given equality, i.e., some sort of "presets" equipped with equivalence relations. This actually makes sense if you think about how we implement abstract sets in computers: each element of the abstract set is represented by a finite sequence of bits, where each element may have many valid representations (and this is unavoidable in general). Let me give two specific examples:
a natural number $n \in \mathbb{N}$ is represented in the usual binary system, and let us allow leadings zeroes, so that $42$ is represented by $101010$ as well as $0101010$, $00101010$, etc.
a (computable) real $x \in \mathbb{R}$ is represented by machine code (a binary string) that computes arbitrarily good approximations of $x$. Specifically, a piece of code $p$ represents $x$ when $p(n)$ outputs a rational number that differs from $x$ by at most $2^{-n}$. Of course we only represent computable reals this way, and every computable real has many different representations.
Let me write $\mathbb{R}$ for the set of computable reals, because those are the only reals relevant to this discussion.
An essential difference between the first and the second example is that there is a computable canonical choice of representatives for elements of $\mathbb{N}$ (chop off the leading zeroes), whereas there is no such canonical choice for $\mathbb{R}$, for if we had it we could decide equality of computable reals and consequently solve the Halting problem.
According to the constructive interpretation of logic, a statement of the form
$\forall x \in X . \exists y \in Y . R(x, y)$
holds if there is a program $p$ which takes as input a representative for $x \in X$ and produces a representative for $y \in Y$, together with a witness for $R(x,y)$. Crucially, $p$ need not respect equality of $X$. For example,
$\forall x \in \mathbb{R} . \exists n \in \mathbb{N} . x < n$
is accepted because we can write a program which takes as input a representative of $x$, namely a program $p$ as described above, and outputs a natural number larger than $x$, for example $round(p(0)) + 1000$. However, the number $n$ will necessarily depend on $p$, and there is no way too make it depend only on $x$ (computably).
Let us have a look at the axiom of choice again:
$(\forall x \in X . \exists y \in Y . R(x,y)) \implies \exists f \in Y^X . \forall x \in X . R(x,f(x))$
We accept this if there is a program which takes as input a $p$ witnessing totality of $R$ and outputs a representative of a choice function $f$, as well as a witness that $\forall x \in X. R(x, f(x))$ holds. This is probematic because $p$ need not respect equality of $X$, whereas a representative for $f$ must respect equality. It is not clear where we could get it from, and in specific examples we can show that there isn't one. Already the following fails:
$(\forall x \in \mathbb{R} . \exists n \in \mathbb{N} . x < n) \implies \exists f \in \mathbb{N}^\mathbb{R} . \forall x \in \mathbb{R} . x < f(x)$.
Indeed, every computable map $f : \mathbb{R} \to \mathbb{N}$ is constant (because a non-constant one would allow us to write a Halting oracle).
However, if we specialize to countable choice
$(\forall n \in \mathbb{N} . \exists y \in Y . R(n,y)) \implies \exists f \in Y^\mathbb{N} . \forall n \in \mathbb{N} . R(n,f(n))$
then we can produce the desired program. Given $p$ that witnesses totality of $R$, define the following program $q$ that represents a choice function: $q$ takes as input a binary representation of a natural number $n$, possibly with leading zeroes, chops of the leading zeroes, and applies $p$. Now, even if $p$ did not respect equality of natural numbers, $q$ does because it applies $p$ to canonically chosen representatives.
In general, we will accept choice for those sets $X$ that have computable canonical representatives for their elements. Ok, this was a bit quick, but I hope I got the idea accross.
Let me finish with a general comment. Most working mathematicians cannot imagine alternative mathematical universes because they were thoroughly trained to think about only one mathemtical universe, namely classical set theory. As a result their mathematical intuition has fallen a victim to classical set theory. The first step towards understanding why someone might call into question a mathematical principle which seems obviously true to them, is to broaden their horizon by studying other mathematical universes. On a smaller scale this is quite obvious: one cannot make sense of non-Euclidean geometry by interpreting points and lines as those of the Euclidean plane. Similarly, you cannot understand in what way the axiom of choice could fail by interpreting it in classical set theory. You must switch to a different universe, even though you think there isn't one... Of course, this takes some effort, but it's a real eye-opener.
The Axiom of Choice is a principle that applies to arbitrary families of arbitrary sets, and this is a realm where the concept of recusive functions or Turing Turing computability simply does not apply. For example, mathematicians may use AC to select elements of subsets of a (possibly uncountable dimension) vector space in order to form a basis---you iteratively pick a vector outside the span of what you have so far---and it simply doesn't make sense in this generality for such a function to be recursive or equivalent to a recursive function. This is why people were objecting to your question in the comments.
But let me try to make some sense of the question. Suppose we restrict our choice principle to families of sets that each have at least one computable member. Then, I claim that there is a definable choice function, for we may select from each set in the family the computable member that is computed by the smallest program. Thus, this formulation of what you might mean by ACC is simply provable in ZF. But this function will not in general be itself computable (it merely selects computable members, and this is not the same), and indeed, since the domain of the function is not necessarily $N$, the concept of this function being computable isn't always sensible.
If you intend to have a version of ACC that only applies to countably-indexed families $\langle A_n| n\in N\rangle$, with each $A_n$ a set containing subsets of $N$, at least one of which is computable, then it is provable in ZF that we cannot insist there is always a computable function $f$ such that $f(n)$ is a program computing a member of $A_n$. The reason is that there are only countably many such functions $f$, and we may easily diagonalize against them to produce a bad sequence $\langle A_n | n\in N\rangle$.
If you replace computable with definable, then your principle has a much better chance. One subtle issue, however, is that "being definable" is not first order expressible in set theory, so you cannot state your ACC principle that way. Rather, one can use "ordinal-definable", which is expressible. The principle that every set contains an ordinal-definable element is equivalent (by a previous MO question) to the set-theoretic principle $V=HOD$. And this principle implies AC, in the form that under V=HOD, every family of nonempty sets admits an ordinal definable choice function.
One can also impose more restrictive versisons of definability on the choice functions or on the families. For example, perhaps one wants principles that only apply to sets of reals, and one wants to know when there are, say, projective choice functions. This phenomenon is called uniformization, and is extensively studied in descriptive set theory.
So there are a variety of ways to make sense of your question, and these different interpretations give different answers. So it all depends on what you mean.
Best Answer
There are two ingredients in the Banach-Tarski decomposition theorem:
Most discussion about the theorem revolve around the axiom of choice. I would like to point out that the notion of space can be put under scrutiny as well.
The Banach-Tarski decomposition of the sphere produces non-measurable parts of the sphere. If we restrict the notion of "part" to "measurable subset" the theorem disappears. For instance, if we move over into a model of set theory (without choice) in which all sets are measurable, we will have no Banach-Tarski. This is all well known.
Somewhat amazingly, we can make the Banach-Tarski decomposition go away by extending the notion of subspace, and keep choice too. Alex Simpson in Measure, Randomness and Sublocales (Annals of Pure and Applied Logic, 163(11), pp. 1642-1659, 2012) shows that this is achieved by generalizing the notion of topological space to that of locale. He explains it thus:
Peter Johnstone explained in The point of pointless topology why locales have mathematical significance that goes far beyond fixing a strange theorem about decomposition of the sphere. Why isn't everyone using locales? I do not know, I think it is purely a historic accident. At some point in the 20th century mathematicians collectively lost the idea that there is more to space than just its points.
I personally prefer to blame the trouble on the notion of space, rather than the axiom of choice. As far as possible, geometric problems should be the business of geometry, not logic or set theory. Mathematicians are used to operating with various kinds of spaces (in geometry, in analysis, in topology, in algebraic geometry, in computation, etc.) and so it seems only natural that one should worry about using the correct notion of space first, and about underlying foundational principles later. Good math is immune to changes in foundations.