{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1890","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/1890/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1890/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1890/events","html_url":"https://github.com/agda/agda/issues/1890","id":138340633,"number":1890,"title":"[reflection] defineFun should not depend on current module context when referring to types in that context","user":{"login":"m0davis","id":203587,"avatar_url":"https://avatars.githubusercontent.com/u/203587?v=3","gravatar_id":"","url":"https://api.github.com/users/m0davis","html_url":"https://github.com/m0davis","followers_url":"https://api.github.com/users/m0davis/followers","following_url":"https://api.github.com/users/m0davis/following{/other_user}","gists_url":"https://api.github.com/users/m0davis/gists{/gist_id}","starred_url":"https://api.github.com/users/m0davis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/m0davis/subscriptions","organizations_url":"https://api.github.com/users/m0davis/orgs","repos_url":"https://api.github.com/users/m0davis/repos","events_url":"https://api.github.com/users/m0davis/events{/privacy}","received_events_url":"https://api.github.com/users/m0davis/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2016-03-04T00:40:17Z","updated_at":"2016-03-14T13:01:30Z","closed_at":null,"body":"This is similar to issue #1833. The code below shows that one needs to know the current module context when defining a function that refers to the record ```R```. When within the anonymous module, it needs to have no arguments, but outside, it needs the module's argument. I believe that the intended design is to define all functions in an empty context. I.e. ```mac₁``` should succeed in both cases.\r\n\r\n```\r\n  open import Prelude\r\n  open import Tactic.Reflection\r\n\r\n  module _ (A : Set) where\r\n    record R : Set where\r\n\r\n    `R₀ : Type\r\n    `R₀ = def₀ (quote R)\r\n    \r\n    `R₁ : Term → Type\r\n    `R₁ = def₁ (quote R)\r\n    \r\n    `Nat : Type\r\n    `Nat = def₀ (quote Nat)\r\n    \r\n    helper-type₀ : Type\r\n    helper-type₀ = `R₀ `→ `R₀\r\n   \r\n    helper-type₁ : Type\r\n    helper-type₁ = `R₁ `Nat `→ `R₁ `Nat\r\n   \r\n    helper-term : Term\r\n    helper-term = var₀ 0\r\n   \r\n    helper-patterns : List (Arg Pattern)\r\n    helper-patterns = vArg (var \"_\") ∷\r\n                      []\r\n   \r\n    macro\r\n      mac₀ : Tactic\r\n      mac₀ hole =\r\n        n ← freshName \"n\" -|\r\n        define (vArg n) helper-type₀ (clause helper-patterns helper-term ∷ []) ~|\r\n        typeError [ strErr \"definition succeeded\" ]\r\n\r\n      mac₁ : Tactic\r\n      mac₁ hole =\r\n        n ← freshName \"n\" -|\r\n        define (vArg n) helper-type₁ (clause helper-patterns helper-term ∷ []) ~|\r\n        typeError [ strErr \"definition succeeded\" ]\r\n\r\n    within-module-succeeds₀ : Set\r\n    within-module-succeeds₀ = {!mac₀!}\r\n\r\n    within-module-fails₁ : Set\r\n    within-module-fails₁ = {!mac₁!}\r\n\r\n  outside-module-fails₀ : Set\r\n  outside-module-fails₀ = {!mac₀ Nat!}\r\n    \r\n  outside-module-succeeds₁ : Set\r\n  outside-module-succeeds₁ = {!mac₁ Nat!}\r\n```"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/196300179","html_url":"https://github.com/agda/agda/issues/1890#issuecomment-196300179","issue_url":"https://api.github.com/repos/agda/agda/issues/1890","id":196300179,"user":{"login":"m0davis","id":203587,"avatar_url":"https://avatars.githubusercontent.com/u/203587?v=3","gravatar_id":"","url":"https://api.github.com/users/m0davis","html_url":"https://github.com/m0davis","followers_url":"https://api.github.com/users/m0davis/followers","following_url":"https://api.github.com/users/m0davis/following{/other_user}","gists_url":"https://api.github.com/users/m0davis/gists{/gist_id}","starred_url":"https://api.github.com/users/m0davis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/m0davis/subscriptions","organizations_url":"https://api.github.com/users/m0davis/orgs","repos_url":"https://api.github.com/users/m0davis/repos","events_url":"https://api.github.com/users/m0davis/events{/privacy}","received_events_url":"https://api.github.com/users/m0davis/received_events","type":"User","site_admin":false},"created_at":"2016-03-14T13:01:29Z","updated_at":"2016-03-14T13:01:29Z","body":"Actually, it doesn't! I had (earlier) suspected that it did due to a similarity in problems related module parameters, but as [my latest example] (https://github.com/agda/agda/issues/1890#issuecomment-196102513) shows, this issue is actually quite different from #1363. Importantly, this one is also tougher for me to work around than #1363."}}