Idris 0.9.16 released

A new version of Idris, 0.9.16, has been released. You can find this on hackage, or from the download page.

The tutorial has also been updated.

Thanks as always to everyone who has contributed, either with code, documentation or by testing and reporting issues. You can find the names of all contributors in the CONTRIBUTORS file in the source repository.

Idris is still research software, so we expect there to be bugs. Please don’t keep them to yourself! If you find any problem, please report it on the github issue tracker. It is very helpful if you can also provide a small test case which reproduces your problem.

Also, do let us know how you get on in general either via the mailing list or the #idris channel on

The main new features and updates are:

  • Inductive-inductive definitions are now supported (i.e. simultaneously defined types where one is indexed by the other)
  • Implicits and type class constraints can now appear in scopes other than the top level
  • Importing a module no longer means it is automatically reexported. A new public modifier has been added to import statements, which will reexport the names exported from that module
  • Implemented @patterns. A pattern of the form x@p on the left hand side matches p, with x in scope on the right hand side with value p
  • Vect, Fin and So moved out of prelude into base, in modules Data.Vect, Data.Fin and Data.So respectively
  • A new tactic sourceLocation that fills the current hole with the current source code span, if this information is available. If not, it raises an error
  • :search and :apropos commands can now be given optional package lists to search
  • Better Unicode support for the JavaScript/Node codegen
  • Modules can now have API documentation strings

Additionally, several long-standing issues have been resolved, particularly with pattern matching and coverage checking.