Example foo (f : forall {_ : Type}, Type) : Type.
Abort.