Type checking must be performed in any case, at some level. If we use intrinsic embedded syntaxes, then the implementation of the metalanguage (in a meta-metalanguage) does the type checking. Hence, if we intend to formalize a syntax of type theory which is intended as a metatheoretical setting for mathematics, then I think decidability is quite important.
If we don't intend our type theory to be used as a metatheoretical setting for mathematics, it seems interesting to consider for example a type theory with a family of base types indexed by the circle, the syntax of which I think would not form a set.
That is, if we have a way to represent dependent type theory in Coq, what happens if we add a constructor `a_circle_of_types : circle -> type` to our syntax (for a postulated circle, or HIT)? This should be consistent, to add a family of uninterpreted types, but I believe equality is no longer decidable (since equality of circle is not decidable).
- Jasper Hugunin