Skip to content

Draft: Turn coercion optimization into an optimization pass (#19909)

Adam Gundry requested to merge wip/amg/T19909 into master

This distinguishes between "simple" and "non-simple" coercion optimizations, with "simple" coercion optimizations applied by the simple optimizer (immediately after desugaring) and during simplification, while "non-simple" coercion optimizations are applied during a separate core-to-core pass. At the moment the only coercion optimizations not considered "simple" are the opt_trans_rule cases for pushing transitivity inside axioms.

There are now explicit -fopt-coercion-simple and -fopt-coercion-full options to control these passes. The existing -fno-opt-coercion disables them both, and a new -fopt-coercion enables them both. By default -fopt-coercion-simple is enabled for all optimization levels, while -fopt-coercion-full is enabled only for -O1 and higher.

Open questions:

  • When should we run the non-simple optimization pass? At the moment it is run only once, at the beginning of the pipeline.

  • Should any other coercion optimizations be "non-simple"?

  • Should we perform non-simple optimization of coercions inside types? I've so far refrained from doing so, because I have a hunch that it will be a waste of time, but I haven't got data to back this up.

Edited by Andreas Klebinger

Merge request reports