Should the constructors of Data.Nat._≤_ be declared as instances?

[jamesmckinna]

issue #1919 and its associated PR #1948 had got me thinking again about the basic ordering relation(s) on Nat, as well as a side remark of @Taneb 's about having proofs of m ≤ n "floating around" in the context of #1949 ...

Specifically, _≤_ (and hence everything else provably equivalent to it) is an Irrelevant relation, moreover with disjoint constructors z≤n and s≤s. So it seems, at first blush, that we could replace ostensibly informative assumptions/proofs of m ≤ n by instances... or can we?

Cons: huge knock-on viscosity, for starters; but are there also uses where we couldn't easily/reliably delegate to instance inference during typechecking (hello: transitivity!)?

Pros: not sure! It feels like an itch similar to @MatthewDaggitt 's about {{NonZero n}}: it involves non-trivial re-engineering, but still is/might be an itch worth scratching? UPDATED: it would/might/should also permit a smoother approach to defining functions which have m ≤ n preconditions?

[jespercockx]

Having used instance search in the past, I've come to the conclusion that (for me) using instance arguments for doing proof search is usually a bad idea since you have little control over how instances are resolved. Once you get to some critical point of "too many" instances Agda either becomes very slow or just fails to resolve them.

A less invasive alternative would be to leave the type as it is and instead provide a macro that can automatically resolve simple inequality proofs. You can then use @tactic arguments (https://agda.readthedocs.io/en/v2.6.3/language/reflection.html#tactic-arguments) to make arguments to other proofs be resolved automatically.

[jamesmckinna]

Interesting suggestions, thanks!

Regarding implementation inefficiency, I'm always conscious of the split between 'conceptual purity/desirability' of any design decision and 'implementation feasibility/practicality'. Your comments go more to the latter, and perhaps my thinking on the issue was guided by the former?

[jespercockx]

Whether you use instance arguments or tactics, I think you have already fallen into the trap of thinking about practicality. Otherwise you would just write all the proofs by hand. So the question is just which algorithm you want to use to resolve the proofs for you. And the choice is essentially ease of use (instance arguments) vs flexibility (tactics).

[jamesmckinna]

Closing, in favour of #1998 / #2000