using `algebraMap` in instances

Stream: mathlib4

[Matthew Ballard]

With the change in transparency from Lean 3 to Lean 4, it is a bad idea to build instances using algebraMap since it is not reducible and typeclass synthesis calls unification with reducible and instances transparency.

The path to making algebraMap reducible goes all the way down to making Function.comp reducible. This is also a bad idea.

It seems like the only way out is to declare data, eg toFun explicitly, when building the instance.

Do people have more clever thoughts to escape the current situation?

[Eric Wieser]

Unbundling algebraMap fixes this, right?

[Eric Wieser]

Which is good for other reasons anyway (we can use the same function for towers of monoids)

[Eric Wieser]

goes all the way down to making Function.comp reducible

I'm increasingly beginning to think that independently, Function.comp should be reducible, as it was in Lean 3

[Mario Carneiro]

I think that the case for comp being reducible is the same as for id being reducible

[Anne Baanen]

Eric Wieser said:

Which is good for other reasons anyway (we can use the same function for towers of monoids)

You mean something like the Lift classes I talked about here?