difference between `default_instance` and instance`priority`

Stream: new members

[Asei Inoue]

class Diamond (α : Type) where
  dia : α

notation "⋄" => Diamond.dia

section

local instance instDiaZero : Diamond Nat where
  dia := 0

local instance instDiaOne : Diamond Nat where
  dia := 1

-- there are two instances
-- but latter is used
#guard (⋄ : Nat) = 1

attribute [default_instance] instDiaZero

-- [default_instance] attribute does nothing
#guard (⋄ : Nat) = 1

end

section

local instance (priority := high) instDiaZero' : Diamond Nat where
  dia := 0

local instance instDiaOne' : Diamond Nat where
  dia := 1

-- priority works
#guard (⋄ : Nat) = 0

end

[Asei Inoue]

I do not understand why this behaviour occurs. Please tell me what is the difference between giving the [default_instance] attribute and setting the priority of the instance high.

[Kyle Miller]

default_instance is orthogonal to priority. Priority adjusts the order in which instances are considered. When all instance problems are stuck, then Lean looks for a default_instance that can apply.

Default instances are how number literals eventually become Nat literals if there is no other type information.

[Kyle Miller]

If I remember correctly, the algorithm is

Start:
  try to synthesize all instance problems
  catch stuck instance problems error
    for each stuck problem
      if there is a default instance that applies
        apply it
        goto Start
    throw the stuck instance problems error

[Asei Inoue]

@Kyle Miller Thank you. [default_instance] is for OfNat only? no.