Basically design in dependent types into the language right from the beginning (like Iris) - such that types are first class and can be computed and manipulated

Basically design in dependent types into the language right from the beginning (like Iris) - such that types are first class and can be computed and manipulated like any other language construct.