Equality of functions

Right, the long term solution is generalized existentials, which most recently received some discussion here: Improving the UI of generics.