Display of (redundant/deprecated) pattern synonyms

[jamesmckinna]

An annoyance that seems to be due to this: the emacs tooling seems to prefer less-than-or-equal to _,_ when I do C-c C-c to pattern match on a product when both are in scope, regardless on whether the thing I'm matching has anything to do with natural numbers

Originally posted by @Taneb in #1948 (comment)

[gallais]

If the pattern synonym is not in scope unqualified then it should not be used to resugar.

[jamesmckinna]

If the pattern synonym is not in scope unqualified then it should not be used to resugar.

So is this an agda bug? an emacs issue?
Can it be locally/temporarily hacked with a DISPLAY pragma?

As for the original PR #1948 which introduced the pattern synonym for backwards compatibility, can such things be marked as deprecated? (I wasn't sure at the time)
And, now that it has been merged in to master, I suppose a follow-up PR which removes all the other uses of the redundant synonym might be in order? But how to trigger a warning to other users? And how to fix @Taneb 's problem? It's typical to import Data.Nat.Base unqualified, which introduces the synonym...

[Taneb]

If the pattern synonym is not in scope unqualified then it should not be used to resugar.

The issue is, it's very easy and common to have both the actual constructor, _,_, and the pattern synonym in scope, if someone imports both Data.Nat.Base and Data.Product.Base without an import list (I do this a lot)

So is this an agda bug? an emacs issue?

It could be called an agda bug, but I wouldn't be surprised if it's deliberate behaviour reasonable in some contexts.

Can it be locally/temporarily hacked with a DISPLAY pragma?

I don't think so? If I'm reading the Agda docs right, pattern synonyms have an implicit DISPLAY pragma

[gallais]

So is this an agda bug? an emacs issue?

A design bug in the standard library?

For now, pattern synonyms are untyped (cf. agda/agda#2069) and so their resugaring also is.

[jamesmckinna]

A separate issue might be, also/independently, to reconsider the refactoring, not in favour of reverting the changes, but in enhancing the definitions in Algebra.Definitions.RawMagma to be fully-fledged top-level records, rather than proxying via Σ-types? Sigh...

[jamesmckinna]

So is this an agda bug? an emacs issue?

A design bug in the standard library?

Well, I introduced it... so I'd welcome a steer towards how best to fix it without having to tackle the RawMagma definition first.

For now, pattern synonyms are untyped (cf. agda/agda#2069) and so their resugaring also is.

Yes. But see above.

[jamesmckinna]

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):

• add hiding (less-than-or-equal) to all client imports of Data.Nat.Base; this is probably the easiest for the time being, but is perhaps maximally irritating to users;
• deprecate the pattern synonym, and remove all uses of it from the library; this isn't a solution per se, unless coupled with the first suggestion; but would at least speed up adoption of the new representation; NB developing new proofs for the modules in which it was previously used is proving (sic) more tiresome than I had hoped/expected... :-(
• remove the pattern synonym entirely, which may break client code unexpectedly, so needs careful documentation as a breaking change (this may end up being the simplest moststraightforward thing to do, however, modulo the above);
• redevelop the RawMagma machinery (I don't see myself being able to do this for v2.0, so barring someone else's heroic effort, one of the above approaches needs to be taken otherwise).

Any offers as to which you/we/users might prefer/be able to tolerate as an interim stopgap? Any other alternatives?

[gallais]

Add an extra cornercase to Agda so that we don't resugar pattern synonyms marked as DEPRECATED?
But of course the ergonomics would still be bad for people not living on the Agda bleeding edge.

Edit:

Ah but IIRC we don't really handle deprecated pattern synonyms? (at least it's the case for syntax: agda/agda#6915)
And we don't actually have DEPRECATED, we only have WARNING_ON_USAGE. 😧

[MatthewDaggitt]

redevelop the RawMagma machinery (I don't see myself being able to do this for v2.0, so barring someone else's heroic effort, one of the above approaches needs to be taken otherwise).

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.