Unexpected lack of error message

[alanz]

Using current develop branch (3a9957985b63f7977f77badf2463c16ea7f54eb4)

In the following there is a typo, in that the final n is not capitalised

{-@ predicate QPairSize N X Y = X + N == qsize (fst Y) + qsize (snd Y) && qsize (fst Y) == n  @-}

I would expect an error/warning about n not being bound, or not being in scope.

If I change it to

{-@ predicate QPairSize N X Y = X + N == qsize (fst Y) + qsize (snd Y) && qsize (fst Y) == nn @-}

I get what I would expect

 /home/alanz/tmp/haskell-liquidhaskell-tutorial/liquidhaskell-tutorial/src/az-09.hs:157:13: Error: Bad Type Specification
 Main.take :: n:{v : Int | v >= 0} -> x:{v : (Queue a) | qsize v >= n} -> {v : ({v : (Queue a) | qsize v == n}, (Queue a)) | qsize x + n == qsize (fst v) + qsize (snd v)
                                                                                                                             && qsize (fst v) == nn}
     Sort Error in Refinement: {v##1 : (Tuple  (Main.Queue  a_aBn)  (Main.Queue  a_aBn)) | (qsize x + n == qsize (fst v##1) + qsize (snd v##1)
                                                                                            && qsize (fst v##1) == nn)}
     Unbound Symbol nn
 Perhaps you meant: n

But this refinement type is declared at the top level, and the only occurrences of n are as parameters in various functions. Loading the code into ghci and doing :i n says it is not in scope.

[nikivazou]

Thanks!

We need to type check the predicate aliases and not their unrollings! I though we were type checking the predicate aliases but seems that we are not, as @alanz error is only appearing at the type of take where the predicate is expanded.

[ranjitjhala]

Oops, yes this is bad, thanks for pointing it out @alanz

However, the better thing would be to transition fully to the the {-@ inline @-} mechanism which basically lets you convert Haskell functions into predicates. (This would let us reuse GHC's type, and scope checkers without having to rewrite them...)

So you can write

{-@ inline qPairSize @-}

qPairSize :: Int -> Int -> Int -> Bool

qPairSize n x y =

     x + n == qsize (fst y) + qsize (snd y)

  && qsize (fst y) == n

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/Books.hs

(This is a relatively new feature, I should update the tutorial with it...)

On Thu, Mar 9, 2017 at 1:34 AM, Niki Vazou notifications@github.com wrote:

Thanks!

We need to type check the predicate aliases and not their unrollings! I though we were type checking the predicate aliases but seems that we are not, as @alanz https://github.com/alanz error is only appearing at the type of take where the predicate is expanded.

— 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/947#issuecomment-285152731, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOMQlMgflrkr57t7_pK1bc4a-fKwwks5rjwmygaJpZM4MXPJF .

[alanz]

Thanks. I tried the example in Book.hs from the link, and then tweaked it slightly, to use 2 different variants with a tuple in it.

Simply putting either of the following in Book.hs will cause liquidhaskell dev branch to complain.

{-@ inline customerGetsDiscount1 @-}
customerGetsDiscount1 :: (Customer, Int) -> Bool
customerGetsDiscount1 (c, i) = c == Vip && i >= BOOK_THRESHOLD

gives

/home/alanz/tmp/haskell-liquidhaskell-tutorial/liquidhaskell-tutorial/src/Book.hs:25:12: Error: Bad Type Specification
 Books.customerGetsDiscount1 :: x:(Customer, Int) -> {VV : Bool | VV <=> select_(,)_1 x == Books.Vip
                                                                         && select_(,)_2 x >= 2}
     Sort Error in Refinement: {VV : bool | (VV <=> select_(,)_1 x##1 == Books.Vip##rlx
                                                    && select_(,)_2 x##1 >= 2)}
     Unbound Symbol select_(,)_1
 Perhaps you meant: len, strLen

whereas

{-@ inline customerGetsDiscount2 @-}
customerGetsDiscount2 :: (Customer, Int) -> Bool
customerGetsDiscount2 x = (fst x) == Vip && (snd x) >= BOOK_THRESHOLD

gives

/home/alanz/tmp/haskell-liquidhaskell-tutorial/liquidhaskell-tutorial/src/Book.hs:31:27-56: Error: Liquid Type Mismatch

 31 | customerGetsDiscount2 x = (fst x) == Vip && (snd x) >= BOOK_THRESHOLD
                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {VV : Bool | VV <=> ?d
                              && ?b}

   not a subtype of Required type
     VV : {VV : Bool | VV <=> fst x == Books.Vip
                              && snd x >= 2}

   In Context
     ?c : Customer

     ?e : {?e : Int | ?e == 2}

     ?b : {?b : Bool | ?b <=> ?a >= ?e}

     x : (Customer, Int)

     ?d : {?d : Bool | ?d <=> ?c == Books.Vip}

     ?a : Int

[nikivazou]

We do not have good support for automatically encoding imported data types (like lists and tuples) in the logic yet. To make your second example work, you need to teach Liquid Haskell how the Haskell functions fst and snd are encoded in the logic, by writing the below assumptions

{-@ assume fst :: x:(a, b) -> {v:a | v == fst x } @-}
{-@ assume snd :: x:(a, b) -> {v:b | v == snd x } @-}

[alanz]

Thanks, that sorts out the customerGetsDiscount2 version, as expected.

I think it is this issue which is tripping me up in the last part of section 09 of the tutorial, those assumptions should perhaps be added to the top of the file.

[ranjitjhala]

@nikivazou is the issue is that fst and snd are not proper measures, so would the following work?

{-@ measure myFst @-}
myFst (x, y) = x

{-@ measure mySnd @-}
mySnd (x, y) = y

and then use myFst and mySnd instead of fst and snd in customerGetsDiscount?

On Fri, Mar 10, 2017 at 1:24 AM, Alan Zimmerman notifications@github.com wrote:

Thanks, that sorts out the customerGetsDiscount2 version, as expected.

I think it is this issue which is tripping me up in the last part of section 09 of the tutorial, those assumptions should perhaps be added to the top of the file.

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

[alanz]

It does fix customerGetsDiscount2.

That is basically the renamed definition from import/GHC/Base.spec,

measure fst :: (a,b) -> a
fst (a,b) = a

measure snd :: (a,b) -> b
snd (a,b) = b

I would expect this to be used when using the --scrape-imports flag, and it is brought into scope when that is done. But it does not have the same effect as putting it directly in the file as myFst, mySnd.

[ranjitjhala]

Hmm, indeed that is quite a puzzle.

@nikivazou do you know why this happens?

(Is this to do with our "import" mechanism?

I wonder if it will work if we just put

those definitions in include/Prelude.spec?

On Sat, Mar 11, 2017 at 1:35 PM, Alan Zimmerman notifications@github.com wrote:

It does fix customerGetsDiscount2.

That is basically the renamed definition from import/GHC/Base.spec,

measure fst :: (a,b) -> a fst (a,b) = a

measure snd :: (a,b) -> b snd (a,b) = b

I would expect this to be used when using the --scrape-imports flag, and it is brought into scope when that is done. But it does not have the same effect as putting it directly in the file as myFst, mySnd.

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