Re: How to set idScope properly when converting LhsExpr GhcPs to CoreExpr?

[Yiyun Liu]

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/49b33d42bdefb597ac8fab49bb4cea4969c929b3/src/Test/Plugin.hs#L101) 
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
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
contains a minimal
example that demonstrates the issue. In the CoreExpr returned by
elabRnExpr
,
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

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

Re: How to set idScope properly when converting LhsExpr GhcPs to CoreExpr?

[Richard Eisenberg]

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
> 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
> contains a minimal
> example that demonstrates the issue. In the CoreExpr returned by
> elabRnExpr
> ,
> 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

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

How to set idScope properly when converting LhsExpr GhcPs to CoreExpr?

[Yiyun Liu]

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
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
contains a minimal
example that demonstrates the issue. In the CoreExpr returned by
elabRnExpr
,
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