Same flexibility in synth of ($ f x) as of (@ p r).
Closed this issue · 6 comments
Currently it will not work unless both sides are of the form ($ f x) at the same time.
@favonia Ah, good point.
Let me think about this a bit; it would help if you could give an example that was problematic.
In the case of path application, IIRC this was necessary because there is a non-computational equality p @ 0 = foo for any path; but what is the analogous thing for functions?
I don't have a concrete example yet, but I suppose we might want to prove ($ f x y) and ($ g y) are equal?
@favonia In this case, it would suffice to show that ($ f x) = g; I guess under the current state of affairs, it would be necessary to prove this before hand.
For better or for worse, the idea behind the synth stuff is that it represents a phase where only structural equality is considered. Sometimes structural equality is not the right choice...
@jonsterling The point is that Fun.EqApp would call Synth on ($ f x) and g, and then that would result into a Match exception without further explanation. Even manual refine would not work. This probably means we have to rewrite one side first, and I feel it is a little bit too demanding.
@favonia Hmm, that's a reasonable point. My thinking before was that synth should figure out sufficient conditions for two neutral terms to be equal, but maybe instead it should not try to do equality, and should only try to figure out membership.