[Haskell] really undecidable instances?

[Johannes Waldmann]

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/ -------