What kind of "infinite sets" do constructivists use?
The question is a little vague because the term "constructivism" is not defined properly, and indeed there are several varieties of this. In constructivism according to Errett, the answer to your query is probably simpler than you think: you most likely won't find an occurrence of anything like "$\mathcal P(M)$" here. The only "completed" infinity that's allowed is $\mathbb N$, and real analysis is developed mainly using $\mathbb N$ (you will agree that you don't need more than that to define a sequence). Of course real numbers occur here but not so much the collection thereof.
So the issue of comparing different infinities does not really arise, since none are considered, though there is a constructive version of Cantor's diagonalisation argument.
There are many kinds of constructivism.
One kind is the non-classical kind, but it seems to me that if a collection is actually well-defined then every possible way to express that it is finite would have a well-defined truth-value as well, philosophically speaking. It may be that different definitions of "finite" are not equivalent, but all the statements involved ought to have classical truth-values if they have well-defined meaning at all.
This does not mean that non-classical logic is pointless. Just for example, intuitionistic logic is tied to programs and modal logic via the BHK interpretation and Kripke frames. But one must not confuse truth with knowledge or constructibility. For example, we know that the halting problem cannot be solved. This is a boolean fact. Yes, there is a computer program that would generate a counter-example (program,input) pair to any given claimed halting oracle, but the mere notion of the halting problem itself requires the (classical) assumption that any program run on an input will either halt or not halt.
Also, from a logic perspective, any reasonable foundational system for logic itself must interpret classical PA (discrete ordered semi-ring axioms plus induction) for even basic syntactic concepts like provability to be meaningful. It is then philosophically justifiable to extend it to ACA, which is nothing more than adding conservative extension plus the full induction schema. It turns out that lots of real analysis can be done within ACA.
One could extend to predicative higher-order arithmetic, by having base sorts $nat$ and $bool$ and a sort $S \to T$ for all functions from $S$ to $T$, for any sorts $S,T$. (Note that a set in ACA can be thought of as a member of $nat \to bool$.) One is permitted to construct an object only if its defining formula quantifies only over $nat$, which is conservative over PA. One also adds the full induction schema (which can be justified meta-logically), which makes it stronger than PA. It suffices for practically all concrete mathematics (though of course it is incomplete).
Within ACA, it is easy to define a set $S$ to be infinite (7) iff $∀x{∈}S\ ∃y{∈}S\ ( \ y>x \ )$. Note that all your six definitions except for Tarski-infinite can be expressed in ACA via appropriate coding. To express Tarski-infinite you need to have at least (predicative) higher-order arithmetic. Side remark: Your definition (4) should say "non-empty chain".
It turns out that when restricted to the language of ACA, all 5 expressible definitions are equivalent, because every set in ACA is a subset of $nat$ and we have well-ordering of $nat$, which eliminates the need for any choice. $ \def\pow{\mathcal{P}} $
We can sort of express Tarski-infinite in ACA in terms of existence of a sequence of sets instead of a set of sets, namely that for each $S⊆nat$ we say that $S$ is Tarski-infinite iff $∃f{∈}nat{→}\pow(S)$ $∀k{∈}nat$ $( \ f(k) \subsetneq f(k+1) \ )$. Note that members of $nat{→}\pow(S) ≅ nat{→}(nat{→}bool)$ can be easily encoded in ACA via currying. This version of Tarski-infinite is equivalent to the others as well.
It is when you want to talk about sets beyond second-order that things get interesting. From the viewpoint of ZFC, higher-order arithmetic has a model with full powersets, and uncountable sets can be very strange. We do not have a well-ordering of the set of subsets of naturals, unless we have some kind of choice axiom.
Choice can be justified easily if the intended model is countable, because then it could be interpreted as using the well-ordering of the intended model. This is why choice is often considered acceptable in constructive type theories (but not intuitionistic type theories). But if the intended model is not countable, such as with ZFC, then it is more difficult to justify choice, unless one literally believes in the platonic existence of full powersets, in which case 'obviously' choice holds.
In general, it is true that many mathematical concepts split into multiple variants in constructive foundations. Well-ordering is another one, where the definition ( no strictly decreasing sequence ) is equivalent to ( every non-empty subset has a minimum ) in general only in the presence of a weak form of choice. But it should not be surprising that we do not need choice to prove equivalence for countable well-orderings.