Finish implementing a type inferencer.

Implement a type inferencer for expressions based on algorithm W and
using the unifier in HOL/examples/unification/triangular/first-order.
So far it is untested and unverified.