I am trying to write a row polymorphic function working with a record of 2 fields, but field names are not fixed.
Snippet for a record with 1 field is working:
foo ::
forall @f1 s b.
IsSymbol f1 =>
Cons f1 Boolean b s =>
Record s ->
Record s
foo = R.set (Proxy @f1) true <<< R.set (Proxy @f1) true
useFoo :: { f1 :: Boolean }
useFoo = foo @"f1" { f1: false }
Is there a way to compose types to describe a record more fields?
Try 1
bar ::
forall f1 f2 s0 s1 s2.
IsSymbol f1 =>
IsSymbol f2 =>
Cons f1 Boolean s0 s1
Cons f2 Boolean s1 s2 =>
Record s2 ->
Record s2
bar = R.set (Proxy @f1) true <<< R.set (Proxy @f2) true
Error:
No type class instance was found for
Prim.Row.Cons f16
t1
t2
s27
while applying a function set
of type IsSymbol t0 => Cons @Type t0 t1 t2 t3 => Cons @Type t0 t4 t2 t5 => Proxy @Symbol t0 -> t4 -> Record t3 -> Record t5
to argument Proxy
Try2:
bar ::
forall @f1 @f2 s0 s1 s2 s.
IsSymbol f1 =>
IsSymbol f2 =>
Union s1 s2 s =>
Cons f1 Boolean s0 s1 =>
Cons f2 Boolean s0 s2 =>
Record s ->
Record s
bar = R.set (Proxy @f1) true <<< R.set (Proxy @f2) true
Thanks, now it is working, but could you explain why my first version is wrong?
Cons f2 Boolean s1 s2<=> s2 type is a s1 type with field f2 Cons f1 Boolean s0 s1<=> s1 type is a s0 type with field f1
s2 type should have both fields f2 and f1 because of transitivity
The Cons type class is a 4-way relation which asserts that one row of types can be obtained from another by inserting a new label/type pair on the left.
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.