> Agda and Coq retain inference and decidability by sacrificing Turing completeness. I don't know if I would phrase it that way, but there's a more important s

> Agda and Coq retain inference and decidability by sacrificing Turing completeness. I don't know if I would phrase it that way, but there's a more important slight of hand going on here and I think chongli was right in spirit. Haskell takes care of (most) type level things for you with inference. Coq and Agda allow you to give very precise types to things, but those very precise types involve values that are not automatically inferred for you. It's certainly not the case that you can write the same annotation-free function in Coq that you would have written in Haskell and have a very precise type inferred for you.