> Type-checking is undecidable. This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e.

> Type-checking is undecidable. This is only true if you allow non-total functions in your types, which most dependently-typed languages don't by default (i.e. the condition implied by your soundness condition). By default in e.g. both Idris and Agda type-checking is decidable.