{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/5996","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/5996/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/5996/comments","events_url":"https://api.github.com/repos/coq/coq/issues/5996/events","html_url":"https://github.com/coq/coq/issues/5996","id":267334732,"node_id":"MDU6SXNzdWUyNjczMzQ3MzI=","number":5996,"title":"constr:(...) builds ill-typed terms (or loses universe constraints)","user":{"login":"JasonGross","id":396076,"node_id":"MDQ6VXNlcjM5NjA3Ng==","avatar_url":"https://avatars0.githubusercontent.com/u/396076?v=4","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"labels":[{"id":698064744,"node_id":"MDU6TGFiZWw2OTgwNjQ3NDQ=","url":"https://api.github.com/repos/coq/coq/labels/part:%20tactics","name":"part: tactics","color":"dddddd","default":false}],"state":"open","locked":false,"assignee":{"login":"mattam82","id":98373,"node_id":"MDQ6VXNlcjk4Mzcz","avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false},"assignees":[{"login":"mattam82","id":98373,"node_id":"MDQ6VXNlcjk4Mzcz","avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false}],"milestone":null,"comments":13,"created_at":"2017-10-21T00:13:12Z","updated_at":"2018-09-11T16:48:32Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"#### Version\r\n\r\nThe Coq Proof Assistant, version 8.7.0 (October 2017)\r\ncompiled on Oct 18 2017 11:37:05 with OCaml 4.02.3\r\n\r\n#### Operating system\r\n`Linux jgross-Leopard-WS 4.4.0-66-generic #87-Ubuntu SMP Fri Mar 3 15:29:05 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux`\r\nDistributor ID: Ubuntu\r\nDescription:    Ubuntu 16.04.2 LTS\r\nRelease:        16.04\r\nCodename:       xenial\r\n\r\n#### Description of the problem\r\n\r\n```coq\r\nGoal Type.\r\n  let c := constr:(prod nat nat) in\r\n  let c' := (eval pattern nat in c) in\r\n  let c' := lazymatch c' with ?f _ => f end in\r\n  let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in\r\n  exact c''.\r\nDefined. (* Error: Illegal application:\r\nThe term \"prod\" of type \"Type -> Type -> Type\"\r\ncannot be applied to the terms\r\n \"P\" : \"Type\"\r\n \"P\" : \"Type\"\r\nThe 1st term has type \"Type@{Top.4}\" which should be coercible to\r\n \"Type@{Coq.Init.Datatypes.23}\". *)\r\n```\r\n\r\n1. I think this shouldn't happen\r\n2. It might be nice to have a primitive to refresh universes of a constr and recompute new universe constraints"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/420341692","html_url":"https://github.com/coq/coq/issues/5996#issuecomment-420341692","issue_url":"https://api.github.com/repos/coq/coq/issues/5996","id":420341692,"node_id":"MDEyOklzc3VlQ29tbWVudDQyMDM0MTY5Mg==","user":{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"created_at":"2018-09-11T16:48:32Z","updated_at":"2018-09-11T16:48:32Z","author_association":"MEMBER","body":"> Can you be more specific about how it doesn't scale to complex datatypes?\r\n\r\nHow do you perform variable expansion on closures returning or taking terms as arguments? Every type needs to come with a way to lift the variables it recursively contains.\r\n\r\n> if we only need to do this check on context extensions\r\n\r\nThat won't be sufficient. Remember the dreaded list of `clear` issues?\r\n\r\n> My goal is that Ltac2 should allow users who want fast code and know what they're doing to get fast code, and should also make it hard for users who don't know what they're doing to shoot themselves in the foot (at least behavior-wise) without noticing.\r\n\r\nI think that the cache solution is the easiest one that satisfies both criteria. You can always provide a function that produces a term whose cache is the current state, and that blindly trusts the user about this."}}
{"actor":{"display_login":"ppedrot"}}