Here is a partial answer.
Godel's theorem connects logic and set theory. Syntax is the part of the logic, it's where the formulas and proofs live; set theory is the part of the semantics, where the interpretations and models live. Of course one can have them relocated to other contexts, but classically I think that it's a theorem about logic and set theory.
It is provable without the axiom of choice that if we have an infinite tree whose nodes are the natural numbers, and every level of the tree is finite, then there is a branch in that tree. If we omit the requirement that the nodes of the tree are the natural numbers, it won't be true anymore and counterexamples do exist (by which I mean, consistent with $\sf ZF$, of course).
Similarly, given a countable language we write the proof of the completeness theorem for that language, and all our uses of the axiom of choice will be mitigated by the fact that we have a uniform enumeration of all the objects of interest. Therefore some fragment of the completeness theorem is in fact provable without any appeal to the axiom of choice.
On the other hand, the completeness theorem is not about countable languages. It is about any language of first-order logic. So we can have a lot of function symbols, or constants, or so on. So what about the above proof? Well, it can be shown that if the language is well-orderable, then indeed we can repeat the same arguments and everything is well-orderable uniformly and everything is fine.
But alas, without the axiom of choice, not every set can be well-ordered. And that where the non-constructive nature of the proof sneaks in. Let me give a particular counterexample.
Example:
We say that a set $A$ is amorphous if it is infinite, and cannot be written as a disjoint union of two infinite sets. One can show that if $A$ is an amorphous set, then there is no way to linearly order $A$. That is, there is no $R\subseteq A\times A$ such that $(A,R)$ is a linearly ordered set.
Suppose that $A$ is an amorphous set (and it is consistent that such set exists), and let $\mathcal L$ be the language in which $<$ is a binary relation symbol, and for every $a\in A$ there is a constant symbol $c_a$.
We write the axioms, $\varphi$ is the conjuction of the statements $<$ is a linear order, and for every distinct $a,b\in A$ we write $\varphi_{a,b}:=c_a\neq c_b$. This theory is consistent, because if it were to prove a contradiction there would be a finite number of $a\in A$ whose constants appear in the proof, but then we can construct a finite linear order which will be an interpretation of these axioms. This is impossible of course.
However, the theory as a whole, despite being consistent, does not have a model. Because in any model of the theory, reducing just to the constants will have defined a linear order of $A$, and $A$ itself is an amorphous set, so it cannot be linearly ordered.
So where is the axiom of choice coming into the play? When we construct models we need to make some arbitrary choices along the way. When the language is well-ordered then we can delegate these choices to the well-ordered and uniformly make them all; but when the language is an arbitrary set which may not be well-orderable to begin with, then the axiom of choice is needed.
In fact, one can prove that the completeness theorem (and its equivalent, the compactness theorem) is equivalent to the ultrafilter lemma, stating that every filter can be extended to an ultrafilter. These all are also equivalent to many other weak choice principles such as Tychonoff theorem for Hausdorff spaces, or the Boolean Prime Ideal theorem.
So what is missing from this answer? Well, I don't know about contexts where the WKL is not provable, so I cannot help in that aspect. But hopefully this answer shed some light on where the theorem is using fragments of choice and non-constructiveness.
Interest in alternative systems never dies. Although ZF-style set theory (or more precisely in my opinion, "cumulative-hierarchy-style set theory") is by far dominant, there's no inherent reason for that to remain the case forever, and there's certainly no reason to abandon the study of alternative set theories in general. Limitation of size does play an important role in such theories, so I'd say that the answer to your question is a weak "no."
However, I think this also misses the broader question: why did limitation of size (at least as such) fade away in the first place? We have to understand that before we decide what role limitation of size should play in the next set theory we cook up.
First, we remember that there are really two pieces to limitation of size. The first is that any class which surjects onto the universe of sets is a proper class. You mention that limitation of size is arguably too strong; well, this half of limitation of size is too weak to be useful on its own (although it's an important motivating force - e.g. behind replacement). The worryingly strong direction is the converse, which says that any class which does not so surject is a set.
The intuitive point now is that essentially as long as we have regularity and enough replacement - and I'll call this "cumulative-hierarchy-style" class or set theory - we can show that any proper class surjects onto the ordinals. Namely, sending $x$ to the rank of $x$ gives a surjection onto a cofinal class of ordinals, and the Mostowski collapse turns this into a surjection onto the whole class of ordinals. So by composing surjections, limitation of size holds iff there is a surjection from the ordinals to all sets. This in turn is equivalent to the existence of a well-ordering of the universe of all sets, aka global choice.
Now the key point is the above makes sense in mere set theory (in particular, ZF). Of course, on the face of it that's nonsense since we talked explicitly about classes, which we can't do in ZF. Instead, in ZF everything is about (parameter-)definable classes. But the above argument still essentially goes through, and we can prove that given a model $M$ of ZF (or indeed much less), if every parameter-definable class in $M$ is either a set in $M$ or definably surjects onto $M$, then there is a parameter-definable surjection of the $M$-ordinals onto $M$, and the converse holds as well.
It turns out that this can be collapsed into a single first-order(!) statement: namely, that there is some set $A$ such that every set is definable from $A$ together with an ordinal. (This isn't hard to see - we just say "$x$ is the $\alpha$th element of the well-ordering of $V$ induced by $s$," where $s$ is our $\{A\}$-definable surjection from the ordinals to $V$.) This can be written as "$V=$ HOD[A] for some set $A$." In case we have a parameter-freely definable surjection from the ordinals to $V$, we get $V=$ HOD. Just like in the case of the axiom of constructibility it's not immediately clear that this is actually first-order expressible, but a neat trick with the reflection principle shows that it is. So limitation of size for definable classes is a first-order principle even in mere set theory (or at least, in ZF). Now HOD and its variants are extremely important concepts in modern set theory even ignoring foundational considerations, so the "HOD-language" tends to win out (and certainly wins out when looking at ZF or its extensions).
The final piece of this picture is the shift in interpretation. Initially we may have thought of limitation of size as a maximizing principle (anything that could be a set, is), but in light of its equivalence with $V=$ HOD (ignoring parameters for now for simplicity) it threatens to take on the opposite character in cumulative-hierarchy-style set theory: which is more restrictive, that every set have some ordinal defining it or that there be no ordinal which lets us define some fixed set? The cumulative hierarchy idea pushes against the "obviously maximizing" nature of limitation of size. So it's hard to justify using limitation of size as a centerpiece of a set theory if we're committed to the centrality of the cumulative hierarchy idea and to the value of maximization of mathematical concepts, and these seem more deeply entrenched.
Best Answer
tl;dr In the first section I explain why constructive rejection of choice would not necessarily mean being in favor of negating it. Sections II and III talk about the status of choice itself, and why many constructivists prefer not to take even positive anti-Choice axioms. Finally, Section IV provides a partial answer the question you probably intended to ask (the one about anti-Choice axioms in mathematics without LEM in general, rather than the philosophical constructivism)
I. Constructivists are a diverse bunch, not cogs in some kind of unified political movement. There are no chief whips to tell you whether you can or cannot use various axioms. At best, there are some identifiable schools whose adherents reliably take various axioms (such as the Russian school of constructive mathematics, associated with Markov's principle; or Intuitionism, associated with Brouwer's fan theorem), but not all constructivists belong to any of these.
Moreover, not many people who work primarily (or even exclusively!) in constructive mathematics have constructivist convictions. Most of the highest-profile contributors to constructive mathematics advocate some form of mathematical pluralism [1].
At this point, constructive mathematics usually just refers to mathematics done without the principle of excluded middle, and without other principles, such as the full axiom of choice, that would imply it. Constructivists themselves might decide to do constructive mathematics, usually for some kind of philosophical reason [2].
Accordingly, the fact that constructivists are forced to reject the Axiom of Choice in no way implies that they'd all be in favor of its negation. Certainly, constructivists universally reject e.g. excluded middle, but that does not mean they are in favor of negating it! (See also the Denial section of Bauer's Five Stages essay.)
II. There's more than meets the eye about "Choice implies Excluded Middle", though.
Consider the following principle: "if $\forall x \in A. \exists y \in B. \varphi(x,y)$ holds, then we have a function $f: A \rightarrow B$ so that $\forall x \in A. \varphi(x,f(x))$ holds". It looks exactly like the Axiom of Choice ruled out by Diaconescu's theorem (take $\varphi(x,y)$ to denote $y\in x$). Nonetheless, the principle is validated by the Brouwer-Heyting-Kolmogorov interpretation, and is in fact a fully provable theorem of Martin-Löf's Constructive Type Theory!
How do we explain this? How can the status of this principle be so so different in constructive type theory and constructive set theories?! Well, Diaconescu's proof uses multiple principles about sets and set-formation, not just the Axiom of Choice in isolation. Accordingly, the interaction of all the principles used in the proof lead to Excluded Middle, not any one of them. We can put the blame on Choice and reject it, or we can choose to weaken some other principle to prevent the proof from going through. E.g. a more thorough analysis might identify set theory's ability to form unrestricted quotients as the culprit, or in some cases even instances of separation). The former leads to the observation that "extensional Choice" or "setoid Choice" does imply Excluded Middle, even in type theory. The introduction of propositional truncations (which might itself be a subject of some controversy in some schools) and Homotopy Type Theory allows ever more stringent analyses about what sorts of choice principles should be admissible -- and indeed endless debates about which of these principles even deserve the name Axiom of Choice. The Coq Choice facts page provides a good, referenced summary of Choice principles in type theory.
At this point one should mention the fact that some forms of Choice tend to have quite tame consequences over constructive mathematics, even when they have wild consequences over a corresponding classical system. Adding the Axiom of Choice in the form $(\forall x \in \mathbb{N}. \exists y \in \mathbb{N}. \varphi(x,y)) \rightarrow \exists f: \mathbb{N} \rightarrow \mathbb{N}. \forall x \in \mathbb{N}. \varphi(x,f(x))$ to higher-order Peano Arithmetic yields a far more powerful system. Adding it to higher-order Heyting arithmetic has no arithmetic consequences at all.
III. So, how often do constructivists take positive axioms that altogether clash with Choice? In my experience, not that often.
First of all, the Brouwer-Heyting-Kolmogorov interpretation fully justifies Choice: if you practice constructivism because you find the BHK interpretation compelling in some sense, it makes no sense to take axioms that contradict it.
Second of all, a constructivist usually sacrifices Excluded Middle not on a whim, but to achieve some higher constructive goals. Goals such as the existence property, that from a proof of $\exists x. \varphi(x)$ you can without creative work extract some kind of object $t$ that actually satisfies $\varphi(t)$ [3]. Similarly, the disjunction property, which states that from a proof of $A \vee B$ you can without creative work extract either a proof of $A$ or a proof of $B$. These both fail in classical systems.
When the constructivist sacrifices Excluded Middle to obtain a constructive system obeying such desirable properties, it wouldn't really make sense to then adopt a new principle which breaks these properties. This rules out Determinacy, which asserts the existence of winning strategies for various games, but does not provide any methods for finding these strategies (hence breaking the existence property), or even the identity of the winner (hence breaking the disjunction property).
Even universalizing principles, which state that the only examples of some phenomenon are the nice, constructible ones, may in fact seem undesirable from this perspective! Consider the functor $\mathrm{Hom}(\mathbb{N}, -): \mathrm{FinSet} \rightarrow \mathrm{Set}$ and the inclusion functor $\iota: \mathrm{FinSet} \rightarrow \mathrm{Set}$. I once proposed (a more general form of) the following axiom, convenient for category theory: $\mathrm{Nat}(\mathrm{Hom}(\mathbb{N}, -), \iota) \cong \mathbb{N}$. This would constitute a straightforward generalization of the Yoneda lemma, which gives that for a finite set $F$, the natural transformations $\mathrm{Hom}(F, -)$ to the inclusion functor $\iota$ correspond to elements of $F$. It's a positive principle, and not compatible with full Choice since it implies the non-existence of nonprincipal ultrafilters. Moreover, it's easy to see that the only natural transformations from $\mathrm{Hom}(\mathbb{N}, -)$ to $\iota$ that you can actually construct are in fact the evaluation maps at some natural number. And yet this principle is still non-constructive: if you hand me a natural transformation from $\mathrm{Hom}(\mathbb{N}-)$ to $\iota$, I won't be able to constructively recognize which natural number you used to construct it!
The late Troelstra's Uniformity Principle also has a nice topological/constructive universalizing motivation, and breaks LEM (and Choice) in various satisfying ways when added to constructive set theory. Yet it also fails to retain constructive character, similarly to my Yoneda-type axiom above.
It's also worth mentioning that positive anti-Choice principles tend to give you some Choice -- even classically, where Determinacy implies Countable Choice, although it contradicts full Choice. In constructive set theories, you would not want to admit principles which constructively contradict full Choice, but give you some Choice: a little Choice goes a long way toward Excluded Middle.
IV. If you give up on retaining the constructive character of your system, you can add several principles to a constructive set theory (or a topos) that contradict Excluded Middle. The Kock-Lawvere axiom in smooth topoi is a famous example: it contradicts the theorem of classical algebra stating that fields lack zero-divisors. This is the domain of pluralism, more so than constructivism (although I wouldn't rule out a constructive interpretation of smooth topoi one day).
But even in Boolean topoi, failures of Choice are useful: see about $G$-$\mathrm{Set}$ here. Alas, I personally don't know any "mathematically natural" Boolean topoi which would obey some analogue of Determinacy, or other positive anti-Choice principles (except insofar as the Boolean-valued models of set theory itself are "mathematically natural").
Finally, in type theory, you can sometimes get around the phenomenon discussed above, that postulates tend to break existence properties, by taking negated or double-negated forms of your axioms. The Coquand et al. paper on the subject is very nice. However, by doing this, one gets back precisely to the realm of the "too negative" axioms!
[1] I will not talk about the views of pluralists here, and what axioms they take or not take. Partly because I'm not one of them, and partly because some pluralists seemingly have a whole lot of time and opportunity to talk about it, so information about their views is easy to come by.
[2] But this is not a necessity either: e.g. I'm philosophically a more extreme constructivist than most, but all my work uses LEM, because I prefer to focus on academic opportunities over philosophical purity. I wish things would be different, but fat chance of that.
[3] In the study of proof theory and pure logic, one calls this the existence property. There is an unfortunate terminological clash, where in constructive set theories, the "existence property" refers to a subtly different principle (one that, funnily enough, tends to fail for these systems). In set theories, the so-called "numerical existence property" is much closer to what we simply call the existence property in logic. Canonicity in type theory is again closely related.