Function compile_nested_poly 

pub fn compile_nested_poly(
    ctx: &Context,
    decl: &NestedDecl,
    num_params: usize,
    levels: &[String],
) -> KernelResult<Compiled>

compile_nested_with_params for a universe-polymorphic family (UTree.{u} (α : Type u)).

Every emitted member is universe polymorphic over exactly the declaration’s levels and lives in the declaration’s own sort; the inductive, its siblings and their constructors are referenced at exactly those levels. An occurrence of the inductive at any other universe instance is non-uniform and refused, as Lean refuses it.