"You can inspect types and build new types at compile time" is a key affordance of dependently typed languages.