This is a model-theoretic questions. Let $M$ be a $R$-module. Our language will be the standard language of modules, i.e. the language of abelian groups together with an unary function symbol for every $r\in R$. We also may require that $M$ has quantifier elimination.

Is every $pp$-definable subgroup of $M^n$ which is definable by a quantifier-free formula already definable by a conjunction of equations?

A motivation for this question is that then quantifier elimination already implies weak elimination of imaginaries: By stability it is enough to show that every global type has a canonical base. Note that every global $n$-types is a generic type of coset of a type-pp-definable subgroups of $M^n$. Now each of the pp-definable subgroup we Then if our question is true, then each $pp$-definable subgroup will be definable by a conjunction of equations. Hence there exits some $R$-matrix $A$ such that this $pp$-subgroup will be the kernel of $A$. We have that $Ax$ is the canonical parameter of the coset $x+A$. And therefore we have found a canonical base.

If $M$ is an abelian group (or more general $R$ a principal ideal domain) then this questions boils down to the following:

Does quantifier elimination implies that for every $n$ there exists some $m$ such that $nM=M[m]$ ($x$ can be divided by $n$ if and only if $m.x=0$)?

The reason for this that by the elementary divisor theorem every $pp$-formula will be equivalent to a conjunction of formulas $\exists y (n.y=\sum_i z_i.x_i$).