in type inference, always bind the return type of
functions, but not the arguments.
add some type annotations in rewrite systems