coe conflict in concrete categories

Stream: mathlib4

[Yury G. Kudryashov]

We have docs4#ConcreteCategory.hasCoeToSort. OTOH, for some bundled concrete categories we have coercions like docs4#CommRingCat.instCoeSortCommRingCatType

[Yury G. Kudryashov]

Since Lean 4 unfolds coercions, instances defined for one of these coercions (e.g., CommRing) won't work for the other.

[Yury G. Kudryashov]

Probably, Lean 3 was able to see that two has_coe_sort instances are defeq.

[Yury G. Kudryashov]

I see two possible solutions:

1. Define ConcreteCategory.α or ConcreteCategory.Carrier and use it instead of X.α everywhere.
2. Redefine ConcreteCategory so that coercions is an outParam argument and supply Bundled.α in the Bundled instance.

[Yury G. Kudryashov]

Do I miss some better solution?

[Yury G. Kudryashov]

The second approach would force us to unfold the definition of a Functor in ConcreteCategory.

[Yury G. Kudryashov]

While the first one drops very convenient X.α.

[Yury G. Kudryashov]

Ping here

[Jujian Zhang]

Also there are conflict about function coercion, there is ConcreteCategory.hasCoeToFun and coercion from FunLike instances when CommRing or similiar categories are in considerations. See also here

[Scott Morrison]

@Yury G. Kudryashov, could you point to a situation where there is a problem because of these two unrelated coercions? Sorry, I'm still trying to understand what's going on here.

[Yury G. Kudryashov]

In !4#4531

[Yury G. Kudryashov]

Sorry, let me check

[Yury G. Kudryashov]

Yes, in !4#4531

[Yury G. Kudryashov]

This file enables (locally) the generic coercion

[Yury G. Kudryashov]

But some instances assume the Bundled-specific coercion.

[Yury G. Kudryashov]

In Lean 3, both were hidden behind coe and were defeq.

[Yury G. Kudryashov]

Here they're still defeq but instances can no longer see it.