DefEq transitivity failures for unit-like eta

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The criteria for isDefEqUnitLike is not strong enough, and leads to failures of transitivity of the definitional equality:

Steps to Reproduce

example (p : α → Unit) : p = λ _ => ()   := rfl --works
example (q : α → Unit) : (λ _ => ()) = p := rfl --works
example (p q : α → Unit) : p = q         := rfl --fails

structure Foo where
    foo : Unit

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

structure Bar : Type where
    bar : True

example (p : Bar) : p = ⟨.intro⟩ := rfl --works
example (q : Bar) : ⟨.intro⟩ = q := rfl --works
example (p q : Bar) : p = q := rfl --fails

Expected behavior: All these examples should work

Actual behavior: some fail

Reproduces how often: 100%

Versions

4.0.0-nightly-2023-06-01

Additional Information

Agda supports eta-for-unit defeq, and uses a type-based approach similar to lean's for its record types and arrow types. Currently in lean, unit-like types are inductive types with one constructor and no fields in said constructor. The fix would be to extend this criteria such that any arrow type whose codomain is unit-like is itself unit-like, and any structure-like inductive for which all fields are unit-like is itself unit-like.

Start by reproducing the examples in the issue and inspecting the implementation of isDefEqUnitLike, the entry point named in the report. Compare the current criteria with the proposed arrow and structure cases. Done means all listed rfl examples succeed without breaking existing definitional-equality behavior.