Skip to content

Less coercion optimization for non-newtype axioms

Adam Gundry requested to merge wip/amg/tweak-co-opt into master

Recently (partly prompted by #22323) I've been thinking again about #8095. It is clear that (a) the coercion optimizer is a terrible pessimization in some cases involving type families, but (b) it is sometimes necessary in other cases to avoid coercion size explosion during simplification. Previously our efforts have focused on changing the representation of coercions to be more compact (either by zapping or directed coercions), but this tends to impede coercion optimization. We've also wondered about deploying the coercion optimizer more selectively (#19909) but not thought so much about changing its behaviour.

This one-line (!) patch takes a different tack: avoid the worst cases in the coercion optimizer, by skipping the problematic rules. In particular, these are the "Push transitivity inside axioms" rules where the axiom comes from a type family. So we continue trying to optimize newtype axioms, which is relatively likely to be useful, but don't bother considering type family axioms.

Local testing suggests this gives pretty good results, but let's see what CI says. Of course this isn't as massive an improvement as using directed coercions in cases where they work perfectly, but it is simple and unlikely to regress performance except in very unlikely cases where type family axiom cancellation was previously crucial.

If this works, we should think about Note [Why call checkAxInstCo during optimisation]. I think (but have not carefully verified) that with this change the calls to checkAxInstCo are redundant, because they matter only for closed type family axioms, not newtype axioms. If so, we can possibly skip the calls, and move checkAxInstCo to GHC.Core.Lint where it belongs. (EDIT: I've now moved checkAxInstCo back to GHC.Core.Lint.)

Edited by Adam Gundry

Merge request reports