ranjitjhala
commented
4 years ago Ouch sorry about this! Is there some way you can point us to your repo so we can try to replicate? Specifically I’m wondering what the definition of the various VectorX aliases look like...
On Mon, Feb 3, 2020 at 8:39 AM Wen Kokke notifications@github.com wrote:
This is a bit of a frustrating bug report to write.
There is a problem with reflection that I've encountered several times, but it's unclear to me how to minimize my code to isolate the issue. I am writing a tool for verifying neural networks using Liquid Haskell. At the moment, my project https://github.com/wenkokke/leadbeater fails to compile with the following error:
:1:1-1:1: Error
elaborate PLE1 195 failed on:
... && Leadbeater.Network.norm == Leadbeater.LinearAlgebra.map lam lam_arg##1 : real . Leadbeater.Prelude.rdiv lam_arg##1 (Leadbeater.LinearAlgebra.sumPos xs) ...with error
Unbound symbol xs --- perhaps you meant: fst ?in environment
...I've omitted a huge number of lines, basically containing the reflection of every single line of Haskell in my current codebase.
The problem seemingly lies with the following snippet https://github.com/wenkokke/leadbeater/blob/master/src/Leadbeater/Network.hs#L60-L63 :
{-@ reflect norm @-}
{-@ norm :: xs:VectorNE Rpos -> VectorX R xs @-} norm :: Vector R -> Vector R
norm xs = let s = sumPos xs in map (
rdivs) xsIt seems that Liquid Haskell somehow reflects the xs in the let binding as a literal xs. This problem remains if I rewrite the norm function to inline the definition for s, or to factor the lambda out into a top-level function:
{-@ reflect norm @-}
{-@ norm :: xs:VectorNE Rpos -> VectorX R xs @-} norm2 :: Vector R -> Vector R
norm2 xs = map (
rdivsumPos xs) xs{-@ reflect norm @-}
{-@ norm :: s:Rpos -> xs:VectorNE Rpos -> VectorX R xs @-} norm3' :: R -> Vector R -> Vector R
norm3' s xs = map (
rdivs) xs{-@ reflect norm3 @-}
{-@ norm3 :: xs:VectorNE Rpos -> VectorX R xs @-} norm3 :: Vector R -> Vector R
norm3 xs = norm3' (sumPos xs) xs
This is where things get weird. If I only build and verify my library, which includes the norm function, everything checks out. The error above only happens if I also verify my tests. The error itself is the failure to elaborate the following definition https://github.com/wenkokke/leadbeater/blob/master/test/perceptron.hs#L26-L37, which doesn't even use norm:
{-@ reflect example @-}
{-@ example :: NetworkN 2 1 @-} example :: Network
example = NLast
( Layer { bias = 0.184 , weights = (1 >< 2) [ 0.194 , 0.195 ] , activation = Sigmoid } )(The only function in the above definition is >< https://github.com/wenkokke/leadbeater/blob/master/src/Leadbeater/LinearAlgebra.hs#L137-L140, the rest are all constructors and constants.)
Similarly, if I extract the code involved in defining norm, as I've done here https://gist.github.com/wenkokke/8e46debb9d6e8177e007f1e545110f47, everything checks just fine.
If you have any idea what may be causing this, please let me know, I'd be happy to investigate more and provide further evidence.
— 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/1601?email_source=notifications&email_token=AAMS4OEHIW7ZXM5MI62DS7LRBBCEXA5CNFSM4KPIKKC2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IKUWXXA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OGTQAAEHQQHXCJJAY3RBBCEXANCNFSM4KPIKKCQ .
wenkokke
nikivazou
yiyunliu
facundominguez
This is a bit of a frustrating bug report to write.
There is a problem with reflection that I've encountered several times, but it's unclear to me how to minimize my code to isolate the issue. I am writing a tool for verifying neural networks using Liquid Haskell. At the moment, my project fails to compile with the following error:
I've omitted a huge number of lines, basically containing the reflection of every single line of Haskell in my current codebase.
The problem seemingly lies with the following snippet:
It seems that Liquid Haskell somehow reflects the
xsin the let binding as a literalxs. This problem remains if I rewrite thenormfunction to inline the definition fors, or to factor the lambda out into a top-level function:This is where things get weird. If I only compile and verify the library, which includes the
normfunction, everything checks just fine. The error above only happens if I also compile and verify my test. The error itself is the failure to elaborate the following definition, which doesn't even usenorm:(The only function in the above definition is
><, the rest are all constructors and constants.)Similarly, if I extract the code involved in defining
norm, as I've done here, everything checks just fine...If you have any idea what may be causing this, please let me know, I'd be happy to investigate more and provide further evidence.