You are, of course, right about EvenInt being easy to express in a type system. In fact, I believe type systems are generally so expressive as to allow just about any constraint to be expressed (eventually..).

I notice a lot of arguments on this topic resolve to "but Turing", which is not completely uncalled for but I think misses the point a bit. Not because it is wrong, but because it highlights the wrong property.

I don't doubt, say, Brainfucks ability to express any arbitrary computation, but I do doubt its ability to do so sanely. Now you may say Haskell's type system is very clean, but some constraints will definitely push it out of its comfort zone. I'm not saying it won't be able to express them, but I am claiming there will be dragons. One example of a constraint that's at least awkward is when the absence of a fixed type is part of the design. There are of course myriad solutions to this problem but they generally all require not quite so straightforward constructions that eventually might make sense with enough exposure, but whose complexity can actually be disproportionate to the value of the guarantee.

It's very much a testament to the genius of languages like F# and Haskell that you have to think hard of practical counter-examples.

That said, I actually think the Dark/Light polarity rears its head again even deep inside Haskell as any sufficiently complicated software system encounters barriers it needs to overcome and those require carefully constructed escape hatches: unsafePerformIO, metaprogramming, that is to say, the (relative) Dark Side.

In that metaphor undisciplined use of Lisp is like a vast, dark gravitational field of possibility and Haskell is like a sea of light with some carefully marked dark patches.