{"action":"created","issue":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/653","repository_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell","labels_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/653/labels{/name}","comments_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/653/comments","events_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/653/events","html_url":"https://github.com/ucsd-progsys/liquidhaskell/pull/653","id":143727691,"number":653,"title":"Add refinement types for the `bytestring` library","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":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":12,"created_at":"2016-03-26T16:36:30Z","updated_at":"2016-03-31T23:05:07Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/pulls/653","html_url":"https://github.com/ucsd-progsys/liquidhaskell/pull/653","diff_url":"https://github.com/ucsd-progsys/liquidhaskell/pull/653.diff","patch_url":"https://github.com/ucsd-progsys/liquidhaskell/pull/653.patch"},"body":"The general rules I applied for refinements were:\r\n\r\n* Preconditions were only added for things that would cause crashes or\r\n  exceptions.  I did not protect against silly but valid inputs (like\r\n  `Data.ByteString.take (-1)`)\r\n* I added as many postconditions as humanly possible\r\n* I did not add refinements for deprecated functions in order to avoid Liquid\r\n  Haskell failing when the `bytestring` library eventually eliminates them\r\n\r\nI didn't cover every single module in the `bytestring` library.  The modules that\r\nI haven't done yet are all the `Builder`-related modules:\r\n\r\n* `Data.ByteString.Builder`\r\n* `Data.ByteString.Builder.Extra`\r\n* `Data.ByteString.Builder.Prim`\r\n* `Data.ByteString.Lazy.Builder`\r\n* `Data.ByteString.Lazy.Builder.ASCII`\r\n* `Data.ByteString.Lazy.Builder.Extras`"},"comment":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/comments/204165194","html_url":"https://github.com/ucsd-progsys/liquidhaskell/pull/653#issuecomment-204165194","issue_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/653","id":204165194,"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},"created_at":"2016-03-31T23:05:07Z","updated_at":"2016-03-31T23:05:07Z","body":"Okay, so my guess for why this is happening is that Liquid Haskell only applies the `*.spec` file if you import the module of that name, but since `Data.ByteString.Internal` is not importing itself then Liquid Haskell doesn't check the `Data/ByteString/Internal.spec` file"}}