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.