Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Local inference not working #1679

Closed
ranjitjhala opened this issue May 20, 2020 · 1 comment
Closed

Local inference not working #1679

ranjitjhala opened this issue May 20, 2020 · 1 comment

Comments

@ranjitjhala
Copy link
Member

Thanks to @hafizhmakmur

ucsd-progsys/liquidhaskell-tutorial#94

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

(why does the presence of the GHC sig test :: Int -> Bool make a difference?)

{-@ 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.

@facundominguez
Copy link
Collaborator

In the latest LH, both snippets above are accepted, and so are the snippets in ucsd-progsys/liquidhaskell-tutorial#94.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants