We study the $\miniMIL$ calculus, which
contains singleton types $\ks{\c}$ classifying terms of base
type provably equivalent to the term $\c$.  The system includes
dependent types for pairs and functions ($\Sigma$ and $\Pi$) 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
$\ec{\G}{\c_1}{\c_2}{\k}$ can depend both on the typing context $\G$
and on the particular type $\k$ at which $\c_1$ and $\c_2$
are compared.  \iffalse Thus, standard context-insensitive rewriting
methods are not directly applicable.  \fi

We show how to prove decidability of term equivalence, hence of type
checking, in $\lambdasingle$ by exhibiting a type-directed
algorithm for directly computing normal forms.  The correctness of
normalization 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
corresponding 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.

The $\miniMIL$ calculus models type constructors and kinds in the
intermediate language used by the TILT compiler for Standard~ML
to implement the SML module system.  The
decidability of $\miniMIL$ term equivalence allows us to show
decidability of type checking for TILT's intermediate language.  We
also obtain a consistency result that allows us to prove type safety
for the intermediate language.  The algorithms derived here form the
core of the type checker used for internal type checking in TILT.