Add unfoldings for local bindings outside the simplifier
Motivation
I am working on a Core plugin that is interested in unfoldings. The natural place for such a plugin to run is at the start of the pipeline. However, if we look around at that point, we see:
- Bindings from other modules have unfoldings.
- Some bindings from other packages have unfoldings (as we'd expect, depending on
INLINEABLE
etc.) - Local bindings do not have unfoldings.
After some poking around, I think these are actually added by the simplifier (see completeBinding
). I'm not really sure why it happens there, but it would be nice to be able to ensure that the unfoldings were present without having to run the whole simplifier, which does many other things too.
Proposal
Move the creation of local unfoldings somewhere else, maybe desugaring?