Idris 0.9.7 released

A new version of Idris, 0.9.7, has been released on hackage. There are only a few user visible changes.

  • implicit keyword, for implicit type conversion
  • Added Effects package, accessed with -p effect
  • Primitives for 8,16,32 and 64 bit integers

There is a small number of internal changes, some of them very large:

  • Changed unification so that it keeps track of failed constraints in case later information helps to resolve them
  • Distinguishing parameters and indices in data types
  • Faster termination/coverage checking
  • Split ‘javascript’ target into ‘javascript’ and ‘node’

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on