Anomaly with explicit universe +1 and template polymorphism

[SkySkimmer]

Inductive foo@{u} (A:Type@{u}) : Type@{u+1} := .

Check foo(foo (foo nat)).
(* anomaly unable to handle arbitrary u+k <= v *)