We say that a system is a computational type theory if it is a type theory defined by not a bunch of inference rules, but some sort of Martin-Löfian meaning explanations (e.g. in the sense of NuPRL). Now according to Martin-Löf's meaning explanations [1], a hypothetical judgment of the form $$ x_1 : A_1, ..., x_n : A_n \vdash a : A \qquad\qquad\qquad\qquad\qquad\qquad (1)$$ means that $$ \vdash a[x_1,...,x_n/a_1,...,a_n] : [x_1,...,x_n/a_1,...,a_n]A \qquad (2)$$ for all closed terms $a_1 : A_1, ..., a_n : A_n$ (and also that this judgment should be functional in respect to judgmental equality, but I don't need to tackle this issue here).
This means, among other things, that the judgment $$ x : \mathsf{empty} \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad\qquad\qquad\quad (3)$$ is derivable in the theory, since there are no closed terms of the empty type (for the condition given is vacuously true). But also that less obvious judgments are also vacuously evident: $$ x : \mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty}) \vdash \mathsf{1} : \mathsf{nat} \to \mathsf{nat} \qquad\qquad\qquad\qquad (4)$$ since any closed term of $\mathsf{nat} \times (\mathsf{nat} \to \mathsf{empty})$ gives us a closed term of $\mathsf{empty}$, which should have none.
My question is:
What is a nice way to implement a type checker for such a hypothetical judgments?
(I'm aware that the problem is undecidable in general, but in theory this should affect us only in the sense that we are unable to rule out all invalid judgments).
For simplicity, we can suppose that we already have a type checking algorithm for categorical judgments.
IMHO$-$and in the spirit of the universal introduction rule of predicate logic$-$the obvious type checking algorithm for (1) to say that it is valid whenever $$\vdash a[x_1,...,x_n/t_1,...,t_n] : [x_1,...,x_n/t_1,...,t_n]A$$ for a list of arbitraries closed terms $t_1 : A_1 ,..., t_n : A_n $ (since we can't possibly consider each closed term of such types). However, this algorithm is clearly unable to validate sequents such as (3), let alone (4).
There is a quick highly-inelegant fix, which is to add the condition that if you find $x : \mathsf{empty}$ in the context list, halt and automatically recognize the whole sequent as true. But what about not-so-evident vacuously evident judgments such as (4)?
Anyway, how would a correct, elegant and general approach look like?
PS: I'm sorry if the question is not precise enough, but I can't think of a better way to state it.
[1] Martin-Löf, Constructive Mathematics and Computer Programming, 1982.
