search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

Bytestring: Bad Invariant Specification #1469

Open dmalkr opened 5 years ago

dmalkr commented 5 years ago

I have next error while checking my project:

Targets: ..../Types.hs

**** [Checking: ..../Types.hs] ***************

**** DONE:  A-Normalization ****************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

 /home/dima/.cabal/store/ghc-8.6.4/liquidhaskell-0.8.6.0-d7cc81ea49ae54f2df8b094bf77129aa890aaad87fb289bec4d1e07914d5d071/share/include/Data/ByteString/Lazy.spec:8:11: Error: Bad Invariant Specification
     invariant  {bs : Data.ByteString.Lazy.Internal.ByteString | 0 <= bllen bs}
     Sort Error in Refinement: {bs : Data.ByteString.Lazy.Internal.ByteString | 0 <= bllen bs}
     Unbound symbol bllen --- perhaps you meant: bslen ?

 /home/dima/.cabal/store/ghc-8.6.4/liquidhaskell-0.8.6.0-d7cc81ea49ae54f2df8b094bf77129aa890aaad87fb289bec4d1e07914d5d071/share/include/Data/ByteString/Lazy.spec:10:11: Error: Bad Invariant Specification
     invariant  {bs : Data.ByteString.Lazy.Internal.ByteString | bllen bs == stringlen bs}
     Sort Error in Refinement: {bs : Data.ByteString.Lazy.Internal.ByteString | bllen bs == stringlen bs}
     Unbound symbol bllen --- perhaps you meant: bslen ?

P.S. Do you need small code example for reproduce this error?

ranjitjhala commented 5 years ago

Thanks for posting these and my apologies — it looks like we have a huge gap in our regression tests so as another issue noted, the specs have “bitrotted”.

If you have a small example that would be good, but I think I should be able to reproduce and fix this regardless.

On Fri, Apr 19, 2019 at 10:13 PM Dmitry Krylov notifications@github.com wrote:

I have next error while checking my project:

Targets: ..../Types.hs

** [Checking: ..../Types.hs] *****

DONE: A-Normalization ****

** DONE: annotate *****

** RESULT: ERROR ***

/home/dima/.cabal/store/ghc-8.6.4/liquidhaskell-0.8.6.0-d7cc81ea49ae54f2df8b094bf77129aa890aaad87fb289bec4d1e07914d5d071/share/include/Data/ByteString/Lazy.spec:8:11: Error: Bad Invariant Specification invariant {bs : Data.ByteString.Lazy.Internal.ByteString | 0 <= bllen bs} Sort Error in Refinement: {bs : Data.ByteString.Lazy.Internal.ByteString | 0 <= bllen bs} Unbound symbol bllen --- perhaps you meant: bslen ?

/home/dima/.cabal/store/ghc-8.6.4/liquidhaskell-0.8.6.0-d7cc81ea49ae54f2df8b094bf77129aa890aaad87fb289bec4d1e07914d5d071/share/include/Data/ByteString/Lazy.spec:10:11: Error: Bad Invariant Specification invariant {bs : Data.ByteString.Lazy.Internal.ByteString | bllen bs == stringlen bs} Sort Error in Refinement: {bs : Data.ByteString.Lazy.Internal.ByteString | bllen bs == stringlen bs} Unbound symbol bllen --- perhaps you meant: bslen ?

P.S. Do you need small code example for reproduce this error?

— 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/1469, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4ODYCSEC64CJDZR4RWDPRKQ7DANCNFSM4HHI64VQ .

ranjitjhala commented 5 years ago

Ok I take that back -- I am unable to reproduce this with the few tests I wrote :(

Can you let me know if you have a test to reproduce?

dmalkr commented 5 years ago

Ok, I will make example tomorrow!

ranjitjhala commented 5 years ago

Thanks, much appreciated!!!

https://inboxwhenready.org/?utm_campaign=signature&utm_medium=email&utm_source=signature I'm using Inbox When Ready https://inboxwhenready.org/?utm_campaign=signature&utm_medium=email&utm_source=signature to protect my focus.

On Sat, Apr 20, 2019 at 3:14 PM Dmitry Krylov notifications@github.com wrote:

Ok, I will make example tomorrow!

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1469#issuecomment-485183527, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OBP3MPOUA6WJDBK423PROISRANCNFSM4HHI64VQ .

dmalkr commented 5 years ago

Heh, it's a very tricky error.

First, it does not occur in module, which uses ByteString, but in module, that import it!

AND it is need to import Data.Aeson.

Look, SomeByteStrings.hs:

{-# LANGUAGE OverloadedStrings   #-}
module SomeByteStrings (initializeTables) where

import qualified Data.ByteString.Lazy as LBS
import qualified Database.SQLite.Simple           as SQL

initializeTables :: SQL.Connection -> IO ()
initializeTables conn = do
  SQL.execute_ conn "CREATE TABLE IF NOT EXISTS tbl (a INT NOT NULL UNIQUE)"
  -- ...

and MyImport.hs:

module MyImport where

import qualified Data.Aeson
import SomeByteStrings

Now, let's check MyImport.hs:

% liquid MyImport.hs
LiquidHaskell Version 0.8.6.0, Git revision 580aef36671058c9f8a28bf5900acf41d70b4f89 (dirty) no git information
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: ./SomeByteStrings.hs
         MyImport.hs

**** [Checking: ./SomeByteStrings.hs] ******************************************

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

Working 100% [=================================================================]

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************

**** [Checking: MyImport.hs] ***************************************************

**** DONE:  A-Normalization ****************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

 /home/dima/.cabal/store/ghc-8.6.4/liquidhaskell-0.8.6.0-746b7ff032c4c7e234f0326a22fac63567938f210dacd0e48da65a3c7edf3aaf/share/include/Data/ByteString/Lazy.spec:8:11: Error: Bad Invariant Specification
     invariant  {bs : Data.ByteString.Lazy.Internal.ByteString | 0 <= bllen bs}
     Sort Error in Refinement: {bs : Data.ByteString.Lazy.Internal.ByteString | 0 <= bllen bs}
     Unbound symbol bllen --- perhaps you meant: bslen ?

 /home/dima/.cabal/store/ghc-8.6.4/liquidhaskell-0.8.6.0-746b7ff032c4c7e234f0326a22fac63567938f210dacd0e48da65a3c7edf3aaf/share/include/Data/ByteString/Lazy.spec:10:11: Error: Bad Invariant Specification
     invariant  {bs : Data.ByteString.Lazy.Internal.ByteString | bllen bs == stringlen bs}
     Sort Error in Refinement: {bs : Data.ByteString.Lazy.Internal.ByteString | bllen bs == stringlen bs}
     Unbound symbol bllen --- perhaps you meant: bslen ?
dmalkr commented 5 years ago

Data.Aeson is from aeson: https://hackage.haskell.org/package/aeson-1.4.2.0.

Liquid Haskell is fresh, and from develop branch.

nilehmann commented 4 years ago

If you do import Data.Int ( Int64 ) in the file you are verifying you don't get the error, so I assume it has something to do with being unable to define bllen here because GHC.Int.Int64 is not found.