-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Display of (redundant/deprecated) pattern synonyms #2216
Comments
If the pattern synonym is not in scope unqualified then it should not be used to resugar. |
So is this an As for the original PR #1948 which introduced the pattern synonym for backwards compatibility, can such things be marked as |
The issue is, it's very easy and common to have both the actual constructor,
It could be called an
I don't think so? If I'm reading the Agda docs right, pattern synonyms have an implicit |
A design bug in the standard library? For now, pattern synonyms are untyped (cf. agda/agda#2069) and so their resugaring also is. |
A separate issue might be, also/independently, to reconsider the refactoring, not in favour of reverting the changes, but in enhancing the definitions in |
Well, I introduced it... so I'd welcome a steer towards how best to fix it without having to tackle the
Yes. But see above. |
OK, so after experimenting a bit, there seems to be a spectrum of 'solutions' to the problem, according to how much effort they require on the user's part vs that of the developer(s):
Any offers as to which you/we/users might prefer/be able to tolerate as an interim stopgap? Any other alternatives? |
Add an extra cornercase to Agda so that we don't resugar pattern synonyms marked as DEPRECATED? Edit: Ah but IIRC we don't really handle deprecated pattern synonyms? (at least it's the case for syntax: agda/agda#6915) |
This seems like the right thing to do. Looking at it, it shouldn't be that hard as it's not yet widely used. I'll see what I can put together. |
@gallais yes I found it was indeed ok to 'deprecate' pattern synonyms via |
@MatthewDaggitt thanks for picking this up!? ... but maybe your solution is (simply!) the right way to go!? I guess I couldn't/can't see far enough ahead to see if your solution avoids creating any hostages to fortune downstream... but that may very well be (my aiming for) the perfect being the enemy of the good (enough)... ;-) |
And ... hard not to feel that all of this arises for the sake of the original decision to avoid the breaking change of removing |
Originally posted by @Taneb in #1948 (comment)
The text was updated successfully, but these errors were encountered: