{"action":"created","issue":{"url":"https://api.github.com/repos/ucsd-progsys/liquid-fixpoint/issues/59","labels_url":"https://api.github.com/repos/ucsd-progsys/liquid-fixpoint/issues/59/labels{/name}","comments_url":"https://api.github.com/repos/ucsd-progsys/liquid-fixpoint/issues/59/comments","events_url":"https://api.github.com/repos/ucsd-progsys/liquid-fixpoint/issues/59/events","html_url":"https://github.com/ucsd-progsys/liquid-fixpoint/issues/59","id":69688798,"number":59,"title":"Crash on Untyped Qualifiers","user":{"login":"nikivazou","id":714933,"avatar_url":"https://avatars.githubusercontent.com/u/714933?v=3","gravatar_id":"","url":"https://api.github.com/users/nikivazou","html_url":"https://github.com/nikivazou","followers_url":"https://api.github.com/users/nikivazou/followers","following_url":"https://api.github.com/users/nikivazou/following{/other_user}","gists_url":"https://api.github.com/users/nikivazou/gists{/gist_id}","starred_url":"https://api.github.com/users/nikivazou/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikivazou/subscriptions","organizations_url":"https://api.github.com/users/nikivazou/orgs","repos_url":"https://api.github.com/users/nikivazou/repos","events_url":"https://api.github.com/users/nikivazou/events{/privacy}","received_events_url":"https://api.github.com/users/nikivazou/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":14,"created_at":"2015-04-20T21:45:42Z","updated_at":"2015-04-21T21:38:21Z","closed_at":null,"body":"The following [code](https://github.com/ucsd-progsys/liquid-fixpoint/blob/master/external/fixpoint/tests/UnTypedQuals.fq)\r\n\r\n~~~\r\nqualif Auto1(VV : FAppTy SumFst.L  a_apx): ((? barr([VV])) <=> true) // \"tests/pos/fixme.hs\" (line 3, column 12)\r\nqualif Auto2(VV : FAppTy SumFst.L  a_apx): (bar([VV]) = 0) // \"tests/pos/fixme.hs\" (line 3, column 12)\r\n\r\nconstant bar : func(0, [FAppTy SumFst.L  int; int])\r\nconstant barr : func(0, [FAppTy SumFst.L  int; bool])\r\n~~~\r\n\r\nCrashes with \r\n\r\n~~~\r\nNo type for barr([VV])z3Pred: error converting (barr(VV) <=> true)\r\nFatal error: exception Assert_failure(\"tpGen.ml\", 355, 24)\r\n~~~\r\n\r\nI.e. the `Auto1` qualifier is untyped. But these is no such issue for the `Auto2` qualifiers. \r\nSo, @ranjitjhala do we allow unsorted qualifiers or not?\r\n\r\nThe above error is created from the following liquidHaskell code\r\n\r\n~~~\r\ndata L a = Nil\r\n\r\n{-@ measure bar :: L Int -> Int\r\n    bar Nil = 0\r\n  @-}\t\r\n\r\n{-@ measure barr :: L Int -> Prop\r\n    barr Nil = true\r\n  @-}\t  \r\n~~~\r\n\r\nWhere the qualifiers are stripped from the type of Nil\r\n\r\n~~~\r\nNil :: {v:L a | bar v == 0 && barr v <=> true} \r\n~~~"},"comment":{"url":"https://api.github.com/repos/ucsd-progsys/liquid-fixpoint/issues/comments/94949819","html_url":"https://github.com/ucsd-progsys/liquid-fixpoint/issues/59#issuecomment-94949819","issue_url":"https://api.github.com/repos/ucsd-progsys/liquid-fixpoint/issues/59","id":94949819,"user":{"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},"created_at":"2015-04-21T21:38:21Z","updated_at":"2015-04-21T21:38:21Z","body":"Can you explain \"2\" ? How does LH exactly use this feature? (Whats a\nconcrete example?)\n\nOn Tue, Apr 21, 2015 at 2:35 PM, Niki Vazou <notifications@github.com>\nwrote:\n\n> Nice!\n>\n> The issue is that I can see why both should fail, but liquidHaskell\n> depends on them not failing (see \"2\" above).\n>\n> So if we fix liquid-fixpoint so that they both fail, we will break\n> liquidHaskell.....\n>\n> At least, both (Auto1 and Auto2) should be treated in the same way\n> (either both fail or none.)\n>\n> --\n> Reply to this email directly or view it on GitHub\n> <https://github.com/ucsd-progsys/liquid-fixpoint/issues/59#issuecomment-94949218>\n> .\n>\n\n\n\n-- \nRanjit.\n"}}