{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1691","labels_url":"https://api.github.com/repos/agda/agda/issues/1691/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1691/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1691/events","html_url":"https://github.com/agda/agda/issues/1691","id":112022098,"number":1691,"title":"Internal error using --sharing: src/full/Agda/TypeChecking/CompiledClause/Match.hs:189","user":{"login":"mechvel","id":1506057,"avatar_url":"https://avatars.githubusercontent.com/u/1506057?v=3","gravatar_id":"","url":"https://api.github.com/users/mechvel","html_url":"https://github.com/mechvel","followers_url":"https://api.github.com/users/mechvel/followers","following_url":"https://api.github.com/users/mechvel/following{/other_user}","gists_url":"https://api.github.com/users/mechvel/gists{/gist_id}","starred_url":"https://api.github.com/users/mechvel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mechvel/subscriptions","organizations_url":"https://api.github.com/users/mechvel/orgs","repos_url":"https://api.github.com/users/mechvel/repos","events_url":"https://api.github.com/users/mechvel/events{/privacy}","received_events_url":"https://api.github.com/users/mechvel/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/enhancement","name":"enhancement","color":"84b6eb"},{"url":"https://api.github.com/repos/agda/agda/labels/master","name":"master","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/Priority-High","name":"Priority-High","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/Sharing","name":"Sharing","color":"ededed"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":10,"created_at":"2015-10-18T14:05:59Z","updated_at":"2015-10-22T08:38:45Z","closed_at":null,"body":"This is on  Development Agda October-17, 2015.\r\n```agda\r\nopen import Relation.Binary.PropositionalEquality as PE using (_≡_)\r\nopen import Data.Nat.Base using (ℕ; suc; pred; _∸_)\r\n\r\n∸1≗pred :  ∀ {n} → n ∸ 1 ≡ pred n\r\n∸1≗pred {0}     = PE.refl\r\n∸1≗pred {suc _} = PE.refl\r\n```\r\n      `agda $agdaLibOpt --sharing Nat0.agda`\r\n\r\nreports\r\n```\r\nAn internal error has occurred. Please report this as a bug.\r\nLocation of the error: src/full/Agda/TypeChecking/CompiledClause/Match.hs:189\r\n```"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/150148828","html_url":"https://github.com/agda/agda/issues/1691#issuecomment-150148828","issue_url":"https://api.github.com/repos/agda/agda/issues/1691","id":150148828,"user":{"login":"mechvel","id":1506057,"avatar_url":"https://avatars.githubusercontent.com/u/1506057?v=3","gravatar_id":"","url":"https://api.github.com/users/mechvel","html_url":"https://github.com/mechvel","followers_url":"https://api.github.com/users/mechvel/followers","following_url":"https://api.github.com/users/mechvel/following{/other_user}","gists_url":"https://api.github.com/users/mechvel/gists{/gist_id}","starred_url":"https://api.github.com/users/mechvel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mechvel/subscriptions","organizations_url":"https://api.github.com/users/mechvel/orgs","repos_url":"https://api.github.com/users/mechvel/repos","events_url":"https://api.github.com/users/mechvel/events{/privacy}","received_events_url":"https://api.github.com/users/mechvel/received_events","type":"User","site_admin":false},"created_at":"2015-10-22T08:38:45Z","updated_at":"2015-10-22T08:38:45Z","body":"On Wed, 2015-10-21 at 15:29 -0700, WolframKahl wrote:\n> Sergei,\n> \n> I recommend that you try Andrea's patch from #1625 (comment) --- with\n> that and with --no-sharing I am getting the best results so far.\n> \n> Wolfram\n> \n> —\n> Reply to this email directly or view it on GitHub.\n\n\n\nThank you.\nSo far,  Dev Agda of Oct.19   has a bug #1695, so that I cannot use it\nin my program neither under  --no-sharing  nor under  --sharing.\n\nDo you suggest to apply this patch to  Development Agda of October 19 ? \n\nMay be, I need to wait for the development version to become a bit more\nstable. \n\n------\nSergei\n\n"}}