Translating typed functional language to untyped lambda calculus
There's an old way of doing what you're asking for, coming from domain theory. Let $D$ be the collection of all values of the untyped $\lambda$-calculus. We can undestand $D$ to be some sort of a domain, or the set of closed normal terms, it does not really matter. We define a type to be a retraction $r : D \to D$, i.e., a continuous map (or a closed term if you want definable types) such that $r \circ r = r$. Such an $r$ represents the collection of its fixed points $D_r = \{x \in D \mid r(x) = x\}$. The map $r$ itself is a coercion from $D$ to $D_r$. Because it is a retraction, it does not do anything to elements of $D_r$.

Now, given any map $f : D \to D$ say that it maps $D_r$ to $D_q$ when $f = q \circ f \circ r$. This equation says that:


$f$ is already determined by its restriction $f{\restriction}_{D_r}$ to $D_r$ (because $f = f{\restriction}_{D_r} \circ r$),
the image of $f$ is contained in $D_q$ (because $f = q \circ f$).


Putting these two together, we see that $f$ can be thought of as going from $D_r$ to $D_q$ (it is important that $f$ does not carry any additional information about how to map elements outside $D_r$, or else we could  have several different functions that all act the same way on $D_r$).

Actually, any map $g : D \to D$ can be coerced to a map from $D_r$ to $D_q$ by the retraction $g \mapsto q \circ g \circ r$.

Let us see how this relates to your question. You would like to have a way of saying that a map $f$ maps integers to integers (I presume you mean natural numbers since you speak of Church numerals). So what we need is a map $r$ such that $r (r x) = x$ if, and only if, $x$ represents an integer. Once we have such a map we can express the fact that $f$ maps integers to integers with the equation $f = r \circ f \circ r$.

So it remains to write down a map $r$ in the untyped $\lambda$-calculus whose fixed points are Church numerals (and also some diverging terms which denote bottom). I think this might work:
$$r(x) = \mathtt{rec}\;\mathtt{Z}\;(\lambda n\,y \,. \mathtt{S}\,y)\;x,$$
where $\mathtt{rec}$ is a simple recursor over natural numbers, $\mathtt{Z}$ is zero and $\mathtt{S}$ is successor. Intuitively, speaking, if $x$ behaves like a natural number, then $r(x)$ will "rebuild" it into standard form $\mathtt{S}(\mathtt{S}(\cdots \mathtt{Z}))$.

We need to be a bit careful about how $\mathtt{rec}$ is implemented. It has to satisfy
$$\mathtt{rec}\;x\;f\;\mathtt{Z} = x$$
and
$$\mathtt{rec}\;x\;f\;(\mathtt{S}\,n) = f\;n\;(\mathtt{rec}\;x\;f\;n),$$
and it should "crash" when we feed it something that does not behave like a numeral.