Type inhabitation

In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem:^[1] given a type ${\displaystyle \tau }$ and a typing environment ${\displaystyle \Gamma }$, does there exist a ${\displaystyle \lambda }$-term M such that ${\displaystyle \Gamma \vdash M:\tau }$? With an empty type environment, such an M is said to be an inhabitant of ${\displaystyle \tau }$.