And you don't need cut in logic either: https://philpapers.org/rec/BOODEC

It's just that your typeable program might take more data to store than there are bits in the universe.

I'm not saying that types are bad. They aren't.

I'm saying they aren't magic and they come with a trade off.

Types are the closest thing to a free lunch that exists in this fallen world. Yes they're not perfect because nothing is, but their cost/benefit is astonishingly good.

A shoe five sizes too small is very comfortable for someone who cut off his toes.

It would be a mistake to conclude that this means shoes are pointless or there's no such thing as a shoe that fits well.

Indeed, there are other invariants to type systems that are much better than cutting off your toes.