sort polymorphic constants are not handled properly

[tabareau]

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). *)