Type inference of pair (product) types I am looking into Hindler-Milney type system and I am trying to add support for
the pair type. In Pierces book, he introduces special language constructs for creation of pairs and getting their elements.

What I am interested in is the following. What if I don't introduce new constructs, yet use special functions with this signatures: 

$$pair: \alpha \rightarrow \beta \rightarrow \alpha \times \beta $$ 

$$proj1: \alpha \times \beta \rightarrow \alpha$$ 

$$proj2: \alpha \times \beta \rightarrow \beta $$

If I use Wand's algorithm for type inference, after collecting all equations between type expressions and solving it a bit, I get the following equation
for $((pair\; 2\;) 4): \tau$:

$$\alpha \rightarrow \beta \rightarrow \alpha \times \beta = Int \rightarrow Int \rightarrow \tau$$

It seems to me that the unification algorithm should infer at the end that $\tau = Int \times Int$. Is this true? 

Do I really need a special construct for pairs? Is there something conceptually wrong with this? Probably their is, so it would be great if someone could point me out. 

Note that I would also prefer using special constructs as that way looks cleaner and easier to program with; this question is just for my complete understanding of the subject.
You can use things like pair, proj ... as constants only. That works
very well conceptually. Nevertheless, there are reasons why 
programming languages tend to use special syntactic forms for the like of
products:


Readability, e.g. ( M, N ) reads more natural than pair M N to
some.
For efficient reductions. It is possible to code the reductions for
pairs up in pure$\lambda$-calculus, but that's usually not as efficient.
Finally, you'd need a polymorphic typing system for this to work.


As an aside, the formalisation of logics in interactive proof assistants 
like Isabelle is based on a similar idea, called logical frameworks.