instance priorities and parents

Stream: lean4

[Matthew Ballard]

How do you think Lean should fill the value for A in baz below?

variable (α : Type _) [Inhabited α]

class A where
  a : α

instance (priority := 100) foo : A α where
  a := default

class B extends A α where
  b : α

instance (priority := 75) bar : B α where
  b := default

class C extends A α where
  c : α

instance baz : C α where
  c := default
#print baz

[Kevin Buzzard]

Oh! Your point is that it uses B.toA (and in particular bar) despite this having a lower priority than the directly available foo?

[Kevin Buzzard]

[Meta.synthInstance] ✅ A α ▼
  [] new goal A α ▼
    [instances] #[foo, @B.toA, @C.toA]
  [] ✅ apply @C.toA to A α ▼
    [tryResolve] ✅ A α ≟ A α ▶
    [] no instances for C α ▶
  [] ✅ apply @B.toA to A α ▶

etc etc, with B.toA before foo because it was defined later it has default priority, and B.toA can be made to work so it works.

[Matthew Ballard]

B.toA doesn't have the lower priority unfortunately. Once it commits to that only bar is left.

The values 100 vs 75 are in many places in mathlib. So a fix there would be bump the 100 to default + 1.

But my point is that when the user sets these priorities they probably want foo in place of bar in the end.

[Matthew Ballard]

A specific example of this pair of priorities is SubXClass vs SubX in the algebraic hierarchy.

[Kevin Buzzard]

attribute [instance 99] B.toA also fixes it -- i.e. "don't just set the priority of bar low, set the priority of its projections low too just to make sure". Oh but wait, this is no good, because in general you don't want to be messing with B, it's just bar you want to be the last option :-/

[Jireh Loreaux]

Didn't we have a PR that was doing exactly this? Maybe #6403

[Jireh Loreaux]

Agreed though, I woudl have expected / intended foo here instead of B.toA.

[Eric Wieser]

lean4#2325 is related here, which advocates changing those inherited priorities

[Matthew Ballard]

Here is a example in the wild: I needed to explicitly specify s.toRing for (s : Subring R) to keep Lean from backdooring a CommRing.toRing built using the SubringClass instance on Subring.