why `priority := low` is not needed?

Stream: general

[Asei Inoue]

/-- `Arity α` is a type class that gives the arity (number of arguments) of the type `α`. -/
class Arity (α : Type) where
  arity : Nat

instance (α β : Type) [Arity β] : Arity (α → β) where
  arity := 1 + (Arity.arity β)

instance (α : Type) : Arity α where
  arity := 0

-- The arity of a non-function type is 0
#guard Arity.arity Nat = 0

-- The arity of a single-argument function type is 1
#guard Arity.arity (Nat → Bool) = 1

-- The arity of a two-argument function type is 2
#guard Arity.arity (Nat → Bool → String) = 2

-- A function type that takes a tuple has “one argument”, so the arity is 1
#guard Arity.arity (Nat × Bool → String) = 1

[Asei Inoue]

My Question

instance (α : Type) : Arity α where
  arity := 0

This instance is for the base case, and normally one would specify priority := low.
However, as in the code above, it seems to work fine even without specifying priority := low.
I thought Lean usually gives priority to instances declared later, so why does the code above work without any issues?

[Robin Arnez]

More generic instances are always tried later

[Asei Inoue]

So does that mean there is absolutely no need to specify priority := low?

[Robin Arnez]

Well, if you had another generic instance XYZ α → Arity α because of something like extends Arity α, priority := low might be better for disambiguation

[Robin Arnez]

Even then, it might not be explicitly needed but might be better for clarity

[Jovan Gerbscheid]

The way Lean determines the order of instances is:

1. compare the given priority
2. compare where the instances are stored in the discrimination tree. The consequence of this is that more specific instances are tried before more generic instances.
3. first try instances that are declared later

So yes, there is technically no need to specify priority := low in your example. But as @Robin Arnez said, specifying the low priority explicit makes the code much easier to understand.

[Asei Inoue]

Thank you!!