Type error stating `x = x`

Stream: general

[Eric Wieser]

A puzzle; for what term x are x = sorry and sorry = x legal, but x = x a type error?

Answer: (f : ∀ {n : ℕ}, ℕ)

example (f) : (f : ∀ {n : ℕ}, ℕ) = sorry := sorry  -- ok
example (f) : sorry = (f : ∀ {n : ℕ}, ℕ) := sorry -- ok
example (f) : (f : ∀ {n : ℕ}, ℕ) = (f : ∀ {n : ℕ}, ℕ) := sorry -- type error