Idris 0.9.20 released

A new version of Idris, 0.9.20, has been released. You can find this on hackage, or from the download page. Documentation is available from Updates are detailed below.

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

Language updates

  • Improved unification by implementing a pattern unification rule
  • Changed scoping rules for unbound implicits: any name which would be a valid unbound implicit is now always an unbound implicit. This is much more resilient to changes in inputs, but does require that function names be explicitly qualified when in argument position.
  • Name binding in patterns follows the same rule as name binding for implicits in types: names which begin with lower case letters, not applied to any arguments, are treated as bound pattern variables.
  • The previous syntax for tactic proofs and the previous interactive prover are now deprecated in favour of reflected elaboration. They will be removed at some point in the future.
  • The syntax `{{n}} quotes n without resolving it, allowing short syntax for defining new names. `{n} still quotes n to an existing name in scope.
  • A new primitive operator prim__strSubstr for more efficient extraction of substrings. External code generators should implement this.
  • Added %deprecate directive, which gives a warning and a message when a deprecated name is referenced.

Library updates

  • The Neg class now represents numeric types which can be negative. As such, the (-) operator and abs have been moved there from Num.
  • A special version of (-) on Nat requires that the second argument is smaller than or equal to the first. minus retains the old behaviour, returning Z if there is an underflow.
  • The (+), (-), and (*) operations on Fin have been removed.
  • File IO operations (for example openFile/fread/fwrite) now return Either FileError ty where the return type was previously ty to indicate that they may fail.
  • New Logging Effects have been added to facilitate logging of effectful programmes.
  • Elaborator reflection is now a part of the prelude. It is no longer necessary to import Language.Reflection.Elab.
  • The PERF effect allows for simple performance metrics to be collected from Effectful programs.
  • Some constructors that never actually occurred have been removed from the TT and Raw reflection datatypes in Language.Reflection.

Tool updates

  • Records are now shown as records in :doc, rather than as the underlying datatype
  • iPKG files have a new option pkgs which takes a comma-separated list of package names that the idris project depends on. This reduces bloat in the opts option with multiple package declarations.
  • iPKG files now allow executable = "your filename here" in addition to the existing executable = yourFilenameHere style. While the unquoted version is limited to filenames that look like namespaced Idris identifiers (, the quoted version accepts any valid filename.
  • Add definition command (\d in Vim, Ctrl-Alt-A in Atom, C-c C-s in Emacs) now adds missing clauses if there is already a definition.

Miscellaneous updates

  • Disable the deprecation warnings for %elim and old-style tactic scripts with the --no-elim-deprecation-warnings and --no-tactic-deprecation-warnings flags.