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 f

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