instance transparency

Stream: general

[Floris van Doorn]

In docs#tactic.transparency there are 5 transparency settings:

all : tactic.transparency
semireducible : tactic.transparency
instances : tactic.transparency
reducible : tactic.transparency
none : tactic.transparency

I always thought that the lower transparency settings always involved fewer declarations. However, I just noticed that the instances transparency even applies to instances that are marked @[irreducible] (which means it applies to some definitions that semireducible doesn't apply to):

@[irreducible] instance has_zero.bool : has_zero bool :=
{ zero := ff }

open tactic
run_cmd do
e ← to_expr ``(0 : bool),
trace e, -- 0
e2 ← whnf e transparency.instances,
trace e2, -- ff
e3 ← whnf e transparency.semireducible,
trace e3, -- 0
skip

Is this intended? It sounds unwanted - I think of the instance transparency to unfold slightly more definitions than the reducible ones.
Background: I tried adding @[simps] to docs#category_theory.iso.op, but this gives an error, because @[simps] has unfolded the (irreducible) type when applying whnf ... transparency.instances to the type.

[Floris van Doorn]

This is fixed in lean#538. Thanks @Gabriel Ebner!