typeclasses and binding order

Stream: general

[Dean Young]

Supposing I have different instances of a type class, how do I tell Lean to always try matching one before the other?

[Arthur Paulino]

In Lean 4 (maybe in Lean 3 as well) you can define (priority := low/high)

[Dean Young]

can you link me to an example?

[Arthur Paulino]

From Init/SizeOf.lean:

class SizeOf (α : Sort u) where
  sizeOf : α → Nat

export SizeOf (sizeOf)

protected def default.sizeOf (α : Sort u) : α → Nat
  | _ => 0

instance (priority := low) (α : Sort u) : SizeOf α where
  sizeOf := default.sizeOf α

[Eric Wieser]

This is generally not a good way to use typeclasses. Mathlib tends to use priority as a form of optimization, not to actually change behavior

[Dean Young]

ok I'll keep the binding order to the notation then