Unification changes

Remove the horrible fudge which allowed some function arguments to be
unified in order to deal with type classes. Instead, record which
function variables are expected to be injective, and postpone any
attempt to unify function applications until later.

Still not completely right (there is another horrible fudge to remove),
and this will mean some programs which previously type checked will not
now. More to come...
Another unification fix

Removes 'matching' hack, which would sometimes cause function
applications in patterns to be unified when they shouldn't have been.
Fixes #898.
Add new regression test
Fix parameter propagation