Zulip Chat Archive

Stream: new members

Topic: difference between `default_instance` and instance`priority`


Asei Inoue (Sep 22 2024 at 16:45):

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 (Sep 22 2024 at 16:46):

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 (Sep 22 2024 at 17:58):

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 (Sep 22 2024 at 18:00):

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 (Sep 23 2024 at 02:05):

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


Last updated: May 02 2025 at 03:31 UTC