Zulip Chat Archive

Stream: mathlib4

Topic: instances are no longer protected


Floris van Doorn (Nov 24 2022 at 16:25):

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 (Nov 24 2022 at 16:43):

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

Kyle Miller (Nov 24 2022 at 16:52):

#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 (Nov 24 2022 at 16:55):

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 (Nov 24 2022 at 16:56):

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

Eric Wieser (Nov 24 2022 at 17:00):

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

Floris van Doorn (Nov 24 2022 at 17:30):

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 (Nov 24 2022 at 17:41):

I suggest we leave instances anonymous where possible

Eric Wieser (Nov 24 2022 at 17:55):

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


Last updated: Dec 20 2023 at 11:08 UTC