How to get unfoldings inside a GHC plugin

[Jonathan Arnoult]

Hello,

I am working on Liquid Haskell, and I'd like to use the unfoldings of
definitions located in interface files to unfold them in proofs.

Liquid Haskell is a GHC plugin that runs in the type checking phase at the
moment, and for analysis purposes it also compiles the module down to Core.
I have found that unfolding information is available in the mi_decls field
of ModIface, and in the field realUnfoldingInfo of IdInfo. However, my
first attempts to grab for these fields yield no unfoldings either because
they have been erased (mi_decls is filled with an error call in
loadInterface) or they were not constructed to begin with
(realUnfoldingInfo is set to NoUnfolding).

In my setting, I have the name of a function, and I would need to retrieve
the unfoldings (if they exist) from some environment. Does this environment
exist already that is reachable to a plugin? Or do I need to construct it
somehow?

I also found that GHC makes a distinction between interface files in
external packages and the home package, while I really would like to get
the unfolding from wherever they happen to be.

Any advice is appreciated.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240806/6a19958f/attachment.html>