It’s ‘row types aren’t unordered’ week here on discourse.purescript.org!
When you call R.set (Proxy @f1) true, what the compiler needs to know is Cons f1 Boolean _ s2, because what you give that function is a Record s2. You’re effectively asking why the compiler doesn’t infer the existence of Cons f1 Boolean _ s2 from the Cons f1 Boolean s0 s1 and the Cons f2 Boolean s1 s2 it has in scope.
In this special case, the compiler theoretically could make that inference, because both Cons instances are talking about Boolean. But consider the more general case of inferring a Cons f1 a _ s2 from Cons f1 a s0 s1 and Cons f2 b s1 s2, where a and b are different types. Imagine making the following variable substitutions:
-
f1="x" -
f2="x" -
s0=() -
s1=(x :: a) -
s2=(x :: b, x :: a)
Now Cons f1 a s0 s1 and Cons f2 b s1 s2 both hold, but Cons f1 a _ s2 won’t hold for any row you put in the wildcard position. So it would be incorrect for the compiler to make that inference in the general case.
We probably don’t have logic for the special case of two Cons instances in scope with equal second argument type because it isn’t a case that comes up in practice that often, but maybe that’s worth revisiting in a feature request if you can make the argument.
As general advice, if a low-level function has a constraint, you’ll trip yourself up less if you propagate that constraint faithfully up your call chain instead of trying to infer clever ways you could adapt that constraint to something else that should be equivalent. Especially when row types are involved, the compiler doesn’t always have the same ideas about what constraints are equivalent—and regardless of whether the compiler is right or you are right (and both have been known to happen), at the end of the day the compiler decides what it accepts.