I've got a few network services working with Idris and they run okay. The compilation time grows so quickly you can't use it for very large projects though.

Honestly, Haskell dependent-typing is SO MUCH MORE COMPLEX than Idris's "well what if I just write a function that takes a type?" approach, it's not even funny. Even the author of singleton says it's a rough landscape.

Haskell's going to get much closer with QuantifiedConstraints in ghc 8.6, in that it'll simplify a lot of this work, but it's still years out from the simplicity and library unification.

Can you elaborate on the DT / QuantifiedConstraints connection a bit? I haven't thought enough yet about QuantifiedConstraints to see the everyday benefits, but I'm getting contact-excited by everybody else's anticipation of it. I'd love to get some concrete benefits to hold in mind.

I’ve often thought Idris would be useful for expressing the core business logic of your program, and the you’d use the Haskell or JS backend to do the user-facing parts.

For me it was also very interesting read, and I also reached a similar conclusion.

Such language features are still too complex for the regular kind of software development many of us do, as the whole team has to fully grasp it.

Any thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive libraries that Haskell brings to the table.

Usually, Agda programs would not use Haskell libraries very much, even though they could. The reason seems to be that it is an unstable language and we are still figuring out how to do dependent types correctly. To me, working in Agda is like working in a very powerful version of Haskell, but for most people it's more about working in a research language. Idris and Agda are quite similar: don't build a company on them, but expect really cool ideas to spawn from them. Dependent types is really an awesome idea.