instances are no longer protected

Stream: mathlib4

[Floris van Doorn]

I just found out that in Lean 4 instances are not protected by default. E.g. the following fails without the protected tag:

protected instance OrderDual.Pow [h : Pow α β] : Pow αᵒᵈ β := h
instance OrderDual.Pow' [h : Pow α β] : Pow α βᵒᵈ := h

That is very unfortunate. Is that something Core Lean 4 is willing to change?

[Sebastian Ullrich]

I'm not sure I understand the issue, what fails without protected?

[Kyle Miller]

#mwe:

def od (α : Type _) := α

postfix:max "ᵒᵈ" => od

instance OrderDual.Pow [h : Pow α β] : Pow αᵒᵈ β := h
instance OrderDual.Pow' [h : Pow α β] : Pow α βᵒᵈ := h
/- error on `Pow α β` argument
function expected at
  Pow
term has type
  _root_.Pow ?m.6684ᵒᵈ ?m.6685
-/

[Kyle Miller]

This is the same surprising namespace behavior I was complaining about. The Pow in the second line is referring to OrderDual.Pow rather than Pow itself because the instance definition is taking place in the OrderDual namespace.

[Sebastian Ullrich]

Oh wow, I completely missed it even after participating in the other thread...

[Eric Wieser]

Isn't the convention to call the instance instPow instead to avoid this issue?

[Floris van Doorn]

I was not aware of this naming convention. This convention is currently followed by ~2 out of ~160 manually named instances in Mathlib4. So it's clearly not a well-established convention.

[Yakov Pechersky]

I suggest we leave instances anonymous where possible

[Eric Wieser]

Isn't instPow the name that used when they're anonymous?