[jessaustin]

Maybe I'm misunderstanding, but Kutta's description seems to handle 1) and 2) just fine. An additional requirement of "guaranteeing 'yes' on every correctly typed program" would lead to contradiction, but the point is that you don't need that requirement in practice.

[Kutta]

You're not misunderstanding. In short, we should rightfully expect our dependent type checker to be sound, if not complete. Weaker, non-dependent type systems can have complete checkers though, see for example

http://www.mpi-sws.org/~neelk/bidir.pdf

[dllthomas]

Hmm. Conceivably. I will have to revisit when I have more bandwidth.