I'm not sure about the history. It looks like UHC supported existential types at some point, but I'm not sure how that would interact with what I am presuming i

I'm not sure about the history. It looks like UHC supported existential types at some point, but I'm not sure how that would interact with what I am presuming is a more sophisticated system in GHC Haskell. This post had some interesting tidbits about technical challenges, but I didn't fully grasp everything on first read: http://blog.ezyang.com/2016/04/hindley-milner-with-top-level-existentials/ http://blog.ezyang.com/2016/04/hindley-milner-with-top-level... I really like tome's observation in the other comment: universally-quantified types have a direct encoding in System F as type abstractions, but there is no such direct encoding for existentially-quantified types.