A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance