Coq and Agda are both based on dependent types, but Agda is more of an in-progress research language whereas Coq is currently quite useful for doing proofs in p

Coq and Agda are both based on dependent types, but Agda is more of an in-progress research language whereas Coq is currently quite useful for doing proofs in practice. Haskell doesn't have full support for dependent types (yet). The Haskell community is very cautious with adding features that make type inference undecidable (like dependent types), so what people do is gradually add type system features onto GHC and then gate them behind feature flags. So you can do some of the things you can do in Agda in Haskell (like GADTs, kind promotion, limited type functions, etc.) but not everything. The advantage of Haskell's conservative approach is that it's actually very useful for writing programs, whereas Coq is only really meant for writing proofs and Agda is more of a research testbed than a production language.