[cies]

For me Idris has best type holes.

[dannyobrien]

Yes, and Idris actively encouraged iterative development that was based around its holes -- the book by Idris' creator Edwin Brady, Type-Driven Development[1], is an eye-opening introduction to this style of coding.

[1] - https://www.manning.com/books/type-driven-development-with-i...