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

[jamesmckinna]

Fixes #2504 , following the discussion there and on #2503 , which this also refactors.

Tagged as breaking, although the only known use of this relation in the wild is from the OP of #2503 , and the CHANGELOG documents the only possible (?) source of breaking behaviour, namely supplying implicit arguments to the new pattern synonym for the former non-linear constructor ≤‴-refl. Hence v2.2, not v3.0... but I'm happy to row back on that.

[jamesmckinna]

@tsung-ju Could you please check that your development is compatible with these changes?

[tsung-ju]

Hi, I tried the new version, and it indeed only breaks in places where I supplied implicit argument to ≤‴-refl. After changing those to ≤‴-reflexive {m=m} refl and adding the necessary imports, everything worked as before.

Out of curiosity, is it possible to add an implicit argument to ≤‴-refl? I tried something like

pattern ≤‴-refl {m} = ≤‴-reflexive {m=m} refl

but that doesn’t seem to work.

[jamesmckinna]

@tsung-ju thanks very much for doing a smoke test on these changes!

I, too, had problems defining a pattern synonym which takes an additional implicit argument; I imagined that this might be because m and n are declared as parameters to the relation, rather than indices... so, in some sense, in any context in which ≤‴-reflexive (or ≤‴-refl) would be a legal pattern, the values of those parameters must already be known. I may raise on issue on the main Agda tracker about this, but only when/if this PR gets approval to merge. I certainly found it puzzling...

In the meantime, I conjecture that no use of the implicit argument(s) should actually be needed, but I'd be interested to see examples where that is actually necessary... so I am surprised that you did seem to need them, and found the solution to be to explicitly supply them via an inlined version. If you are willing to post them, suggest that you do so on issue #2504 itself (where the design and its behaviour is discussed), rather than this PR (where those are implemented).

UPDATED: I did a bit more poking around. It seems that if you do wish to supply m as a named implicit parameter during pattern matching, you should do so before using the ≤‴-refl pattern... as any attempt to supply it explicitly (to the pattern synonym) raises an error. Similarly when supplying it as a named implicit in the form ≤‴-reflexive {m = m} refl (ie inlining the 'intended' pattern synonym).

UPDATED: Indeed, some more investigation points the way, by way of Agda.Builtin.Equality and its constructor, refl: if you try instead to supply an implicit argument m to refl, Agda helpfully points out that refl takes 0 arguments... because they are all already supplied as parameters to the data type. So, in this instance, there isn't any way that ≤‴-reflexive could take an implicit argument m... it would have to be supplied as part of the pattern matching telescope of bindings prior to that pattern occurring. Hope this helps!

In the meantime, thanks again, and for the original PR #2503 which prompted these investigations!

[MatthewDaggitt]

Okay, looks reasonable.

[JacquesCarette]

Seems reasonable to me as well - but not pushing 'merge', as 'seems reasonable' feels like too low a bar.

[jamesmckinna]

@JacquesCarette this PR and #2523 are individual instances of refactoring along the lines of #2519 , which I took directly from your comments on #2504 .

Very happy to pause developments in this direction, but please, comment on #2519 if you have objections to it!?

[JacquesCarette]

I think the changes here are fine, I'm probably uncomfortable because Data.Nat.Base._≤‴_ shouldn't exist at all (in that module, at least), so that's clouding my vision of the local value of this change. So I'm asking for another opinion.

[jamesmckinna]

Agree that long-term (post-v3.0?) we shouldn't pollute Data.Nat.Base with all these relations, but for v2.x...