Idris 0.9.12 released

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

The tutorial has also been updated.

There are some changes in this release which may break old code, specifically laziness, codata and the effects library have been significantly updated. Full details are in the new tutorial, and in the Effects tutorial.

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.

Being research software, 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

Details of the new feature and updates follow.


Laziness is now implemented via the type system, using the following constructs:

Lazy : Type -> Type
Delay : a -> Lazy a
Force : Lazy a -> a

Both Delay and Force may be left implicit, so laziness is usually silent apart from an explicit Lazy in a type, e.g.

boolCase : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
boolCase True  t e = t
boolCase False t e = e


Similarly, codata is now implemented via the type system, using the following constructs:

Inf : Type -> Type
Delay : a -> Inf a
Force : Inf a -> a

Again, both Delay and Force may be left implicit. Data types may mix data and codata. Old style codata declarations are still supported, where Inf is added implicitly. The following declarations are therefore equivalent:

codata Stream : Type -> Type where
  (::) : a -> Stream a -> Stream a

data Stream : Type -> Type where
  (::) : a -> Inf (Stream a) -> Stream a

Lazy and Inf are closely related (in fact, the underlying implementation uses the same type). The only difference in practice is in totality checking, where Lazy is erased (i.e. terms are checked for termination normally, ignoring laziness annotations), and Inf uses a productivity checker, where any use of Delay must be constructor guarded.

Metavariables in types

Proof search now works for metavariables in types, giving some interactive type inference. For example:

vec : ?vtype
vec = with Vect ["a","b","c"]

This can either be solved interactively, using :ps at the REPL, or the appropriate vim mode or emacs mode commands. e.g. assuming it is defined on line 37 of vtest.idr:

*vtest> :ps 37 vtype
Vect 3 String

Alternatively, it can be solved explicitly in code:

vec : ?vtype
vec = with Vect ["a","b","c"]

vtype = proof search

Documentation comments

There is a new syntax for inline documentation. Documentation starts with |||, and
arguments are documented by preceding their name with @. For example:

||| Add two natural numbers
||| @ n the first number (examined by the function)
||| @ m the second number (not examined)
plus (n, m : Nat) -> Nat

Other changes

There have been several improvements in robustness and efficiency. Other changes are:

  • JavaScript and Node codegen now understand the %include directive.
  • Concept of null is now understood in the JavaScript and Node codegen.
  • Lots of performance patches for generated JavaScript.
  • New commands :eval (:e) and :type (:t) in the prover, which either normalise or show the type of expressions.
  • Allow type providers to return postulates in addition to terms.
  • Syntax for dealing with match failure in <- and pattern matching let.
  • Allow the auto-solve behaviour in the prover to be disabled, for easier debugging of proof automation. Use :set autosolve and :unset autosolve.
  • Updated effects library.
  • New :apropos command at REPL to search documentation, names, and types.
  • Unification errors are now slightly more informative.
  • Add covering function option, which checks whether a function and all descendants cover all possible inputs (subset of total).