Imported record function is not reflected.

zgrannan commented 4 years ago

Assume we have the following two files:

ReflectSource.hs

{-@ LIQUID "--reflection" @-}
module ReflectSource where

data Wrapper = Wrapper {
  f :: Int
}

{-@ reflect g @-}
g :: Wrapper -> Int
g w = f w + 1

ImportIssue.hs

{-@ LIQUID "--reflection" @-}
module ImportIssue where
import ReflectSource

Running liquid ReflectSource.hs is successful However, running liquid ImportIssue.hs yields the following output

Error: Illegal type specification for `ReflectSource.g`

 8 | {-@ reflect g @-}
                 ^

     ReflectSource.g :: lq1:ReflectSource.Wrapper -> {VV : GHC.Types.Int | VV == g lq1
                                                                           && VV == f lq1 + 1}
     Sort Error in Refinement: {VV : int | (VV == ReflectSource.g lq1
                                            && VV == ReflectSource.f lq1 + 1)}
     Unbound symbol ReflectSource.f --- perhaps you meant: ReflectSource.g ?

It appears that Liquid Haskell is not aware of the function f. A workaround is to add the data definition in liquid-haskell style comments in ReflectSource.hs:

{-@
data Wrapper = Wrapper {
  f :: Int
}
@-}

ranjitjhala commented 4 years ago

Unfortunately for some technical reason involving name resolution all reflected functions have to be exported.

Though it would be nice to not have this restriction...

On Fri, Mar 6, 2020 at 6:08 AM Zack Grannan notifications@github.com wrote:

Assume we have the following two files:

ReflectSource.hs

{-@ LIQUID "--reflection" @-}module ReflectSource where data Wrapper = Wrapper { f :: Int}

{-@ reflect g @-}g :: Wrapper -> Int g w = f w + 1

ImportIssue.hs

{-@ LIQUID "--reflection" @-}module ImportIssue whereimport ReflectSource

Running liquid ReflectSource.hs is successful However, running liquid ImportIssue.hs yields the following output

Error: Illegal type specification for ReflectSource.g

8 | {-@ reflect g @-} ^
 ReflectSource.g :: lq1:ReflectSource.Wrapper -> {VV : GHC.Types.Int | VV == g lq1
                                                                       && VV == f lq1 + 1}
 Sort Error in Refinement: {VV : int | (VV == ReflectSource.g lq1
                                        && VV == ReflectSource.f lq1 + 1)}
 Unbound symbol ReflectSource.f --- perhaps you meant: ReflectSource.g ?
It appears that Liquid Haskell is not aware of the function f. A workaround is to add the data definition in liquid-haskell style comments in ReflectSource.hs:

{-@data Wrapper = Wrapper { f :: Int} @-}

— 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/1624?email_source=notifications&email_token=AAMS4OF3NKFIID6VFU3H4ATRGD7UZA5CNFSM4LDA7BRKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4ITDUI7A, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OBMKZ6TABL65FMT36TRGD7UZANCNFSM4LDA7BRA .

nikivazou commented 4 years ago

The reflected function g is actually exported. The issue here is that the record selector f 1/ is exported by Haskell, but 2/ is not exported in the logic.

In short, if we reflect and export a function g we should export in the logic all the functions g is using in its definition, including record selectors (otherwise, the error message makes no sense ...)

ucsd-progsys / liquidhaskell

Imported record function is not reflected. #1624