We have to be careful in how we define "equality" in the above sentence, including class constraints that (may) have superclass equality constraints.
Indeed. That’s what happens now.
I do think this would work.
Cool. Nick or Iavor: would you like to turn this conversation into a ticket?
(Although it is technically user-facing, it is a very small corner and I’m not sure it would need a GHC proposal – others may want to comment.)
Simon
From: Richard Eisenberg
A. An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.
We have to be careful in how we define "equality" in the above sentence, including class constraints that (may) have superclass equality constraints. I do think this would work. Richard