rfl error message

Stream: general

[Marcus Rossel]

Is the following behavior expected? (I'm aware that the theorem doesn't hold)

import Mathlib

example [i : DivisionCommMonoid Real] :
    @DivisionMonoid.toDivInvMonoid Real (@DivisionCommMonoid.toDivisionMonoid Real i) =
    Real.instDivInvMonoid :=
  rfl
/-
type mismatch
  rfl
has type
  ?m.15 = ?m.15 : Prop
but is expected to have type
  i.toDivInvMonoid = Real.instDivInvMonoid : Prop
-/

I find the error message a bit surprising.

[Aaron Liu]

What exactly is surprising?

[Riccardo Brasca]

Your theorem says that any structure of DivisionCommMonoid on ℝ is equal to the "standard" one. I guess this is not what you wanted to state.

[Eric Wieser]

by rfl gives you a much better error, because it is a tactic not just a theorem

[Riccardo Brasca]

Ah you're complaining about the error, sorry.

[Kenny Lau]

I understand the complaint if you're comparing with the message generated by by rfl, but... I feel like they're really saying the same thing if you understand what ? means

[Kenny Lau]

specifically, ? is an attempt to unify expressions

[Marcus Rossel]

I think what I find confusing is that if I assumed that what I'm proving is true, then my reading of the error message would be:

i.toDivInvMonoid is defeq to Real.instDivInvMonoid, so why doesn't rfl just unify both of those terms with ?m.15?

[Kenny Lau]

I see, now I understand.

[Marcus Rossel]

But to @Eric Wieser's point, by rfl produces a nice error message.

[Kyle Miller]

It's too bad that when Lean tries unifying @Eq A a b with @Eq X x y that there's no partial progress. Either A =?= X, a =?= x, and b =?= y all succeed, or it fails.

If there were partial progress (maybe with unification hints?) you would see

type mismatch
  rfl
has type
  i.toDivInvMonoid = i.toDivInvMonoid : Prop
but is expected to have type
  i.toDivInvMonoid = Real.instDivInvMonoid : Prop

which is a little better.

[Jz Pan]

Maybe it's better to say "rfl probably has type" in the error message indicating for uncertainty.