For the record, a little more digging turned up this http://portal.acm.org/citation.cfm?id=583852.581496 which answers most of my questions. On Feb 10, 2006, at 2:02 PM, Robert Dockins wrote:

OK. I've been doing a little thinking about type lambda in Haskell.

Now, I understand the prevailing wisdom is that adding type lambda and/or partially applied type synonyms to the haskell type system would make type checking/inference undecidable. The reason given is that higher-order unification is undecidable.

I have to admit that I don't fully understand this reason. Setting aside typeclasses for now, it seems to me that type expressions together with the kind system are just the simply-typed lambda calculus with unit, which is well known to be strong normalizing. So any type with kind * has a normal form with (by definition) no internal redexes. I think this is sufficient to guarantee that all type lambdas are removed. Now you can proceed using first-order unification, which is decidable. Of course, all valid expressions have kind * (ignoring unboxing and other trickiness for now).

So where have I gone wrong? Do typeclasses complicate the matter? Or have I missed something more basic?

Thanks, Rob Dockins

Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG