Maybe Haskell is bad from practical perspective, but not from theoritical. So it has a strong appeal towards academics and purists.
> It is as if Haskell doesn’t want “normal” people to understand it
Well, yeah kind of. I don't think it's as hostile as that though, the language isn't actively against "normal" people (I guess, that means your common or garden OOP programmer) it just doesn't actively court them.
The comments about how the community treat newcomers are quite interesting though and if they are true then that's pretty shitty behaviour. It's one thing if the language isn't aimed at a given demographic of programmers, but it's another thing for people to use it as an excuse to beat down and berate others.
I mean, joking aside, it's always fascinating when people can't wrap their minds around the idea that their criteria for success or quality or goodness are subjective and not universal.
Agda is so “correct” that the language is total and not Turing complete with the exception of a “partiality monad” that allows for partial and Turing complete computations — similarly to how Haskell isolates effects on the world from the main language and encapsulates them into a special type, Agda isolates partial computations.
And this language is very much used within specific academic fields.