ucsd-progsys / liquidhaskell-tutorial

Tutorial for LiquidHaskell
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
MIT License
75 stars 27 forks source link

A curious case with Where #94

Open hafizhmakmur opened 4 years ago

hafizhmakmur commented 4 years ago

I was trying to figure out how to make my code safe and then I try to isolate the problem when I stumbled upon a curious case.

I make this code and it's unsafe as expected. But then I try to tinker around the code and it results in this code which is safe! Eventhough aaaa actually doesn't change at all, adding an irrelevant function which just so happens to have an exact definition with the function in Where in aaaa makes it safe somehow.

I eventually found out that you need to make a specification also for the function defined in Where (in this case {-@ test :: (Ord a, Num a) => x:a -> {y:Bool | y <=> (x > 0)} @-}) to make the function passed safe but this particular case still seems like an odd behavior to me.

ranjitjhala commented 4 years ago

Hmm, interesting, thanks for letting me know!

It's also further puzzling to me that the below is SAFE

{-@ aaaa :: Int -> Maybe {y:Int | y > 0} @-}
aaaa :: Int -> Maybe Int
aaaa dim
   | test dim  = Just dim
   | otherwise = Nothing
   where
        test :: Int -> Bool
        test dim = dim > 0

but that the following variant is UNSAFE

{-@ aaaa :: Int -> Maybe {y:Int | y > 0} @-}
aaaa :: Int -> Maybe Int
aaaa dim = if test dim then Just dim else Nothing
   where
        test :: Int -> Bool
        test dim = dim > 0

I wonder if it has to do with how GHC core gets generated for the two cases.

I will file this as an LH issue! thanks!

rosekunkel commented 4 years ago

In the safe variant, test gets inlined.

ranjitjhala commented 4 years ago

Hmm this should work even if test is NOT inlined (but is a local, non top level function) is GHC somehow making it a top level thing?

On Tue, May 26, 2020 at 10:00 AM Rose Kunkel notifications@github.com wrote:

In the safe variant, test gets inlined.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/94*issuecomment-634150899__;Iw!!Mih3wA!UgaBclG4X7fIzVUXjik-0KQ5AcYfmygkK8XBnFXXVfe_OBqQl1PEkQIiCjGg7GJl$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OAVOBWLBHOSGET4SK3RTPYSBANCNFSM4NGAYLBQ__;!!Mih3wA!UgaBclG4X7fIzVUXjik-0KQ5AcYfmygkK8XBnFXXVfe_OBqQl1PEkQIiCtt9uQiY$ .