Indeed, the article has it backwards. The types are always there. Your program will fail at runtime if it's not correct. The type system merely surfaced that.
Complexity in the types happens when the type system isn't expressive enough. Or when you're trying to do something that would make the compiler try to solve the halting problem.
To that last point, this is why the PLT community has pushed in the direction that Agda / Idris has. Kind of like how we realized years (decades?) ago that we didn't need pointer arithmetic, there's been a realization that "total" isn't actually that helpful, and it's okay if we didn't have languages that could express the halting problem.
That's the hope, but saying there's something wrong is insufficient. The compile-time errors need to be understandable, or it's just going to be frustrating.
Maybe we should judge compile-time constraint systems by how easy it is for the library author to add good error messages for misuse?
Complexity in the types happens when the type system isn't expressive enough. Or when you're trying to do something that would make the compiler try to solve the halting problem.
To that last point, this is why the PLT community has pushed in the direction that Agda / Idris has. Kind of like how we realized years (decades?) ago that we didn't need pointer arithmetic, there's been a realization that "total" isn't actually that helpful, and it's okay if we didn't have languages that could express the halting problem.