Counterexamples for Lean's type system

What question should the reference manual answer?

What theoretically desirable properties of type systems is Lean known not to possess (e.g., subject reduction, canonicity, ?) and what are concrete examples of these violations?

Additional context

Searching for these topics on the Lean Zulip returns various long discussions which are not always easy to follow, not least because they often assume context from elsewhere (e.g., Twitter (which is not easy to access for everyone, the Rocq issue tracker (which assumes that you can read Rocq), or Mario Carneiro's thesis (which assumes that you can read type theoretic notation)). In addition, if there are examples, they are often in Lean 3 or no-longer-compiling old Lean 4.

It would be great to have all of these examples in one place together with good explanations, and given that the reference manual is a place to look up the details and it has a chapter on Lean's type system, I thought that this might be in scope for the reference manual.

Examples of code that I think would be great to keep up-to-date and explain in detail are this and this.

Start with the reference manual's existing chapter on Lean's type system, then review the two linked Zulip discussions and verify their examples against current Lean 4. The work is done when the relevant missing properties, concrete counterexamples, and explanations are consolidated in one up-to-date reference-manual section.