Remove `=` sugar for propositional Equality about idris2

[buzden]

What I always liked about = comparing to === is that it has a presedence lower than even infix 0, hence the clean look for function signatures that serve as properties of equality. Current infix 6 is okay for === meaning an alternative comparison function to ==, but propositional equality type plays a different role.

= as a symbol for propositional equality has the benefit of being easy to type and easy to read for newcomers

I don't feel myself a newcomer, but I personally still find = much easier to read than === in most of the cases.

---

Another downside of === being the only standard operator for propositional equality is that === operator is used not only for the propositional equality, for instance it is used for equality-based checks in propety-based testing libraries.

---

You considered the only alternative of doing nothing. In the motivation section (along with unique presedence of =, which I really like) you mention ambiguity problem. I can propose an alternative solution alternative to yours one: instead of removing = in favor of explicit ~=~ and ===, we can consider removing only ambuguous semantics of =, say, sticking it to ===, since this is the most used case for it.

[andrevidela]

What I always liked about = comparing to === is that it has a precedence lower than even infix 0

I also like this, and experimented with the compiler to make = a proper operator with precedence -1 and that seemed to work. I think it would be a reasonable change to make (===) have a compiler-only precedence (like -1), but I wasn't sure if that was something that the people really want, or need. I'd love for more people to chime in on that topic.

Another downside of === being the only standard operator for propositional equality is that === operator is used not only for the propositional equality, for instance it is used for equality-based checks in propety-based testing libraries.

Not a problem with the new fixity namespace features. The compiler can detect if there is a conflicting fixity and generate the appropriate program if necessary. In this instance it would mean hiding the built-in fixity for (===) and calling equality in application position (Builtin.(===) a b).

I can propose an alternative solution alternative to yours one: instead of removing = in favor of explicit = and ===

I think that's a great idea, however it does not really address the upgrade path problem which is the main body of this proposal. We would still need to provide a way to upgrade without breaking existing code-bases. Like mentionned at the end: we don't really have to, but that's the essence of this proposal, to do something nice while learning something on the way there. I know we have a lot of issues right know with code synthesis and this would be a great time to review the infrastructure around it.

[mattpolzin]

I can propose an alternative solution alternative to yours one: instead of removing = in favor of explicit = and ===

I think that's a great idea, however it does not really address the upgrade path problem

I can see it as being a drop-in idea for the end-goal with your proposed solution for migration still being applicable. I think I like the idea of = remaining equivalent to === (possibly modulo precedence, though I didn't know they had different precedence and I am not sure I think that specific point is a benefit). I also like the idea of offering code actions that desugar various kinds of things.

The desugar code action initially seemed of arguable use to me outside of this very specific migration need, but the more I think on it the more I can imagine situations where lifting a with block into a standalone helper function could indeed be desirable.

I saved this for last because it is a bit "sunk-cost-ty" but I'm in favor of past work that served to differentiate e.g. assignment from equality by introducing := so we have in some areas already begun to narrow in on = being used for equality; this would seem to make those distinctions unnecessary and a bit of a bummer from the perspective of wanting = to be useful for something. Of course, = would still be used for function clauses, but regardless I don't think we have ambiguity problems between the equals of function clauses and the equals of an equality.