Separate renaming and typechecking into bona fide separate phases?
This is sort of a question feature request hybrid. Why are they done together? I see a bunch of booleans asking whether to keep renamed syntax. That seems lousy: it would be much nicer to just rename, and then put the info in the type-checker so the caller can decide whether to keep. Perhaps the issue is renaming is demand-driven and done concurrently? I cannot really imagine how this works with the current algorithm, but it's the only justification I could think of.