Simon Peyton-Jones wrote:
It's all very delicate. I believe, though I am not certain, that in the absence of functional dependencies, removing at least one type constructor might be an example of a rule that is sufficient to ensure termination. There are lots of such rules. Alas none known to me capture all cases.
Of course they couldn't - because of undecidability of termination (of term rewriting, or Prolog-like programs). But then, there are a lot of (nontrivially) decidable subcases, and consequently there are quite a few automated methods for termination proofs, see http://www.lri.fr/%7Emarche/termination-competition/2005/ Would it be interesting to "beef up" the termination analysis in ghc a bit, using some of those methods? But then, the current solution is just use "-fundecidable.." and the see if the type checker (apparently) loops. This might still be more efficient than invoking a larger machinery that would prove (non)termination because after the proof you'd still have to invest the time into doing the rewrite sequence. Best regards, -- -- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 -- ---- http://www.imn.htwk-leipzig.de/~waldmann/ -------