> As the typed FP ecosystem is moving towards dependent typing (Agda, Idris, Lean)

I'm not really sure where the borders of "the typed FP language ecosystem" would be but feel pretty certain that such a thing would enclose also F#, Haskell, and OCaml. Any one of which has more users and more successful "public facing" projects than the languages you mentioned combined. This is not a dig on those languages, but they are niche languages even by the standards of the niche we're talking about.

You could argue that they point to the future but I don't seriously believe a trend among them represents a shift in the main stream of functional programming.