updated unification and substitution
Signature no longer maps symbols to types, but
strings to (typed) symbols