This paper says: "In the presence of a unit type, $\eta$-reduction is not even locally confluent on well-typed terms [20]."
[20] is a reference to a 300-page book with no further details and I cannot find the relevant example there. So can you give an example of $\eta$-reduction not being locally confluent on well-typed terms?