{"action":"closed","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2216","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2216/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2216/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2216/events","html_url":"https://github.com/agda/agda/issues/2216","id":179469499,"number":2216,"title":"GHC backend error","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":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2016-09-27T11:40:08Z","updated_at":"2016-09-27T13:10:26Z","closed_at":"2016-09-27T13:10:26Z","body":"```\r\nprivate\r\n  absv : Float → Float\r\n  absv x with x <? 0.0\r\n  absv x | yes _ = -1.0 * x\r\n  absv x | no _ = x\r\n\r\nmean : ∀ {n} → Vec Float (ℕ.suc n) → Float\r\nmean xs = primFloatDiv (foldl _+_ 0.0 xs) (primNatToFloat (length xs))\r\n\r\nstandardDeviation : ∀ {n} → Vec Float (ℕ.suc n) → Float\r\nstandardDeviation xs = let μ = mean xs in mean ((λ x → absv (primFloatMinus x μ)) <$> xs)\r\n\r\nz-score : (μ σ x : Float) → Float\r\nz-score μ 0.0 x = 0.0\r\nz-score μ σ x = primFloatDiv (primFloatMinus x μ) σ\r\n```\r\n\r\nThe above code type checks, but when I try to compile it I get `An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/Compiler/ToTreeless.hs:194`.\r\n\r\nThe problem seems to be in `z-score` (probably the pattern match on `0.0`), because when I comment it out, the error goes away."}}
{"actor":{"display_login":"UlfNorell"}}