Either justify the roundabout `Ren` approach or replace it with something simpler

[nfrisby]

One consequence of this being a project I used to learn about the type checker and OutsideIn(X) is that there's plenty of design decisions I'm not sure about.

In particular, I don't have a rock solid motivation for using the Ren constraints instead of maintaining a separate and private substitution. I have a jumble of reasons why I think it might be better this way (not re-implementing unification, sharing knowledge with other plugins, avoiding loops where the plugin just keeps generating the same idempotent equality), but I really need to flesh them out and write up a good motivation for this approach.