find universe level dependencies among applications

Stream: lean4

[Thomas Murrills]

To prevent an #xy issue, here's the full context: given an expression of the form .app (.app (... (.app f a)...) y ) z, I'm writing a function which (lambda-)abstracts the last n explicit arguments "as much as possible". "As much as possible" means that if there's e.g. an implicit argument α which is in the backwards dependencies of to-be-abstracted arguments—but not in the backwards dependencies of anything else—it gets abstracted as well.

I have code that does this just fine typically, but it relies on the backDeps field of elements of (← getFunInfo f).paramInfo to figure out dependencies. This means that universe levels aren't accounted for.

Is there some similar data to backDeps for figuring out universe level dependencies hidden somewhere, and for replacing existing levels with level mvars? I'm unfamiliar with the particulars of resolving levels, so I might be confused as to "when" this all needs to happen.

If not, would it at least maybe be possible to take the "nuclear option" and erase universe levels everywhere in the expression, then re-infer them? If f happens to be a .const, this might be easy enough to do (untested), but this isn't fully general—plus, I'd hope there's a cleaner option! :)