rfl vs by rfl in instance diamonds

Stream: mathlib4

[Eric Wieser]

In #6391 (using instances only on that branch), I found an instance diamond which fails to unify with rfl but succeeds with by rfl:

example : StarOrderedRing.toStarRing = Complex.instStarRingComplexToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRing :=
  by rfl  -- ok

example : StarOrderedRing.toStarRing = Complex.instStarRingComplexToNonUnitalSemiringToNonUnitalCommSemiringToNonUnitalCommRingCommRing :=
  rfl -- fails

[Eric Wieser]

Perhaps even more scarily, the term generated by by rfl doesn't appear to work if you try to use it directly

[Eric Wieser]

Is this a transitivity failure in defeq (which we know are possible) turning up in a place that we didn't expect?

[Eric Wieser]

Nevermind, the problem was between the chair and keyboard. This is still weird behavior, but not really something we care about:

def foo : ℕ := 1
lemma bar : ℕ := 1
example : foo = bar := rfl -- fails
example : foo = bar := by rfl -- ok

[Eric Rodriguez]

What do you mean the term that by rfl produces? Shouldn't that be rfl??

[Kevin Buzzard]

Just to be clear (it was a while before I spotted it) -- bar should be a def not a lemma.

[Damiano Testa]

@Eric Rodriguez, I think that Eric refers to this:

def foo : ℕ := 1
lemma bar : ℕ := 1
--example : foo = bar := rfl -- fails

theorem RFL : foo = 1 := rfl
theorem byRFL : foo = bar := by rfl

#print byRFL -- theorem byRFL : foo = bar := Eq.refl foo
#print RFL   -- theorem RFL : foo = 1 := rfl

byRFL produces Eq.refl foo.

[Damiano Testa]

... and the worrying part:

example : foo = bar := Eq.refl foo
/-
type mismatch
  Eq.refl foo
has type
  foo = foo : Prop
but is expected to have type
  foo = bar : Prop
-/

[Kevin Buzzard]

"worrying" only if you're going to make data with lemmas and then are interested in analysing why random stuff is now broken

[Damiano Testa]

Yes, I agree that it is not worrying, but the error message does not make it clear where the issue is, so it might be tricky to debug.