{"action":"closed","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2964","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2964/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2964/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2964/events","html_url":"https://github.com/agda/agda/issues/2964","id":298008118,"number":2964,"title":"Mismatch between order of matching in clauses and case tree; subject reduction broken","user":{"login":"jespercockx","id":2910371,"avatar_url":"https://avatars2.githubusercontent.com/u/2910371?v=4","gravatar_id":"","url":"https://api.github.com/users/jespercockx","html_url":"https://github.com/jespercockx","followers_url":"https://api.github.com/users/jespercockx/followers","following_url":"https://api.github.com/users/jespercockx/following{/other_user}","gists_url":"https://api.github.com/users/jespercockx/gists{/gist_id}","starred_url":"https://api.github.com/users/jespercockx/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jespercockx/subscriptions","organizations_url":"https://api.github.com/users/jespercockx/orgs","repos_url":"https://api.github.com/users/jespercockx/repos","events_url":"https://api.github.com/users/jespercockx/events{/privacy}","received_events_url":"https://api.github.com/users/jespercockx/received_events","type":"User","site_admin":false},"labels":[{"id":245647489,"url":"https://api.github.com/repos/agda/agda/labels/pattern-matching","name":"pattern-matching","color":"ededed","default":false},{"id":245647317,"url":"https://api.github.com/repos/agda/agda/labels/type:%20bug","name":"type: bug","color":"c60205","default":false}],"state":"closed","locked":false,"assignee":{"login":"jespercockx","id":2910371,"avatar_url":"https://avatars2.githubusercontent.com/u/2910371?v=4","gravatar_id":"","url":"https://api.github.com/users/jespercockx","html_url":"https://github.com/jespercockx","followers_url":"https://api.github.com/users/jespercockx/followers","following_url":"https://api.github.com/users/jespercockx/following{/other_user}","gists_url":"https://api.github.com/users/jespercockx/gists{/gist_id}","starred_url":"https://api.github.com/users/jespercockx/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jespercockx/subscriptions","organizations_url":"https://api.github.com/users/jespercockx/orgs","repos_url":"https://api.github.com/users/jespercockx/repos","events_url":"https://api.github.com/users/jespercockx/events{/privacy}","received_events_url":"https://api.github.com/users/jespercockx/received_events","type":"User","site_admin":false},"assignees":[{"login":"jespercockx","id":2910371,"avatar_url":"https://avatars2.githubusercontent.com/u/2910371?v=4","gravatar_id":"","url":"https://api.github.com/users/jespercockx","html_url":"https://github.com/jespercockx","followers_url":"https://api.github.com/users/jespercockx/followers","following_url":"https://api.github.com/users/jespercockx/following{/other_user}","gists_url":"https://api.github.com/users/jespercockx/gists{/gist_id}","starred_url":"https://api.github.com/users/jespercockx/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jespercockx/subscriptions","organizations_url":"https://api.github.com/users/jespercockx/orgs","repos_url":"https://api.github.com/users/jespercockx/repos","events_url":"https://api.github.com/users/jespercockx/events{/privacy}","received_events_url":"https://api.github.com/users/jespercockx/received_events","type":"User","site_admin":false}],"milestone":null,"comments":6,"created_at":"2018-02-17T14:21:17Z","updated_at":"2018-02-20T09:55:12Z","closed_at":"2018-02-20T09:55:12Z","author_association":"CONTRIBUTOR","body":"While checking a definition by pattern matching, Agda uses left-to-right matching for the previous clauses. After the definition is checked, Agda uses the case tree computed by the coverage checker. Unfortunately, these don't always give the same result. For example, consider the following function:\r\n```agda\r\nf : (A : Set) → A → Bool → A ≡ Bool → Bool\r\nf .Bool true true refl = true\r\nf _     _    _    _    = false\r\n```\r\nThe coverage checker will first split on the third argument, then on the fourth, and finally on the second. So when using the standard left-to-right matching, `f Bool false x refl` computes to `false`, but the case tree will get stuck on the free variable `x` instead.\r\n\r\nThis can be exploited to break subject reduction:\r\n```agda\r\nopen import Agda.Builtin.Bool\r\nopen import Agda.Builtin.Equality\r\n\r\nrecord R : Set₁ where\r\n  field\r\n    fun  : (A : Set) → A → Bool → A ≡ Bool → Bool\r\n    rule : ∀ x → fun Bool false x refl ≡ false\r\nopen R\r\n\r\ntest : R\r\nfun test .Bool true true refl = true\r\nfun test _     _    _    _    = false\r\nrule test x = refl\r\n```\r\nWe have that `rule test x` of type `fun Bool false x refl ≡ false` computes to `refl`, but `refl` is not actually a well-typed term of this type. Indeed, the following fails:\r\n```agda\r\nfails : ∀ x → fun test Bool false x refl ≡ false\r\nfails x = refl\r\n```\r\nError:\r\n```\r\nfun test Bool false x refl != false of type Bool\r\nwhen checking that the expression refl has type\r\nfun test Bool false x refl ≡ false\r\n```\r\nA very drastic fix would be to only allow left-to-right splitting in the coverage checker, but this would be overly restrictive. A proper fix would probably require interleaving LHS checking, coverage checking, and the construction of the case tree. \r\n\r\nApart from breaking subject reduction, I think this is also worrying because there's no easy way to read the splitting order (and hence the computational meaning) of `f` from its definition. But this is not the first time we have such a problem. Perhaps we should instead do as Epigram did and record the case tree more explicitly in the definition of a function."}}
{"actor":{"display_login":"jespercockx"}}