This is correct but just delays the problem. It is still impossible to type level-generic functions (i.e. functions that work for all type levels).

The basic fundamental reality that no type theory has offered is an ability to type everything