We won't get anywhere without a definition, but I think most would disagree about the Clojure coment. They even assert it on the home page http://clojure.org . It's probably better to think of FP as a continuum rather than black and white.
While Idris may be able to eliminate some of the typing constructs in Haskell, I don't think one can say it would be easier to program in than Haskell. The chain of having to assert proofs to the compiler is an extra burden (i.e. refl).
Also, saying that a Pure FP language (Idris) is easier than a non-pure language (Scala), for someone without extensive FP backround, is an interesting comment. Part of the intimidation of Haskell is it's purity, and this extends to Idris.
"Practical" Haskell programming very quickly devolves into carefully constructed stacks of monad transformers. "Practical" Idris programming lives in a modality of extensible effects. These are objectively easier to get started with.
(Moreover, I did also include SML in my list of languages better for beginners than Haskell and Scala incidentally. If the purity is the problem, then SML is a great place to start. Begin with proving by induction that an SML program is pure or impure—this will motivate having it internalized in the type theory.)
Moreover, you don't even need to use the "proving" parts of Idris. You can use the fragment of Idris which is a fixed Haskell, and move on up to the more interesting bits when they become useful to you. For instance, you can write partial programs (and coprograms) in Idris without doing any proofs; then at the end, you can have someone help you shore it up with proofs that it is sound.
While Idris may be able to eliminate some of the typing constructs in Haskell, I don't think one can say it would be easier to program in than Haskell. The chain of having to assert proofs to the compiler is an extra burden (i.e. refl).
Also, saying that a Pure FP language (Idris) is easier than a non-pure language (Scala), for someone without extensive FP backround, is an interesting comment. Part of the intimidation of Haskell is it's purity, and this extends to Idris.