I don't think 0001 is right either, although maybe for somewhat different reasons. First, I think it only considers VAR OP CONST style clauses, but that is leaving money on the table, because given a.x = b.x AND mumble(a.x), we can decide to instead test mumble(b.x) if the equality operator in question has is-binary-identical semantics. It does not seem necessary for a first patch to deal with both that and the somewhat more pleasing case where we're making deductions based on operator families ... but we shouldn't commit to a design for the VAR OP CONST case without understanding how it could be generalized.
I can follow up with this and +1 with the statement.
Second, it looks to me like the patch takes the rather naive strategy of enforcing the derived clauses everywhere that they can legally be put, which seems certain not to be optimal.
If we can have some agreement (after more discussion) the EC filter is
acceptable on semantics level, I think we may have some chances to