search

ucsd-progsys / liquidhaskell

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

Error on import of peekCString #1487

Open googleson78 opened 5 years ago

googleson78 commented 5 years ago

When trying to check the following file:

import Foreign.C.String (peekCString)

liquid errors out:

tauren :: /tmp/liquid » cat asdf.hs
import Foreign.C.String (peekCString)
tauren :: /tmp/liquid » liquid asdf.hs
LiquidHaskell Version 0.8.6.0 [develop@574d17ba012dffcff5a736e15cd0a603bf0f558d (Tue Apr 23 20:05:03 2019 -0700)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: asdf.hs

**** [Checking: asdf.hs] *******************************************************

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

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

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

 <no source information>:0:0: Error: Illegal type specification for `GHC.Tuple.(,)`
     GHC.Tuple.(,) :: forall a##xo b##xo <p2 :: a##xo b##xo -> Bool> .
                      x_Tuple21:a##xo
                      -> x_Tuple22:{VV : b##xo<p2 x_Tuple21> | true}
                         -> {VV : (a##xo, b##xo)<\_ VV -> {VV : _<p2> | true}> | x_Tuple22 VV == x_Tuple22
                                                                                 && x_Tuple21 VV == x_Tuple21
                                                                                 && cStringLen VV == x_Tuple22
                                                                                 && snd VV == x_Tuple22
                                                                                 && fst VV == x_Tuple21}
     Sort Error in Refinement: {VV : (Tuple a##11 b##12) | (x_Tuple22 VV == x_Tuple22##GHC.Tuple.(,)
                                                            && x_Tuple21 VV == x_Tuple21##GHC.Tuple.(,)
                                                            && cStringLen VV == x_Tuple22##GHC.Tuple.(,)
                                                            && snd VV == x_Tuple22##GHC.Tuple.(,)
                                                            && fst VV == x_Tuple21##GHC.Tuple.(,))}
     Cannot unify a##11 with (GHC.Ptr.Ptr Foreign.C.Types.CChar) in expression: cStringLen VV << ceq2 >>

I tried playing around with flags mentioning imports, but I couldn't get it to ignore peekCString. Am I doing something wrong?

ranjitjhala commented 5 years ago

Hoops this is terrible I will look into it and fix it this morning !

On Thu, May 9, 2019 at 4:48 AM Georgi Lyubenov notifications@github.com wrote:

When trying to check a file with the following content:

import Foreign.C.String (peekCString)

liquid errors out:

tauren :: /tmp/liquid » cat asdf.hs

import Foreign.C.String (peekCString)

tauren :: /tmp/liquid » liquid asdf.hs

LiquidHaskell Version 0.8.6.0 [develop@574d17ba012dffcff5a736e15cd0a603bf0f558d (Tue Apr 23 20:05:03 2019 -0700)]

Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: asdf.hs

** [Checking: asdf.hs] *****

DONE: A-Normalization ****

** DONE: annotate *****

** RESULT: ERROR ***

:0:0: Error: Illegal type specification for `GHC.Tuple.(,)` GHC.Tuple.(,) :: forall a##xo b##xo Bool> . x_Tuple21:a##xo -> x_Tuple22:{VV : b##xo | true} -> {VV : (a##xo, b##xo)<\_ VV -> {VV : _ | true}> | x_Tuple22 VV == x_Tuple22 && x_Tuple21 VV == x_Tuple21 && cStringLen VV == x_Tuple22 && snd VV == x_Tuple22 && fst VV == x_Tuple21} Sort Error in Refinement: {VV : (Tuple a##11 b##12) | (x_Tuple22 VV == x_Tuple22##GHC.Tuple.(,) && x_Tuple21 VV == x_Tuple21##GHC.Tuple.(,) && cStringLen VV == x_Tuple22##GHC.Tuple.(,) && snd VV == x_Tuple22##GHC.Tuple.(,) && fst VV == x_Tuple21##GHC.Tuple.(,))} Cannot unify a##11 with (GHC.Ptr.Ptr Foreign.C.Types.CChar) in expression: cStringLen VV << ceq2 >> I tried playing around with flags mentioning imports, but I couldn't get it to ignore peekCString. Am I doing something wrong? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub , or mute the thread .
googleson78 commented 5 years ago

Upon tinkering a bit more: This is fine:

import Foreign.C.String (CString)

However this is not:

import Foreign.C.String (CString)

x :: CString
x = undefined

Error:

tauren :: /tmp/liquid » cat asdf.hs
import Foreign.C.String (CString)

x :: CString
x = undefined
tauren :: /tmp/liquid » liquid asdf.hs
LiquidHaskell Version 0.8.6.0 [develop@574d17ba012dffcff5a736e15cd0a603bf0f558d (Tue Apr 23 20:05:03 2019 -0700)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: asdf.hs

**** [Checking: asdf.hs] *******************************************************

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

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

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

 <no source information>:0:0: Error: Illegal type specification for `GHC.Tuple.(,)`
     GHC.Tuple.(,) :: forall a##xo b##xo <p2 :: a##xo b##xo -> Bool> .
                      x_Tuple21:a##xo
                      -> x_Tuple22:{VV : b##xo<p2 x_Tuple21> | true}
                         -> {VV : (a##xo, b##xo)<\_ VV -> {VV : _<p2> | true}> | x_Tuple22 VV == x_Tuple22
                                                                                 && x_Tuple21 VV == x_Tuple21
                                                                                 && cStringLen VV == x_Tuple22
                                                                                 && snd VV == x_Tuple22
                                                                                 && fst VV == x_Tuple21}
     Sort Error in Refinement: {VV : (Tuple a##11 b##12) | (x_Tuple22 VV == x_Tuple22##GHC.Tuple.(,)
                                                            && x_Tuple21 VV == x_Tuple21##GHC.Tuple.(,)
                                                            && cStringLen VV == x_Tuple22##GHC.Tuple.(,)
                                                            && snd VV == x_Tuple22##GHC.Tuple.(,)
                                                            && fst VV == x_Tuple21##GHC.Tuple.(,))}
     Cannot unify a##11 with (GHC.Ptr.Ptr Foreign.C.Types.CChar) in expression: cStringLen VV << ceq2 >>

In general any mention of the type CString causes this, I think (even as a field in a datatype).

ranjitjhala commented 5 years ago

:(

The bad news: this is an instance of a rather general problem -- so common we have a label for it! -- that I really should get to fixing but haven't found the time.

The good news: you can work around it by running with the --prune-unsorted flag, so 

liquid --prune-unsorted asdf.hs

or if you prefer, just add that flag to the top of the file, via:

{-@ LIQUID "--prune-unsorted" @-}

import Foreign.C.String (peekCString)

...

Will leave this open till I can get around to fixing this...

googleson78 commented 5 years ago

Thanks for the fast response! I am willing to help if it's matter of implementation (i.e. has some guidelines /documentation on what needs to be done).

facundominguez commented 4 months ago

Will leave this open till I can get around to fixing this...

What would the fix be? Replacing the measures with reflected functions perhaps?