Extensional equivalence and singleton types

We study the λS ≤ calculus, which contains singleton types S(M) classifying terms of base type provably equivalent to the term M. The system includes dependent types for pairs and functions ( and ) and a subtyping relation induced by regarding singletons as subtypes of the base type. The decidability of type checking for this language is non-obvious, since to type check we must be able to determine equivalence of well-formed terms. But in the presence of singleton types, the provability of an equivalence judgment M1 ≡ M2: A can depend both on the typing context and on the particular type A at which M1 and M2 are compared. We show how to prove decidability of term equivalence, hence of type checking, in λS ≤ by exhibiting a type-directed algorithm for directly computing normal forms. The correctness of nor-malization is shown using an unusual variant of Kripke logical relations organized around sets; rather than defining a logical equivalence relation, we work directly with (subsets of) the corre-sponding equivalence classes. We then provide a more efficient algorithm for checking type equivalence without constructing normal forms. We also show that type checking, subtyping, and all other judgments of the system are decidable