Verify that names are bound at the right type

[paulstansifer]

If one writes a macro that promises to bind a to Int for a particular argument term, soundness requires that this actually takes place.

(This corresponds to the difference between FreshML and Pure FreshML, but the Pure FreshML (and Romeo) solution to this problem is an unacceptable burden to the programmer.)

We must make a conservative approximation; there's no practical way to allow all cases where the programmer could prove that they would do so. In particular, I think we want to take advantage of the fact that macros are usually built by calling other macros, not by calling functions.

I think that the Rust borrow checker is the rough kind of thing this needs (however, this should be a simpler problem).