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.
As others have noted there are several different meanings for constructive.
I. Constructive proof in the sense of constructive mathematics
This meaning views an object as existing if we have a description of how to construct the objects (though we don't really need to carry it out), and there are several distinct constructive views. Saying a proof is constructive or not can be ambiguous without specifying which school of constructive mathematics we are talking about.
By the way, it can be the case that we can convert a non-constructive proof to a constructive one (Georg Kreisel's unwinding program or Ulrich Kohlenbach's proof mining program). That does not make the original proof constructive!
Note that algorithmic computability is just one of several constructive perspectives. For example, in intuitionism there are objects which are not algorithmically computable. A way of understanding this is to remember that Churth-Turing thesis is not an axiom that is accepted by all constructivist, there can be constructions which are not algorithmic in the instuitionistic view.
II. Constructive in the sense of complexity theory
This is a more recent meaning. We mean a proof of existence of an object is constructive if it gives directly a method of efficiently computing/constructing the object. This is the more common meaning of the word in combinatorics these days, e.g. in Robin A. Moser's "A constructive proof of the Lovasz Local Lemma" paper from 2008.
Constructive is used in the sense of efficient algorithms in complexity theory, for example, constructive in Alexander Razborov and Steven Rudich's "Natural Proofs" paper means that the property used in the lower-bound proof is efficiently computable.
Note that the proof itself can be non-constructive in the sense of meaning I while remaining constructive in this sense. You can give an efficient algorithm to compute some object and the correctness and efficiency proofs can be non-constructive. We don't have many interesting examples, but a good example would be the Robertson-Seymour theorem. See also Are there non-constructive algorithm existence proofs?
III. Proof complexity perspective
This is kind of the intersection of the previous two, though I don't recall anyone refer to it as "constructive proof" (probably because they are aware of both previous meanings and don't want to confuse people further :).
Here not only the object should be computable efficiently but the correctness and efficiency proofs must use only efficient concepts. The Robertson-Seymour theorem is an example of an efficient algorithm where we don't have a proof using only efficient concepts. I can give more artificial examples to distinguish between this and the meaning in the previous section but I don't recall any other natural ones.
Best Answer
Yes.
We take a fixed diophantine equation in variables $y,x_1, x_2, \ldots, x_k$. Task: for an input $n \in \mathbb{Z}$, output either
It is clear that for any diophantine equation, there is a program which performs this task. If there are five values of $y$ for which solutions exist, you need only have the program output these for all inputs. If there are fewer than four values of $y$ for which solutions exist, once you know the solutions, then writing the program is trivial.
However, telling whether a solution exists to a diophantine equation is undecidable.