# Constructive proof of existence of maximal ideal

Let $R$ be a unital commutative ring. We know that the existence of a maximal ideal of any such $R$ is equivalent to the axiom of choice.

My question is, for what kind of $R$ is there a constructive proof that$R$ has a maximal ideal?

This problem is very hard, even for rings that we can list the elements effectively. For example, in $\mathbb Q[X]$, such a proof as you require will give a algorithm capable of calculating the factorization of every rational polynomial.
It is possible to give a different answer using results from Reverse Mathematics. In Reverse Mathematics there is a classification of theorems expressed in a countable language in proof systems of different strengths. The main ones are: $$RCA_{0} < WKL_{0} < ACA_{0}$$.
In $$RCA_{0}$$ it is possible to provide (essentially constructive) definitions (for example of Countable Commutative Rings and Ideals), and of elementary lemmas, but $$RCA_{0}$$ is usually not powerful enough to prove corresponding major theorems.
Theorem III.5.4. $$ACA_{0}$$ proves that every countable commutative ring has a maximal ideal.