So now I can rephrase my original question. It might still be naive and vague, but it’s not based on complete ignorance. It’s the best I can do, and it does capture what I am wondering about.
I’ve been learning Idris. I didn’t know anything about dependent types before this point, but I think dependent typing is great–useful, powerful, elegant, interesting, fun–and Idris makes it pretty easy to use, I feel. Not always conceptually easy, but the syntax seems quite natural. And it’s just fascinating.
[“learning Idris”: So that there’s no misunderstanding, one might think that this means I have a deeper understanding of Haskell or Agda or something else than I do. What it means is that I know bits of basic Haskell and I’m working through Edwin Brady’s Type-Driven Development with Idris using Idris 2. Glancing through that book would show roughly what my level of understanding is like.]
So what I was wondering–this was what I originally wanted to know, but didn’t ask about–is how soon dependent types in Haskell will have similar capabilities to DT in Idris, and syntactic convenience that is close to that of DT syntax in Idris. (I’m not expecting identical syntax, and I understand that because of the additional capabilities and syntax of Haskell, it’s possible that DT syntax for Haskell might turn out to be a little less nice than in Idris. That’s why I said “close to”.)
Or, come to think of it, what I really want to know is–when I can have this much fun and power in Haskell–along with everything else that Haskell has to offer.
I’m not expecting that a good answer is possible at this point. “Who knows?” is probably appropriate. Or: “I don’t know what you really mean.” (Because I don’t think I can spell it all out.)