{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1712","labels_url":"https://api.github.com/repos/agda/agda/issues/1712/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1712/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1712/events","html_url":"https://github.com/agda/agda/issues/1712","id":115191945,"number":1712,"title":"__IMPOSSIBLE__ triggered in conApp","user":{"login":"Blaisorblade","id":289960,"avatar_url":"https://avatars.githubusercontent.com/u/289960?v=3","gravatar_id":"","url":"https://api.github.com/users/Blaisorblade","html_url":"https://github.com/Blaisorblade","followers_url":"https://api.github.com/users/Blaisorblade/followers","following_url":"https://api.github.com/users/Blaisorblade/following{/other_user}","gists_url":"https://api.github.com/users/Blaisorblade/gists{/gist_id}","starred_url":"https://api.github.com/users/Blaisorblade/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Blaisorblade/subscriptions","organizations_url":"https://api.github.com/users/Blaisorblade/orgs","repos_url":"https://api.github.com/users/Blaisorblade/repos","events_url":"https://api.github.com/users/Blaisorblade/events{/privacy}","received_events_url":"https://api.github.com/users/Blaisorblade/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-11-05T01:52:29Z","updated_at":"2015-11-05T18:23:21Z","closed_at":null,"body":"I have a non-minimized bug report on a codebase of mine, that I wanted to port from Agda 2.4.0.2 to Agda 2.4.2. For now I fear I'll have to suspend the effort, because of this Agda crash.\r\n\r\nWith [this commit](https://github.com/inc-lc/ilc-agda/commit/52d780fa6fc41420c5854ec8cf38978b0671285c), with Agda 2.4.2.4, I get\r\n```\r\n  Checking Parametric.Change.Validity (/Users/pgiarrusso/AeroFS/Repos/ilc-agda-bluevelvet/Parametric/Change/Validity.agda).\r\nconApp: constructor Base.Change.Algebra.ChangeAlgebraFamily.family with fields [Base.Change.Algebra.ChangeAlgebraFamily.change-algebra] projected by Base.Change.Algebra.ChangeAlgebra.Change\r\nAn internal error has occurred. Please report this as a bug.\r\nLocation of the error: src/full/Agda/TypeChecking/Substitute.hs:108\r\n```\r\n[Relevant location](https://github.com/agda/agda/blob/2.4.2.4/src/full/Agda/TypeChecking/Substitute.hs#L108).\r\n\r\nWith 2.4.2, I think I get the same error:\r\n```\r\n  Checking Parametric.Change.Validity (/Users/pgiarrusso/AeroFS/Repos/ilc-agda-bluevelvet/Parametric/Change/Validity.agda).\r\nconApp: constructor Base.Change.Algebra.ChangeAlgebraFamily.family with fields [Base.Change.Algebra.ChangeAlgebraFamily.change-algebra] projected by Base.Change.Algebra.ChangeAlgebra.Change\r\nAn internal error has occurred. Please report this as a bug.\r\nLocation of the error: src/full/Agda/TypeChecking/Substitute.hs:92\r\n```\r\n[Relevant location]\r\n(https://github.com/agda/agda/blob/2.4.2/src/full/Agda/TypeChecking/Substitute.hs#L92).\r\n\r\nBoth traces are reproducible in a checkout with\r\n```\r\nagda-2.4.2.4 +RTS -s -RTS -i . -i $AGDA_LIBRARY_PATH Parametric/Change/Validity.agda\r\n```\r\nwith the Agda standard library for 2.4.2.4, commit agda/agda-stdlib@f071e972bbf01f778545df88fcf3fa0465ebc1e2.\r\n\r\nShould this be relevant, this codebase uses instance parameters, heavily parameterized modules, and lots of reexports."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/154144301","html_url":"https://github.com/agda/agda/issues/1712#issuecomment-154144301","issue_url":"https://api.github.com/repos/agda/agda/issues/1712","id":154144301,"user":{"login":"asr","id":635804,"avatar_url":"https://avatars.githubusercontent.com/u/635804?v=3","gravatar_id":"","url":"https://api.github.com/users/asr","html_url":"https://github.com/asr","followers_url":"https://api.github.com/users/asr/followers","following_url":"https://api.github.com/users/asr/following{/other_user}","gists_url":"https://api.github.com/users/asr/gists{/gist_id}","starred_url":"https://api.github.com/users/asr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/asr/subscriptions","organizations_url":"https://api.github.com/users/asr/orgs","repos_url":"https://api.github.com/users/asr/repos","events_url":"https://api.github.com/users/asr/events{/privacy}","received_events_url":"https://api.github.com/users/asr/received_events","type":"User","site_admin":false},"created_at":"2015-11-05T18:23:21Z","updated_at":"2015-11-05T18:23:21Z","body":">> The issue is fixed in the master branch\r\n\r\n> Really?\r\n\r\nYou are right. I neither know if the issue is fixed in master.\r\n\r\n"}}