Add syntactic equality relation

In several places, it would be useful to have a syntactic equality relation, ~S#.

• Under this relation, two types are equal if they respond equal to tcEqType, up to zonking. (This means: no rewriting, but we can zonk and look through type synonyms.)
• The evidence for t1 ~S# t2 is always Refl.

With such an equality relation, we could:

• Get rid of IsRefl#. Currently, the representation polymorphism checks emit a nominal equality ki ~# concrete_tv, and when we don't support rewriting (because of PHASE 1 of FixedRuntimeRep) we additionally emit IsRefl# ki concrete_tv. Instead, we should syntactically unify ki with concrete_tv in PHASE 1.

• Enforce a specific runtime rep. Suppose we want to enforce that a type ty :: TYPE rr has a specific runtime representation specific_rr, without any coercions needed, (e.g. LiftedRep if we want to enforce liftedness). Then we can syntactically unify rr with specific_rr. Example of when this is useful: \x -> (x, True). At the lambda, x comes into scope with type x :: alpha :: TYPE rr. Later we find that it must be lifted because it's an argument to the tuple.

Implementation

A useful property of (~S#) is that it can be solved or refuted without ever generating any constraints. So this should NOT be a new constructor of EqRel, because we have no need for a syntactic equality predicate. All we need is a counterpart to uType that works at the syntactic level, doing unification as it goes, and never deferring to the main constraint solver.