Definition id {A} (x : A) := x.
Fail Compute id.