We study an extension of the second-order calculus of bounded quantifi
cation, System F-less than or equal to, with bounded existential types
. Surprisingly, the most natural formulation of this extension lacks t
he important minimal typing property of F-less than or equal to, which
ensures that the set of types possessed by a typeable term can be cha
racterized by a single least element. We consider alternative formulat
ions and give an algorithm computing minimal types for the slightly we
aker Kernel Fun variant of F-less than or equal to.