{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8850","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8850/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8850/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8850/events","html_url":"https://github.com/coq/coq/pull/8850","id":375169219,"node_id":"MDExOlB1bGxSZXF1ZXN0MjI2Njc3NTM4","number":8850,"title":"Local universes for opaque polymorphic constants.","user":{"login":"SkySkimmer","id":2461932,"node_id":"MDQ6VXNlcjI0NjE5MzI=","avatar_url":"https://avatars1.githubusercontent.com/u/2461932?v=4","gravatar_id":"","url":"https://api.github.com/users/SkySkimmer","html_url":"https://github.com/SkySkimmer","followers_url":"https://api.github.com/users/SkySkimmer/followers","following_url":"https://api.github.com/users/SkySkimmer/following{/other_user}","gists_url":"https://api.github.com/users/SkySkimmer/gists{/gist_id}","starred_url":"https://api.github.com/users/SkySkimmer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SkySkimmer/subscriptions","organizations_url":"https://api.github.com/users/SkySkimmer/orgs","repos_url":"https://api.github.com/users/SkySkimmer/repos","events_url":"https://api.github.com/users/SkySkimmer/events{/privacy}","received_events_url":"https://api.github.com/users/SkySkimmer/received_events","type":"User","site_admin":false},"labels":[{"id":485986179,"node_id":"MDU6TGFiZWw0ODU5ODYxNzk=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20feature","name":"kind: feature","color":"0e8a16","default":false},{"id":777223550,"node_id":"MDU6TGFiZWw3NzcyMjM1NTA=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20benchmarking","name":"needs: benchmarking","color":"c2e0c6","default":false},{"id":665075119,"node_id":"MDU6TGFiZWw2NjUwNzUxMTk=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20documentation","name":"needs: documentation","color":"D7ACAC","default":false},{"id":733571551,"node_id":"MDU6TGFiZWw3MzM1NzE1NTE=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20overlay","name":"needs: overlay","color":"0f1170","default":false},{"id":394846778,"node_id":"MDU6TGFiZWwzOTQ4NDY3Nzg=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20progress","name":"needs: progress","color":"ffd062","default":false},{"id":614883102,"node_id":"MDU6TGFiZWw2MTQ4ODMxMDI=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20rebase","name":"needs: rebase","color":"d4c5f9","default":false},{"id":394846679,"node_id":"MDU6TGFiZWwzOTQ4NDY2Nzk=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20review","name":"needs: review","color":"f9d0c4","default":false},{"id":723364268,"node_id":"MDU6TGFiZWw3MjMzNjQyNjg=","url":"https://api.github.com/repos/coq/coq/labels/part:%20kernel","name":"part: kernel","color":"dddddd","default":false},{"id":755681591,"node_id":"MDU6TGFiZWw3NTU2ODE1OTE=","url":"https://api.github.com/repos/coq/coq/labels/part:%20universes","name":"part: universes","color":"dddddd","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/16","html_url":"https://github.com/coq/coq/milestone/16","labels_url":"https://api.github.com/repos/coq/coq/milestones/16/labels","id":3512681,"node_id":"MDk6TWlsZXN0b25lMzUxMjY4MQ==","number":16,"title":"8.10+beta1","description":"","creator":{"login":"Zimmi48","id":1108325,"node_id":"MDQ6VXNlcjExMDgzMjU=","avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"open_issues":107,"closed_issues":221,"state":"open","created_at":"2018-07-20T18:48:13Z","updated_at":"2018-11-05T12:20:03Z","due_on":null,"closed_at":null},"comments":8,"created_at":"2018-10-29T19:01:04Z","updated_at":"2018-11-05T12:20:03Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/8850","html_url":"https://github.com/coq/coq/pull/8850","diff_url":"https://github.com/coq/coq/pull/8850.diff","patch_url":"https://github.com/coq/coq/pull/8850.patch"},"body":"This lets opaque polymorphic constants have universes which are needed for the body but which do not need to be provided when using the constant (because we guarantee that some acceptable universe always exists, and since the constant is opaque it can't be observed).\r\nFor instance, \r\n~~~coq\r\nSet Printing Universes.\r\nSet Universe Polymorphism.\r\nLemma foo : Type.\r\nProof. exact (forall _ : Type, Type).\r\nQed.\r\n\r\nPrint foo.\r\n(*\r\nfoo@{Top.1} = \r\nType@{Top.2} -> Type@{Top.3}\r\n     : Type@{Top.1}\r\n(* Top.1 |= Prop < Set\r\n            Set < Top.1\r\n            local: {Top.3 Top.2} |= Top.2 < Top.1\r\n                                    Top.3 < Top.1\r\n                                     *)\r\n\r\nfoo is universe polymorphic\r\n*)\r\nDefinition bar@{i|Set < i} := foo@{i}.\r\n~~~\r\n\r\nThis is compatibility breaking for those using explicit universe instances (unless they have no opaque definitions I guess). I didn't make the others yet but see the HoTT overlay at https://github.com/SkySkimmer/HoTT/commit/2d4bf3814b1c2a72fb910f072e714c9c1e792b45 for what it gives us in the wild. For instance removing the need to pass around upper bound universes like https://github.com/SkySkimmer/HoTT/commit/2d4bf3814b1c2a72fb910f072e714c9c1e792b45#diff-e2b7e5e83439b62c3f9c1764d6f5eaf1L391 and removing lots of manually minimizing universes.\r\n\r\nThis can be disabled by unsetting `Private Polymorphic Universes`, such that `Qed` has no semantic difference other than blocking unfolding.\r\n\r\nTODO:\r\n- document\r\n- improve printing?"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/435855117","html_url":"https://github.com/coq/coq/pull/8850#issuecomment-435855117","issue_url":"https://api.github.com/repos/coq/coq/issues/8850","id":435855117,"node_id":"MDEyOklzc3VlQ29tbWVudDQzNTg1NTExNw==","user":{"login":"SkySkimmer","id":2461932,"node_id":"MDQ6VXNlcjI0NjE5MzI=","avatar_url":"https://avatars1.githubusercontent.com/u/2461932?v=4","gravatar_id":"","url":"https://api.github.com/users/SkySkimmer","html_url":"https://github.com/SkySkimmer","followers_url":"https://api.github.com/users/SkySkimmer/followers","following_url":"https://api.github.com/users/SkySkimmer/following{/other_user}","gists_url":"https://api.github.com/users/SkySkimmer/gists{/gist_id}","starred_url":"https://api.github.com/users/SkySkimmer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SkySkimmer/subscriptions","organizations_url":"https://api.github.com/users/SkySkimmer/orgs","repos_url":"https://api.github.com/users/SkySkimmer/repos","events_url":"https://api.github.com/users/SkySkimmer/events{/privacy}","received_events_url":"https://api.github.com/users/SkySkimmer/received_events","type":"User","site_admin":false},"created_at":"2018-11-05T12:20:03Z","updated_at":"2018-11-05T12:20:03Z","author_association":"CONTRIBUTOR","body":">Sorry to insist, but I'd rather fix the pretty printer so that you can (more) easily copy past the constraints rather than provide yet another Set option (and the multiple code paths). Of course my position stands only If the reason for the option is just migrating... if there are other reasons I'm fine with the option.\r\n\r\nMostly I don't want to force Qed to have different results than Defined other than opacity."}}
{"actor":{"display_login":"SkySkimmer"}}