incorrect assumption about dot notation declaration name

Stream: lean4

[Kevin Buzzard]

def semiconj_by {M : Type _} (a x y : M) : Prop := a = x ∧ y = a

def commute {M : Type _} (a b : M) : Prop := semiconj_by a b b

theorem semiconj_by.cast_int_mul_right {M : Type _} {a x y : M} (h : semiconj_by a x y) : h = h := rfl

namespace commute

-- this works
theorem cast_int_mul_right' (M : Type _) (a : M) (h : commute a a) : h = h := h.cast_int_mul_right

-- this doesn't
theorem cast_int_mul_right (M : Type _) (a : M) (h : commute a a) : h = h := h.cast_int_mul_right
/-
fail to show termination for
  commute.cast_int_mul_right
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'commute.cast_int_mul_right' does not take any (non-fixed) arguments
-/

end commute

Here commute is a specialization of semiconj_by. The lemma semiconj_by.cast_int_mul_right exists, and dot notation is smart enough to interpret h.cast_int_mul_right as semiconj_by.cast_int_mul_right h if h : commute .... Indeed the primed lemma commute.cast_int_mul_right' works fine. But when trying to define commute.cast_int_mul_right, Lean presumably correctly interprets h.cast_int_mul_right as semiconj_by.cast_int_mul_right h (so the proof parses) but at a later stage Lean decides to reject the declaration because it incorrectly decides that it's circular. So somehow two parts of Lean are interpreting the same thing in different ways.

[James Gallicchio]

I think it's actually interpreting it the same at all stages...

My impression is that the dot notation looks through definitions to resolve names, but only if the original type's namespace doesn't have a matching identifier. In the non-primed case, the namespace does have the matching identifier, before unfolding the commute definition, so the commute identifier takes precedence.

Here you can either mark commute.cast_int_mul_right as nonrec, or just refer in the body to semiconj_by.cast_int_mul_right directly

Maybe we should add a warning for when dot-notation could be elaborated multiple ways by unfolding/not unfolding definitions, but that might be too expensive to check.

[Kevin Buzzard]

Ha you're probably right! Thanks!