C++ : imperative language whose type system is a Turing-complete functional language (with rather twisted syntax)
Haskell: functional language whose type system is a Turing- complete logic programming language (with rather twisted syntax)
Since not all Turing machines halt, and since the halting problem is undecidable, this means not only that some Haskell programs will make the type checker loop forever, but that there is no possible meta- checker that could warn us when that would happen.
Do not forget that both functional dependencies and associated types come with syntactic restrictions that are there just to "tame" the Turing completeness, i.e., to guarantee that type checking will actually terminate. (I do agree that these restrictions, for functional dependencies anyway, can be thought of as twisted in their own right, but then again, there's no such thing as a free lunch.) Admittedly, it's my experience that whenever one wants to do something interesting (and here I mean "interesting" in a way that you would probably label as "rather twisted" ;-)), one has to bypass these restrictions (and, hence, allow for potentially undecidable instances). Now, I haven't really worked with associated types (or, for that matter, associated type synonyms), but my hope is that, when using those, turning off the checks is needed less often. We'll see. Another option would be not to care that much about looping type checkers: when it loops, you'll probabely notice it quite soon already :-). That said, that would not be the option I'd pick though: being restricted to, say, structural recursion on the type-level could well cause your type-level programs to be better organised. Cheers, Stefan