Actually, there is no need to lower the level here, as this is already done by the call to rue.
However, there is no need to lower the level in funct either, so just remove the line.

In principal mode, the code type_sfunct above would call generalize_structure on funct.exp_type, which puts it at generic level, right? Could it be that the line you removed is meant to un-do that generalization, and should stay?

Looking at the git history, relevant commits are 0a82360, which introduced the generalization of func.exp_type (with a matching instance call at the end of application typing) and 0edba97, which turned the instance call into the manual lowering there is in trunk.

Yes, we already checked the history, but I'm still not clear why this would be needed.
It is only useful if the original type of funct.exp_type escapes in the type of the application, but my intuition would be that we only use instances of it when typing the application. I will check again, but this looks like a spurious step.