Is there a decision procedure for *monadic* intuitionist first-order logic?

In Ch. 19 of the 4th edition of Methods of Logic, Quine gives a decision procedure for classical monadic first order logic (technically it's a decision procedure for what he calls "Boolean statement schemata", which are identical to first order sentences containing no universal quantifiers or relational predicates, and with every existential quantifier in prenex position modulo negations. Every monadic first order sentence can be translated into such a form.)

The procedure requires translating the "Boolean term schema" (e.g. $P \to Q$ is the term schema of $\exists x (Px \to Qx)$) to conjunctive normal form. Because the CNF form of a sentence in classical logic is not (necessarily) equivalent to the CNF form of the same sentence in intuitionist logic due to the lack of an equivalency rule for double-negation in intuitionist logic, I'm not sure if the procedure can be adapted. I don't think it can be straightforwardly adapted at least.

I'm doing some dependently typed programming and knowledge of a decision procedure for monadic intuitionist/constructivist logic would be immensely helpful if it exists. Does it? If so, could someone point me to a reference?

Tl;dr -- the answer is "no", and you can find a proof in Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Predicate Letter, by Ryabakov and Shkatov, available here. Precisely:

There is no procedure to decide the truth of positive intuitionistic formulas using only one monadic predicate and $2$ variables

Notice this is consistent with Pilcrow's answer, since we can faithfully translate intuitionistic single-variable monadic formulas into the (decidable) modal logic $\mathsf{MIPC}$.

Now, to explain where my initial (and incorrect) comment came from:

The usual proof of the corresponding fact for classical logic is a "filtration argument". We first prove

Let $\varphi$ be a formula with (monadic) predicates $P_1, \ldots, P_n$ and variables $x_1, \ldots, x_m$.

If $\varphi$ is (classically) satisfiable, it is (classically) satisfiable in a model of size $\leq m 2^n$

Then all that's left is to say that, by the completeness theorem, $\varphi$ is provable if and only if $\lnot \varphi$ is not satisfiable. But by the above theorem it suffices to check if any models of size $\leq m 2^n$ satisfy $\lnot \varphi$, and this is a finite check (albeit a large one).

Now, the hiccup comes when we pass to the intuitionistic setting. Now our models are more involved. In particular, while classical models can all be taken to have truth values in $\{0,1\}$, intuitionistic models need to take values in arbitrary heyting algebras. The "$2$" in $2^n$ comes from enumerating every possible assignment of truth values to the $P_1, \ldots P_n$, but now there might be more than two possible truth values. The natural idea is to try and prove a theorem of the form

Let $\varphi$ be a formula with (monadic) predicates $P_1, \ldots, P_n$ and variables $x_1, \ldots, x_m$.

If $\varphi$ is intuitionistically satisfiable, it is intuitionistically satisfiable in a model of size $\leq m 2^n$ taking truth values in a heyting algebra of size $\leq \ldots$ something.

Then we would have a larger check to go through, but it would still be finite. When writing my comment, I was remembering a result that intuitionistic propositional logic is decidable because we can bound the size of the heyting algebras of interest (albeit double exponentially), see MJD's answer here for example. I thought we could use this to also bound the size of a heyting algebra involved in the semantics of IPC, but it looks like we can't.

Again, you can find a proof of the undecidability in the linked paper by Ryabakov and Shkatov. For an older, and less sharp account (it puts no bound on the necessary number of variables, but the corresponding proof is easier), you can see Chapter $14$ of Semantical Investigations of Heyting's Intuitionistic Logic by Gabbay.

I hope this helps ^_^

Monadic fragments of first-order logics (in the sense of one-variable fragments, not in the sense of fragments with only unary predicates) can equivalently be seen as modal logics where the box and diamond operators correspond to universal and existential quantifiers. In the case of classical first-order logic, the corresponding modal logic is the classical modal logic S5. This was proved by M. Wajsberg in 1933. The logic S5 has a Kripke semantics which simply consists of sets equipped with an equivalence relation. It is axiomatized by finitely many axioms and rules, and it has the finite model property, meaning that each non-theorem of S5 can be refuted in a finite Kripke frame for S5. This yields a decision procedure: each theorem has a finite proof, and each non-theorem has a finite refutation.

Analogous facts hold for the monadic fragment of intuitionistic first-order logic, which was identified by R.A. Bull as the intuitionistic modal logic MIPC:

R. A. Bull. MIPC as the formalisation of an intuitionist concept of modality. The Journal of Symbolic Logic, Vol. 31, No. 4, pp. 609–616, 1966

The signature of MIPC extends the signature of intuitionistic propositional logic by a box and a diamond operator. The logic is again axiomatized by a finite number of axioms and rules. Its Kripke semantics consists of partially ordered sets with a binary equivalence relation satisfying certain conditions. The logic MIPC has the finite model property with respect to this semantics, therefore it is decidable.

If you want a more constructive answer (which perhaps someone else with more insight into MIPC will be able to provide), a good starting point would be to look for calculi for the logic MIPC.