Failure of transitivity for eta

Stream: lean4

[Arthur Adjedj]

Hi, I believe to have found an issue with eta-expansion of "unit-like" types. In particular, it isn't transitive in certain cases such as this one:

structure Foo where
    a : Unit

example (p: Foo) : p = ⟨()⟩ := rfl --works
example (p q: Foo) : p = q := rfl --fails :(

The issue seems to be that the is_def_eq_unit_like function checks only for inductive types with one constructor and no fields to the constructor, where it should check for inductives with one constructor for which all fields are themselves unit-like . Should I open an issue ?

On another note, perhaps it would be nice/desirable for eta-expansion to also apply to empty types, such that examples like these would work as well ?

inductive Bad where

example (a b : Bad) : a = b := rfl --fails

[Kevin Buzzard]

Just to spell this out explicitly, Arthur's example is a new (to me) example of failure of transitivity of rfl:

structure Foo where
    a : Unit

@[reducible] def q : Foo := ⟨()⟩

instance : Inhabited Foo := ⟨q⟩

opaque p : Foo
opaque r : Foo

example : p = q := rfl
example : q = r := rfl
example : p = r := rfl -- fails

[Gabriel Ebner]

This is not intentional, but not a big priority either unless it breaks something actually important. I'd file it as a bug.

[Arthur Adjedj]

It seems like eta-expansion fails to trigger in in more than one scenario, and not only for structures, but functions as well:

example (f : Nat → Unit) : f = (λ _ => ()) := rfl --works
example (f g : Nat → Unit) : f = g := rfl --fails

I'll open an issue then. thanks for the input @Gabriel Ebner

[François G. Dorais]

Is eta enabled globally now? I thought it was partly disabled due to performance issues.

[François G. Dorais]

Maybe I'm just thinking about eta for structures?

[Arthur Adjedj]

Eta is globally enabled for functions and structures, there's no option to turn it off AFAIK

[Eric Wieser]

The only thing that was ever disabled was eta for structures (aka one-constructor inductives) during typeclass search

[Eric Wieser]

But that's now enabled too