Turn the coercion optimizer into a proper simplifier pass

As I've noted previously (#12765 (comment 338362)) the performance of the coercion optimizer can be terrible in some cases. And yet we call it (frequently) from the simple optimizer.

In particular I think this results from the opt_trans_rule cases to push transitivity inside axioms, which if axiom :: F tys ~ ty will try very hard to find patterns like axiom gs1 ; g ; sym (axiom gs2) and collapse them to some F g'. But this doesn't happen very often, and I think matchAxiom can do quite a lot of unsuccessful work.

Discussing this on a call, @simonpj suggested that instead we should make the full coercion optimizer into a normal simplifier pass, and instead have a much smaller "simple coercion optimizer" that might do little more than substCo and a reflexivity check. Then we could experiment with when to run the full coercion optimizer pass in the pipeline (e.g. perhaps it makes sense to run once soon after desugaring and once right at the end).