Is Quantified Constraints Really an Extension?

Many of the biggest changes are at least partially driven by industry. I've been quite stunned by the extent to which it's an industry that some of these more exotic corners of the type system in particular are most widely used. In industry, you think I want this code to still work in 10 years and be refactorable. And then once they get the idea about expressing the intent in a type system, they really want to do it. They're very annoyed if they can't.