[ refactor ] Change definition of Data.Nat.Base._≤′_

[jamesmckinna]

This is exactly analogous to #2504 , in line with #2519 .
Potentially breaking, but all tests pass on stdlib without changes.
Possible downstream improvement for tackling #2442 ?

[JacquesCarette]

This seems very reasonable to me.

[jamesmckinna]

Re: breaking/v3.0 I guess you're right @MatthewDaggitt although as with #2504 I'm not clear whether this relation has any external use; internally it exists as a mediator for Data.Nat.Induction, moreover one which has been previously refactored extensively so that the single proof involved <⇒<′ already goes via a pattern synonym <′-base... which in fact is (equivalent to) the one introduced by this PR...

... but I should consider uncoupling the last commit to CHANGELOG, as this was made on the assumption that the two PRs would be merged under v2.2...

[MatthewDaggitt]

I havered on this. I mean the previous change was also similarly breaking and got merged. I think the rule we seem to be converging on is that if we break implicit arguments then it is fine?

[jamesmckinna]

I havered on this.

Fair enough! This relation is actually used in stdlib (but, as usual, we can't speak for external client uses), so I took care to investigate how, and hence whether the consequences of this breaking change would cash out adversely. But I concluded: not.

I mean the previous change was also similarly breaking and got merged. I think the rule we seem to be converging on is that if we break implicit arguments then it is fine?

That's as may be, but AFAIAC, this is purely in the spirit of #2519 : ie. make the reflexivity constructor take a proof of equality explicitly. The implicit/explicit distinction is moot as far as this PR is concerned, I think?

All that said, is it a non-breaking change to replace the (new) pattern synonym with:

pattern ≤′-refl {m} = ≤′-reflexive {n = m} refl

If so, happy to make that change!

[jamesmckinna]

The argument for making a breaking change in #2504 was that there were no uses of it in the library, and only one external user (whose PR prompted this whole cycle of refactoring), who could absorb the change without difficulty.

But hopefully the non-breaking suggestion that I make above (which I conjecture is even equivalent to the previous version, because of the way unification works; it might only fail if {n = m} were ever to be supplied explicitly) mops up any 'accidnetal' breakges...?

[JacquesCarette]

These suggestions make sense to me.

[MatthewDaggitt]

Yup, upon reflection happy to merge this either way, but even better if we can make it non-breaking.