Do more coercion optimisation on the fly
When studying #15019 (closed), I looked at CoreOpt.pushCoValArg
. I saw lots of attempted decompositions in pushCoValArg
,
which were trying to do decomposeFunCo
on
C @g1 ; sym (C @g2)
where
axiom C a = a -> a
But the smart mkNthCo
can't make progress on this, so we get
Nth:2 (C @g1 ; sym (C @g2))
and these things stack up if there is a chain of applications in Simplify.simplCast
.
The coercion optimiser will optimise this coercion to
(g1 ; sym g2) -> (g1 ; sym g2)
and now the smart mkNthCo
in decomposeFunCo
will succeed.
Possible idea: make this optimization part of mkTransCo
so that it
happens on the fly.
(Annoyingly, I can't remember which of the three test cases mentioned in #15109 (closed) displayed this behaviour.)