That's a good question that i had previously noted for followup, but I never followed up.
slide 50: how does agda check termination.
http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf
http://research.microsoft.com/en-us/news/features/terminator...
Does Haskell allow you to assert that a function (like, say, the Sieves of Eratosthenes algorithm) does terminate, so that it may use that info to make additional simplifications?