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