{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2226","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2226/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2226/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2226/events","html_url":"https://github.com/agda/agda/issues/2226","id":179977165,"number":2226,"title":"open {{...}} gets hiding wrong","user":{"login":"identicalsnowflake","id":9684869,"avatar_url":"https://avatars.githubusercontent.com/u/9684869?v=3","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":245647317,"url":"https://api.github.com/repos/agda/agda/labels/bug","name":"bug","color":"fc2929","default":true},{"id":245649400,"url":"https://api.github.com/repos/agda/agda/labels/instance","name":"instance","color":"ededed","default":false},{"id":245647532,"url":"https://api.github.com/repos/agda/agda/labels/modules","name":"modules","color":"ededed","default":false},{"id":257165441,"url":"https://api.github.com/repos/agda/agda/labels/regression","name":"regression","color":"e11d21","default":false}],"state":"open","locked":false,"assignee":{"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},"assignees":[{"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}],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/16","html_url":"https://github.com/agda/agda/milestones/2.5.2","labels_url":"https://api.github.com/repos/agda/agda/milestones/16/labels","id":1713715,"number":16,"title":"2.5.2","description":null,"creator":{"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},"open_issues":8,"closed_issues":202,"state":"open","created_at":"2016-04-18T13:25:09Z","updated_at":"2016-11-28T15:49:24Z","due_on":null,"closed_at":null},"comments":11,"created_at":"2016-09-29T07:55:57Z","updated_at":"2016-11-28T21:18:28Z","closed_at":null,"body":"``` haskell\n\nopen import Agda.Builtin.Float\nopen import Reflection\nopen import Data.List hiding (_++_)\nopen import Data.Unit\n\n-- Reflection overhead\n\ninfixl 6 _>>=_\n_>>=_ = bindTC\n\ndefToTerm : Name → Definition → List (Arg Term) → Term\ndefToTerm _ (function cs) as = pat-lam cs as\ndefToTerm _ (constructor′ d) as = con d as\ndefToTerm _ _ _ = unknown\n\nderefImmediate : Term → TC Term\nderefImmediate (def f args) = getDefinition f >>= λ f' → returnTC (defToTerm f f' args)\nderefImmediate x = returnTC x\n\nreflectTerm : Name → TC Term\nreflectTerm n = getType n >>= λ ty → getDefinition n >>= λ x → derefImmediate (defToTerm n x []) >>= λ x → checkType x ty\n\nmacro\n  reflect : Name → Term → TC ⊤\n  reflect n a = reflectTerm n >>= quoteTC >>= unify a\n\n{- Define typeclass Semigroup a => Plus a -}\n\nrecord SemigroupLaws {ℓ} (t : Set ℓ) : Set ℓ where\n  infixr 5 _++_\n  field\n    _++_ : t → t → t\n    -- associative : ∀ {a b c} → (a ++ b) ++ c ≡ a ++ b ++ c\n\nrecord PlusOp {ℓ} (t : Set ℓ) : Set ℓ where\n  field\n    semigroup : SemigroupLaws t\n\n  infixr 6 _+_\n  _+_ = SemigroupLaws._++_ semigroup\n\ninstance\n  floatPlus : PlusOp Float\n  floatPlus = record { semigroup = record { _++_ = Agda.Builtin.Float.primFloatPlus } }\n\nopen PlusOp {{...}}\n\n-- The issue:\n\nworks : Float\nworks = PlusOp._+_ floatPlus 3.0 5.0\n\nresultWorks : Term\nresultWorks = reflect works\n\nfails : Float\nfails = 3.0 + 5.0\n\nresultFails : Term\nresultFails = reflect fails\n```\n\nConsider the conflict above between `works/resultWorks` and `fails/resultFails`. Either `checkType` or the initial reflection process is conflating information about how instance arguments are handled.\n\nEDIT: The error in `resultFails` is `Found an implicit application where an explicit application was\nexpected`\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/263397274","html_url":"https://github.com/agda/agda/issues/2226#issuecomment-263397274","issue_url":"https://api.github.com/repos/agda/agda/issues/2226","id":263397274,"user":{"login":"identicalsnowflake","id":9684869,"avatar_url":"https://avatars.githubusercontent.com/u/9684869?v=3","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},"created_at":"2016-11-28T21:18:28Z","updated_at":"2016-11-28T21:18:28Z","body":"@UlfNorell Awesome! I'm so glad to hear this, since this is an important issue for me. I'm definitely not using the reflection APIs to cross-compile code (because that would be ridiculous), but if I were, I'd say that solving this issue would be an *amazing* productivity boost."}}
{"actor":{"display_login":"identicalsnowflake"}}