{"action":"created","issue":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/638","repository_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell","labels_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/638/labels{/name}","comments_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/638/comments","events_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/638/events","html_url":"https://github.com/ucsd-progsys/liquidhaskell/issues/638","id":141141015,"number":638,"title":"`false` after bind type-checks for some monads but not others","user":{"login":"Gabriel439","id":1313787,"avatar_url":"https://avatars.githubusercontent.com/u/1313787?v=3","gravatar_id":"","url":"https://api.github.com/users/Gabriel439","html_url":"https://github.com/Gabriel439","followers_url":"https://api.github.com/users/Gabriel439/followers","following_url":"https://api.github.com/users/Gabriel439/following{/other_user}","gists_url":"https://api.github.com/users/Gabriel439/gists{/gist_id}","starred_url":"https://api.github.com/users/Gabriel439/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Gabriel439/subscriptions","organizations_url":"https://api.github.com/users/Gabriel439/orgs","repos_url":"https://api.github.com/users/Gabriel439/repos","events_url":"https://api.github.com/users/Gabriel439/events{/privacy}","received_events_url":"https://api.github.com/users/Gabriel439/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/labels/bug","name":"bug","color":"fc2929"},{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/labels/unsoundness","name":"unsoundness","color":"e11d21"}],"state":"open","locked":false,"assignee":{"login":"ranjitjhala","id":1650232,"avatar_url":"https://avatars.githubusercontent.com/u/1650232?v=3","gravatar_id":"","url":"https://api.github.com/users/ranjitjhala","html_url":"https://github.com/ranjitjhala","followers_url":"https://api.github.com/users/ranjitjhala/followers","following_url":"https://api.github.com/users/ranjitjhala/following{/other_user}","gists_url":"https://api.github.com/users/ranjitjhala/gists{/gist_id}","starred_url":"https://api.github.com/users/ranjitjhala/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ranjitjhala/subscriptions","organizations_url":"https://api.github.com/users/ranjitjhala/orgs","repos_url":"https://api.github.com/users/ranjitjhala/repos","events_url":"https://api.github.com/users/ranjitjhala/events{/privacy}","received_events_url":"https://api.github.com/users/ranjitjhala/received_events","type":"User","site_admin":false},"milestone":null,"comments":9,"created_at":"2016-03-16T01:02:37Z","updated_at":"2016-03-16T04:24:49Z","closed_at":null,"body":"The following code correctly fails to type-check:\r\n\r\n```haskell\r\n{-@\r\nerror :: { x : String | false } -> a\r\n@-}\r\n\r\nexample :: Maybe ()\r\nexample = do\r\n    _ <- return ()\r\n    error \"URK\"\r\n```\r\n\r\n... but if you replace `Maybe` in the above example with `Data.Binary.Get` then the code successfully type-checks.\r\n\r\nI tested a variety of monads to see which ones type-checked and which ones did not.\r\n\r\nMonads that do not type-check for the above code:\r\n\r\n* `Maybe`\r\n* `Either e`\r\n* `[]`\r\n* `Identity`\r\n* `Proxy`\r\n* `Monad m => m` (i.e. generalizing the constraint to any `Monad`)\r\n* `State`\r\n* `Cont`\r\n* `Managed`\r\n\r\nMonads that type-check for the above code:\r\n\r\n* `Turtle.Shell`\r\n* `Data.Binary.Get`\r\n* `Data.Serialize.Get`\r\n\r\nNote that the last few monads **do** fail to type-check if you change the code to:\r\n\r\n```haskell\r\nexample :: Shell ()\r\nexample = do\r\n    return () -- (i.e. use `(>>)` instead of `(>>=)`)\r\n    error \"URK\"\r\n```\r\n\r\nIn my particular case I was interested in `Data.Serialize.Get`, which is why I'm trying to figure out why it does not detect an `error`-induced failure after a `(>>=)`."},"comment":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/comments/197147315","html_url":"https://github.com/ucsd-progsys/liquidhaskell/issues/638#issuecomment-197147315","issue_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/638","id":197147315,"user":{"login":"gridaphobe","id":201997,"avatar_url":"https://avatars.githubusercontent.com/u/201997?v=3","gravatar_id":"","url":"https://api.github.com/users/gridaphobe","html_url":"https://github.com/gridaphobe","followers_url":"https://api.github.com/users/gridaphobe/followers","following_url":"https://api.github.com/users/gridaphobe/following{/other_user}","gists_url":"https://api.github.com/users/gridaphobe/gists{/gist_id}","starred_url":"https://api.github.com/users/gridaphobe/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gridaphobe/subscriptions","organizations_url":"https://api.github.com/users/gridaphobe/orgs","repos_url":"https://api.github.com/users/gridaphobe/repos","events_url":"https://api.github.com/users/gridaphobe/events{/privacy}","received_events_url":"https://api.github.com/users/gridaphobe/received_events","type":"User","site_admin":false},"created_at":"2016-03-16T04:24:49Z","updated_at":"2016-03-16T04:24:49Z","body":"@ranjitjhala sorry, I meant a `.dot` file, ie for graphviz.\r\n\r\n@Gabriel439 yep, that's why LH is able to \"prove\" the `error` call safe. It infers false and can then prove anything it that branch. But it shouldn't be able to prove false here!"}}