> I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice. Edit (too late to edit the original comment): After

> I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice. Edit (too late to edit the original comment): After thinking about the kinds of type errors I've seen in my proofs, I think Coq's inference algorithm is based on unification (not bidirectional?). Whatever it is, it's quite nice to work with in any case.