Hacker News Reader

It's not intending to be a general purpose language, and as such doesn't have a lot of features that make software engineering easier. In fact, it intentionally has a phenomenally slow compiler, because the compiler is solving or attempting to solve various NP-Complete problems simultaneously.

Think of it as a language that will help build tools, analyzers, and possibly linkable libraries for small scale but highly security-critical components, but not necessarily the language you want to use to build an app server.

although, if you don't use any refinement types in your program, i don't see why you can't write general purpose programs and extract code to Ocaml and F#

Lean is quite nice dependently typed language https://leanprover.github.io/

What do you think of Idris?

Idris certainly is nice but I doubt anyone uses it for real stuff.