constructor isn't defeq to eta value for mutual definitions

Stream: lean4

[Jakub Nowak]

namespace NotMutual

structure Bar : Type where
  n : Nat

structure Foo : Type where
  bar : Bar

example (foo : Foo) : Prop := by
  have h₁ : foo = ({ bar := foo.bar } : Foo) := rfl
  have h₂ : foo = Foo.mk foo.bar := rfl
  sorry

end NotMutual


namespace Mutual

mutual

  structure Foo : Type where
    bar : Bar

  structure Bar : Type where
    n : Nat

end

example (foo : Foo) : Prop := by
  have h₁ : foo = ({ bar := foo.bar } : Foo) := rfl
  have h₂ : foo = Foo.mk foo.bar := rfl  -- Type mismatch
  sorry

end Mutual

Not sure if this is something that should be reported as an issue?

Btw, the fact that delaboration isn't idempotent in this case was a source of confusion for me (#new members > Prove termination of mutually recursive definitions).

[Robin Arnez]

It fails because it isn't defeq. Structure eta only applies to non-recursive inductives with one constructor.

[Jakub Nowak]

Robin Arnez said:

It fails because it isn't defeq. Structure eta only applies to non-recursive inductives with one constructor.

But this defeq works: foo = ({ bar := foo.bar } : Foo), while this doesn't foo = Foo.mk foo.bar. So it seems like structure eta works, but only with ({ bar := foo.bar } : Foo), and not with Foo.mk foo.bar.

[Robin Arnez]

That's not quite right. The structure instance elaborator uses a version of structure eta, presumably also to counteract some of the flattening it does:
https://github.com/leanprover/lean4/blob/c76411d6c55dfc292934d80914dfa6e5f77598f3/src/Lean/Elab/StructInst.lean#L881
... but this isn't guaranteed to be a defeq transformation! So specifically:

mutual

  structure Foo : Type where
    bar : Bar

  structure Bar : Type where
    n : Nat

end

-- fails, goal foo = { bar := foo.bar }
example (foo : Foo) : ({ bar := foo.bar } : Foo) = Foo.mk foo.bar := rfl

... I guess the delaboration doesn't make it any better though...

[Jakub Nowak]

Maybe it would be possible to apply the same elaboration to both structure instance and constructor syntaxes?

If not, then I would say to not delaborate constructor to structure instance syntax, as they're not the same and it's causing confusion. Maybe we could also lint/warn against usage of constructor when structure instance syntax is viable?