I’ve just implemented this in master, allowing implicits in arbitrary scopes, and it’ll be in the next hackage release. It’s not well tested yet though! I have at least tried the following simple examples, and a few others: appShow : Show a => ({b : _} -> Show b => b -> String) -> a … Read more
Edwin Brady has a repo full of demos at https://github.com/edwinb/idris-demos. Among other things, it has a playable space invaders game, written using SDL bindings, Effects, and the !-effect syntax (basically an alternate syntax to do-notation / >>=). Also, we attempt to maintain a listing of some available libraries on the wiki: https://github.com/idris-lang/Idris-dev/wiki/Libraries