Uniqueness types[1], which are inspired by ownership types and borrowed pointers in the Rust language, and should eventually be able to provide compile-time guarantees that critical program fragments will never allocate. If this was achieved, Idris would potentially be usable for tasks that previously necessitated using either C, C++ or Rust.
Partial evaluation[2], which can also be used to improve performance by specialising type classes and higher order functions. Another use is creating speedy interpreters/EDSLs, with the one in [3] being competitive in speed with Java in spite of only being an interpreter.
Uniqueness types can also be used for safe in-place updates of a datastructure. The following map function, for instance, where UList is a UniqueType, will be compiled to code that updates the list in-place, avoiding allocating a new list:
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
2. https://github.com/idris-lang/Idris-dev/wiki/Static-Argument...