{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/1141","repository_url":"https://api.github.com/repos/FStarLang/FStar","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/1141/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/1141/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/1141/events","html_url":"https://github.com/FStarLang/FStar/issues/1141","id":244132510,"number":1141,"title":"Positivity check should not ignore all effects","user":{"login":"mtzguido","id":4195583,"avatar_url":"https://avatars2.githubusercontent.com/u/4195583?v=4","gravatar_id":"","url":"https://api.github.com/users/mtzguido","html_url":"https://github.com/mtzguido","followers_url":"https://api.github.com/users/mtzguido/followers","following_url":"https://api.github.com/users/mtzguido/following{/other_user}","gists_url":"https://api.github.com/users/mtzguido/gists{/gist_id}","starred_url":"https://api.github.com/users/mtzguido/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mtzguido/subscriptions","organizations_url":"https://api.github.com/users/mtzguido/orgs","repos_url":"https://api.github.com/users/mtzguido/repos","events_url":"https://api.github.com/users/mtzguido/events{/privacy}","received_events_url":"https://api.github.com/users/mtzguido/received_events","type":"User","site_admin":false},"labels":[{"id":714747218,"url":"https://api.github.com/repos/FStarLang/FStar/labels/component/typechecker","name":"component/typechecker","color":"c5def5","default":false},{"id":90066076,"url":"https://api.github.com/repos/FStarLang/FStar/labels/kind/bug","name":"kind/bug","color":"fef2c0","default":false},{"id":856029000,"url":"https://api.github.com/repos/FStarLang/FStar/labels/kind/unsoundness","name":"kind/unsoundness","color":"fef2c0","default":false},{"id":258450829,"url":"https://api.github.com/repos/FStarLang/FStar/labels/priority/high","name":"priority/high","color":"c2e0c6","default":false}],"state":"closed","locked":false,"assignee":{"login":"aseemr","id":3921573,"avatar_url":"https://avatars3.githubusercontent.com/u/3921573?v=4","gravatar_id":"","url":"https://api.github.com/users/aseemr","html_url":"https://github.com/aseemr","followers_url":"https://api.github.com/users/aseemr/followers","following_url":"https://api.github.com/users/aseemr/following{/other_user}","gists_url":"https://api.github.com/users/aseemr/gists{/gist_id}","starred_url":"https://api.github.com/users/aseemr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aseemr/subscriptions","organizations_url":"https://api.github.com/users/aseemr/orgs","repos_url":"https://api.github.com/users/aseemr/repos","events_url":"https://api.github.com/users/aseemr/events{/privacy}","received_events_url":"https://api.github.com/users/aseemr/received_events","type":"User","site_admin":false},"assignees":[{"login":"aseemr","id":3921573,"avatar_url":"https://avatars3.githubusercontent.com/u/3921573?v=4","gravatar_id":"","url":"https://api.github.com/users/aseemr","html_url":"https://github.com/aseemr","followers_url":"https://api.github.com/users/aseemr/followers","following_url":"https://api.github.com/users/aseemr/following{/other_user}","gists_url":"https://api.github.com/users/aseemr/gists{/gist_id}","starred_url":"https://api.github.com/users/aseemr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aseemr/subscriptions","organizations_url":"https://api.github.com/users/aseemr/orgs","repos_url":"https://api.github.com/users/aseemr/repos","events_url":"https://api.github.com/users/aseemr/events{/privacy}","received_events_url":"https://api.github.com/users/aseemr/received_events","type":"User","site_admin":false}],"milestone":null,"comments":4,"created_at":"2017-07-19T18:29:47Z","updated_at":"2018-04-29T10:14:40Z","closed_at":"2018-04-29T10:14:40Z","author_association":"CONTRIBUTOR","body":"Currently, the positivity check for inductives is disabled (assumed valid for a given constructor) when the negativity occurs with a non-Tot (nor GTot) effect in its codomain, thus, types such as\r\n```\r\nnoeq type negative =\r\n  | Blah : (negative -> Dv negative) -> negative\r\n```\r\nare accepted, which is pretty sweet since they would never compromise consistency anyway, as a `DIV` computation can never become `Tot`. However, given our DM4F magic, some effects can actually disappear into `Tot`, and we should check positivity of them. Here's a proof of False exploiting that:\r\n\r\n```\r\nmodule Bug\r\n\r\nlet id (a:Type) = unit -> M a\r\n\r\nval return_id : (a:Type) -> (x:a) -> id a\r\nlet return_id a x = fun _ -> x\r\n\r\nval bind_id : (a:Type) -> (b:Type) -> (f:id a) -> (g:a -> id b) -> id b\r\nlet bind_id a b f g = fun _ ->\r\n  let r = f () in g r ()\r\n\r\ntotal reifiable reflectable new_effect {\r\n  IDN : (a:Type) -> Effect\r\n  with repr     = id\r\n     ; bind     = bind_id\r\n     ; return   = return_id\r\n}\r\n\r\neffect ID (a:Type) = IDN a (fun () p -> forall x. p x)\r\n\r\nunopteq\r\ntype np (a : Type) =\r\n    | Mk : (np a -> ID a) -> np a\r\n\r\nval self : (#a:Type) -> np a -> ID a\r\nlet self #a v =\r\n    match v with\r\n    | Mk f -> f v\r\n\r\nval loop : (#a:Type) -> (a -> a) -> a\r\nlet loop #a f = reify (self (Mk (fun x -> f (self x)))) ()\r\n\r\nval falso : squash False\r\nlet falso = loop (fun x -> x)\r\n```\r\n(this is also a diverging Tot term)\r\n\r\nIn short, maybe we should really check if the effect we're traversing is marked as total or not?  This proof works the same without the `total` flag in the dm4f declaration, but that could be fixed by reifying non-total DM4F effects into Div instead of Tot, right?"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/385240699","html_url":"https://github.com/FStarLang/FStar/issues/1141#issuecomment-385240699","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/1141","id":385240699,"user":{"login":"aseemr","id":3921573,"avatar_url":"https://avatars3.githubusercontent.com/u/3921573?v=4","gravatar_id":"","url":"https://api.github.com/users/aseemr","html_url":"https://github.com/aseemr","followers_url":"https://api.github.com/users/aseemr/followers","following_url":"https://api.github.com/users/aseemr/following{/other_user}","gists_url":"https://api.github.com/users/aseemr/gists{/gist_id}","starred_url":"https://api.github.com/users/aseemr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aseemr/subscriptions","organizations_url":"https://api.github.com/users/aseemr/orgs","repos_url":"https://api.github.com/users/aseemr/repos","events_url":"https://api.github.com/users/aseemr/events{/privacy}","received_events_url":"https://api.github.com/users/aseemr/received_events","type":"User","site_admin":false},"created_at":"2018-04-29T10:14:40Z","updated_at":"2018-04-29T10:14:40Z","author_association":"CONTRIBUTOR","body":"Thanks for the reports @mtzguido. This is fixed in master, both the examples fail now."}}
{"actor":{"display_login":"aseemr"}}