Inductive Existential : Type :=
| witness : forall T:Type, T -> Existential
| nothing.

Check Existential.
  (* : Type@{max(Set, Top.11+1)}

     Existential is in type 2 *)

Fail Check (witness Existential (witness bool true)).
(* this must live in type 3 to hold a value of type 2 *)

(* it needs to be polymrphic for this to work *)
Polymorphic Inductive PolyExistential : Type :=
| poly_witness : forall T:Type, T -> PolyExistential
| poly_nothing.

Check (poly_witness PolyExistential (poly_witness bool true)).
      (* ^ this is in type(3)        ^ this is in type(2)