Fixed a type inference bug; functions now immediately gain functional type.

In higher order matching during type inference, some matches are deferred
until later, to increase the probability of success. However, for term
combinations of a function being applied to an argument, if the type
of the function is a higher order pattern, e.g., ``:'a 'P``, then
unifying ``:'a 'P`` with ``:<arg type> -> 'u`` for a fresh uvar 'u
may not ensure that the resulting type of the function is an -> type!

The fix is to first ensure that the higher order type variable 'P
is unified with \'b. 'b 'P1 -> 'b 'P2 for fresh uvars 'P1 and 'P2,
so that even if the higher order match is not completely resolved
immediately, at least we do have that 'a 'P = 'a 'P1 -> 'a 'P2 is
in fact a functional type.