Function explicit_levels 

pub fn explicit_levels(ctx: &Context, t: &Term) -> Term

The levels the Term kernel’s application rule infers for a bare reference to a universe-polymorphic declaration (type_checker::implicit_levels_for_head), written out. The declaration’s level parameters become metavariables; left to right, each argument whose domain mentions one solves it from the argument’s type; a head whose every level is solved becomes Const at those levels. A head left with an unsolved level stays a bare reference, which the core refuses rather than guesses at.

This is elaboration, outside the trusted core: the core checks the explicit term it produces, so a level chosen wrongly here can only make a declaration fail, never let one through.