Instance diamond in algebra hierarchy?

Stream: mathlib4

[Michael Stoll]

Consider:

import Mathlib.Algebra.Ring.Equiv

/-- A type synonym. -/
def Foo (R : Type*) := R

namespace Foo

variable {R : Type*} [Semiring R]
/- remove `[Semiring R]` --> error goes away -/

instance instSemiring [Semiring R] : Semiring (Foo R) := inferInstanceAs (Semiring R)

instance instRing [Ring R] : Ring (Foo R) := inferInstanceAs (Ring R)

example [Ring R] : True := by
  let i : NonUnitalNonAssocSemiring (Foo R) := NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
  let i' : NonUnitalNonAssocSemiring (Foo R) :=  NonAssocSemiring.toNonUnitalNonAssocSemiring
  have : i = i' := rfl -- error
  sorry

variable (R) in
/-- Canonical (semi)ring equivalence between `Foo R` and `R`. -/
def equiv [Semiring R] : Foo R ≃+* R := RingEquiv.refl _

variable [Ring R]

/- equiv x : Foo R ≃+* R -/
#check Foo.equiv R

/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @Distrib.toMul (Foo R)
    (@NonUnitalNonAssocSemiring.toDistrib (Foo R) NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring)
inferred
  @Distrib.toMul (Foo R) (@NonUnitalNonAssocSemiring.toDistrib (Foo R) NonAssocSemiring.toNonUnitalNonAssocSemiring)
-/
#check (Foo.equiv R).symm

What is going on here? How can the spurious [Semiring R] variable that none of the declarations actually use lead to non-defeq instances in the example? And why is the problem triggered by applying RingEquiv.symm and not already on Foo.equiv R?

[Eric Wieser]

/- remove `[Semiring R]` --> error goes away -/

Yes, because your example is example [Semiring R] [Ring R]

[Michael Stoll]

Hovering says Foo._example.{u_1} {R : Type u_1} [Ring R] : True, so no [Semiring R]?

[Eric Wieser]

Not if you comment out the line that fails

[Eric Wieser]

Or change it to have : i = i' := by exact rfl

[Eric Wieser]

If you try:

def foo [Ring R] : True := by
  let i : NonUnitalNonAssocSemiring (Foo R) := NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring
  let i' : NonUnitalNonAssocSemiring (Foo R) :=  NonAssocSemiring.toNonUnitalNonAssocSemiring
  have : i = i' := rfl -- error
  sorry

#print foo

then you'll see that the error somehow truncates the term after the first let

[Eric Wieser]

(remember that example means def)

[Michael Stoll]

OK, thanks. I came across this in file#Mathlib/Analysis/Normed/Ring/WithAbs :

variable {R S K : Type*} [Semiring R] [OrderedSemiring S] [Field K]

/-- Type synonym for a semiring which depends on an absolute value. This is a function that takes
an absolute value on a semiring and returns the semiring. We use this to assign and infer instances
on a semiring that depend on absolute values. -/
@[nolint unusedArguments]
def WithAbs : AbsoluteValue R S → Type _ := fun _ => R

namespace WithAbs

variable (v : AbsoluteValue R ℝ)

/-- Canonical equivalence between `WithAbs v` and `R`. -/
def equiv : WithAbs v ≃ R := Equiv.refl (WithAbs v)

-- (...)

instance instSemiring : Semiring (WithAbs v) := inferInstanceAs (Semiring R)

instance instRing [Ring R] : Ring (WithAbs v) := inferInstanceAs (Ring R)

-- (...)

instance normedRing {R : Type*} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing (WithAbs v) :=
  v.toNormedRing

and I got the error (on (WithAbs.equiv v).symm) after changing equiv to be a semiring isomorphism.

I bet this is not the only place in Mathlib where this problematic setup shows up...

[Sébastien Gouëzel]

This can only fail in sections which don't have lemmas or theorems (as for these the unused linter would fire), so it shouldn't happen often.

[Michael Stoll]

I think the problem is that the declaration indeed uses both arguments, which leads to the failure. (I did not get any linter warnings.)