Various type theories have, over the years, explored extending the definitional equality with a variety of eta-laws and various forms of proof irrelevance.
Quite a lot of systems manage eta for functions, because (as Thierry Coquand observed), you can eta-expand on a tit-for-tat basis, even if your equality test is not type directed. Whenever you are checking
f = \ x -> t, you may readily test
\ y -> f y = \ x -> t instead (choosing
y fresh), if
f is not already eta-expanded. Crucially, if neither side is already of the form
\ x -> t, then eta-expansion makes no difference to the problem.
Agda certainly manages eta for records, because its equality is type-directed. Two records are equal exactly if they are equal fieldwise, which makes it a delight to define the unit type as the record type with no fields. (You can do syntactic eta-expansion tit-for-tat for pairs, but not for unit. For unit, if neither side is already canonical, eta-expansion makes a big difference to the problem!)
Are there any systems (in a good state of repair) which identify all terms in the empty type? That's a little trickier to manage, but I know some systems (because I built them) which did it. It's nice to have, because it means you can form the set of things which are not bad as dependent pairs of a thing and a proof that it's not bad: to prove that two such pairs are equal, you need only prove that the things are equal, because all inhabitants of
Bad thing -> False are equal by eta for functions then falsity.
If you're working on a type theory for a proof assistant, have you got definitional equality for an absurd type? If so, I'd like to know (and I'm guessing Lean steps up, here). If not, what's stopping you? (I seem to remember that there was some sort of snag in Agda, but I can't for the life of me remember what it was.)