Diamond issue in Algebra.Star.Basic

Stream: mathlib4

[Frédéric Dupuis]

In mathlib4#1331, a diamond issue has showed up that has me stumped. Here's a MWE of the problem:

import Mathlib.Algebra.Ring.Aut

class StarRing' (R : Type _) [NonUnitalSemiring R]
def starGizmo [CommSemiring R] [StarRing' R] : R → R := id
lemma starGizmo_foo [CommRing R] [StarRing' R] (x : R) : starGizmo x = x  := rfl    -- failed to synthesize instance StarRing' R

If we unpack this a bit, we find out that Lean is failing to unify @StarRing' R NonUnitalCommSemiring.toNonUnitalSemiring with @StarRing' R NonUnitalRing.toNonUnitalSemiring. It's easy to check that these two are in fact defeq. I don't know what's going on; perhaps @Gabriel Ebner or @Mario Carneiro could have a look...?

[Frédéric Dupuis]

@Jireh Loreaux

[Eric Wieser]

Are you sure they're defeq?

[Eric Wieser]

This looks like something that is only true because of structure eta, and a problem that we didn't have in lean 3 due to the use of old flat structures

[Frédéric Dupuis]

This works, at any rate:

example [CommRing R] : @StarRing' R NonUnitalCommSemiring.toNonUnitalSemiring =
    @StarRing' R NonUnitalRing.toNonUnitalSemiring := rfl

[Heather Macbeth]

If they're not defeq, seems like it would break the whole linear/semilinear map setup.

[Chris Hughes]

Eric Wieser said:

This looks like something that is only true because of structure eta, and a problem that we didn't have in lean 3 due to the use of old flat structures

Structural eta is a defeq in Lean4

[Eric Wieser]

Indeed; my unfounded hunch was that somehow it's a "lesser" defeq that can't be applied in all cases

[Kevin Buzzard]

Minimised here.