instance search + semireducible

Stream: general

[Reid Barton]

While we're on a nearby topic, I've been meaning to ask: is it still the plan for Lean 4 to use semireducible transparency when deciding whether to apply an instance? (@Sebastian Ullrich?)
This would be a pretty significant change to certain parts of mathlib, and I'd like to start exploring the consequences of such a change, but I don't want to do it if it's not actually going to happen.

[Reid Barton]

(My Lean 4 build is now failing for reasons apparently unrelated to cmake, so I figured it's easiest to just ask.)

[Sebastien Gouezel]

Currently, Lean 3 is not even using the instances transparency flag and falls back to reducible (see lean#244), so this would be a pretty big change indeed.

[Reid Barton]

Hmm, I guess that must only happen in sufficiently complicated situations (which is consistent with the linked Zulip discussion) because I know I have seen examples where instance search can unfold the definitions of instances.

[Sebastian Ullrich]

Reid Barton said:

While we're on a nearby topic, I've been meaning to ask: is it still the plan for Lean 4 to use semireducible transparency when deciding whether to apply an instance?

I don't know/remember anything about that. https://github.com/leanprover/lean4/blob/master/src/Init/Lean/Meta/SynthInstance.lean#L545

[Reid Barton]

Hmm, thanks. Maybe it was a short-lived idea.