BTW, since I just realized I was insufficiently clear about the Coq example, I should clarify--in a dependently typed language, synthesizing the right type can

BTW, since I just realized I was insufficiently clear about the Coq example, I should clarify--in a dependently typed language, synthesizing the right type can actually require synthesizing a well-typed term (this is where the dependency comes in, after all), so it's not generally easier to synthesize types than terms in such a language. You need a sufficiently complex dependently-typed program for this to start separating itself from "ordinary" difficulties with type inference in practice, but when you start playing around with indexed vectors you run into situations like this a lot--cases where you struggle to even be able to write down the thing you're trying to prove, because the type is only well-formed in a particular context and you need to essentially prove to the compiler that you are in such a context for type inference to remain decidable. For example, to write down (not prove!) an equality between two vectors indexed by their length, at least in Coq (and other type theories without extensional equality, which is in general undecidable), you have to first show that they have the same length--otherwise the expressions are not well-typed. The length can be any well-typed term of type nat, and like I said before Coq is far more than powerful enough to express Peano arithmetic, so you can see already that synthesizing an equality type between two vectors is just as difficult as proving an equality between two natural numbers, so it is very much undecidable in general. In fact, it is quite difficult to write down in practice even in some surprisingly simple cases! The actual proof term, however, is usually something like a pattern match on some other equality followed by the creation of a function that pattern matches on another equality, etc. down the line, until it returns the unhelpful constructor `eq_refl` (which basically just says `x = x`). So all of the interesting work in such cases has transferred to the type system, with the proof term basically just there to perform type casts and coercions.