{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/3031","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/3031/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/3031/comments","events_url":"https://api.github.com/repos/agda/agda/issues/3031/events","html_url":"https://github.com/agda/agda/issues/3031","id":314319045,"number":3031,"title":"Recent inference change?","user":{"login":"identicalsnowflake","id":9684869,"avatar_url":"https://avatars0.githubusercontent.com/u/9684869?v=4","gravatar_id":"","url":"https://api.github.com/users/identicalsnowflake","html_url":"https://github.com/identicalsnowflake","followers_url":"https://api.github.com/users/identicalsnowflake/followers","following_url":"https://api.github.com/users/identicalsnowflake/following{/other_user}","gists_url":"https://api.github.com/users/identicalsnowflake/gists{/gist_id}","starred_url":"https://api.github.com/users/identicalsnowflake/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/identicalsnowflake/subscriptions","organizations_url":"https://api.github.com/users/identicalsnowflake/orgs","repos_url":"https://api.github.com/users/identicalsnowflake/repos","events_url":"https://api.github.com/users/identicalsnowflake/events{/privacy}","received_events_url":"https://api.github.com/users/identicalsnowflake/received_events","type":"User","site_admin":false},"labels":[{"id":245647644,"url":"https://api.github.com/repos/agda/agda/labels/eta","name":"eta","color":"ededed","default":false},{"id":245648192,"url":"https://api.github.com/repos/agda/agda/labels/irrelevance","name":"irrelevance","color":"ededed","default":false},{"id":245647680,"url":"https://api.github.com/repos/agda/agda/labels/meta","name":"meta","color":"ededed","default":false},{"id":245648572,"url":"https://api.github.com/repos/agda/agda/labels/records","name":"records","color":"ededed","default":false},{"id":245647317,"url":"https://api.github.com/repos/agda/agda/labels/type:%20bug","name":"type: bug","color":"c60205","default":false},{"id":257165441,"url":"https://api.github.com/repos/agda/agda/labels/type:%20regression","name":"type: regression","color":"e11d21","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/21","html_url":"https://github.com/agda/agda/milestone/21","labels_url":"https://api.github.com/repos/agda/agda/milestones/21/labels","id":2669111,"number":21,"title":"2.5.4","description":null,"creator":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars3.githubusercontent.com/u/1155218?v=4","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},"open_issues":81,"closed_issues":129,"state":"open","created_at":"2017-07-29T20:30:27Z","updated_at":"2018-04-23T19:53:23Z","due_on":null,"closed_at":null},"comments":4,"created_at":"2018-04-14T10:41:35Z","updated_at":"2018-04-25T07:45:57Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"This may or may not be intentional, but there has been a recent (within the past 2 weeks) change to inference:\r\n\r\n```agda\r\nopen import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_+_)\r\nimport Agda.Builtin.Nat as N\r\nopen import Agda.Builtin.TrustMe\r\nopen import Agda.Builtin.Equality renaming (_≡_ to _≡≡_)\r\n\r\n\r\nrecord Σ (A : Set) (B : A → Set) : Set where\r\n  constructor _,_\r\n  field\r\n    proj₁ : A\r\n    proj₂ : B proj₁\r\n\r\nopen Σ public\r\n\r\n_×_ : ∀ (A : Set) (B : Set) → Set\r\na × b = Σ a λ _ → b\r\n\r\n∃ : ∀ {A : Set} → (A → Set) → Set\r\n∃ = Σ _\r\n\r\ndata ⊥ : Set where\r\n\r\nrecord Fin (n : ℕ) : Set where\r\n  field\r\n    m : ℕ\r\n    .p : ∃ λ k → (ℕ.suc k N.+ m) ≡≡ n\r\n\r\n\r\napply2 : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {a b : t₁} → (f : t₁ → t₂) → a ≡≡ b → f a ≡≡ f b\r\napply2 f refl = refl\r\n\r\n\r\nprivate\r\n  lem : ∀ m → .(∃ λ x → (suc (x N.+ m) ≡≡ 0)) → ⊥\r\n  lem _ (_ , ())\r\n\r\npred : ℕ → ℕ\r\npred zero = 0\r\npred (suc n) = n\r\n\r\ninfixl 60 _+_\r\n_+_ : ∀ {m n} → Fin m → Fin n → Fin (pred (m N.+ n))\r\n_+_ {m} {n} record { m = a ; p = c₁ , p₁ } record { m = b ; p = c₂ , p₂ } = record {\r\n    m = a N.+ b\r\n  ; p = (c₁ N.+ c₂) , primTrustMe\r\n  }\r\n\r\nS : ∀ {n} → Fin n → Fin (suc n)\r\nS = _+_ record { m = 1 ; p = zero , refl }\r\n\r\n\r\nto : ∀ {n} → Fin n → Fin n\r\nto record { m = zero ; p = p } = record { m = zero ; p = p }\r\nto {zero} record { m = (suc m) ; p = p } with lem (suc m) p\r\n... | ()\r\nto {suc n} record { m = (suc m) ; p = (k , p) } = S (to record { m = m ; p = k , primTrustMe })\r\n\r\nfrom = to\r\n\r\nl1 : ∀ {n} (x : Fin n) → S (from x) ≡≡ from (S x)\r\nl1 {zero} record { m = m ; p = p } with lem m p\r\n... | ()\r\nl1 {suc n} record { m = zero ; p = p } = refl\r\nl1 {suc n} record { m = (suc m) ; p = k , p } = apply2 S (l1 record { m = m ; p = k , primTrustMe })\r\n\r\niso : ∀ {n} → (x : Fin n) → from (to x) ≡≡ x\r\niso {zero} record { m = m ; p = p } with lem m p\r\n... | ()\r\niso {suc n} record { m = zero ; p = p } = refl\r\niso {suc n} record { m = (suc m) ; p = p@(k , _) } =\r\n  let\r\n    w : Fin n\r\n    w = record { m = m ; p = k , primTrustMe }\r\n    v : S (from (to w)) ≡≡ S w\r\n    v = apply2 S (iso w)\r\n  in\r\n  {!!}\r\n```\r\n\r\nAt commit 23ef599 (end of March), this is accepted, but currently, it shows some yellow inference problem in `apply2 S (iso w)`."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/384191674","html_url":"https://github.com/agda/agda/issues/3031#issuecomment-384191674","issue_url":"https://api.github.com/repos/agda/agda/issues/3031","id":384191674,"user":{"login":"UlfNorell","id":447950,"avatar_url":"https://avatars0.githubusercontent.com/u/447950?v=4","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},"created_at":"2018-04-25T07:45:57Z","updated_at":"2018-04-25T07:45:57Z","author_association":"OWNER","body":"Here's a version that fails as far back as I could test (`2.4.0`):\r\n\r\n```agda\r\nopen import Agda.Builtin.Nat\r\nopen import Agda.Builtin.Equality\r\n\r\nrecord Fin (n : Nat) : Set where\r\n  constructor mkFin\r\n  field\r\n    m  : Nat\r\n    .p : Nat\r\n\r\ncong : {A B : Set} {a b : A} (f : A → B) → a ≡ b → f a ≡ f b\r\ncong f refl = refl\r\n\r\nS : ∀ {n} → Fin n → Fin (suc n)\r\nS (mkFin a k) = mkFin (suc a) (suc k)\r\n\r\npostulate\r\n  to   : ∀ {n} → Fin n → Fin n\r\n  idem : ∀ {n} → (x : Fin n) → to (to x) ≡ x\r\n\r\nmodule _ (n m : Nat) .(k : Nat) where\r\n\r\n  w : Fin n\r\n  w = mkFin m k\r\n\r\n  mutual\r\n    X : Fin n\r\n    X = _\r\n\r\n    -- Works on =< 2.5.3 if removing this:\r\n    constr : S w ≡ S X\r\n    constr = refl\r\n\r\n    fails-to-solve-X : S (to (to w)) ≡ S w\r\n    fails-to-solve-X = cong {b = X} S (idem w)\r\n\r\n  works : S (to (to w)) ≡ S w\r\n  works = cong {b = mkFin _ _} S (idem w)\r\n```\r\n\r\nI guess this is the point where we start up the debate over the semantics of the `regression` label again..."}}
{"actor":{"display_login":"UlfNorell"}}