dsimp in instances

Stream: mathlib4

[Yury G. Kudryashov]

git grep -nH -A1 '^instance' | grep -B1 dsimp shows that many instances use dsimp mydef; infer_instance pattern. It inserts id in the resulting instance. Am I right that this is a bad idea for instances with data? Or this changed in Lean 4?

[Yury G. Kudryashov]

Another bunch of instances use unfold for the same purpose.

[Eric Wieser]

Doesn't inferInstanceAs insert a wrapper function too?

[Eric Wieser]

I think we tried to avoid this pre-emptively in Lean 3 because at best it was just one more trivial thing to unfold

[Yury G. Kudryashov]

No, in some cases Lean 3 failed to unfold id.

[Yury G. Kudryashov]

We migrated from pi_instance to manual instances because of that.

[Yury G. Kudryashov]

inferInstanceAs is an abbrev, id is @[inline]

[Yury G. Kudryashov]

As far as I understand, abbrevs are reducible.

[Yury G. Kudryashov]

@Mario Carneiro Should we get rid of those dsimps?

[Mario Carneiro]

instances are usually unfolded at default reducibility, so it shouldn't matter

[Yury G. Kudryashov]

Did it change from Lean 3 to Lean 4? I remember that we had lots of @[reducible] non-instances in mathlib3.