We outline a new approach to showing the decidability of type checking for type theories with beta-eta-equality, relevant to foundations for modules systems and type theory-based proof systems. The key to the approach is a syntactic translation mapping terms in the beta-eta presentation into their full eta-expansions in the beta presentation. Decidability of type checking is lifted from the target beta presentation to the beta-eta presentation. The approach extends to other inductive types with a single constructor, and is demonstrated for singleton types and sigma-types.