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 c

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 http://www.mpi-sws.org/~neelk/bidir.pdf