My point is that's not as interesting or practical as a type system for which you can write an expression that can't be checked. They may be roughly equivalent,

My point is that's not as interesting or practical as a type system for which you can write an expression that can't be checked. They may be roughly equivalent, but only one is esoteric.