How do we uncurry functions when they are polymorphic? For example, is it possible to uncurry the following types? If so what is the uncurried type?
The other answers are good, I just wanted to make it explicit that currying for dependent types is $$ \textstyle \prod (x : A) . \prod (y : B(x)) . C(x, y) \ \cong \ \prod (p : \sum (x : A) . B(x)) . C(\pi_1(p), \pi_2(p)) $$ which is more suggestive in Agda-style notation: $$ (x : A) \to (y : B(x)) \to C(x,y) \ \cong\ (p : (x : A) \times B(x)) \to C(\pi_1(p), \pi_2(p)) $$ In your case, replace $\Pi$ and $\Sigma$ with $\forall$ and $\exists$.
The uncurrying process will lead to existential types. Since the adjoint of $(X\to)$ is $(X\times\vphantom{Y})$ and the adjoint of $(\forall X.)$ is $(\exists X.)$, it is appearently inevitable. Also, it will lead to types depending on terms (where simple types only depends on types themselves, and polymorphism allows terms to depend on types). So generally it is not doable in your restricted type system.
Let's write these in more suggestive notations. The usual currying/uncurrying converts between $X \to Y \to Z$ and $X \times Y \to Z$. But the former can be written in the product notation: $\prod_{x:X} \prod_{y:Y} Z$, where $\prod_{y:Y}Z$ means the product of many copies of $Z$, one for each element $y$ of $Y$, which is a function from $Y$ to $Z$. The latter can be written as $\prod_{p:X\times Y} Z$. And $A \times B$ can be rewritten as $\sum_{a:A}B$, which is the sum of many copies of $B$, one for each element $a$ of $A$.
This notation is easily generalized to polymorphic types (or even more generally, dependent types), simply by allowing the inner expression to depend on the variable: $\prod_{X : *} X \to A$ means the product of $X \to A$ for every type $X$. So we can make the more general currying/uncurrying process: $$\prod_{x:X}\prod_{y:Y_x} Z_{x, y} \Leftrightarrow \prod_{p:\sum_{x:X} Y_x} Z_{\pi_1(p), \pi_2(p)},$$ where $\pi_i(p)$ is the projection that selects the $i$-th element.
Back to the question itself. The first one is actually a function of three arguments. So just turning it into $\forall X. (X\times \mathtt{int}) \to X$ is just uncurrying the second and third argument. The uncurried form neccesarily involves dependent types: $\forall (p:\exists X. X\times \mathtt{int}). \pi_1(p)$. The rest can be done similarly.
I can only think of some uncurrying of 1 and 3.
Alternatively, if we can apply an isomorphism, (3) can be rewritten as $$ \forall X. int \rightarrow (X \times int) \rightarrow X $$ and then, by uncurrying $$ \forall X. (int \times X \times int) \rightarrow X $$
In my view, it is more interesting when we also have existential types in the calculus and the returned type does not involve $X$. E.g., we can perform a kind of uncurring on $$ \forall X. X \rightarrow (X \rightarrow int) \rightarrow int $$ and get $$ (\exists X. X \times (X \rightarrow int)) \rightarrow int $$ which is isomorphic to $$ int \rightarrow int $$
