Type inference of pair (product) types
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.