Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and without the axiom of choice, and assuming powersets are available.
(One can contemplate working in a predicative setting such as CZF, where the Dedekind reals form a class, but I fail to see how it is useful to discuss countability of reals in a setting that does not even allow the formation of reals as a bona fide set.)
#### Which reals?
There are three standard constructions of reals, which differ constructively:
* **Cauchy reals** $\mathbb{R}_c$ are constructed as a quotient of rational Cauchy sequences.
* **Dedekind reals** $\mathbb{R}_d$ are constrcuted as (double-sided) Dedekind cuts of rationals.
* **MacNeille reals** $\mathbb{R}_m$ are constructed as a certain weaker version of Dedekind cuts of rationals.
We have $\mathbb{R}_c \subseteq \mathbb{R}_d \subseteq \mathbb{R}_m$, where all three inclusions might be proper.
The MacNeille reals fail to satisfy $0 < x \lor x < 1$, which makes them less useful.
Without countable choice, the Cauchy reals are not nice, either. One cannot even show that they are Cauchy-complete.
So the canonical construction for reals is by Dedekind cuts, so most constructive mathematics is done with $\mathbb{R}_d$. (Note also that $\mathbb{R}_c = \mathbb{R}_d$ in the presence of countable choice.)
### Countability and subcountability
The definition of countability that works well is: $A$ is **countable** if there is a surjection $\mathbb{N} \to 1 + A$. When $A$ is inhabited this is equivalent to having a surjection $\mathbb{N} \to A$.
A set $A$ is **subcountable** if there is $S \subseteq \mathbb{N}$ and a surjection $S \to A$. In particular, every subset of $\mathbb{N}$ is subcountable.
A set $A$ is **uncountable** if it is not countable. A stronger property is **sequence-avoiding**: for every sequence $\mathbb{N} \to A$ there is an element of $A$ that is not a term of the sequence.
**Theorem:** *The MacNeille reals are sequence-avoiding, thus uncountable.*
*Proof.* See [A constructive Knaster–Tarski proof of the uncountability of the reals](https://arxiv.org/abs/1902.07366) by Ingo Blechschmidt and Matthias Hutzler. $\Box$
**Theorem:** *$\lbrace 0, 1\rbrace^\mathbb{N}$ and $\mathcal{P}(\mathbb{N})$ are sequence-avoiding, thus uncountable.*
*Proof.* Cantor's diagonal method is constructive. Given $f : \mathbb{N} \to \lbrace 0, 1\rbrace^\mathbb{N}$, the sequence $n \mapsto 1 - f(n)(n)$ differs from $f(n)$ in the $n$-th place. Similarly, given $g : \mathbb{N} \to \mathcal{P}(\mathbb{N})$, the set $\lbrace n \in \mathbb{N} \mid n \notin f(n) \rbrace$ differs from $f(n)$ at $n$.
$\Box$
Caveats:
1. Constructively the set of binary sequences $\lbrace 0, 1\rbrace^\mathbb{N}$, the powerset $\mathcal{P}(\mathbb{N})$, and the reals (of any kind) *cannot* be shown to be in bijective correspondence.
2. It cannot be shown constructively that every real has a digit expansion, so we cannot carry out the diagonal method on $\mathbb{R}$ that way. (This is also a good reason for *not* teaching uncountability of the reals using decimal expansions. The method of nested intervals is to be preferred, as it works with either excluded middle or countable choice.)
**Theorem:** *If excluded middle holds then $\mathbb{R}_c = \mathbb{R}_d = \mathbb{R}_m$, and they are all sequence-avoiding, thus uncountable.*
*Proof.* See notes from your freshman year in analysis. $\Box$
**Theorem:** *If countable choice holds then $\mathbb{R}_c = \mathbb{R}_d$ and they are both sequence-avoiding, thus uncountable.*
*Proof.* See for example Bishop's book “Foundations of constructive analysis" (1967, Section 2.2), where the method of nested intervals is employed, using countable choice. $\Box$
Contrary to classical mathematics, subcountability has very little to do with countability, apart from the obvious observation that every countable set is subcountable.
**Theorem:** *There is a topos in which there is an injection $\mathbb{R}_d \to \mathbb{N}$ and $\mathbb{R}_d$ is sequence-avoiding, so there is no surjection $\mathbb{N} \to \mathbb{R}_d$.*
*Proof.* This happens in the realizability topos on Joel Hamkins's infinite-time Turing machines. I have not actually written this down, but the embedding is done much the same way as the embedding $\mathbb{N}^\mathbb{N} \to \mathbb{N}$ in [An injection from the Baire space to natural numbers](https://doi.org/10.1017/S0960129513000406). The idea is that infinite-time Turing machines can compute from any code of a rational Cauchy sequence converging to $x$ a canonical such code. $\Box$
It has also been known since at least the 1980's that in the effective topos $\mathbb{R}_d$ is subcountable and sequence-avoiding.
### Further remarks about “sizes” of sets
When you enter the constructive world, you should leave classical ideas about size behind.
**Theorem:** *Suppose the following principle holds: if there are injections $A \to B$ and $B \to A$ then there is a bijection $A \to B$. Then excluded middle holds.*
*Proof.* See [Cantor–Bernstein implies Excluded Middle](https://arxiv.org/abs/1904.09193) by Chad Brown and Cécilia Pradic. $\Box$
**Theorem:** *Suppose the following principle holds: every subset of a finite set is finite. Then excluded middle holds.*
*Proof.* See the Anger stage of [Five stages of accepting constructive mathematics](http://dx.doi.org/10.1090/bull/1556). $\Box$
**Theorem:** *If every subcountable set is countable and Markov principle holds, then excluded middle holds.*
*Proof.* See Proposition 2.6 of [Every metric space is separable in function realizability](https://doi.org/10.23638/LMCS-15%282%3A14%292019) by Andrej Bauer and Andrew Swan. $\Box$