Well if one is looking for proofs, I think this is hard while remaining abstract from specific languages. I could counter that support for parametric polymorph

Well if one is looking for proofs, I think this is hard while remaining abstract from specific languages. I could counter that support for parametric polymorphism is poor in OO langs as much as you claim support for ad-hoc polymorphism is poor in FP langs. (but I don't place much stock in any of the aforementioned claims outside of some kind of artifical, academic context) Real-world problems that aren't an academic edge-cases will be supported by both FP and OO. Multimethods give you ad-hoc polymorphism in an uptyped setting.