DefEq transitivity failures for eta

[arthur-adjedj]

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.

[arthur-adjedj]

I've taken the liberty of making a fix for this issue on a fork, by extending the criteria for which a type may be considered unit-like. Would a PR for this be welcomed ?