A curious case with Where

[hafizhmakmur]

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]

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]

In the safe variant, test gets inlined.

[ranjitjhala]

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 ***@***.***> 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$> .