Existential types: HM versus System F