Stream: general

Topic: priority 10 vs 100

Reid Barton (Aug 28 2020 at 20:19):

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 (Aug 28 2020 at 20:21):

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 (Aug 28 2020 at 20:34):

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 (Aug 28 2020 at 20:38):

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

Reid Barton (Aug 28 2020 at 20:40):

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

Kevin Buzzard (Aug 28 2020 at 20:41):

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

Reid Barton (Aug 28 2020 at 20:42):

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

Reid Barton (Aug 28 2020 at 20:43):

There are very few instances of has_pow anyways.

Reid Barton (Aug 28 2020 at 20:44):

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 (Aug 28 2020 at 20:57):

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

Floris van Doorn (Aug 28 2020 at 21:36):

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.

Last updated: May 16 2021 at 05:21 UTC