Definitional reduction issues in lean

Stream: Type theory

[Joseph Hua]

https://github.com/coq/coq/issues/10871

I read here that you can have "a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all)" and would like to know what examples there are of it. If I understand correctly this has to do with quotient types, but I don't know the connection.

[Mario Carneiro]

See section 3.1.2 "Failure of subject reduction" in https://github.com/digama0/lean-type-theory/releases/tag/v1.0