Clojure has little relevance to functional programming: functions are the smoke, but types are the fire. F# might be a good choice for an introduction though (if you're willing to sacrifice the good parts of ML for the bad parts of .Net).
Scala and Haskell both have (in decreasing order) massively more complicated type systems than Idris, so I would certainly not recommend those! Moreover, good Scala and Haskell code tends to be way more difficult to understand initially than good Idris code. YMMV.
An introductory language needs to be simple enough that a learner can hold all of it in her/his head. SML and Idris fit that bill, IMO, in a way that Haskell and Scala cannot.
I don't know that much about Idris, but from my understanding, its type system is more advanced than Haskell's, because dependent types by definition contain more information than the (independent?) types used in Haskell (can't comment on scala). Haskell as a language with all of its various extensions and bells and whistles is surely far more complicated, having been around a great deal longer and with a massive compiler and numerous features, but from my knowledge it's incorrect to say Idris is simpler than Haskell, at least in regards to its type system.
Idris's types system is both more advanced and simpler than Haskell's. For example, "vanilla" Haskell's type system implements (amongst other things) functions, records, parametric polymorphism and typeclasses. Idris implements (amongst other things) dependent functions and dependent records.
Idris doesn't need to support (non-dependent) functions or parametric polymorphism, since they're just special-cases of dependent functions. Likewise, typeclasses are just special-cases of dependent records.
When we consider Haskell extensions, many of them are designed to introduce dependently-typed idioms (eg. DataKinds). This makes Idris automatically simpler, since it supports those idioms directly and doesn't have to offer all of the non-dependent parts of Haskell.
On the other hand, typical Haskell programs may use types in a simpler way than typical Idris programs, but that's a separate point. We can focus on simple programs while learning.
To be fair, Idris does not in general support parametric polymorphism, though you could extend it to do so.
Idris has a quantifier which is called Pi in type theory, and this is not the same as Forall (the quantifier present in Haskell and ML). Forall gives you guarantees about uniform behavior over the domain of quantification (this is parametricity), whereas Pi does not.
Idris does however recover parametricity anyway for types, since it lacks an eliminator for the universe (i.e. it doesn't have type-case). But it doesn't have parametric polymorphism for values.
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.
Scala and Haskell both have (in decreasing order) massively more complicated type systems than Idris, so I would certainly not recommend those! Moreover, good Scala and Haskell code tends to be way more difficult to understand initially than good Idris code. YMMV.
An introductory language needs to be simple enough that a learner can hold all of it in her/his head. SML and Idris fit that bill, IMO, in a way that Haskell and Scala cannot.