{"action":"opened","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2342","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2342/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2342/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2342/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2342","id":84232001,"number":2342,"title":"INTERNAL ERROR: Nothing to fill in.","user":{"login":"jfdm","id":331273,"avatar_url":"https://avatars.githubusercontent.com/u/331273?v=3","gravatar_id":"","url":"https://api.github.com/users/jfdm","html_url":"https://github.com/jfdm","followers_url":"https://api.github.com/users/jfdm/followers","following_url":"https://api.github.com/users/jfdm/following{/other_user}","gists_url":"https://api.github.com/users/jfdm/gists{/gist_id}","starred_url":"https://api.github.com/users/jfdm/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jfdm/subscriptions","organizations_url":"https://api.github.com/users/jfdm/orgs","repos_url":"https://api.github.com/users/jfdm/repos","events_url":"https://api.github.com/users/jfdm/events{/privacy}","received_events_url":"https://api.github.com/users/jfdm/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-06-02T22:02:17Z","updated_at":"2015-06-02T22:02:17Z","closed_at":null,"body":"Playing around with Effects and this logging effect causes an internal error on Line 46 col 7\r\n\r\n```idris\r\n||| A logger with custom logging levels.\r\n||| This doesn't compile due to strange internal error.\r\nmodule Effect.AdvLogger\r\n\r\nimport Effects\r\n\r\n||| The Logging API\r\ndata Logging : Effect where\r\n    Log : (Eq a, Show a, Ord l) =>\r\n          (lvl:l) -> (cs : List a) -> (msg : String)\r\n        -> Logging () (l, List a) (\\v => (l, List a))\r\n\r\n||| The Logging Effect\r\n||| @lTy The type of the logging levels\r\n||| @cTy The type of the categories.\r\nLOG : (lTy : Type) -> (cTy : Type) -> EFFECT\r\nLOG lTy cTy = MkEff (lTy, List cTy) Logging\r\n\r\n||| Logging in IO\r\ninstance Handler Logging IO where\r\n    handle (l,cs) (Log lvl cs' msg) k = do\r\n      case compare lvl l of\r\n        GT => k () (l,cs)\r\n        _  =>  do\r\n          let res = and $ map (\\x => elem x cs') cs\r\n          let prompt = if isNil cs then \"\" else show cs\r\n          if res || isNil cs\r\n            then do\r\n              printLn $ unwords [prompt, \":\", msg]\r\n              k () (l,cs)\r\n            else k () (l,cs)\r\n\r\n||| The log function.\r\nlog : (Show a, Eq a, Ord l) =>\r\n      l -> List a -> String -> Eff () [LOG l a]\r\nlog lvl cs msg = call $ Log lvl cs msg\r\n\r\n--- Example Innvocation\r\nnamespace Main\r\n  doubleFunc : Nat -> Eff Nat [LOG Nat String]\r\n  doubleFunc x = do\r\n    log 2 [\"NumOps\"] $ unwords [\"Doing the double with\", show x ]\r\n    pure (x+x)\r\n\r\n  main : IO ()\r\n  main = do\r\n     x <- runInit [(2,[\"NumOps\"])] (doubleFunc 3)\r\n     printLn x\r\n\r\n-- Local Variables:\r\n-- idris-packages: (\"effects\")\r\n-- End:\r\n```"}}