Import issues + reflection

[nikivazou]

Consider file A.hs that uses reflection and defines a data type Term with a measure and an invariant.

File B.hs defines a data type that is using Term: data Program l = Term l.

File C.hs is only importing B:

module T1326C where

import T1326B 

{-@ measure terminates :: Program l -> Bool @-}

But then it throws an error that the measure of A is not defined. If we also import A

module T1326C where

import T1326A 
import T1326B 

{-@ measure terminates :: Program l -> Bool @-}

there is an error that the selectors of A are not defined. To make C go through you also need to add the reflect flag

{-@ LIQUID "--reflect" @-}
module T1326C where

import T1326A 
import T1326B 

{-@ measure terminates :: Program l -> Bool @-}

No errors now!

[ranjitjhala]

Yes this is a “known” issue in that I think Ryan Scott also hit it at some point. Thanks for bumping it; should be fixed maybe when we properly solve the import issue using ghc annotations.

For now this issue can serve to document the workaround!

On Thu, May 31, 2018 at 7:02 AM Niki Vazou notifications@github.com wrote:

Consider file A.hs https://github.com/ucsd-progsys/liquidhaskell/blob/ec68ad1e80eeacfe2f1fc09d976c44162994668b/tests/todo/T1326A.hs that uses reflection and defines a data type Term with a measure and an invariant.

File B.hs https://github.com/ucsd-progsys/liquidhaskell/blob/cdc6349668292448e7a1ff6f0342aa5cee267a08/tests/todo/T1326B.hs defines a data type that is using Term: data Program l = Term l.

File C.hs https://github.com/ucsd-progsys/liquidhaskell/blob/d979e3a1ae6bfe451f41b4bb88f70d338baa54d5/tests/todo/T1326C.hs is only importing B:

module T1326C where

import T1326B

{-@ measure terminates :: Program l -> Bool @-}

But then it throws an error that the measure of A is not defined. If we also import A

module T1326C where

import T1326A import T1326B

{-@ measure terminates :: Program l -> Bool @-}

there is an error that the selectors of A are not defined. To make C go through you also need to add the reflect flag

{-@ LIQUID "--reflect" @-} module T1326C where

import T1326A import T1326B

{-@ measure terminates :: Program l -> Bool @-}

No errors now!

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1326, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOOBpH9SWpJThjv49Erx1jIkPRuq8ks5t3_URgaJpZM4UVFK6 .

[nikivazou]

@ranjitjhala, what do you mean "solve the import issue using ghc annotations"? Is this plan documented somewhere or is anyone working on it?

[ranjitjhala]

I need to page this back in (I think I made an issue of it, IIRC @gridaphobe and maybe @jprider63 commented on it...)

Long story short: the key idea is to use GHC annotations instead of the .bspec files to save all spec related information, but I really should write this down somewhere before proceeding.

[jprider63]

Are you thinking of #1305?

[jprider63]

If we make a compiler plugin/extension, this is the workflow I was thinking about:

• GHC does an initial parse.
• GHC passes LH the AST. LH parses the refinements, inserts the GHC annotations, and sends GHC back an updated AST.
• GHC does normal type checking, transitions to core, etc.
• LH does refinement type checking. In addition, it can send GHC back information like if there are dead code paths, rewriting rules for proven optimizations, etc.

The GHC annotations would need to be standardized across GHC/base versions.

[ranjitjhala]

Ah yes thanks!!!

On Tue, Jun 26, 2018 at 6:31 AM JP notifications@github.com wrote:

Are you thinking of #1305 https://github.com/ucsd-progsys/liquidhaskell/issues/1305?

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1326#issuecomment-400309290, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHvsg4Cm6eViFLQKu2B5Trt1XJroks5uAjehgaJpZM4UVFK6 .

[facundominguez]

Now LH runs as a compiler plugin, and the description of Niki stays pretty much accurate.