Add unfoldings for local bindings outside the simplifier
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
- 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.
Move the creation of local unfoldings somewhere else, maybe desugaring?