Comment by hither_shores

> You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.

It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.