I thank @evancz for explaining why he has implemented (==) as he had. His reasons are practical. I particularly like:
(3) [to avoid disruption due to] the eventual introduction of an
equatabletype
I read this as placing a high value on consistency with the math and logic definition of equality for functions. I think this is a reasonable point of view, even though the original poster describes it as overly aggressive.
If we had a partial implementation of the math-and-logic definition, then I think the development tool-chain would be a good place to use it. It could be used, as evancz says, to prove that optimizations (and refactoring simplifications) preserve the semantics of the code.
By the way, in his Structured programming with goto statements (1974), Don Knuth explores the idea of what he calls an interactive program manipulation system. This seems to be similar to what evancz described. Such a system is perhaps a refactoring assistant, much as Coq and Lean are proof assistants.