The key point is that, as Bauer mentions, countable choice refers to the statement "every family of inhabited sets indexed by $\mathbb{N}$ has a choice function". In other words, given a family $(A_n)_{n\in\mathbb{N}}$ such that each $A_n$ is inhabited, there exists a function $f:\mathbb{N}\to\bigcup A_n$ such that $f(n)\in A_n$ for each $n$.
Classically, you could deduce the axiom of choice for finite families from this statement by putting your finite family in bijection with the first $n$ natural numbers and then extending the family in some arbitrary way on the rest of the natural numbers. Constructively, however, you can't do this, because there isn't necessarily a natural number $n$ such that your finite set has exactly $n$ elements! Indeed, this is crucially exactly what is going on in the proof of excluded middle from choice: if you knew the set $\{A,B\}$ had a cardinality that was a natural number, that would decide $P$: $P$ is true if $\{A,B\}$ has $1$ element and $\neg P$ is true if it has $2$ elements.
In what follows, work in your favorite foundational theory: one where it is sensible to talk about an object $\mathbb{N}$ satisfying the Peano axioms, about proofs, consistency, etc. and where you can prove the incompleteness theorems. For example Aczel's CZF, or even Martin-Löf Type Theory are suitable, constructive foundational systems.
Start with an effectively axiomatized, consistent first-order theory $T$ extending Peano Arithmetic. (What is a consistent theory? Precisely what your foundational theory proves is a consistent theory!)
Since $T$ is consistent, there is no proof of $\bot$ starting from the axioms of $T$ (this is the usual definition of consistency). But recall that, by construction, the arithmetical sentence $\mathrm{Con}(T)$ holds in $\mathbb{N}$ precisely if there does not exist an arithmetically coded proof of $\bot$ starting from the axioms of the theory $T$.
We now sketch a proof that the consistency of $T$ implies that $\mathrm{Con}(T)$ holds in $\mathbb{N}$. Assume for a contradiction that there exists an arithmetically coded proof of $\bot$ starting from the axioms of the theory $T$. Inductively* undo the arithmetic coding to produce a genuine proof of $\bot$ starting from the axioms of $T$. This contradicts the fact that $T$ is consistent, so our assumption must have been wrong, and therefore there is no arithmetically coded proof of $\bot$ starting from the axioms of the theory $T$. By definition this means that $\mathrm{Con}(T)$ holds in $\mathbb{N}$. Since we didn't invoke excluded middle or double-negation elimination anywhere, our proof is constructive.
We conclude that
- $T$ does not prove $\mathrm{Con}(T)$, but
- $\mathrm{Con}(T)$ holds in $\mathbb{N}$.
We are done. Notice that we didn't need to define anything like a computable $\mathrm{eval}_\mathbb{N}$ (which is, by the way, not possible). We did have to set up the notion of "sentence holding in a structure" to say what it means for $\mathrm{Con}(T)$ to hold in $\mathbb{N}$, but that works via the usual Tarskian paraphrasis, and does not require anything non-constructive. We also had to know that the Gödel/Rosser proofs of the incompleteness theorems (the versions not mentioning "truth") are constructive: Gödel points this out explicitly in his original papers.
edit: To answer your question in the comment below, I sketch a Tarskian definition of satisfaction in $\mathbb{N}$ using Agda notation. This one works for relational languages (which is sufficient for everything done above): the definition for languages with function symbols is a tad bit more complicated, but proceeds along similar lines. Below the type of variables, Var, is assumed to be something like $x_1,x_2,\dots$ of variables, so that you can compare them by index (but really any type with decidable equality would do). Satisfaction is defined with respect to a substitution $\sigma$ that maps free variables to their values: since sentences have no free variables, the choice of $\sigma$ does not really matter.
_[_≔_] : (Var → ℕ) → Var → ℕ → Var → ℕ
σ [ x ≔ n ] = σ' where
σ' : Var → ℕ
σ' y with compare y x
σ' y | equal .x = n
σ' y | less _ _ = σ y
σ' y | greater _ _ = σ y
_tarski_ : (Var → ℕ) → Formula → Set
σ tarski (atomic_equals x y) = σ x ≡ σ y
[...]
σ tarski (P ∧ Q) = (σ tarski P) × (σ tarski Q)
[...]
σ tarski (all x P) = ∀ (n : ℕ) → (σ [ x ≔ n ]) tarski P
* The exact details depend on how you defined the notion of proof. You use the fact that the length of a proof is a natural number (i.e. belongs to $\mathbb{N}$) to make the induction work, and if you defined it in a sufficiently clever way, you need not do any work at all.
Best Answer
The first step of your reasoning here is faulty. We can't get a surjection from $A$ onto $A → B$ from Reynolds' bijection. At least, it would be big news, because by the rest of your argument, it would mean that System F is not consistent, which in turn would mean either that some widely believed/imitated proofs are actually faulty, or something like ZF had proved a contradiction.
Your Lawvere argument is why "negative" inductive types are problematic to have in a type theory. They allow a $T$ such that $T \cong A^T$, which quickly leads to looping terms in $A$ via a translation of Lawvere's argument. However, System F does not let you define these "negative" types. It only has fixed points of "positive" operations like $A^{A^-}$. That is positive due to being, "double negative," but it is still positive.
The reasoning behind Reynolds' last step is that there is no bijection $A → Ω^{Ω^A}$, where $Ω$ is the set of truth values. This holds even constructively. The classical aspect is taking $2$, the booleans, to be the set of truth values. This is a definable type in System F, so in a classical set theoretic semantics Reynolds' type would need to be interepreted as a fixed point of the double power set operator, which doesn't exist.
However, constructively, $2^A$ is not the power set of $A$, but the decidable subsets of $A$, and there can be fixed points of $2^{2^-}$. The obvious counterpoint to the Reynolds paper is "Polymorphism is Set Theoretic Constructively." But for instance this article might be a little simpler to think about as an introduction, and leads to the idea that you can have a situation where $ℕ \cong 2^{2^ℕ}$ constructively (also, check the comments for a link to a paper on this being the case for classical topological spaces).