Bad coercion optimisation for (ax ty; sym (ax ty))

Consider this newtype

newtype N a = MkN a
-- ax :: forall a. N a ~R a

and this coercion

     (ax a ; sym (ax a))

Well, that's just Refl, right? Alas not in GHC. We have this very clever rule

-- Push transitivity inside axioms
opt_trans_rule is co1 co2

  -- See Note [Push transitivity inside axioms] and
  -- Note [Push transitivity inside newtype axioms only]
  -- TrPushSymAxR
  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
  , isNewTyCon (coAxiomTyCon con)
  , True <- sym
  , Just cos2 <- matchAxiom sym con ind co2
  , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
  = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst

You can see typeset rules in the paper Evidence normalisation in System FC. The rule is AxSuckR in Fig 8.

The details are a bit gnarly but we get this:

    (ax a ; sym (ax a))  -->   ax (sym (ax a))

Here:

  ax a :: N a ~ a
  sym (ax a) :: a ~ N a
  ax (sym (ax a)) :: N a ~ N a

So yes, the result is Refl, but is disguised in a way that the coercion optimiser can't optimise -- a sad lack of confluence in the coercion-optimisation rules.

I don't know how to fix the lack of confluence, but it turns that simply testing for (ax ty; sym (ax ty)), before doing the AxSuckR tests, is enough. That is, simply re-order the equations in opt_trans_rule.

@rae @adamgundry @sheaf will be interested