Switch Positive/Negative/etc. to use irrelevant instance arguments

[MatthewDaggitt]

This plays the same game with Positive/Negative/NonPositive/NonNegative as #1538 did with NonZero. We get all the same benefits as the NonZero case. Will post something about on Zulip and the mailing list tomorrow.

[mechvel]

Positivity/negativity has sense for any Ordered (Abelian) Group.
There _<_ is agreed with _+_ in a certain way.
It is desirable to have the corresponding general definition.
For Integer, the Negative predicate can be expressed as the -[1+_] constructor.
But this does not work for Rational and some other domains.
_< zero for Negative has sense for any ordered Abelian group.

[technicalguy]

In my Agda work I've found that instance arguments can sometimes slow type checking down a lot. Are there any benchmarks of before and after this change? That aside, sounds great!

[MatthewDaggitt]

Positivity/negativity has sense for any Ordered (Abelian) Group.

@mechvel I agree, it should be possible to generalise the definitions if done carefully. However this PR is very much about using the definitions and the changes are almost entirely agnostic to the definitions themselves. I'll make a note of your comment in #1175 so it doesn't get forgotten when we come around to generalising the other definitions.

In my Agda work I've found that instance arguments can sometimes slow type checking down a lot. Are there any benchmarks of before and after this change? That aside, sounds great!

That's an excellent question @technicalguy . Looking at the test suite, it took 11m 58s to type-check this PR, whereas looking at the last 7 runs of the test on master I get:

12m 26s
11m 25s
11m 53s
12m 00s
11m 53s
11m 13s
11m 11s

Lot's of variability there, but I think it's clear that it hasn't significantly boosted type-checking time, even with 100+ uses of instance arguments. I think primarily this is because the instance search is never more than single layer deep at the moment. However even with that single layer of search, there's a ton of benefits. If and when we address #1565 and try and make instance search deeper we should re-evaluate the performance impact.