In a recent development, I used the
no-eta-equality attribute on a record. The motivation in that case was ad hoc: I noticed that I'd get better metavariable resolution for uses of definitions like
map-⊗ᴿ if I could make
_⊗ᴿ_ more opaque. However, it got me wondering whether I could be taking more advantage of
no-eta-equality by recognising some patterns in which it is useful.
Are there any best practices or heuristics to decide whether to use
no-eta-equality on a given record? Are there cases where both choices are justifiable? And what are the costs and benefits in each case?