{"action":"created","issue":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/595","labels_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/595/labels{/name}","comments_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/595/comments","events_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/595/events","html_url":"https://github.com/ucsd-progsys/liquidhaskell/issues/595","id":129266095,"number":595,"title":"Dependent field refinements dropped when using field accessor functions","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":9,"created_at":"2016-01-27T20:56:32Z","updated_at":"2016-01-28T04:51:50Z","closed_at":null,"body":"The following program correctly type-checks:\r\n\r\n```haskell\r\nimport Data.Vector\r\n\r\n{-@\r\ndata Test = Test\r\n    { v  :: Vector ()\r\n    , x0 :: { x0 : Bool | vlen v < 1 ==> Prop x0 }\r\n    }\r\n@-}\r\n\r\ndata Test = Test\r\n    { v  :: Vector ()\r\n    , x0 :: Bool\r\n    }\r\n\r\nexample :: Test -> ()\r\nexample (Test v_ x0_) =\r\n    if x0_\r\n    then ()\r\n    else v_ ! 0\r\n```\r\n\r\nHowever, if I change `example` to use field accessors instead of pattern matching on the constructor then the program fails to type-check:\r\n\r\n```haskell\r\nimport Data.Vector\r\n\r\n{-@\r\ndata Test = Test\r\n    { v  :: Vector ()\r\n    , x0 :: { x0 : Bool | vlen v < 1 ==> Prop x0 }\r\n    }\r\n@-}\r\n\r\ndata Test = Test\r\n    { v  :: Vector ()\r\n    , x0 :: Bool\r\n    }\r\n\r\nexample :: Test -> ()\r\nexample t =\r\n    if x0 t\r\n    then ()\r\n    else v t ! 0\r\n```"},"comment":{"url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/comments/175975146","html_url":"https://github.com/ucsd-progsys/liquidhaskell/issues/595#issuecomment-175975146","issue_url":"https://api.github.com/repos/ucsd-progsys/liquidhaskell/issues/595","id":175975146,"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-01-28T04:51:50Z","updated_at":"2016-01-28T04:51:50Z","body":"As discussed on slack, the refined selector types **do** in fact work.\r\n\r\nhttp://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1453956403_1038.hs\r\n\r\nThe problem was with a misunderstanding of the relative precedences of `&&` and `=>` :)"}}