Nasty order of arguments dependency for @[refl]

Stream: mathlib4

[Anatole Dedecker]

It seems that the @[refl] tag is now behaving much more strictly regarding the order of arguments. I spent 10 minutes wondering why the refl tag on docs#ring_equiv.refl didn't work, and I realized it depends on the order of implicit arguments in the definition of RingEquiv!

import Mathlib.Algebra.Group.Opposite
import Mathlib.Algebra.Hom.Ring
import Mathlib.Logic.Equiv.Set

structure RingEquiv₁ (R S : Type _) [Mul R] [Mul S] [Add R] [Add S] extends R ≃ S, R ≃* S, R ≃+ S
structure RingEquiv₂ (R S : Type _) [Mul R] [Add R] [Mul S] [Add S] extends R ≃ S, R ≃* S, R ≃+ S

variable [Mul R] [Add R]

@[refl] -- works
def refl₁ : RingEquiv₁ R R :=
  { MulEquiv.refl R, AddEquiv.refl R with }

@[refl] -- fails
def refl₂ : RingEquiv₂ R R :=
  { MulEquiv.refl R, AddEquiv.refl R with }

Is this a known issue?

[Anatole Dedecker]

(Also, is there really no way to remove the empty with without Lean thinking this is a set ?)

[Mario Carneiro]

if you remove the with then it's not a structure instance at all

[Mario Carneiro]

the structure instance syntax does support { a, b } but that is shorthand for { a := a, b := b } not { a, b with }

[Mario Carneiro]

this looks like the same issue that was recently fixed for @[symm], the attribute check is too strict

[Anatole Dedecker]

Mario Carneiro said:

the structure instance syntax does support { a, b } but that is shorthand for { a := a, b := b } not { a, b with }

Oh okay so basically with is the new .. (with different syntax of course)?

[Mario Carneiro]

yes