The type definitions have basically always been misused anyway. It's a shoehorning of formal proofs from the 70s onto modern concepts, and it doesn't really work.

Though, really, I'm just quoting Anthony Liguori from 6 years ago, so credit where it's due:

https://news.ycombinator.com/item?id=2614975