Hi all, We have a function in Liquidhaskell's code base for converting refinement expressions into GHC's core expressions using the GHC API. Its implementation is based on tcRnExpr https://gitlab.haskell.org/ghc/ghc/-/blob/ghc-8.10.6-release/compiler/typech...except we keep the typechecked expression and desugar it before returning. However, our function fails to set the idScope information properly when LiquidHaskell is invoked as a plugin (installed as a typeCheckResultAction). This repo https://github.com/yiyunliu/ghc-elaboration-testcontains a minimal example that demonstrates the issue. In the CoreExpr returned by elabRnExpr https://github.com/yiyunliu/ghc-elaboration-test/blob/cb7397884b7949e6b7fb66..., every symbol from the current module that's being compiled is labeled as local. The README.md file shows how the exported symbol testPlus is marked as local in QQQ.hs, the module where it's defined. Is there a function we should call to set the idScope information properly? Thanks, -Yiyun