Account for skolem escape in mightEqualLater

This MR:

1. Refactors checkTyEqRhs to allow it be called in pure contexts, which means it skips doing any on-the-fly promotion.
2. Calls checkTyEqRhs in mightEqualLater to check whether it a MetaTv can unify with a RHS or whether that would cause e.g. skolem escape errors or concreteness errors.