priority 10 vs 100

Stream: general

[Reid Barton]

Is there any systematic meaning to the use of priority 10 versus priority 100 for instances?
The "default priority" library note suggests using 100, but there are also many uses of priority 10.
I see that @Floris van Doorn changed many priorities to 10 in #1485 but then used 100 as the value in #1724.
I guess the question is whether there is some general rule that can usually tell me whether to use 10 or 100, and whether the current mix of 10s and 100s is information to be preserved or a historical accident.

[Reid Barton]

I see that #1485 changed priorities from 0 to 10 while #1724 changed them from 1000 to 100, so there seems to be some logic to it, but it could be that most of the instances that had priority 0 were of the sort that should have priority 100 and actually caused instances before we enforced the lowered priority with a linter.

[Floris van Doorn]

I think for a large part is a historical accident, but there is some logic to it.
I want classical.prop_decidable to fire after any [priority 100] instances. I intentionally made some priorities other than 100, if my guess was that they would be more applicable (or less expensive) or less applicable (more expensive) than other instances with priority 100. That is mostly guesswork though.

[Reid Barton]

OK, I'll go through the priority 10 instances and try to guess whether there is a good reason for them

[Reid Barton]

Haha, the first instance I come across with a weird priority is monoid.has_pow

[Kevin Buzzard]

Are you going to redefine it so it's the same way around as nat.pow?

[Reid Barton]

Now I'm wondering whether it's useful to make a standard 1000 priority instance for nat

[Reid Barton]

There are very few instances of has_pow anyways.

[Reid Barton]

OK, maybe I should be more specific: is there ever a good reason for an extends instance to have a priority like 10?

[Reid Barton]

I guess there ended up being only one case I cared about. #3968

[Floris van Doorn]

Reid Barton said:

OK, maybe I should be more specific: is there ever a good reason for an extends instance to have a priority like 10?

If the class is rarely used, and is unlikely to solve a random type-class problem.