Why not always use Inf instead of Lazy in Idris?

Question

I find that Lazy and Inf is very close:

Lazy and Inf are closely related (in fact, the underlying implementation uses the same type). The only difference in practice is in totality checking, where Lazy is erased (i.e. terms are checked for termination normally, ignoring laziness annotations), and Inf uses a productivity checker, where any use of Delay must be constructor guarded.

As described above, the underlying implementation of Lazy and Inf is the same one, the only difference is about totality checking.

I think always use Inf seems much more natural, which is more close to the lazy we used in Haskell, and wondering what is the scene in production which we must use Lazy -- which always do a deep totality checking?

Misreport

I'm just guessing here, but I think Inf is for codata and Lazy is for data. Due to totality the lazy data should produce the same result as strict data, just with a different evaluation order and hence performance profile. – Ciccia

It seems that Lazy is not very useful as a Type, since the evaluation strategy doesn't need to be part of the type signature (and it is also impossible) – Misreport

This is what I've been thinking as well. Lazy does the same thing. – Slovak