Idris 0.9.18 released

A new version of Idris, 0.9.18, 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 changes

  • There is a new syntax for records, corresponding to type class syntax (which is also a record-like structure). See dependent records in the documentation
  • Records can now be coinductive, using the corecord keyword
  • Type class constructors can be given user accessible names (corresponding to the new record syntax)
  • if...then...else is now built in syntax rather than a syntax macro, desugaring to ifThenElse. This is for cleaner overloading and better error messages in domain specific languages.
  • Pattern matching lambdas and case expressions can now be labelled impossible, in
    the same way as top level patterns
  • Added a %hint function annotation, which allows functions to be used in proof search for auto arguments. Only functions which return instances of a data or record type are allowed as hints
  • Strings are now UTF8 encoded, and Idris source is assumed to be UTF8 encoded
  • Some reorganisation of primitives:
    • Buffer and BitVector removed (due to insufficient testing and lack of a maintainer)
    • Float renamed to Double
    • Externally defined primitives now supported with %extern directive
    • Ptr and ManagedPtr removed and replaced with external primitives
  • New quotation syntax `{n} for a quotation of the reflected representation of the name n. If n is lexically bound, then the resulting quotation will be for it, whereas if it is not, then it will succeed with a quotation of the unique global name that matches
  • As usual, lots of improvements and fixes in elaboration, especially with type class resolution
    and name disambiguation

Library changes

  • The default Semigroup and Monoid instances for Maybe are now prioritised choice, keeping the first success as Alternative does. The version that collects successes is now a named instance
  • The return types of Vect.findIndex, Vect.elemIndex and Vect.elemIndexBy were changed from Maybe Nat to Maybe (Fin n)

Tool changes

  • :exec REPL command now takes an optional expression to compile and run/show
  • A new :browse command shows the contents of a namespace
  • Agda-style semantic highlighting is supported over the IDE protocol