Hi Richard, Thanks for the reply. The problem has something to do with how LH currently handles symbols. Internally, LH uses the idScope field to identify whether a symbol is exported and handles them differently (e.g. erase the unique id only when the symbol is exported). Ideally, we want LH to be aware of the case where an exported Id is labeled as local but it's probably easier to let GHC set the idScope as if we were accessing from a different module. We tried using tidyExpr to turn the LocalIds into GlobalIds (https://github.com/jprider63/ghc-elaboration-test/blob/49b33d42bdefb597ac8fa...) but the output expression still shows lid for QQQ. Are there any flags we need to set to "trick" GHC into setting those ids as globals? Thanks, -Yiyun On 8/31/21 3:25 PM, Richard Eisenberg wrote:

I took a look at this today. I found

...

Note [GlobalId/LocalId] ~~~~~~~~~~~~~~~~~~~~~~~ A GlobalId is * always a constant (top-level) * imported, or data constructor, or primop, or record selector * has a Unique that is globally unique across the whole GHC invocation (a single invocation may compile multiple modules) * never treated as a candidate by the free-variable finder; it's a constant!

A LocalId is * bound within an expression (lambda, case, local let(rec)) * or defined at top level in the module being compiled * always treated as a candidate by the free-variable finder

After CoreTidy, top-level LocalIds are turned into GlobalIds This suggests that the output you're seeing -- with "lid" in QQQ and "gid" in PPP -- is correct. What has drawn your attention to this problem? Is there something else that's misbehaving?

Thanks, Richard

...

On Aug 25, 2021, at 4:16 PM, Yiyun Liu wrote:

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

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs