When a sort poly constant is translated, the sort variable is not propagated and thus substituted with Type instead.
Given that the names of universe level change also, I suspect that the instance is not propagated at all, and
infer again at definition time.
#[universes(polymorphic)]
Definition id_poly@{s;l} (A:Type@{s;l}) : A -> A := fun x => x.
Definition id@{l} := id_poly@{Type;l}.
Parametricity id_poly.
Parametricity id.
(* Error: Universe instance length for id_poly_R is (1 | 1) but should be (0 | 1). *)
When a sort poly constant is translated, the sort variable is not propagated and thus substituted with Type instead.
Given that the names of universe level change also, I suspect that the instance is not propagated at all, and
infer again at definition time.