[jerf]

With appropriate compiler flags, you can make up any sort of contracts you like in Haskell. But there's no guarantee that the compilation process will terminate if you do, even putting aside the impenetrability of the resulting code. Haskell is not a general purpose proof assistant, and the typing definitely has limits both practical and theoretical. Abstractly, static types can represent anything, however we (by which I mean humanity in general) certainly do not know how to use such powerful types in real, general purpose code.

If you want to go that road, look up Agda or Coq.

[prodigal_erik]

Why do people worry about compilers hanging or giving up? If I know how to kill the failed compile and fix my program so that it is provably type-safe before shipping, I don't really care how many undecidable programs could also exist because I no longer have to ship one of those.

[jerf]

Because if the compiler hangs, you don't get any executable code. And in the specific case of Haskell, we are talking about type constraints that are perfectly cromulent, are perfectly correctly expressed and mean something in some abstract mathematical world in which your have infinite compiler time, but in the real world will simply never finish compiling. It's not because you've failed and you can fix it by twiddling something, it's because Haskell is not actually that sort of language, and if you try to actually use the type system as a Turing-complete constraints satisfaction language, you'll get exponential performance... or doubly-exponential performance, or worse, though it stops mattering pretty quickly.

In both theory and practice, this means you can't really use Haskell that way. It's a typed language with the ability to occasionally skirt the limits, ride the line, and dip into a bit of undecidability when useful (and with a real, in-practice risk of it blowing up in your face even so), not a language in which one routinely uses the type system in a "Turing complete manner", if I may be allowed to gloss over precisely what that means. Richer type systems is a topic of ongoing research, but is not a solved problem.

[prodigal_erik]

So the problem is that there are too many useful programs which can't be expressed in a practically decidable form, or there's no clear way to get from a form that isn't to a similar-enough form that would be, like knowing what strategies ghc uses to narrow the search space or something?

[scarmig]

While we're at it, what would be really cool is if we could design a program to automatically look at the Haskell program, decide if it's undecidable, and fix it.