{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1740","labels_url":"https://api.github.com/repos/agda/agda/issues/1740/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1740/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1740/events","html_url":"https://github.com/agda/agda/issues/1740","id":121244672,"number":1740,"title":"Rewrite on reflexive equality should no be a no-op","user":{"login":"UlfNorell","id":447950,"avatar_url":"https://avatars.githubusercontent.com/u/447950?v=3","gravatar_id":"","url":"https://api.github.com/users/UlfNorell","html_url":"https://github.com/UlfNorell","followers_url":"https://api.github.com/users/UlfNorell/followers","following_url":"https://api.github.com/users/UlfNorell/following{/other_user}","gists_url":"https://api.github.com/users/UlfNorell/gists{/gist_id}","starred_url":"https://api.github.com/users/UlfNorell/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/UlfNorell/subscriptions","organizations_url":"https://api.github.com/users/UlfNorell/orgs","repos_url":"https://api.github.com/users/UlfNorell/repos","events_url":"https://api.github.com/users/UlfNorell/events{/privacy}","received_events_url":"https://api.github.com/users/UlfNorell/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-12-09T13:54:40Z","updated_at":"2015-12-09T15:34:28Z","closed_at":null,"body":"Sometimes you use `rewrite` to prove something about a function defined by `rewrite`. For instance,\r\n\r\n````agda\r\nopen import Common.Equality\r\nopen import Common.Bool\r\n\r\nT : Bool → Set\r\nT true  = Bool\r\nT false = true ≡ false\r\n\r\nfoo : (a b : Bool) → a ≡ b → T a → T b\r\nfoo a b eq x rewrite eq = x\r\n\r\ndata _≅_ {A : Set} (x : A) : {B : Set} → B → Set where\r\n  refl : x ≅ x\r\n\r\nworks : ∀ a b (eq : a ≡ b) (t : T a) → foo a b eq t ≅ t\r\nworks a b eq t rewrite eq = refl\r\n\r\nfails : ∀ a (eq : a ≡ a) (t : T a) → foo a a eq t ≡ t\r\nfails a eq t rewrite eq = refl\r\n-- Error:\r\n-- foo a a eq t | a | eq != t of type T a\r\n-- when checking that the expression refl has type foo a a eq t ≡ t\r\n````\r\nWith the change where wildcards no longer need to be dotted (#1605), the fix to #1110 (d6fcedb1) should be much simpler (just desugar rewrite to use a wildcard for the left-hand side).\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/163294327","html_url":"https://github.com/agda/agda/issues/1740#issuecomment-163294327","issue_url":"https://api.github.com/repos/agda/agda/issues/1740","id":163294327,"user":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"created_at":"2015-12-09T15:34:28Z","updated_at":"2015-12-09T15:34:28Z","body":"The naive fix does not work, though, see test case for #1402:\r\n```agda\r\npostulate eq : Set1 ≡ Set1\r\n\r\ntest : Set1\r\ntest rewrite eq = Set\r\n```\r\nThis fails then with error:\r\n```\r\nSet₁ !=< .w of type Set₂\r\nwhen checking that the expression Set has type .w\r\n```\r\nThe generated auxiliary function is:\r\n```\r\ntest-aux : (w : Set2) (eq : w ≡ w) → w\r\ntest-aux _ refl = Set\r\n```\r\nI guess we have to first fix #520, then we can fix this."}}