[math-fun] ceylon type system is turing complete?

My view: if it is Turing-undecidable whether you have written a legal program, then it was a bad programming language. So if this is true, Ceylon is bad (C++ definitely bad by this criterion).