ie we can get a Prop equivalent to any Set, in this example equivalent to nat.

Inductive Foo@{i} (A:Type@{i}) : Type := foo : (nat:Type@{i}) -> Foo A.
Arguments foo {_} _.

Check Foo True : Prop. (* should fail *)

Definition bar : Foo True -> nat := fun '(foo x) => x.

Definition foo_bar n : foo (bar n) = n.
Proof. destruct n;reflexivity. Qed.

Definition bar_foo n : bar (foo n) = n.
Proof. reflexivity. Qed.

I think we can't actually get a proof of false from this without the kind of axiom which breaks impredicative set but still marking as critical.

The root cause is that we typecheck the inductive with universes considered >= Set but then template polymorphism allows instantiating with Prop.

Not sure if there's a way to trigger this with neither @{i} or explicit #[universes(template)] syntax (if I don't use the @{i} universes unify differently) but plugins could probably do it since a long time ago (maybe since universe polymorphism, maybe before, I don't know how universes worked before).